save
authorPeizhao Ou <peizhaoo@uci.edu>
Sat, 26 Oct 2013 01:26:52 +0000 (18:26 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Sat, 26 Oct 2013 01:26:52 +0000 (18:26 -0700)
grammer/spec_compiler.jj
notes/generated_code_examples.txt
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java

index 8e2477d..22fada8 100644 (file)
@@ -20,6 +20,7 @@
                @InitVar:
                @DefineFunc:
                ...
+               @DefineFunc:
        @Interface_cluster:
                ...
        @Happens-before:
@@ -747,6 +748,7 @@ GlobalConstruct Global_construct() :
 SequentialDefineSubConstruct Global_define() :
 {
        ArrayList<String> initVar, defineFunc, code;
+       ArrayList<ArrayList<String>> defineFuncs;
        ArrayList<VariableDeclaration> declareVars;
        VariableDeclaration declareVar;
 
@@ -755,16 +757,16 @@ SequentialDefineSubConstruct Global_define() :
        {
                declareVars = null;
                initVar = null;
-               defineFunc = null;
+               defineFuncs = new ArrayList<ArrayList<String>>();
        }
        <GLOBAL_DEFINE>
                (<DECLARE_VAR> ((declareVar = TypeParam() ";" {
                        declareVars.add(declareVar); } )*))?
        (<INIT_VAR> (code = C_CPP_CODE(null) { initVar = code; } ))?
-       (<DEFINE_FUNC> (code = C_CPP_CODE(null) { defineFunc = code; }))?
+       (<DEFINE_FUNC> (defineFunc = C_CPP_CODE(null) { defineFuncs.add(defineFunc); }))*
        {
                SequentialDefineSubConstruct res = new
-                       SequentialDefineSubConstruct(declareVars, initVar, defineFunc);
+                       SequentialDefineSubConstruct(declareVars, initVar, defineFuncs);
                //System.out.println(res);
                return res;
        }
index ce40580..95e649a 100644 (file)
@@ -2,14 +2,14 @@
 Global Variable Declaration
 
 /* Include all the header files that contains the interface declaration */
-#include <iostream>
 #inlcude <atomic>
 #include <memory>
 #include <assert.h>
 
 /* Other necessary header files */
+#include <stdint.h>
 #include <specannotation.h>
-#include <spec_tag.h>
+#include <spec_lib.h>
 
 /* All other user-defined functions */
 ALL_USER_DEFINED_FUNCTIONS
@@ -121,8 +121,7 @@ Interface Wrapper
 #include <threads.h>
 #include <cdsannotate.h>
 #include <specannotation.h>
-#include <spec_tag.h>
-#include <spec_private_hashtable.h>
+#include <spec_lib.h>
 
 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
 {
@@ -167,11 +166,8 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
 Potential Commit Point
 
 
-#include <threads.h>
-#include <cdstrace.h>
-#include <cdsannotate.h>
-#include <spec_private_hashtable.h>
 #include <stdint.h>
+#include <cdsannotate.h>
 
 /* Should add the __ATOMIC_RET__ if necessary */
 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
@@ -189,10 +185,7 @@ if (POTENTIAL_CP_DEFINE_CONDITION) {
 Commit Point Define
 
 #include <threads.h>
-#include <cdstrace.h>
 #include <cdsannotate.h>
-#include <spec_private_hashtable.h>
-#include <_spec_sequential_generated.h>
 #include <stdint.h>
 
 /* Should add the __ATOMIC_RET__ if necessary */
@@ -220,10 +213,7 @@ Commit Point Define Check
 
 
 #include <threads.h>
-#include <cdstrace.h>
 #include <cdsannotate.h>
-#include <spec_private_hashtable.h>
-#include <_spec_sequential_generated.h>
 #include <stdint.h>
 
 /* Should add the __ATOMIC_RET__ if necessary */
index 3dbb595..e685bc6 100644 (file)
@@ -54,7 +54,7 @@ public class CodeGenerator {
                this.codeAdditions = new HashMap<File, ArrayList<CodeAddition>>();
 
 
-               _semantics = new SemanticsChecker(_extractor.getConstructs());
+               _semantics = new SemanticsChecker(_extractor);
                try {
                        _semantics.check();
                        System.out.println(_semantics);
index 1f7c3a0..e2ae18b 100644 (file)
@@ -1,6 +1,8 @@
 package edu.uci.eecs.specCompiler.codeGenerator;
 
 import java.util.ArrayList;
+import java.util.HashSet;
+import java.io.File;
 
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
@@ -9,19 +11,21 @@ import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
+import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
 
 public class CodeVariables {
        // C++ code or library
-       public static final String HEADER_THREADS = "threads.h";
+       public static final String HEADER_THREADS = "<threads.h>";
+       public static final String HEADER_STDINT = "<stdint.h>";
        public static final String ThreadIDType = "thrd_t";
        public static final String GET_THREAD_ID = "thrd_current";
        public static final String BOOLEAN = "bool";
        public static final String UINT64 = "uint64_t";
 
        // Model checker code
-       public static final String HEADER_CDSANNOTATE = "cdsannotate.h";
-       public static final String HEADER_SPECANNOTATION = "specannotation.h";
-       public static final String HEADER_CDSTRACE = "cdstrace.h";
+       public static final String HEADER_CDSANNOTATE = "<cdsannotate.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 CDSAnnotateType = "SPEC_ANALYSIS";
 
@@ -45,21 +49,15 @@ public class CodeVariables {
        public static final String ANNO_POST_CHECK = "anno_post_check";
 
        // Specification variables
-       public static final String HEADER_SPEC_SEQUENTIAL = "_spec_sequential.h";
-       public static final String SPEC_SEQUENTIAL_HEADER_MACRO = HEADER_SPEC_SEQUENTIAL
-                       .replace('.', '_').toUpperCase();
-
        public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
-       public static final String VAR_CALL_SEQUENCE_NUM = "call_sequence_num";
 
        // Specification library
+       public static final String HEADER_SPEC_LIB = "<spec_lib.h>";
        public static final String SPEC_QUEUE = "spec_queue";
        public static final String SPEC_STACK = "spec_stack";
        public static final String SPEC_DEQUE = "spec_deque";
        public static final String SPEC_HASHTABLE = "spec_hashtable";
-       public static final String HEADER_SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable.h";
        public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
-       public static final String HEADER_SPEC_TAG = "spec_tag.h";
        public static final String SPEC_TAG = "spec_tag";
        public static final String SPEC_TAG_CURRENT = "current";
        public static final String SPEC_TAG_NEXT = "next";
@@ -81,7 +79,7 @@ public class CodeVariables {
        }
 
        private static String INCLUDE(String header) {
-               return "#include <" + header + ">";
+               return "#include " + header;
        }
 
        private static String DEFINE(String left, String right) {
@@ -104,8 +102,8 @@ public class CodeVariables {
                return structName + "." + field + " = &" + val + ";";
        }
 
-       private static String DECLARE(String structType, String structName) {
-               return structType + " " + structName + ";";
+       private static String DECLARE(String type, String name) {
+               return type + " " + name + ";";
        }
 
        private static String DECLARE_DEFINE(String type, String var, String val) {
@@ -116,23 +114,51 @@ public class CodeVariables {
                return CDSAnnotate + "(" + CDSAnnotateType + ", &" + structName + ");";
        }
 
+       private static HashSet<String> getAllHeaders(SemanticsChecker semantics) {
+               HashSet<String> headers = new HashSet<String>();
+               for (String interfaceName : semantics.interfaceName2Construct.keySet()) {
+                       File f = semantics.interfaceName2Construct.get(interfaceName).file;
+                       headers.addAll(semantics.srcFilesInfo.get(f).headers);
+               }
+               return headers;
+       }
+
        public static ArrayList<String> generateGlobalVarDeclaration(
                        SemanticsChecker semantics, GlobalConstruct construct) {
                ArrayList<String> newCode = new ArrayList<String>();
+               HashSet<String> allHeaders = getAllHeaders(semantics);
 
-               // Header conflicting avoidance macro & headers
-               newCode.add("/** @file " + HEADER_SPEC_SEQUENTIAL);
-               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);
+               // All headers needed by the interface decalration
+               newCode.add(COMMENT("/* Include all the header files that contains the interface declaration */"));
+               for (String header : allHeaders) {
+                       newCode.add(INCLUDE(header));
+               }
                newCode.add("");
-               newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
-               newCode.add(INCLUDE(HEADER_SPECANNOTATION));
-               newCode.add(INCLUDE(HEADER_SPEC_TAG));
+               // Other necessary headers
+               newCode.add(INCLUDE(HEADER_STDINT));
+               newCode.add(INCLUDE(HEADER_CDSANNOTATE));
+               newCode.add(INCLUDE(HEADER_SPEC_LIB));
                newCode.add("");
+
+               SequentialDefineSubConstruct code = construct.code;
+               // User-defined functions
+               newCode.add(COMMENT("All other user-defined functions"));
+               ArrayList<ArrayList<String>> defineFuncs = code.defineFuncs;
+               for (int i = 0; i < defineFuncs.size(); i++) {
+                       newCode.addAll(defineFuncs.get(i));
+                       newCode.add("");
+               }
+
+               // Define necessary info structure
+               newCode.add(COMMENT("Definition of interface info struct (per interface)"));
                
-               
+
+               // User-defined variables
+               ArrayList<VariableDeclaration> varDecls = code.declareVar;
+               for (int i = 0; i < varDecls.size(); i++) {
+                       VariableDeclaration varDecl = varDecls.get(i);
+                       newCode.add(DECLARE(varDecl.type, varDecl.name));
+               }
 
                // printCode(newCode);
                return newCode;
@@ -185,27 +211,22 @@ public class CodeVariables {
                ArrayList<String> newCode = new ArrayList<String>();
 
                // Generate necessary header file (might be redundant but never mind)
-               
 
                // Generate wrapper header
-               
 
                // Wrapper function body
-               
+
                // Interface begin
-               
+
                // Call original renamed function
-               
+
                // HB conditions
-               
-               
+
                // Interface end
-               
 
                // End of the wrapper function
-               
 
-//             printCode(newCode);
+               // printCode(newCode);
                return newCode;
        }
 
@@ -219,11 +240,8 @@ public class CodeVariables {
                newCode.add(COMMENT("Include redundant headers"));
                newCode.add(INCLUDE(HEADER_THREADS));
                newCode.add(INCLUDE(HEADER_CDSTRACE));
-               newCode.add(INCLUDE(HEADER_SPEC_PRIVATE_HASHTABLE));
-               newCode.add(INCLUDE(HEADER_SPEC_SEQUENTIAL));
                newCode.add("");
                // Some necessary function calls
-               
 
                return newCode;
        }
index 495801b..d09a61c 100644 (file)
@@ -1,11 +1,14 @@
 package edu.uci.eecs.specCompiler.codeGenerator;
 
+import java.io.File;
 import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.HashSet;
 
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ClassBeginConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.Construct;
 import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
@@ -13,43 +16,51 @@ import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
+import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
 
 public class SemanticsChecker {
+       public final HashMap<File, SourceFileInfo> srcFilesInfo;
        public final ArrayList<Construct> constructs;
        public final HashMap<String, Construct> CPLabel2Construct;
-       public final HashMap<String, Construct> potentialCPLabel2Construct;
-       public final HashMap<String, Construct> interfaceName2Construct;
+       public final HashMap<String, PotentialCPDefineConstruct> potentialCPLabel2Construct;
+       public final HashMap<String, InterfaceConstruct> interfaceName2Construct;
        public final HashMap<String, Construct> interfaceName2DefineConstruct;
        public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
-       
+
        public final HashMap<String, Integer> interface2Num;
        public final HashMap<String, Integer> hbLabel2Num;
        public final HashMap<String, Integer> commitPointLabel2Num;
 
        private HashMap<String, String> options;
        private HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbConditions;
-       private Construct entryPointConstruct;
-       
+       private ArrayList<EntryPointConstruct> entryPointConstructs;
+       private ClassBeginConstruct classBeginConstruct;
+       private ClassEndConstruct classEndConstruct;
+
        private int _interfaceNum;
        private int _hbLabelNum;
-       private int _commitPointNum;    
+       private int _commitPointNum;
 
-       public SemanticsChecker(ArrayList<Construct> constructs) {
-               this.constructs = constructs;
+       public SemanticsChecker(SpecExtractor extractor) {
+               this.srcFilesInfo = extractor.srcFilesInfo;
+               this.constructs = extractor.getConstructs();
                this.CPLabel2Construct = new HashMap<String, Construct>();
-               this.potentialCPLabel2Construct = new HashMap<String, Construct>();
-               this.interfaceName2Construct = new HashMap<String, Construct>();
+               this.potentialCPLabel2Construct = new HashMap<String, PotentialCPDefineConstruct>();
+               this.interfaceName2Construct = new HashMap<String, InterfaceConstruct>();
                this.interfaceName2DefineConstruct = new HashMap<String, Construct>();
                this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
-               this.entryPointConstruct = null;
-               
+               this.entryPointConstructs = new ArrayList<EntryPointConstruct>();
+               this.classBeginConstruct = null;
+               this.classEndConstruct = null;
+
                this.interface2Num = new HashMap<String, Integer>();
                this.hbLabel2Num = new HashMap<String, Integer>();
                // Immediately init the true HB-condition to be 0
                hbLabel2Num.put("", 0);
-               
+
                this.commitPointLabel2Num = new HashMap<String, Integer>();
-               
+
                _interfaceNum = 0;
                _hbLabelNum = 0;
                _commitPointNum = 0;
@@ -78,16 +89,16 @@ public class SemanticsChecker {
                                                + interfaceName + " doesn't contain HB_codition: "
                                                + label + "!");
                        }
-                       
+
                        // No HB condition label can duplicate!
                        if (hbLabel2Num.containsKey(label)) {
                                throw new SemanticsCheckerException("Happens-before label: "
                                                + label + " duplicates!");
                        }
-                       
+
                        // Number the HB-condition label
                        hbLabel2Num.put(label, _hbLabelNum++);
-               }       
+               }
        }
 
        private void checkLabelDuplication(Construct construct, String label)
@@ -103,17 +114,25 @@ public class SemanticsChecker {
        }
 
        private void postCheck() throws SemanticsCheckerException {
-               // This is a C program, must provide the entry point
-               if (getOption("LANG").equals("C") && entryPointConstruct == null) {
+               // C++ data structure with Class must provide the beginning and ending
+               // of its declaration
+               if (getOption("Class") != null) {
+                       if (classBeginConstruct == null || classEndConstruct == null) {
+                               throw new SemanticsCheckerException(
+                                               "Class must provide the boundary explicitly!");
+                       }
+               }
+               // It must provide the entry point
+               if (entryPointConstructs.size() == 0) {
                        throw new SemanticsCheckerException(
-                                       "C program must provide the entry point!");
+                                       "The program must have at least one entry point!");
                }
 
                // Check if interface define construct labels are correct
                for (String name : interfaceName2DefineConstruct.keySet()) {
                        if (!interfaceName2Construct.containsKey(name)) {
-                               throw new SemanticsCheckerException(
-                                               "Label \"" + name + "\" does not have interface declaration!");
+                               throw new SemanticsCheckerException("Label \"" + name
+                                               + "\" does not have interface declaration!");
                        }
                }
        }
@@ -131,8 +150,9 @@ public class SemanticsChecker {
                                }
                                // Number the interface label
                                interface2Num.put(iConstruct.name, _interfaceNum++);
-                               
-                               interfaceName2Construct.put(iConstruct.name, constructs.get(i));
+
+                               interfaceName2Construct.put(iConstruct.name,
+                                               (InterfaceConstruct) constructs.get(i));
 
                                for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
                                        String label = iConstruct.commitPointSet.get(j);
@@ -164,7 +184,7 @@ public class SemanticsChecker {
                                for (ConditionalInterface left : hbConditions.keySet()) {
                                        HashSet<ConditionalInterface> set = hbConditions.get(left);
                                        checkHBLabelConsistency(left);
-                                       
+
                                        for (ConditionalInterface right : set) {
                                                checkHBLabelConsistency(right);
                                        }
@@ -175,15 +195,16 @@ public class SemanticsChecker {
                                checkLabelDuplication(construct, label);
                                // Number the commit_point label
                                commitPointLabel2Num.put(label, _commitPointNum++);
-                               
-                               potentialCPLabel2Construct.put(label, construct);
+
+                               potentialCPLabel2Construct.put(label,
+                                               (PotentialCPDefineConstruct) construct);
                        } else if (construct instanceof CPDefineCheckConstruct) {
                                CPDefineCheckConstruct theConstruct = (CPDefineCheckConstruct) construct;
                                label = theConstruct.label;
                                checkLabelDuplication(construct, label);
                                // Number the commit_point label
                                commitPointLabel2Num.put(label, _commitPointNum++);
-                               
+
                                CPLabel2Construct.put(label, construct);
                        } else if (construct instanceof CPDefineConstruct) {
                                CPDefineConstruct theConstruct = (CPDefineConstruct) construct;
@@ -191,14 +212,10 @@ public class SemanticsChecker {
                                checkLabelDuplication(construct, label);
                                // Number the commit_point label
                                commitPointLabel2Num.put(label, _commitPointNum++);
-                               
+
                                CPLabel2Construct.put(label, construct);
                        } else if (construct instanceof EntryPointConstruct) {
-                               if (entryPointConstruct != null) {
-                                       throw new SemanticsCheckerException(
-                                                       "More than one entry point!");
-                               }
-                               entryPointConstruct = construct;
+                               entryPointConstructs.add((EntryPointConstruct) construct);
                        } else if (construct instanceof InterfaceDefineConstruct) {
                                InterfaceDefineConstruct theConstruct = (InterfaceDefineConstruct) construct;
                                String name = theConstruct.name;
@@ -207,24 +224,23 @@ public class SemanticsChecker {
                                                        "Interface define label duplicates!");
                                }
                                interfaceName2DefineConstruct.put(name, construct);
+                       } else if (construct instanceof ClassBeginConstruct) {
+                               classBeginConstruct = (ClassBeginConstruct) construct;
+                       } else if (construct instanceof ClassEndConstruct) {
+                               classEndConstruct = (ClassEndConstruct) construct;
                        }
                }
        }
 
        public String toString() {
                StringBuilder sb = new StringBuilder();
-               if (entryPointConstruct == null) {
-                       sb.append("Entry point is not specified!");
-               } else {
-                       sb.append("@Entry_point:\n" + entryPointConstruct);
-               }
-               
+
                sb.append("Interface name 2 Construct:\n");
                for (String interfaceName : interfaceName2Construct.keySet()) {
                        sb.append(interfaceName + "\t"
                                        + interfaceName2Construct.get(interfaceName) + "\n");
                }
-               
+
                sb.append("Interface name 2 define construct:\n");
                for (String interfaceName : interfaceName2DefineConstruct.keySet()) {
                        sb.append(interfaceName + "\t"
index fb6828e..29080a8 100644 (file)
@@ -3,14 +3,15 @@ package edu.uci.eecs.specCompiler.specExtraction;
 import java.util.ArrayList;
 
 public class SequentialDefineSubConstruct {
-       public final ArrayList<String> initVar, defineFunc;
+       public final ArrayList<String> initVar;
+       public final ArrayList<ArrayList<String>> defineFuncs;
        public final ArrayList<VariableDeclaration> declareVar;
 
        public SequentialDefineSubConstruct(ArrayList<VariableDeclaration> declareVar,
-                       ArrayList<String> initVar, ArrayList<String> defineFunc) {
+                       ArrayList<String> initVar, ArrayList<ArrayList<String>> defineFuncs) {
                this.declareVar = declareVar;
                this.initVar = initVar;
-               this.defineFunc = defineFunc;
+               this.defineFuncs = defineFuncs;
        }
 
        public String toString() {
@@ -21,7 +22,9 @@ public class SequentialDefineSubConstruct {
                res.append("@InitVar:\n");
                res.append(ParserUtils.array2Str(initVar));
                res.append("@DefineFunc:\n");
-               res.append(ParserUtils.array2Str(defineFunc));
+               for (int i = 0; i < defineFuncs.size(); i++) {
+                       res.append(ParserUtils.array2Str(defineFuncs.get(i)) + "\n");
+               }
                return res.toString();
        }
 }