projects / cdsspec-compiler.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
fix bugs
[cdsspec-compiler.git] / src / edu / uci / eecs / specCompiler / codeGenerator / CodeVariables.java
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index 980e42064d74cb09dd1533fbeff413e5ab5591d1..4abd5699d300140353f325036966661f72aca8b8 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -33,13 +33,16 @@ public class CodeVariables {
 
        // Model checker code
        public static final String HEADER_CDSANNOTATE = "<cdsannotate.h>";
+       public static final String HEADER_COMMON = "<common.h>";
        public static final String HEADER_SPECANNOTATION = "<specannotation.h>";
        public static final String HEADER_CDSTRACE = "<cdstrace.h>";
-       public static final String CDSAnnotate = "cdsannotate";
+//     public static final String CDSAnnotate = "cdsannotate";
+       public static final String CDSAnnotate = "_Z11cdsannotatemPv";
        public static final String CDSAnnotateType = "SPEC_ANALYSIS";
-       public static final String IDType = "id_t";
+       public static final String IDType = "call_id_t";
 
        public static final String SPEC_ANNO_TYPE = "spec_anno_type";
+       public static final String SPEC_ANNO_TYPE_FUNC_TABLE_INIT = "FUNC_TABLE_INIT";
        public static final String SPEC_ANNO_TYPE_HB_INIT = "HB_INIT";
        public static final String SPEC_ANNO_TYPE_INTERFACE_BEGIN = "INTERFACE_BEGIN";
        public static final String SPEC_ANNO_TYPE_HB_CONDITION = "HB_CONDITION";
@@ -51,6 +54,7 @@ public class CodeVariables {
        public static final String SPEC_ANNOTATION_FIELD_TYPE = "type";
        public static final String SPEC_ANNOTATION_FIELD_ANNO = "annotation";
 
+       public static final String ANNO_FUNC_TABLE_INIT = "anno_func_table_init";
        public static final String ANNO_HB_INIT = "anno_hb_init";
        public static final String ANNO_INTERFACE_BEGIN = "anno_interface_begin";
        public static final String ANNO_INTERFACE_END = "anno_interface_end";
@@ -130,7 +134,15 @@ public class CodeVariables {
                        String val) {
                return structName + "->" + field + " = " + val + ";";
        }
+       
+       private static String ASSIGN_PTR_TO_PTR(String structName, String field, String val) {
+               return structName + "->" + field + " = &" + val + ";";
+       }
 
+       private static String STRUCT_NEW_DECLARE_DEFINE(String type, String name) {
+               return "struct " + type + " *" + name + " = (struct " + type + "*) malloc(sizeof(struct " + type + "));";
+       }
+       
        private static String DECLARE(String type, String name) {
                return type + " " + name + ";";
        }
@@ -145,7 +157,7 @@ public class CodeVariables {
        }
 
        private static String ANNOTATE(String structName) {
-               return CDSAnnotate + "(" + CDSAnnotateType + ", &" + structName + ");";
+               return CDSAnnotate + "(" + CDSAnnotateType + ", " + structName + ");";
        }
 
        private static ArrayList<String> DEFINE_INFO_STRUCT(String interfaceName,
@@ -158,7 +170,7 @@ public class CodeVariables {
                for (int i = 0; i < header.args.size(); i++) {
                        code.add(DECLARE(header.args.get(i)));
                }
-               code.add("} " + interfaceName + "_info {");
+               code.add("} " + interfaceName + "_info;");
                return code;
        }
 
@@ -187,7 +199,7 @@ public class CodeVariables {
                if (!header.returnType.equals("void") || header.args.size() != 0) {
                        String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
                        code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
-                                       BRACE(infoStructType) + "info"));
+                                       BRACE(infoStructType + "*") + "info"));
                        if (!header.returnType.equals("void")) {
                                code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
                                                GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
@@ -221,6 +233,8 @@ public class CodeVariables {
                if (construct.postAction.size() > 0) {
                        code.addAll(construct.postAction);
                }
+               // Return true finally
+               code.add("return true;");
 
                code.add("}");
 
@@ -275,9 +289,12 @@ public class CodeVariables {
                }
                newCode.add("");
                // Other necessary headers
+               newCode.add(INCLUDE(HEADER_STDLIB));
                newCode.add(INCLUDE(HEADER_STDINT));
                newCode.add(INCLUDE(HEADER_CDSANNOTATE));
+               newCode.add(INCLUDE(HEADER_COMMON));
                newCode.add(INCLUDE(HEADER_SPEC_LIB));
+               newCode.add(INCLUDE(HEADER_SPECANNOTATION));
                newCode.add("");
 
                SequentialDefineSubConstruct code = construct.code;
@@ -289,6 +306,13 @@ public class CodeVariables {
                        newCode.addAll(declareStruct);
                        newCode.add("");
                }
+               // User-defined variables
+               ArrayList<VariableDeclaration> varDecls = code.declareVar;
+               for (int i = 0; i < varDecls.size(); i++) {
+                       VariableDeclaration varDecl = varDecls.get(i);
+                       // Don't forget to make them static
+                       newCode.add(makeVariablesStatic(varDecl));
+               }
                // User-defined functions
                newCode.add(COMMENT("All other user-defined functions"));
                ArrayList<ArrayList<String>> defineFuncs = code.defineFuncs;
@@ -304,7 +328,8 @@ public class CodeVariables {
                                        .get(interfaceName);
                        FunctionHeader funcHeader = getFunctionHeader(semantics, iConstruct);
                        // Define necessary info structure
-                       if (!funcHeader.returnType.equals("void") || funcHeader.args.size() > 0) {
+                       if (!funcHeader.returnType.equals("void")
+                                       || funcHeader.args.size() > 0) {
                                newCode.add(COMMENT("Definition of interface info struct: "
                                                + interfaceName));
                                newCode.addAll(DEFINE_INFO_STRUCT(interfaceName, funcHeader));
@@ -316,14 +341,14 @@ public class CodeVariables {
                        // Define ID function
                        newCode.add(COMMENT("ID function of interface: " + interfaceName));
                        newCode.addAll(DEFINE_ID_FUNC(interfaceName, iConstruct.idCode));
-                       newCode.add(COMMENT("End of ID function: + " + interfaceName));
+                       newCode.add(COMMENT("End of ID function: " + interfaceName));
                        newCode.add("");
 
                        // Define check_action function
                        newCode.add(COMMENT("Check action function of interface: "
                                        + interfaceName));
                        newCode.addAll(DEFINE_CHECK_ACTION_FUNC(iConstruct, funcHeader));
-                       newCode.add(COMMENT("End of check action function: + "
+                       newCode.add(COMMENT("End of check action function: "
                                        + interfaceName));
                        newCode.add("");
                }
@@ -332,13 +357,6 @@ public class CodeVariables {
                                .toString(semantics.interfaceName2Construct.size());
                newCode.add(DEFINE("INTERFACE_SIZE", interfaceSize));
                newCode.add(DECLARE("void**", "func_ptr_table"));
-               // User-defined variables
-               ArrayList<VariableDeclaration> varDecls = code.declareVar;
-               for (int i = 0; i < varDecls.size(); i++) {
-                       VariableDeclaration varDecl = varDecls.get(i);
-                       // Don't forget to make them static
-                       newCode.add(makeVariablesStatic(varDecl));
-               }
 
                newCode.add("");
                newCode.add(COMMENT("Define function for sequential code initialization"));
@@ -346,7 +364,7 @@ public class CodeVariables {
                // Init func_ptr_table
                newCode.add(COMMENT("Init func_ptr_table"));
                newCode.add(ASSIGN("func_ptr_table",
-                               "(void**) malloc(sizeof(void*) * 2)"));
+                               "(void**) malloc(sizeof(void*) * " + semantics.interface2Num.size() + " * 2)"));
                for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
                        String interfaceNum = Integer.toString(semantics.interface2Num
                                        .get(interfaceName));
@@ -358,8 +376,19 @@ public class CodeVariables {
                newCode.add("");
                // Init user-defined variables
                newCode.addAll(construct.code.initVar);
+               // Pass function table info
+               newCode.add(COMMENT("Pass function table info"));
+               String structName = "anno_func_table_init", anno = "func_init";
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_FUNC_TABLE_INIT, structName));
+               newCode.add(ASSIGN_TO_PTR(structName, "size", "INTERFACE_SIZE"));
+               newCode.add(ASSIGN_TO_PTR(structName, "table", "func_ptr_table"));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
+               newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_FUNC_TABLE_INIT));
+               newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
+               newCode.add(ANNOTATE(anno));
+
                // Pass Happens-before relationship
-               generateHBInitAnnotation(semantics);
+               newCode.addAll(generateHBInitAnnotation(semantics));
                newCode.add("}");
                newCode.add(COMMENT("End of Global construct generation in class"));
 
@@ -420,20 +449,20 @@ public class CodeVariables {
                                                                .get(right.hbConditionLabel));
                                newCode.add(COMMENT(left + " -> " + right));
 
-                               newCode.add(ANNO_HB_INIT + " " + structVarName + ";");
-                               newCode.add(ASSIGN(structVarName, "interface_num_before",
+                               newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_HB_INIT, structVarName));
+                               newCode.add(ASSIGN_TO_PTR(structVarName, "interface_num_before",
                                                interfaceNumBefore));
-                               newCode.add(ASSIGN(structVarName, "hb_condition_num_before",
+                               newCode.add(ASSIGN_TO_PTR(structVarName, "hb_condition_num_before",
                                                hbLabelNumBefore));
-                               newCode.add(ASSIGN(structVarName, "interface_num_after",
+                               newCode.add(ASSIGN_TO_PTR(structVarName, "interface_num_after",
                                                interfaceNumAfter));
-                               newCode.add(ASSIGN(structVarName, "hb_condition_num_after",
+                               newCode.add(ASSIGN_TO_PTR(structVarName, "hb_condition_num_after",
                                                hbLabelNumAfter));
 
-                               newCode.add(DECLARE(SPEC_ANNOTATION, annotationVarName));
-                               newCode.add(ASSIGN(annotationVarName,
+                               newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, annotationVarName));
+                               newCode.add(ASSIGN_TO_PTR(annotationVarName,
                                                SPEC_ANNOTATION_FIELD_TYPE, SPEC_ANNO_TYPE_HB_INIT));
-                               newCode.add(ASSIGN_PTR(annotationVarName,
+                               newCode.add(ASSIGN_TO_PTR(annotationVarName,
                                                SPEC_ANNOTATION_FIELD_ANNO, structVarName));
                                newCode.add(ANNOTATE(annotationVarName));
                        }
@@ -470,21 +499,29 @@ public class CodeVariables {
                }
 
                // Generate wrapper header
+               // If it's not in a class, we should declare the wrapper function
+               if (semantics.getClassName() == null) {
+                       FunctionHeader renamedHeader = header
+                                       .getRenamedHeader(SPEC_INTERFACE_WRAPPER);
+                       newCode.add(COMMENT("Declaration of the wrapper"));
+                       newCode.add(renamedHeader + ";");
+                       newCode.add("");
+               }
                newCode.add(header.toString() + " {");
                // Wrapper function body
                newCode.add(COMMENT("Interface begins"));
                // Interface begin
                String structName = "interface_begin";
-               newCode.add(DECLARE(ANNO_INTERFACE_BEGIN, "interface_begin"));
-               newCode.add(ASSIGN(structName, "interface_num", interfaceNum));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_INTERFACE_BEGIN, "interface_begin"));
+               newCode.add(ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
                String anno = "annotation_interface_begin";
-               newCode.add(DECLARE(SPEC_ANNOTATION, anno));
-               newCode.add(ASSIGN(structName, "type", SPEC_ANNO_TYPE_INTERFACE_BEGIN));
-               newCode.add(ASSIGN_PTR(structName, "annotation", structName));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
+               newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_INTERFACE_BEGIN));
+               newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
                newCode.add(ANNOTATE(anno));
                // Call original renamed function
                if (header.returnType.equals("void")) {
-                       newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER));
+                       newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER) + ";");
                } else {
                        newCode.add(DECLARE_DEFINE(header.returnType, MACRO_RETURN,
                                        header.getRenamedCall(SPEC_INTERFACE_WRAPPER)));
@@ -496,14 +533,14 @@ public class CodeVariables {
                                        .get(label));
                        newCode.add("if " + BRACE(condition) + " {");
                        structName = "hb_condition";
-                       newCode.add(DECLARE(ANNO_HB_CONDITION, structName));
-                       newCode.add(ASSIGN(structName, "interface_num", interfaceNum));
+                       newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_HB_CONDITION, structName));
+                       newCode.add(ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
 
-                       newCode.add(ASSIGN(structName, "hb_condition_num", hbCondNum));
+                       newCode.add(ASSIGN_TO_PTR(structName, "hb_condition_num", hbCondNum));
                        anno = "annotation_hb_condition";
-                       newCode.add(DECLARE(SPEC_ANNOTATION, anno));
-                       newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_HB_CONDITION));
-                       newCode.add(ASSIGN_PTR(anno, "annotation", structName));
+                       newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
+                       newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_HB_CONDITION));
+                       newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
                        newCode.add(ANNOTATE(anno));
                        newCode.add("}");
                        newCode.add("");
@@ -513,7 +550,7 @@ public class CodeVariables {
                if (!header.returnType.equals("void") || header.args.size() > 0) {
                        infoStructType = interfaceName + "_info";
                        infoName = "info";
-                       newCode.add(DECLARE_DEFINE(infoStructType, infoName,
+                       newCode.add(DECLARE_DEFINE(infoStructType + "*", infoName,
                                        BRACE(infoStructType + "*") + " malloc(sizeof("
                                                        + infoStructType + "))"));
                        if (!header.returnType.equals("void")) {
@@ -528,13 +565,17 @@ public class CodeVariables {
                }
                structName = "interface_end";
                anno = "annoation_interface_end";
-               newCode.add(DECLARE(ANNO_INTERFACE_END, structName));
-               newCode.add(ASSIGN(structName, "interface_num", interfaceNum));
-               newCode.add(ASSIGN(structName, "info", infoName));
-               newCode.add(DECLARE(SPEC_ANNOTATION, anno));
-               newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_INTERFACE_END));
-               newCode.add(ASSIGN_PTR(anno, "annotation", structName));
-               ANNOTATE(anno);
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_INTERFACE_END, structName));
+               newCode.add(ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
+               newCode.add(ASSIGN_TO_PTR(structName, "info", infoName));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
+               newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_INTERFACE_END));
+               newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
+               newCode.add(ANNOTATE(anno));
+               // Return __RET__ if it's not void
+               if (!header.returnType.equals("void")) {
+                       newCode.add("return " + MACRO_RETURN + ";");
+               }
                // End of the wrapper function
                newCode.add("}");
 
@@ -583,13 +624,13 @@ public class CodeVariables {
                // Add annotation
                newCode.add("if (" + construct.condition + ") {");
                String structName = "potential_cp_define", anno = "annotation_potential_cp_define";
-               newCode.add(DECLARE(ANNO_POTENTIAL_CP_DEFINE, structName));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_POTENTIAL_CP_DEFINE, structName));
                String labelNum = Integer.toString(semantics.commitPointLabel2Num
                                .get(construct.label));
-               newCode.add(ASSIGN(structName, "label_num", labelNum));
-               newCode.add(DECLARE(SPEC_ANNOTATION, anno));
-               newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE));
-               newCode.add(ASSIGN_PTR(anno, "annotation", structName));
+               newCode.add(ASSIGN_TO_PTR(structName, "label_num", labelNum));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
+               newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE));
+               newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
                newCode.add(ANNOTATE(anno));
                newCode.add("}");
                return newCode;
@@ -612,13 +653,13 @@ public class CodeVariables {
                // Add annotation
                newCode.add("if (" + construct.condition + ") {");
                String structName = "cp_define_check", anno = "annotation_cp_define_check";
-               newCode.add(DECLARE(ANNO_CP_DEFINE_CHECK, structName));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_DEFINE_CHECK, structName));
                String labelNum = Integer.toString(semantics.commitPointLabel2Num
                                .get(construct.label));
-               newCode.add(ASSIGN(structName, "label_num", labelNum));
-               newCode.add(DECLARE(SPEC_ANNOTATION, anno));
-               newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK));
-               newCode.add(ASSIGN_PTR(anno, "annotation", structName));
+               newCode.add(ASSIGN_TO_PTR(structName, "label_num", labelNum));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
+               newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK));
+               newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
                newCode.add(ANNOTATE(anno));
                newCode.add("}");
                return newCode;
@@ -634,13 +675,13 @@ public class CodeVariables {
                // Add annotation
                newCode.add("if (" + construct.condition + ") {");
                String structName = "cp_define", anno = "annotation_cp_define";
-               newCode.add(DECLARE(ANNO_CP_DEFINE, structName));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_DEFINE, structName));
                String labelNum = Integer.toString(semantics.commitPointLabel2Num
                                .get(construct.label));
-               newCode.add(ASSIGN(structName, "label_num", labelNum));
-               newCode.add(DECLARE(SPEC_ANNOTATION, anno));
-               newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE));
-               newCode.add(ASSIGN_PTR(anno, "annotation", structName));
+               newCode.add(ASSIGN_TO_PTR(structName, "label_num", labelNum));
+               newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
+               newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE));
+               newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
                newCode.add(ANNOTATE(anno));
                newCode.add("}");
                return newCode;
This is the public repository for the CDSSpec specification compiler.