more bug fix
authorPeizhao Ou <peizhaoo@uci.edu>
Sat, 2 Nov 2013 00:36:58 +0000 (17:36 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Sat, 2 Nov 2013 00:36:58 +0000 (17:36 -0700)
12 files changed:
benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
benchmark/linuxrwlocks/linuxrwlocks.c
grammer/spec.txt
grammer/spec_compiler.jj
src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java
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/ParserUtils.java
src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java
src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
test.c

index 299e7a3..c02c0a3 100644 (file)
@@ -95,7 +95,6 @@ class cliffc_hashtable {
                                map = spec_hashtable<TypeK, TypeV*>();
                                id_map = spec_hashtable<TypeK, TypeV*>();
                                tag = Tag();
-                       @DefineFunc:
                        static bool equals_val(TypeV *ptr1, TypeV *ptr2) {
                                // ...
                        }
@@ -369,7 +368,7 @@ friend class CHM;
                @Commit_point_set: Read_Val_Point1 | Read_Val_Point2 | Read_Val_Point3
                @ID: __sequential.getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
+                       TypeV *_Old_Val = __sequential.map.get(key)
                @Post_check:
                        __sequential.equals_val(_Old_Val, __RET__)
                @End
@@ -391,8 +390,8 @@ friend class CHM;
                @ID: __sequential.getKeyTag(key)
                @Action:
                        # Remember this old value at checking point
-                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
-                       @Code: __sequential.map.put(key, &val);
+                       TypeV *_Old_Val = __sequential.map.get(key)
+                       __sequential.map.put(key, &val);
                @Post_check:
                        __sequential.equals_val(__RET__, _Old_Val)
                @End
@@ -411,8 +410,7 @@ friend class CHM;
                        COND_PutIfAbsentSucc :: __RET__ == NULL
                @ID: __sequential.getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
-                       @Code:
+                       TypeV *_Old_Val = __sequential.map.get(key)
                        if (__COND_SAT__)
                                __sequential.map.put(key, &value);
                @Post_check:
@@ -429,8 +427,8 @@ friend class CHM;
                @Commit_point_set: Write_Val_Point
                @ID: __sequential.getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
-                       @Code: __sequential.map.put(key, NULL);
+                       TypeV *_Old_Val = __sequential.map.get(key)
+                       __sequential.map.put(key, NULL);
                @Post_check:
                        __sequential.equals_val(__RET__, _Old_Val)
                @End
@@ -450,7 +448,6 @@ friend class CHM;
                        COND_RemoveIfMatchSucc :: __RET__ == true
                @ID: __sequential.getKeyTag(key)
                @Action:
-                       @Code:
                        if (__COND_SAY__)
                                __sequential.map.put(key, NULL);
                @Post_check:
@@ -470,7 +467,7 @@ friend class CHM;
                        Write_Val_Point
                @ID: __sequential.getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
+                       TypeV *_Old_Val = __sequential.map.get(key)
                @Post_check:
                        __sequential.equals_val(__RET__, _Old_Val)
                @End
@@ -490,7 +487,6 @@ friend class CHM;
                        COND_ReplaceIfMatchSucc :: __RET__ == true
                @ID: __sequential.getKeyTag(key)
                @Action:
-                       @Code:
                        if (__COND_SAY__)
                                __sequential.map.put(key, &newval);
                @Post_check:
index 9dd2bf8..1cbe525 100644 (file)
@@ -45,7 +45,6 @@
                @InitVar:
                        writer_lock_acquired = false;
                        reader_lock_cnt = 0;
-               @DefineFunc:
        @Happens_before:
                # Since commit_point_set has no ID attached, A -> B means that for any B,
                # the previous A happens before B.
@@ -84,10 +83,9 @@ static inline int write_can_lock(rwlock_t *lock)
        @Commit_point_set:
                Read_Lock_Success_1 | Read_Lock_Success_2
        @Check:
-               !__sequential.writer_lock_acquired
+               !writer_lock_acquired
        @Action:
-               @Code:
-               __sequential.reader_lock_cnt++;
+               reader_lock_cnt++;
        @End
 */
 static inline void read_lock(rwlock_t *rw)
@@ -121,10 +119,9 @@ static inline void read_lock(rwlock_t *rw)
        @Commit_point_set:
                Write_Lock_Success_1 | Write_Lock_Success_2
        @Check:
-               !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
+               !writer_lock_acquired && reader_lock_cnt == 0
        @Action:
-               @Code:
-               __sequential.writer_lock_acquired = true;
+               writer_lock_acquired = true;
        @End
 */
 static inline void write_lock(rwlock_t *rw)
@@ -157,15 +154,14 @@ static inline void write_lock(rwlock_t *rw)
        @Commit_point_set:
                Read_Trylock_Point
        @Condition:
-               __sequential.writer_lock_acquired == false
+               writer_lock_acquired == false
        @HB_condition:
                HB_Read_Trylock_Succ :: __RET__ == 1
        @Action:
-               @Code:
-               if (__COND_SAY__)
-                       __sequential.reader_lock_cnt++;
+               if (__COND_SAT__)
+                       reader_lock_cnt++;
        @Post_check:
-               __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
+               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int read_trylock(rwlock_t *rw)
@@ -190,15 +186,14 @@ static inline int read_trylock(rwlock_t *rw)
        @Commit_point_set:
                Write_Trylock_Point
        @Condition:
-               !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
+               !writer_lock_acquired && reader_lock_cnt == 0
        @HB_condition:
                HB_Write_Trylock_Succ :: __RET__ == 1
        @Action:
-               @Code:
-               if (__COND_SAY__)
-                       __sequential.writer_lock_acquired = true;
+               if (__COND_SAT__)
+                       writer_lock_acquired = true;
        @Post_check:
-               __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
+               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int write_trylock(rwlock_t *rw)
@@ -222,9 +217,8 @@ static inline int write_trylock(rwlock_t *rw)
        @Interface: Read_Unlock
        @Commit_point_set: Read_Unlock_Point
        @Check:
-               __sequential.reader_lock_cnt > 0 && !__sequential.writer_lock_acquired
+               reader_lock_cnt > 0 && !writer_lock_acquired
        @Action: 
-               @Code:
                reader_lock_cnt--;
        @End
 */
@@ -246,8 +240,7 @@ static inline void read_unlock(rwlock_t *rw)
        @Check:
                reader_lock_cnt == 0 && writer_lock_acquired
        @Action: 
-               @Code:
-               __sequential.writer_lock_acquired = false;
+               writer_lock_acquired = false;
        @End
 */
 
index ed30de8..1ac8dc1 100644 (file)
@@ -1 +1,55 @@
-void enqueue(queue_t *q, unsigned int val)
+/**
+@Begin
+               @Options:
+                       LANG = C;
+                       CLASS = cliffc_hashtable;
+               @Global_define:
+                       @DeclareVar:
+                       spec_hashtable<TypeK, TypeV*> map;
+                       spec_hashtable<TypeK, Tag> id_map;
+                       Tag tag;
+                       @InitVar:
+                               map = spec_hashtable<TypeK, TypeV*>();
+                               id_map = spec_hashtable<TypeK, TypeV*>();
+                               tag = Tag();
+                       @DefineFunc:
+                       static bool equals_val(TypeV *ptr1, TypeV *ptr2) {
+                               // ...
+                       }
+                       
+                       # Update the tag for the current key slot if the corresponding tag
+                       # is NULL, otherwise just return that tag. It will update the next
+                       # available tag too if it requires a new tag for that key slot.
+                       static Tag getKeyTag(TypeK &key) {
+                               if (id_map.get(key) == NULL) {
+                                       Tag cur_tag = tag.current();
+                                       id_map.put(key, cur_tag);
+                                       tag.next();
+                                       return cur_tag;
+                               } else {
+                                       return id_map.get(key);
+                               }
+                       }
+               
+               @Interface_cluster:
+                       Read_interface = {
+                               Get,
+                               PutIfAbsent,
+                               RemoveAny,
+                               RemoveIfMatch,
+                               ReplaceAny,
+                               ReplaceIfMatch
+                       }
+                       
+                       Write_interface = {
+                               Put,
+                               PutIfAbsent(COND_PutIfAbsentSucc),
+                               RemoveAny,
+                               RemoveIfMatch(COND_RemoveIfMatchSucc),
+                               ReplaceAny,
+                               ReplaceIfMatch(COND_ReplaceIfMatchSucc)
+                       }
+               @Happens_before:
+                       Write_interface -> Read_interface
+               @End
+       */
index 93a5d8b..6a4f61b 100644 (file)
@@ -179,6 +179,8 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
 
                public static String stringArray2String(ArrayList<String> content) {
                        StringBuilder sb = new StringBuilder();
+                       if (content.size() == 1)
+                               return content.get(0);
                        for (int i = 0; i < content.size(); i++) {
                                sb.append(content.get(i) + "\n");
                        }
@@ -309,6 +311,10 @@ SKIP : {
        <UNSIGNED: "unsigned">
 |
        <TEMPLATE: "template">
+|
+       <INLINE: "inline">
+|
+       <STATIC: "static">
 |
        <#DIGIT: ["0"-"9"]>
 |
@@ -514,7 +520,6 @@ void Test() :
        {
                System.out.println(func);
        }
-
        
 }
 
@@ -525,8 +530,8 @@ String ParameterizedName() :
 }
 {
        (str = <IDENTIFIER>.image {res = str;})
-       ("<" str = <IDENTIFIER>.image { res = res + "<" + str; }
-       ("," str = <IDENTIFIER>.image { res = res + ", " + str; })* ">"
+       ("<" str = Type() { res = res + "<" + str; }
+       ("," str = Type() { res = res + ", " + str; })* ">"
        { res = res + ">"; }
        )?
        {
@@ -541,6 +546,7 @@ FunctionHeader FuncDecl() :
        ArrayList<VariableDeclaration> args;
 }
 {
+       (<STATIC> | <INLINE>)*
        ret = Type() 
        funcName = ParseQualifiedName() 
        args = FormalParamList() 
@@ -639,6 +645,7 @@ ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
        (
        t = <CONST> | t = <STRUCT> | t = <CLASS> | t = <UNSIGNED> |
        (t = <TEMPLATE> { inTemplate = true;  })|
+       t = <STATIC> | t = <INLINE> |
        (t = <INCLUDE>
        {
                header = t.image;
@@ -666,11 +673,16 @@ ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
        (t = <DEFINE> { newLine = true; } )
        )
        {
-               text = text + " " + t.image;
+               if (text.equals("")) {
+                       text = t.image;
+               } else {
+                       text = text + " " + t.image;
+               }
                if (newLine) {
                        content.add(text);
                        text = "";
                        newLine = false;
+                       inTemplate = false;
                }
        }
        )+
@@ -798,8 +810,8 @@ ConditionalInterface Conditional_interface() :
        {
                hbConditionLabel = "";
        }
-       interfaceName = <IDENTIFIER>.image (<OPEN_BRACKET> hbConditionLabel =
-       <IDENTIFIER>.image <CLOSE_BRACKET>)?
+       interfaceName = <IDENTIFIER>.image (<OPEN_PAREN> hbConditionLabel =
+       <IDENTIFIER>.image <CLOSE_PAREN>)?
        {
                return new ConditionalInterface(interfaceName, hbConditionLabel);
        }
@@ -812,14 +824,14 @@ void Interface_cluster(GlobalConstruct inst) :
 }
 {
        (clusterName= <IDENTIFIER>.image)
-       <EQUALS> <OPEN_PAREN>
+       <EQUALS> <OPEN_BRACE>
                (condInterface = Conditional_interface()
                { inst.addInterface2Cluster(clusterName, condInterface); } 
                )
                (<COMMA> condInterface = Conditional_interface()
                { inst.addInterface2Cluster(clusterName, condInterface); } 
                )*
-       <CLOSE_PAREN>
+       <CLOSE_BRACE>
 }
 
 void Interface_clusters(GlobalConstruct inst) :
@@ -882,7 +894,7 @@ InterfaceConstruct Interface() :
                        (<CONDITION> (content = C_CPP_CODE(null) { condition = stringArray2String(content); }))?
                        (
                                <HB_CONDITION>
-                               (hbLabel = <IDENTIFIER>.image)
+                               (hbLabel = <IDENTIFIER>.image) <DOUBLECOLON>
                                (content = C_CPP_CODE(null) { hbCondition = stringArray2String(content); })
                                {
                                        if (hbConditions.containsKey(hbLabel)) {
index f127772..a0bc957 100644 (file)
@@ -1,11 +1,14 @@
 package edu.uci.eecs.specCompiler.codeGenerator;
 
 import java.util.ArrayList;
+import java.util.Comparator;
 
 public class CodeAddition {
-       public static class CodeAdditionComparator<CodeAddition> {
-               
-       }
+       public static Comparator<CodeAddition> lineNumComparator = new Comparator<CodeAddition>() {
+               public int compare(CodeAddition addition1, CodeAddition addition2) {
+                       return addition1.lineNum - addition2.lineNum;
+               }
+       };
        
        public final int lineNum;
        public final ArrayList<String> newCode;
index d652584..20f6e53 100644 (file)
@@ -6,6 +6,7 @@ import java.io.FileNotFoundException;
 import java.io.FileReader;
 import java.io.IOException;
 import java.util.ArrayList;
+import java.util.Collections;
 import java.util.HashMap;
 import java.util.Iterator;
 
@@ -19,6 +20,7 @@ import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.IDExtractor;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ParserUtils;
 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
@@ -146,6 +148,25 @@ public class CodeGenerator {
                codeAdditions.get(construct.file).add(addition);
        }
 
+       private ArrayList<String> insertAnnotation2Src(
+                       ArrayList<CodeAddition> additions, ArrayList<String> content) {
+               int totalSize = content.size();
+               for (int i = 0; i < additions.size(); i++) {
+                       totalSize += additions.size();
+               }
+               ArrayList<String> newContent = new ArrayList<String>(totalSize);
+               int curSrcLine = 0;
+               for (int i = 0; i < additions.size(); i++) {
+                       CodeAddition addition = additions.get(i);
+                       if (curSrcLine <  addition.lineNum) {
+                               newContent.addAll(content.subList(curSrcLine, addition.lineNum - 1));
+                               curSrcLine = addition.lineNum;
+                       }
+                       newContent.addAll(addition.newCode);
+               }
+               return newContent;
+       }
+
        public void generateCode() {
                for (int i = 0; i < _semantics.constructs.size(); i++) {
                        Construct construct = _semantics.constructs.get(i);
@@ -159,18 +180,35 @@ public class CodeGenerator {
                                CPDefine2Code((CPDefineConstruct) construct);
                        } else if (construct instanceof CPDefineCheckConstruct) {
                                CPDefineCheck2Code((CPDefineCheckConstruct) construct);
+                       } else if (construct instanceof EntryPointConstruct) {
+                               EntryPoint2Code((EntryPointConstruct) construct);
                        }
                }
+               // Sort code additions
+               for (File file : codeAdditions.keySet()) {
+                       ArrayList<CodeAddition> additions = codeAdditions.get(file);
+                       if (additions.size() == 0) // Simply do nothing, already written
+                                                                               // once
+                               continue;
+                       ArrayList<String> content = _semantics.srcFilesInfo.get(file).content;
+                       Collections.sort(additions, CodeAddition.lineNumComparator);
+                       // Insert generated annotation to the source files
+                       ArrayList<String> newContent = insertAnnotation2Src(additions,
+                                       content);
+                       // Write it back to file
+                       ParserUtils.write2File(file, newContent);
+               }
+
        }
 
        public static void main(String[] argvs) {
                String homeDir = Environment.HOME_DIRECTORY;
                File[] srcFiles = {
-               // new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
-               new File(homeDir
-                               + "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
-//              new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
-//              new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
+                new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+//             new File(homeDir
+//                             + "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
+               // new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+               // new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
                CodeGenerator gen = new CodeGenerator(srcFiles);
                gen.generateCode();
        }
index 8e87cd5..980e420 100644 (file)
@@ -23,6 +23,7 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
 
 public class CodeVariables {
        // C++ code or library
+       public static final String HEADER_STDLIB = "<stdlib.h>";
        public static final String HEADER_THREADS = "<threads.h>";
        public static final String HEADER_STDINT = "<stdint.h>";
        public static final String ThreadIDType = "thrd_t";
@@ -148,12 +149,14 @@ public class CodeVariables {
        }
 
        private static ArrayList<String> DEFINE_INFO_STRUCT(String interfaceName,
-                       FunctionHeader funcDecl) {
+                       FunctionHeader header) {
                ArrayList<String> code = new ArrayList<String>();
                code.add("typedef struct " + interfaceName + "_info {");
-               code.add(DECLARE(funcDecl.returnType, MACRO_RETURN));
-               for (int i = 0; i < funcDecl.args.size(); i++) {
-                       code.add(DECLARE(funcDecl.args.get(i)));
+               if (!header.returnType.equals("void")) {
+                       code.add(DECLARE(header.returnType, MACRO_RETURN));
+               }
+               for (int i = 0; i < header.args.size(); i++) {
+                       code.add(DECLARE(header.args.get(i)));
                }
                code.add("} " + interfaceName + "_info {");
                return code;
@@ -180,17 +183,22 @@ public class CodeVariables {
                code.add("static bool " + interfaceName + "_check_action(void *info, "
                                + IDType + " " + MACRO_ID + ") {");
                code.add(DECLARE("bool", "check_passed"));
-               String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
-               code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
-                               BRACE(infoStructType) + "info"));
-               code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
-                               GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
-               for (int i = 0; i < header.args.size(); i++) {
-                       String type = header.args.get(i).type, var = header.args.get(i).name;
-                       code.add((DECLARE_DEFINE(type, var,
-                                       GET_FIELD_BY_PTR(infoStructName, var))));
+               // Read info struct
+               if (!header.returnType.equals("void") || header.args.size() != 0) {
+                       String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
+                       code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
+                                       BRACE(infoStructType) + "info"));
+                       if (!header.returnType.equals("void")) {
+                               code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
+                                               GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
+                       }
+                       for (int i = 0; i < header.args.size(); i++) {
+                               String type = header.args.get(i).type, var = header.args.get(i).name;
+                               code.add((DECLARE_DEFINE(type, var,
+                                               GET_FIELD_BY_PTR(infoStructName, var))));
+                       }
+                       code.add("");
                }
-               code.add("");
                // __COND_SAT
                if (!construct.condition.equals("")) {
                        code.add(DECLARE_DEFINE("bool", MACRO_COND, construct.condition));
@@ -296,12 +304,14 @@ public class CodeVariables {
                                        .get(interfaceName);
                        FunctionHeader funcHeader = getFunctionHeader(semantics, iConstruct);
                        // Define necessary info structure
-                       newCode.add(COMMENT("Definition of interface info struct: "
-                                       + interfaceName));
-                       newCode.addAll(DEFINE_INFO_STRUCT(interfaceName, funcHeader));
-                       newCode.add(COMMENT("End of info struct definition: "
-                                       + interfaceName));
-                       newCode.add("");
+                       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));
+                               newCode.add(COMMENT("End of info struct definition: "
+                                               + interfaceName));
+                               newCode.add("");
+                       }
 
                        // Define ID function
                        newCode.add(COMMENT("ID function of interface: " + interfaceName));
@@ -442,6 +452,7 @@ public class CodeVariables {
                ArrayList<String> newCode = new ArrayList<String>();
                String interfaceName = construct.name;
                // Generate necessary header file (might be redundant but never mind)
+               newCode.add(INCLUDE(HEADER_STDLIB));
                newCode.add(INCLUDE(HEADER_THREADS));
                newCode.add(INCLUDE(HEADER_CDSANNOTATE));
                newCode.add(INCLUDE(HEADER_SPECANNOTATION));
@@ -472,12 +483,16 @@ public class CodeVariables {
                newCode.add(ASSIGN_PTR(structName, "annotation", structName));
                newCode.add(ANNOTATE(anno));
                // Call original renamed function
-               newCode.add(DECLARE_DEFINE(header.returnType, MACRO_RETURN,
-                               header.getRenamedCall(SPEC_INTERFACE_WRAPPER)));
+               if (header.returnType.equals("void")) {
+                       newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER));
+               } else {
+                       newCode.add(DECLARE_DEFINE(header.returnType, MACRO_RETURN,
+                                       header.getRenamedCall(SPEC_INTERFACE_WRAPPER)));
+               }
                // HB conditions
                for (String label : construct.hbConditions.keySet()) {
                        String condition = construct.hbConditions.get(label);
-                       String hbCondNum = Integer.toString(semantics.interface2Num
+                       String hbCondNum = Integer.toString(semantics.hbLabel2Num
                                        .get(label));
                        newCode.add("if " + BRACE(condition) + " {");
                        structName = "hb_condition";
@@ -490,16 +505,26 @@ public class CodeVariables {
                        newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_HB_CONDITION));
                        newCode.add(ASSIGN_PTR(anno, "annotation", structName));
                        newCode.add(ANNOTATE(anno));
+                       newCode.add("}");
+                       newCode.add("");
                }
                // Interface end
-               String infoStructType = interfaceName + "_info", infoName = "info";
-               newCode.add(DECLARE_DEFINE(infoStructType, infoName,
-                               BRACE(infoStructType + "*") + " malloc(sizeof("
-                                               + infoStructType + "))"));
-               newCode.add(ASSIGN_TO_PTR(infoName, MACRO_RETURN, MACRO_RETURN));
-               for (int i = 0; i < header.args.size(); i++) {
-                       String argName = header.args.get(i).name;
-                       newCode.add(ASSIGN_TO_PTR(infoName, argName, argName));
+               String infoStructType = null, infoName = null;
+               if (!header.returnType.equals("void") || header.args.size() > 0) {
+                       infoStructType = interfaceName + "_info";
+                       infoName = "info";
+                       newCode.add(DECLARE_DEFINE(infoStructType, infoName,
+                                       BRACE(infoStructType + "*") + " malloc(sizeof("
+                                                       + infoStructType + "))"));
+                       if (!header.returnType.equals("void")) {
+                               newCode.add(ASSIGN_TO_PTR(infoName, MACRO_RETURN, MACRO_RETURN));
+                       }
+                       for (int i = 0; i < header.args.size(); i++) {
+                               String argName = header.args.get(i).name;
+                               newCode.add(ASSIGN_TO_PTR(infoName, argName, argName));
+                       }
+               } else {
+                       infoName = "NULL";
                }
                structName = "interface_end";
                anno = "annoation_interface_end";
index 26647f6..ae53d3b 100644 (file)
@@ -121,12 +121,6 @@ public class SemanticsChecker {
                                                + 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++);
                }
index 61d0da7..2cae9b5 100644 (file)
@@ -1,7 +1,12 @@
 package edu.uci.eecs.specCompiler.specExtraction;
 
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.FileWriter;
+import java.io.IOException;
 import java.util.ArrayList;
 
+import edu.uci.eecs.specCompiler.codeGenerator.Environment;
 import edu.uci.eecs.specCompiler.codeGenerator.SemanticsChecker;
 import edu.uci.eecs.specCompiler.grammerParser.ParseException;
 import edu.uci.eecs.specCompiler.grammerParser.SpecParser;
@@ -54,4 +59,26 @@ public class ParserUtils {
                }
                return templateStr;
        }
+       
+       public static void write2File(File file, ArrayList<String> content) {
+               String newFileName = Environment.GENERATED_FILE_DIR + "/" + file.getName();
+               File newFile = new File(newFileName);
+               newFile.getParentFile().mkdirs();
+               if (!newFile.exists()) {
+                       try {
+                               newFile.createNewFile();
+                       } catch (IOException e) {
+                               e.printStackTrace();
+                       }
+               }
+               try {
+                       BufferedWriter bw = new BufferedWriter(new FileWriter(newFile));
+                       for (int i = 0; i < content.size(); i++) {
+                               bw.write(content.get(i) + "\n");
+                       }
+                       bw.flush();
+               } catch (IOException e) {
+                       e.printStackTrace();
+               }
+       }
 }
index 2b9af87..0ac075f 100644 (file)
@@ -28,26 +28,4 @@ public class SourceFileInfo {
                SourceFileInfo another = (SourceFileInfo) o;
                return another.file.equals(file);
        }
-       
-       public void write2File() {
-               String newFileName = Environment.GENERATED_FILE_DIR + "/" + file.getName();
-               File newFile = new File(newFileName);
-               newFile.getParentFile().mkdirs();
-               if (!newFile.exists()) {
-                       try {
-                               newFile.createNewFile();
-                       } catch (IOException e) {
-                               e.printStackTrace();
-                       }
-               }
-               try {
-                       BufferedWriter bw = new BufferedWriter(new FileWriter(newFile));
-                       for (int i = 0; i < content.size(); i++) {
-                               bw.write(content.get(i) + "\n");
-                       }
-                       bw.flush();
-               } catch (IOException e) {
-                       e.printStackTrace();
-               }
-       }
 }
index 8d7a229..52862f4 100644 (file)
@@ -60,7 +60,7 @@ public class SpecExtractor {
                SourceFileInfo srcFileInfo;
                try {
                        srcFileInfo = SpecParser.ParseFile(file);
-                       srcFileInfo.write2File();
+                       ParserUtils.write2File(srcFileInfo.file, srcFileInfo.content);
                        srcFilesInfo.put(file, srcFileInfo);
                } catch (ParseException e) {
                        e.printStackTrace();
diff --git a/test.c b/test.c
index 65c412a..b279809 100644 (file)
--- a/test.c
+++ b/test.c
@@ -2,9 +2,14 @@
 #include <stdlib.h>
 #include <stdint.h>
 
+typedef struct A {
+
+} A;
+
 int main() {
        uint64_t i64 = (uint64_t) NULL;
-       if (i64)
-               printf("True\n");
+       A *a = (A*) malloc (sizeof(A));
+       printf("%d\n", sizeof(A));
+       printf("%d\n", a);
        return 1;
 }