more changes
authorPeizhao Ou <peizhaoo@uci.edu>
Sun, 20 Oct 2013 16:17:26 +0000 (09:17 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Sun, 20 Oct 2013 16:17:26 +0000 (09:17 -0700)
notes/generated_code_examples.txt
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java

index aa0b388..5dc22b7 100644 (file)
@@ -4,58 +4,55 @@ Global Variable Declaration
 /* Include the header files first
 ** This declaration will be written into a header file
 */
-/* @file CDSName.h */
+/* @file _spec_sequential_generated.h */
 /* @brief automatically generated file */
-#ifndef _CDSNAME_H
-#define _CDSNAME_H
+#ifndef __SPEC_SEQUENTIAL_GENERATED_H
+#define __SPEC_SEQUENTIAL_GENERATED_H
 #include <specannotation.h>
 #include <spec_private_hashtable.h>
 
-typedef struct Sequential
-{
-       spec_private_hashtabel cond;
-       spec_private_hashtabel id;
-       spec_private_hashtabel interface;
-       spec_private_hashtabel interface_call_sequence;
+/* Beginning of struct Sequential */
+typedef struct Sequential {
+       spec_private_hashtable cond;
+       spec_private_hashtable id;
+       spec_private_hashtable interface;
+       spec_private_hashtable interface_call_sequence;
 
        /* DefineVar unfolded here */
        spec_private_hashtable Put__Old_Val;
 
-       /* Other user-defined variables */
+       /* Beginning of other user-defined variables */
        bool lock_acquired;
        int reader_lock_cnt;
-} Sequential;
+       /* End of other user-defined variables */
+
+} Sequential; /* End of struct Sequential */
 
+/* Instance of the struct */
 Sequential __sequential;
 
+/* Define function for sequential code initialization */
+void __sequential_init() {
+       /* Init internal variables */
+       init(&__sequential.cond);
+       init(&__sequential.id);
+       init(&__sequential.interface);
+       init(&__sequential.interface_call_sequence);
+       /* Init DefineVars */
+       init(&__sequential.Put__Old_Val);
+       /* Init user-defined variables */
+       lock_acquired = false;
+       reader_lock_cnt = 0;
+}
+
 /* All other user-defined functions */
 ALL_USER_DEFINED_FUNCTIONS
 
-
 #endif
 
 
 
 ******    Example2:    ******
-Global Variable Initialization (Entry Point Unfolding)
-
-#include <spec_private_hashtable.h>
-#include <CDSName.h>
-
-init(&__sequential.condition);
-init(&__sequential.id);
-init(&__sequential.interface);
-init(&__sequential.interface_call_sequence);
-/* DefineVar initialized here */
-init(&Put__Old_Val);
-
-/* User-define variables */
-lock_acquired = false;
-reader_lock_cnt = 0;
-
-
-
-******    Example3:    ******
 Interface Wrapper
 
 /* Include the header files first */
@@ -123,14 +120,14 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
 }
 
 
-******    Example4:    ******
+******    Example3:    ******
 Potential Commit Point
 
 #include <threads.h>
 #include <cdstrace.h>
 #include <cdsannotate.h>
 #include <spec_private_hashtable.h>
-#include <CDSName.h>
+#include <_sepc_sequential_genenrated.h>
 
 thrd_t __tid = thrd_current();
 uint64_t __ATOMIC_RET__ = get_prev_value(tid);
@@ -147,14 +144,14 @@ if (POTENTIAL_CP_DEFINE_CONDITION) {
        cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
 }
 
-******    Example5:    ******
+******    Example4:    ******
 Commit Point Define
 
 #include <threads.h>
 #include <cdstrace.h>
 #include <cdsannotate.h>
 #include <spec_private_hashtable.h>
-#include <CDSName.h>
+#include <_spec_sequential_generated.h>
 
 thrd_t __tid = thrd_current();
 int interface_num = get(&__sequential.interface, tid);
@@ -213,7 +210,7 @@ switch (interface_num) {
 }
 
 
-*****    Example6:    ******
+*****    Example5:    ******
 Commit Point Define Check
 
 
@@ -221,7 +218,7 @@ Commit Point Define Check
 #include <cdstrace.h>
 #include <cdsannotate.h>
 #include <spec_private_hashtable.h>
-#include <CDSName.h>
+#include <_spec_sequential_generated.h>
 
 
 thrd_t __tid = thrd_current();
index d051906..c69473a 100644 (file)
@@ -99,7 +99,7 @@ public class CodeGenerator {
                ArrayList<String> newCode = new ArrayList<String>();
 
                // Generate all sequential variables into a struct
-               newCode.add("struct " + CodeVariables.SPEC_STRUCT + " {\n");
+               newCode.add("struct " + CodeVariables.SPEC_SEQUENTIAL_STRUCT + " {\n");
 
                // Generate the code in global construct first
                SequentialDefineSubConstruct globalCode = construct.code;
index e0a41fa..4ee3e3d 100644 (file)
@@ -3,6 +3,10 @@ package edu.uci.eecs.specCompiler.codeGenerator;
 import java.util.ArrayList;
 
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
+import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
 
 public class CodeVariables {
        // C++ code or library
@@ -33,8 +37,11 @@ public class CodeVariables {
        public static final String ANNO_POST_CHECK = "anno_post_check";
 
        // Specification variables
-       public static final String SPEC_STRUCT = "Sequential";
-       public static final String SPEC_INSTANCE = "__sequential";
+       public static final String SPEC_SEQUENTIAL_HEADER = "_spec_sequential.h";
+       public static final String SPEC_SEQUENTIAL_HEADER_MACRO = SPEC_SEQUENTIAL_HEADER
+                       .replace('.', '_').toUpperCase();
+       public static final String SPEC_SEQUENTIAL_STRUCT = "Sequential";
+       public static final String SPEC_SEQUENTIAL_INSTANCE = "__sequential";
 
        public static final String SPEC_CONDITION = "condition";
        public static final String SPEC_ID = "id";
@@ -47,6 +54,7 @@ public class CodeVariables {
        public static final String SPEC_QUEUE = "spec_queue";
        public static final String SPEC_STACK = "spec_stack";
        public static final String SPEC_HASHTABLE = "spec_hashtable";
+       public static final String SPEC_PRIVATE_HASHTABLE_HEADER = "spec_private_hashtable.h";
        public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
        public static final String SPEC_TAG = "spec_tag";
 
@@ -55,6 +63,144 @@ public class CodeVariables {
        public static final String MACRO_COND = "__COND_SAT__";
        public static final String MACRO_RETURN = "__RET__";
 
+       // Break the code (String) into multiple lines and add it to newCode
+       private static void breakCodeLines(ArrayList<String> newCode, String code) {
+               int begin = 0, end = 0;
+               while (end < code.length()) {
+                       if (code.charAt(end) == '\n') {
+                               String line = code.substring(begin, end);
+                               newCode.add(line);
+                               begin = end + 1;
+                       }
+                       end++;
+               }
+       }
+
+       private static void printCode(ArrayList<String> code) {
+               for (int i = 0; i < code.size(); i++) {
+                       System.out.println(code.get(i));
+               }
+       }
+       
+       public static ArrayList<String> generateGlobalVarDeclaration(
+                       SemanticsChecker semantics, GlobalConstruct construct) {
+               ArrayList<String> newCode = new ArrayList<String>();
+
+               // Header conflicting avoidance macro & headers
+               newCode.add("/** @file " + SPEC_SEQUENTIAL_HEADER);
+               newCode.add(" *  @brief Automatically generated header file for sequential variables");
+               newCode.add(" */");
+               newCode.add("#ifndef " + SPEC_SEQUENTIAL_HEADER_MACRO);
+               newCode.add("#define " + SPEC_SEQUENTIAL_HEADER_MACRO);
+               newCode.add("#include " + "<" + SPEC_PRIVATE_HASHTABLE_HEADER + ">");
+               newCode.add("#include " + "<" + HEADER_SPECANNOTATION + ">");
+
+               // Generate all sequential variables into a struct
+               newCode.add("/* Beginning of struct " + SPEC_SEQUENTIAL_STRUCT + " */");
+               newCode.add("typedef struct " + SPEC_SEQUENTIAL_STRUCT + " {");
+               newCode.add("/* Condition of interface */");
+               newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_CONDITION + ";");
+               newCode.add("/* ID of interface */");
+               newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_ID + ";");
+               newCode.add("/* Current interface call */");
+               newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_INTERFACE + ";");
+               newCode.add("/* Current interface call sequence */");
+               newCode.add(SPEC_PRIVATE_HASHTABLE + " " + SPEC_INTERFACE_CALL_SEQUENCE
+                               + ";");
+               newCode.add("");
+               // DefineVar declaration
+               for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
+                       InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
+                                       .get(interfaceName).construct;
+                       ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
+                       newCode.add("/* DefineVar in " + interfaceName + " */");
+                       for (int i = 0; i < defineVars.size(); i++) {
+                               DefineVar var = defineVars.get(i);
+                               newCode.add(SPEC_PRIVATE_HASHTABLE + " " + var.getNewVarName()
+                                               + ";");
+                       }
+                       newCode.add("");
+               }
+               // Generate user-defined variable declaration
+               newCode.add("/* Beginnint of other user-defined variables */");
+               SequentialDefineSubConstruct globalCode = construct.code;
+               breakCodeLines(newCode, globalCode.declareVar);
+               newCode.add("/* End of other user-defined variables */");
+               // End of struct Sequential
+               newCode.add("} " + SPEC_SEQUENTIAL_STRUCT + "; /* End of struct "
+                               + SPEC_SEQUENTIAL_STRUCT + " */");
+
+               // Generate 
+               
+               // Generate code from the DefineVar, __COND_SAT__ and __ID__
+               // The hashtable in the contract can only contains pointers or integers
+               // __COND_SAT__
+               newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_CONDITION
+                               + ";");
+               // __ID__
+               newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";");
+               // DefineVars
+               for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
+                       InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
+                                       .get(interfaceName).construct;
+                       ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
+                       for (int i = 0; i < defineVars.size(); i++) {
+                               DefineVar var = defineVars.get(i);
+                               newCode.add(CodeVariables.SPEC_HASHTABLE + var.getNewVarName()
+                                               + ";");
+                       }
+               }
+               // __interface
+               newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE
+                               + ";");
+               // __interface_call_sequence
+               newCode.add(CodeVariables.SPEC_HASHTABLE
+                               + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ";");
+               // Interface call sequence varaiable
+               newCode.add(CodeVariables.SPEC_TAG + " "
+                               + CodeVariables.INTERFACE_CALL_SEQUENCE + ";");
+               // End of the struct
+               newCode.add("}");
+
+               // FIXME: Constructor should be modified and put in the right place
+               // Generate constructor (the place to initialize everything!)
+               breakCodeLines(newCode, globalCode.initVar);
+               // __COND_SAT__
+               newCode.add("init_table(&" + CodeVariables.SPEC_CONDITION + ");");
+               // __ID__
+               newCode.add("init_table(&" + CodeVariables.SPEC_ID + ");");
+               // DefineVars
+               for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
+                       InterfaceConstruct iConstruct = (InterfaceConstruct) semantics.interfaceName2Construct
+                                       .get(interfaceName).construct;
+                       ArrayList<DefineVar> defineVars = iConstruct.action.defineVars;
+                       for (int i = 0; i < defineVars.size(); i++) {
+                               DefineVar var = defineVars.get(i);
+                               newCode.add("init_table(&" + var.getNewVarName() + ");");
+                       }
+               }
+               // __interface
+               newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");");
+               // __interface_call_sequence
+               newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE
+                               + ");");
+
+               // Pass the happens-before relationship check here
+               newCode.addAll(CodeVariables.generateHBInitAnnotation(semantics));
+
+               newCode.add("\n");
+
+               // Generate the sequential functions
+               breakCodeLines(newCode, globalCode.defineFunc);
+
+               // The end
+               newCode.add("#endif " + SPEC_SEQUENTIAL_HEADER_MACRO + "\t/* End of "
+                               + SPEC_SEQUENTIAL_HEADER + " */");
+
+               printCode(newCode);
+               return newCode;
+       }
+
        public static ArrayList<String> generateHBInitAnnotation(
                        SemanticsChecker semantics) {
                ArrayList<String> newCode = new ArrayList<String>();
@@ -79,8 +225,9 @@ public class CodeVariables {
                                                + interfaceNumAfter + ";");
                                newCode.add(structVarName + "." + "hb_condition_num_after"
                                                + " = " + hbLabelNumAfter + ";");
-                               
-                               newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &" + structVarName + ");");
+
+                               newCode.add(CDSAnnotate + "(" + CDSAnnotateType + ", &"
+                                               + structVarName + ");");
                        }
                }
                return newCode;