edits

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
index 22e39084f2d696ca773c15566319696942a6c030..a77855add8c9abbf0fde3a794c0f0e53c8f7075c 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
@@ -327,8 +327,8 @@ public class CodeGenerator {
 
        static public void main(String[] args) {
        
-               String[] dirNames = args;
-//             String[] dirNames = Environment.Benchmarks;
+//             String[] dirNames = args;
+               String[] dirNames = Environment.Benchmarks;
 
                for (int i = 0; i < dirNames.length; i++) {
                        String dirName = dirNames[i];

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 6a90a72eec1f286786f847cb945124cee8eb6707..e6fd383e249390613d9fff2fab9905650fc5e9b0 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -214,10 +214,15 @@ public class CodeGeneratorUtils {
                                                + name));
                                code.addLine("typedef struct " + structName + " {");
                                FunctionHeader funcHeader = construct.getFunctionHeader();
-                               // RET
-                               if (!funcHeader.returnType.equals("void"))
+                               // C_RET & also the S_RET
+                               // The idea is that we store the S_RET in the __value struct, and every time we access/update
+                               // S_RET, we actually access "__value->S_RET" (good for read and write)...
+                               if (!funcHeader.returnType.equals("void")) {
                                        code.addLine(TabbedLine(Declare(funcHeader.returnType,
-                                                       SpecNaming.RET)));
+                                                       SpecNaming.C_RET)));
+                                       code.addLine(TabbedLine(Declare(funcHeader.returnType,
+                                                       SpecNaming.S_RET)));
+                               }
                                // Arguments
                                for (VariableDeclaration decl : funcHeader.args) {
                                        code.addLine(TabbedLine(Declare(decl)));
@@ -408,9 +413,18 @@ public class CodeGeneratorUtils {
                                        code.addLine(DeclareDefine(SpecNaming.CString,
                                                        SpecNaming.AppendStr(tmpFunc),
                                                        SpecNaming.EmptyCString));
-                               // JustifyingCondition
-                               tmpFunc = name + "_" + SpecNaming.JustifyingCondition;
-                               if (!construct.justifyingCondition.isEmpty())
+                               // JustifyingPrecondition
+                               tmpFunc = name + "_" + SpecNaming.JustifyingPrecondition;
+                               if (!construct.justifyingPrecondition.isEmpty())
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+                               else
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc),
+                                                       SpecNaming.EmptyCString));
+                               // JustifyingPostcondition
+                               tmpFunc = name + "_" + SpecNaming.JustifyingPostcondition;
+                               if (!construct.justifyingPostcondition.isEmpty())
                                        code.addLine(DeclareDefine(SpecNaming.CString,
                                                        SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
                                else
@@ -627,11 +641,11 @@ public class CodeGeneratorUtils {
                                        code.addLine("");
 
                                }
-                               // Define @JustifyingCondition
-                               if (!construct.justifyingCondition.isEmpty()) {
+                               // Define @JustifyingPrecondition
+                               if (!construct.justifyingPrecondition.isEmpty()) {
                                        code.addLine(ShortComment("Define @"
-                                                       + SpecNaming.JustifyingCondition + " for " + name));
-                                       code.addLine("bool _" + name + "_" + SpecNaming.JustifyingCondition
+                                                       + SpecNaming.JustifyingPrecondition + " for " + name));
+                                       code.addLine("bool _" + name + "_" + SpecNaming.JustifyingPrecondition
                                                        + "(" + SpecNaming.Method + " " + SpecNaming.Method1
                                                        + ", " + SpecNaming.Method + " " + SpecNaming.Method2
                                                        + ") {");
@@ -643,12 +657,40 @@ public class CodeGeneratorUtils {
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
 
-                                       construct.justifyingCondition.align(1);
-                                       code.addLine(TabbedLine(ShortComment("Execute JustifyingCondition")));
-                                       code.addLines(construct.justifyingCondition);
+                                       construct.justifyingPrecondition.align(1);
+                                       code.addLine(TabbedLine(ShortComment("Execute JustifyingPrecondition")));
+                                       code.addLines(construct.justifyingPrecondition);
 
-                                       // By default, we will return true for @PreCondition
-                                       code.addLine(TabbedLine(ShortComment("By default @JustifyingCondition returns true")));
+                                       // By default, we will return true for @JustifyingPrecondition
+                                       code.addLine(TabbedLine(ShortComment("By default @JustifyingPrecondition returns true")));
+                                       code.addLine(TabbedLine("return true;"));
+
+                                       code.addLine("}");
+                                       code.addLine("");
+
+                               }
+                               // Define @JustifyingPostcondition
+                               if (!construct.justifyingPostcondition.isEmpty()) {
+                                       code.addLine(ShortComment("Define @"
+                                                       + SpecNaming.JustifyingPostcondition + " for " + name));
+                                       code.addLine("bool _" + name + "_" + SpecNaming.JustifyingPostcondition
+                                                       + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+                                                       + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+                                                       + ") {");
+
+                                       // Initialize value struct fields
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(
+                                                       SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+                                                       construct);
+                                       fieldsInit.align(1);
+                                       code.addLines(fieldsInit);
+
+                                       construct.justifyingPostcondition.align(1);
+                                       code.addLine(TabbedLine(ShortComment("Execute JustifyingPostcondition")));
+                                       code.addLines(construct.justifyingPostcondition);
+
+                                       // By default, we will return true for @JustifyingPostcondition
+                                       code.addLine(TabbedLine(ShortComment("By default @JustifyingPostcondition returns true")));
                                        code.addLine(TabbedLine("return true;"));
 
                                        code.addLine("}");
@@ -829,17 +871,31 @@ public class CodeGeneratorUtils {
                                                        + "),";
                                }
                                code.addLine(TabbedLine(line, 2));
-                               // JustifyingCondition
+                               // JustifyingPrecondition
+                               line = "new "
+                                               + SpecNaming.NamedFunction
+                                               + "("
+                                               + SpecNaming.AppendStr(name + "_"
+                                                               + SpecNaming.JustifyingPrecondition) + ", "
+                                               + SpecNaming.JustifyingPreconditionType + ", (void*) ";
+                               if (construct.justifyingPrecondition.isEmpty()) {
+                                       line = line + SpecNaming.NullFunc + "),";
+                               } else {
+                                       line = line + "_" + name + "_" + SpecNaming.JustifyingPrecondition
+                                                       + "),";
+                               }
+                               code.addLine(TabbedLine(line, 2));
+                               // JustifyingPostcondition
                                line = "new "
                                                + SpecNaming.NamedFunction
                                                + "("
                                                + SpecNaming.AppendStr(name + "_"
-                                                               + SpecNaming.JustifyingCondition) + ", "
-                                               + SpecNaming.JustifyingConditionType + ", (void*) ";
-                               if (construct.justifyingCondition.isEmpty()) {
+                                                               + SpecNaming.JustifyingPostcondition) + ", "
+                                               + SpecNaming.JustifyingPostconditionType + ", (void*) ";
+                               if (construct.justifyingPostcondition.isEmpty()) {
                                        line = line + SpecNaming.NullFunc + "),";
                                } else {
-                                       line = line + "_" + name + "_" + SpecNaming.JustifyingCondition
+                                       line = line + "_" + name + "_" + SpecNaming.JustifyingPostcondition
                                                        + "),";
                                }
                                code.addLine(TabbedLine(line, 2));
@@ -974,10 +1030,10 @@ public class CodeGeneratorUtils {
                // The very first assignment "
                res.addLine(DeclareDefine(structName, "*" + inst, "(" + structName
                                + "*) " + methodInst + "->" + SpecNaming.MethodValueField));
-               // Don't leave out the RET field
+               // Don't leave out the C_RET field
                if (!construct.getFunctionHeader().isReturnVoid()) {
                        res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
-                                       SpecNaming.RET, inst + "->" + SpecNaming.RET));
+                                       SpecNaming.C_RET, inst + "->" + SpecNaming.C_RET));
                }
                // For arguments
                for (VariableDeclaration decl : construct.getFunctionHeader().args) {
@@ -1124,7 +1180,7 @@ public class CodeGeneratorUtils {
                // Call the actual function
                code.addLine(prefixTabs + "\t"
                                + ShortComment("Call the actual function"));
-               // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
+               // bool C_RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
                code.addLine(prefixTabs + "\t"
                                + construct.getFunctionHeader().getRenamedCall() + ";");
                code.addLine("");
@@ -1138,12 +1194,12 @@ public class CodeGeneratorUtils {
                                + DeclareDefine(structName,
                                                "*" + SpecNaming.InterfaceValueInst, SpecNaming.New
                                                                + Brace(structName)));
-               // Don't leave out the RET field
+               // Don't leave out the C_RET field
                if (!construct.getFunctionHeader().isReturnVoid())
                        code.addLine(prefixTabs
                                        + "\t"
                                        + AssignToPtr(SpecNaming.InterfaceValueInst,
-                                                       SpecNaming.RET, SpecNaming.RET));
+                                                       SpecNaming.C_RET, SpecNaming.C_RET));
                // For arguments
                for (VariableDeclaration decl : construct.getFunctionHeader().args)
                        code.addLine(prefixTabs
@@ -1174,7 +1230,7 @@ public class CodeGeneratorUtils {
 
                // Return if necessary
                if (!construct.getFunctionHeader().isReturnVoid())
-                       code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");
+                       code.addLine(prefixTabs + "\treturn " + SpecNaming.C_RET + ";");
                code.addLine(prefixTabs + "}");
 
                return code;

diff --git a/src/edu/uci/eecs/codeGenerator/Environment.java b/src/edu/uci/eecs/codeGenerator/Environment.java
index bbdfa9ec5dce9bc5015e58e2a0924eb00168d3e2..f9665b7d008f64cddcbc1f2e33b4eeb646046639 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/Environment.java
+++ b/src/edu/uci/eecs/codeGenerator/Environment.java
@@ -37,19 +37,19 @@ public class Environment {
        public final static String MPMC = "mpmc-queue";
        
        public final static String[] Benchmarks = {
-               REGISTER_ACQREL,
-               REGISTER_RELAXED,
+//             REGISTER_ACQREL,
+//             REGISTER_RELAXED,
                MS_QUEUE,
-               LINUXRWLOCKS,
-               MCS_LOCK,
-               DEQUE,
-               TREIBER_STACK,
-               TICKET_LOCK,
-               SEQLOCK,
-               READ_COPY_UPDATE,
-               CONCURRENT_MAP,
-               SPSC,
-               MPMC
+//             LINUXRWLOCKS,
+//             MCS_LOCK,
+//             DEQUE,
+//             TREIBER_STACK,
+//             TICKET_LOCK,
+//             SEQLOCK,
+//             READ_COPY_UPDATE,
+//             CONCURRENT_MAP,
+//             SPSC,
+//             MPMC
        }; 
 
 }

diff --git a/src/edu/uci/eecs/specExtraction/FunctionHeader.java b/src/edu/uci/eecs/specExtraction/FunctionHeader.java
index b79d65ba65a0ab34e6bd79a205a14eba2eb4c862..d07a0a1386714cd71906097986a49377c3b195cf 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/FunctionHeader.java
+++ b/src/edu/uci/eecs/specExtraction/FunctionHeader.java
@@ -164,7 +164,7 @@ public class FunctionHeader {
        public String getRenamedCall(String prefix) {
                String res = "";
                if (!isReturnVoid()) {
-                       res = res + returnType + " " + SpecNaming.RET + " = ";
+                       res = res + returnType + " " + SpecNaming.C_RET + " = ";
                }
                res = res + prefix + "_" + funcName.fullName + "(";
                if (args.size() >= 1) {

diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
index e2b0290685bd0c2d4cedac92383b53330423b029..ddc26145f8f136c40576cb8ec00657d43f6a05ff 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
@@ -30,8 +30,9 @@ public class InterfaceConstruct extends Construct {
        // have other name conflict
        private String structName;
        public final Code preCondition;
-       public final Code justifyingCondition;
+       public final Code justifyingPrecondition;
        public final Code transition;
+       public final Code justifyingPostcondition;
        public final Code postCondition;
        public final Code print;
 
@@ -54,8 +55,9 @@ public class InterfaceConstruct extends Construct {
                this.name = null;
                this.structName = null;
                this.preCondition = new Code();
-               this.justifyingCondition = new Code();
+               this.justifyingPrecondition = new Code();
                this.transition = new Code();
+               this.justifyingPostcondition = new Code();
                this.postCondition = new Code();
                this.print = new Code();
 
@@ -94,9 +96,9 @@ public class InterfaceConstruct extends Construct {
         */
        private Code generateAutoPrintFunction() {
                Code code = new Code();
-               // For RET
+               // For C_RET
                code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType,
-                               SpecNaming.RET));
+                               SpecNaming.C_RET));
                // For arguments
                for (VariableDeclaration decl : funcHeader.args) {
                        String type = decl.type;
@@ -124,8 +126,9 @@ public class InterfaceConstruct extends Construct {
                if (!name.equals(SpecNaming.Interface)
                                && !name.equals(SpecNaming.Transition)
                                && !name.equals(SpecNaming.PreCondition)
-                               && !name.equals(SpecNaming.JustifyingCondition)
+                               && !name.equals(SpecNaming.JustifyingPrecondition)
                                && !name.equals(SpecNaming.SideEffect)
+                               && !name.equals(SpecNaming.JustifyingPostcondition)
                                && !name.equals(SpecNaming.PostCondition)
                                && !name.equals(SpecNaming.PrintValue)) {
                        WrongAnnotationException.err(file, lineNum, name
@@ -181,8 +184,10 @@ public class InterfaceConstruct extends Construct {
                                this.transition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PreCondition)) {
                                this.preCondition.addLines(primitive.contents);
-                       } else if (name.equals(SpecNaming.JustifyingCondition)) {
-                               this.justifyingCondition.addLines(primitive.contents);
+                       } else if (name.equals(SpecNaming.JustifyingPrecondition)) {
+                               this.justifyingPrecondition.addLines(primitive.contents);
+                       } else if (name.equals(SpecNaming.JustifyingPostcondition)) {
+                               this.justifyingPostcondition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PostCondition)) {
                                this.postCondition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PrintValue)) {

diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
index f8925fbd0d7fb1a2d8f42c21e4874bd4911031a8..a12ce256cfe7e72f924524bdec7850117021daba 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
@@ -624,7 +624,7 @@ public class SpecExtractor {
                        lineReader = new LineNumberReader(br);
                        // "/\*\*\s*@(DeclareState|Interface)"
                        Pattern regexpBegin = Pattern
-                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingCondition|Transition|PostCondition|Define)");
+                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingCondition|Transition|JustifyingPostcondition|PostCondition|Define)");
                        Matcher matcher = regexpBegin.matcher("");
 
                        String line;
@@ -654,8 +654,9 @@ public class SpecExtractor {
                                                                beginLineNum);
                                        } else if (constructName.equals(SpecNaming.Interface)
                                                        || constructName.equals(SpecNaming.PreCondition)
-                                                       || constructName.equals(SpecNaming.JustifyingCondition)
+                                                       || constructName.equals(SpecNaming.JustifyingPrecondition)
                                                        || constructName.equals(SpecNaming.Transition)
+                                                       || constructName.equals(SpecNaming.JustifyingPostcondition)
                                                        || constructName.equals(SpecNaming.PostCondition)) {
                                                extractInterfaceConstruct(file, lineReader, line,
                                                                beginLineNum);

diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java
index 5b48c99faf6fb95874a680e498cf61d10e1233c2..9f1c5dde4397c7eb1e893e8ecf6783851c48f0fd 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecNaming.java
+++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java
@@ -33,8 +33,9 @@ public class SpecNaming {
        public static final String Interface = "Interface";
        public static final String Transition = "Transition";
        public static final String PreCondition = "PreCondition";
-       public static final String JustifyingCondition = "JustifyingCondition";
+       public static final String JustifyingPrecondition = "JustifyingPrecondition";
        public static final String SideEffect = "SideEffect";
+       public static final String JustifyingPostcondition = "JustifyingPostcondition";
        public static final String PostCondition = "PostCondition";
        public static final String PrintValue = "Print";
 
@@ -42,8 +43,9 @@ public class SpecNaming {
        public static final String PrintValueType = "PRINT_VALUE";
        public static final String TransitionType = "TRANSITION";
        public static final String PreConditionType = "PRE_CONDITION";
-       public static final String JustifyingConditionType = "JUSTIFYING_CONDITION";
+       public static final String JustifyingPreconditionType = "JUSTIFYING_PRECONDITION";
        public static final String SideEffectType = "SIDE_EFFECT";
+       public static final String JustifyingPostconditionType = "JUSTIFYING_POSTCONDITION";
        public static final String PostConditionType = "POST_CONDITION";
 
        // Ordering point construct
@@ -194,7 +196,8 @@ public class SpecNaming {
        public static final String OldStateInst = "OLD";
        public static final String NewStateInst = "NEW";
        // Specification types and macros
-       public static final String RET = "RET";
+       public static final String C_RET = "C_RET";
+       public static final String S_RET = "S_RET";
        public static final String InterfaceValueInst = "__value";
        
        // The fake ordering point operation