edits

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 1f7059f828004926926c0b0682b52cf909804c9d..03a292b3b6978860bb355081dc7d274a6ca1f3eb 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -47,31 +47,11 @@ typedef union {
        auxiliary check since it is an extra rule for how the interfaces should called.
 */
 
-/**
-       @Begin
-       @Options:
-               LANG = C;
-       @Global_define:
-               @DeclareVar:
-                       bool writer_lock_acquired;
-                       int reader_lock_cnt;
-               @InitVar:
-                       writer_lock_acquired = false;
-                       reader_lock_cnt = 0;
-       @Happens_before:
-               # Since commit_point_set has no ID attached, A -> B means that for any B,
-               # the previous A happens before B.
-               #Read_Unlock -> Read_Lock
-               Read_Unlock -> Write_Lock
-               Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
-               #Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
-
-               Write_Unlock -> Write_Lock
-               Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
-
-               Write_Unlock -> Read_Lock
-               Write_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
-       
+/** @DeclareState:
+               bool writer_lock_acquired;
+               int reader_lock_cnt;
+       @Initial: writer_lock_acquired = false;
+               reader_lock_cnt = 0;
        @Commutativity: Read_Lock <-> Read_Lock: true
        @Commutativity: Read_Lock <-> Read_Unlock: true
        @Commutativity: Read_Lock <-> Read_Trylock: true
@@ -89,7 +69,6 @@ typedef union {
        @Commutativity: Write_Trylock <-> Write_Trylock: !_Method1.__RET__ || !_Method2.__RET__
        @Commutativity: Write_Trylock <-> Write_Unlock: !_Method1.__RET__
        @Commutativity: Write_Trylock <-> Write_Lock: !_Method1.__RET__
-       @End
 */
 
 static inline int read_can_lock(rwlock_t *lock)

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
index 3d6b22470ca62ba93b68ec0582e990551c23448d..b3f1c619acb7f99bd9afce3a17f4ddd9b86d9ef7 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
@@ -306,7 +306,7 @@ public class CodeGenerator {
        }
 
        static public void main(String[] args) {
-               String[] dirNames = { Environment.REGISTER };
+               String[] dirNames = { Environment.REGISTER, Environment.MS_QUEUE, Environment.LINUXRWLOCKS, Environment.MCS_LOCK };
 
                for (int i = 0; i < dirNames.length; i++) {
                        String dirName = dirNames[i];

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index abcb45cab7c0eba50f402b5e475cbbd773e16e5c..005397e5c68b200c9ab244ea583dfa894e54a042 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -155,11 +155,18 @@ public class CodeGeneratorUtils {
                code.addLine("");
 
                // Users included headers
+               // FIXME: We don't add user-defined headers, but as a workaround we only add forward class.
                code.addLine(ShortComment("User included headers go here"));
                for (String header : headerFiles) {
                        code.addLine(IncludeHeader(header));
                }
                code.addLine("");
+               
+//             code.addLine(ShortComment("Forward declaration goes here"));
+//             for (String type : extractor.forwardClass) {
+//                     code.addLine("class " + type + ";");
+//             }
+//             code.addLine("");
 
                code.addLine("using namespace std;");
                code.addLine("");

diff --git a/src/edu/uci/eecs/codeGenerator/Environment.java b/src/edu/uci/eecs/codeGenerator/Environment.java
index d11545d37e5dd1f25ac822f50298b53483e83d31..f323ca7b44ea73fb14a17f48ba4ed8359cdaa8de 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/Environment.java
+++ b/src/edu/uci/eecs/codeGenerator/Environment.java
@@ -23,5 +23,6 @@ public class Environment {
        public final static String REGISTER = "register";
        public final static String MS_QUEUE = "ms-queue";
        public final static String LINUXRWLOCKS = "linuxrwlocks";
+       public final static String MCS_LOCK = "mcs-lock";
 
 }

diff --git a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
index 8c6848a6814834f4cff7b9a8da1d9eb528622765..f49911be2f51497a3268d79bc699fd6407d85974 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
@@ -66,7 +66,7 @@ public class GlobalConstruct extends Construct {
                        if (type.equals("int") || type.equals("unsigned")
                                        || type.equals("unsigned int")
                                        || type.equals("int unsigned") || type.equals("double")
-                                       || type.equals("double")) {
+                                       || type.equals("double") || type.equals("bool")) {
                                // NEW->x = OLD->x;
                                code.addLine(SpecNaming.NewStateInst + "->" + name + " = "
                                                + SpecNaming.OldStateInst + "->" + name + ";");

diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
index 0e470e0e5361bc9f476b6e69f06d21709faffcd2..a7b4fe591926defe578dd785351bc95aaf7b9a0b 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
@@ -37,6 +37,9 @@ public class SpecExtractor {
        public final HashMap<File, EntryConstruct> entryMap;
 
        public final HashSet<String> headerFiles;
+       
+       // In the generated header file, we need to forward the user-defined 
+       public final HashSet<String> forwardClass;
 
        private GlobalConstruct globalConstruct;
 
@@ -46,6 +49,7 @@ public class SpecExtractor {
                OPLabelSet = new HashSet<String>();
                entryMap = new HashMap<File, EntryConstruct>();
                headerFiles = new HashSet<String>();
+               forwardClass = new HashSet<String>();
                globalConstruct = null;
        }
 
@@ -410,6 +414,18 @@ public class SpecExtractor {
                        line = lineReader.readLine();
                        lineNum = lineReader.getLineNumber();
                        construct.processFunctionDeclaration(line);
+                       
+                       // Record those user-defined struct
+                       // RET
+                       String returnType = construct.getFunctionHeader().returnType;
+                       if (SpecUtils.isUserDefinedStruct(returnType))
+                               forwardClass.add(SpecUtils.getPlainType(returnType));
+                       // Arguments
+                       for (VariableDeclaration decl : construct.getFunctionHeader().args) {
+                               if (SpecUtils.isUserDefinedStruct(decl.type))
+                                       forwardClass.add(SpecUtils.getPlainType(decl.type));
+                       }
+                       
                } catch (IOException e) {
                        errMsg = "Spec error in file \""
                                        + file.getName()

diff --git a/src/edu/uci/eecs/specExtraction/SpecUtils.java b/src/edu/uci/eecs/specExtraction/SpecUtils.java
index a9ed016f00b7598eb3ea301dbf46648b5c89e74a..869b9ff81aff63566fbe77445851f7b360182977 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecUtils.java
+++ b/src/edu/uci/eecs/specExtraction/SpecUtils.java
@@ -123,8 +123,7 @@ public class SpecUtils {
         *         annotations or the beginning line of the next primitive
         * @throws WrongAnnotationException
         */
-       public static Primitive extractPrimitive(File file, int beginLineNum,
-                       ArrayList<String> annotations, IntObj curIdx)
+       public static Primitive extractPrimitive(File file, int beginLineNum, ArrayList<String> annotations, IntObj curIdx)
                        throws WrongAnnotationException {
                if (curIdx.getVal() == annotations.size()) // The current index points
                                                                                                        // to the end
@@ -147,9 +146,8 @@ public class SpecUtils {
                }
                // Assert that we must have found one primitive
                if (primitive == null) {
-                       WrongAnnotationException
-                                       .err(file, curLineNum,
-                                                       "Something is wrong! We must have found one primitve here!\n");
+                       WrongAnnotationException.err(file, curLineNum,
+                                       "Something is wrong! We must have found one primitve here!\n");
                }
 
                // Process the current "primitive"
@@ -163,9 +161,8 @@ public class SpecUtils {
                                primitive.addLine(trimmedCode);
                        }
                } else {
-                       WrongAnnotationException
-                                       .err(file, curLineNum,
-                                                       "The state annotation should have correct primitive syntax (sub-annotations)");
+                       WrongAnnotationException.err(file, curLineNum,
+                                       "The state annotation should have correct primitive syntax (sub-annotations)");
                }
 
                // Deal with other normal line. E.g. y = 1;
@@ -187,8 +184,7 @@ public class SpecUtils {
 
                if (primitive.contents.size() == 0) { // The content of the primitive is
                                                                                                // empty
-                       WrongAnnotationException.warning(file, curLineNum, "Primitive "
-                                       + primitive.name + " is empty.");
+                       WrongAnnotationException.warning(file, curLineNum, "Primitive " + primitive.name + " is empty.");
                }
                return primitive;
        }
@@ -228,4 +224,20 @@ public class SpecUtils {
                        return null;
                }
        }
+
+       public static boolean isUserDefinedStruct(String type) {
+               // FIXME: We only consider the type is either a one-level pointer or a
+               // struct
+               String bareType = trimSpace(type.replace('*', ' '));
+               return !bareType.equals("int") && !bareType.matches("unsigned\\s+int") && !bareType.equals("unsigned")
+                               && !bareType.equals("bool") && !bareType.equals("double") && !bareType.equals("float")
+                               && !bareType.equals("void");
+       }
+
+       public static String getPlainType(String type) {
+               // FIXME: We only consider the type is either a one-level pointer or a
+               // struct
+               String bareType = trimSpace(type.replace('*', ' '));
+               return bareType;
+       }
 }