edits

[cdsspec-compiler.git] / src / edu / uci / eecs / codeGenerator / CodeGeneratorUtils.java

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;