minor fix

diff --git a/grammer/util.jj b/grammer/util.jj
index 901e2e6f6fac466097a50336d768546f5f50a9fa..5b5446bb9c102c3882efd813cab07652ea4687be 100644 (file)
--- a/grammer/util.jj
+++ b/grammer/util.jj
@@ -280,7 +280,10 @@ String Type() :
        (<CONST>
        { type = "const"; }
        )?
        (<CONST>
        { type = "const"; }
        )?

-       (((str = <STRUCT>.image | str = <CLASS>.image | str = <UNSIGNED>.image) { type = type + " " + str; })? 
+       (
+               ((str = <STRUCT>.image | str = <CLASS>.image | str = <UNSIGNED>.image) {
+               type = type.equals("") ? type + str : type + " " + str;
+               })? 

        (
        name = ParseQualifiedName() {
                if (!type.equals(""))
        (
        name = ParseQualifiedName() {
                if (!type.equals(""))

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
index 02c6067fb386ee901552415a9a3a7d436984e523..2543d5cc45ca41629b802bf9ee00f55ac9b844b3 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
@@ -318,12 +318,12 @@ public class CodeGenerator {
        }
 
        static public void main(String[] args) {
        }
 
        static public void main(String[] args) {

-//             String[] dirNames = { Environment.REGISTER, Environment.MS_QUEUE,
-//                             Environment.LINUXRWLOCKS, Environment.MCS_LOCK,
-//                             Environment.DEQUE };
-               String[] dirNames = args;
+               String[] dirNames = { Environment.REGISTER, Environment.MS_QUEUE,
+                               Environment.LINUXRWLOCKS, Environment.MCS_LOCK,
+                               Environment.DEQUE, Environment.TREIBER_STACK };
+//             String[] dirNames = args;

 
 

-               for (int i = 0; i < dirNames.length; i++) {
+               for (int i = 5; i < dirNames.length; i++) {

                        String dirName = dirNames[i];
                        System.out.println("/**********   Processing " + dirName
                                        + "    **********/");
                        String dirName = dirNames[i];
                        System.out.println("/**********   Processing " + dirName
                                        + "    **********/");

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 2914d49b6d7e1b41ac40beeae61acd11f96896f2..08b9f7a448ed5ff25a62bd103efe2e7afe870a59 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -529,7 +529,11 @@ public class CodeGeneratorUtils {
                        code.addLine(TabbedLine("#define " + decl.name + " "
                                        + SpecNaming.StateInst + "->" + decl.name));
                }
                        code.addLine(TabbedLine("#define " + decl.name + " "
                                        + SpecNaming.StateInst + "->" + decl.name));
                }

-               code.addLine(TabbedLine(ShortComment("User-defined intial state code")));
+               if (!globalConstruct.autoGenInitial)
+                       code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
+               else
+                       // Auto-generated the initialization function
+                       code.addLine(TabbedLine(ShortComment("Auto-generated state intialization code")));

                // Align the code with one tab
                globalConstruct.initState.align(1);
                code.addLines(globalConstruct.initState);
                // Align the code with one tab
                globalConstruct.initState.align(1);
                code.addLines(globalConstruct.initState);


@@ -580,7 +584,12 @@ public class CodeGeneratorUtils {
                        fieldsInit.align(1);
                        code.addLines(fieldsInit);
                        code.addLine("");
                        fieldsInit.align(1);
                        code.addLines(fieldsInit);
                        code.addLine("");

-                       code.addLine(TabbedLine(ShortComment("Execute the print-out")));
+                       if (!globalConstruct.autoGenPrint)
+                               code.addLine(TabbedLine(ShortComment("Execute user-defined state printing code")));
+                       else
+                               // Auto-generated the copy function
+                               code.addLine(TabbedLine(ShortComment("Execute auto-generated state printing code")));
+                       

                        // Align the code with one tab
                        globalConstruct.printState.align(1);
                        code.addLines(globalConstruct.printState);
                        // Align the code with one tab
                        globalConstruct.printState.align(1);
                        code.addLines(globalConstruct.printState);


@@ -726,7 +735,11 @@ public class CodeGeneratorUtils {
                                        code.addLines(fieldsInit);
 
                                        construct.print.align(1);
                                        code.addLines(fieldsInit);
 
                                        construct.print.align(1);

-                                       code.addLine(TabbedLine(ShortComment("Execute Print")));
+                                       if (!construct.autoGenPrint)
+                                               code.addLine(TabbedLine(ShortComment("Execute user-defined value printing code")));
+                                       else
+                                               // Auto-generated the value printing function
+                                               code.addLine(TabbedLine(ShortComment("Execute auto-generated value printing code")));

                                        code.addLines(construct.print);
 
                                        code.addLine("}");
                                        code.addLines(construct.print);
 
                                        code.addLine("}");

diff --git a/src/edu/uci/eecs/codeGenerator/Environment.java b/src/edu/uci/eecs/codeGenerator/Environment.java
index 9640ffea16b544830014055382990d69b69bc21f..84fc4ee57ed842d9005d602898429217304f1d3a 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/Environment.java
+++ b/src/edu/uci/eecs/codeGenerator/Environment.java
@@ -25,5 +25,6 @@ public class Environment {
        public final static String LINUXRWLOCKS = "linuxrwlocks";
        public final static String MCS_LOCK = "mcs-lock";
        public final static String DEQUE = "chase-lev-deque-bugfix";
        public final static String LINUXRWLOCKS = "linuxrwlocks";
        public final static String MCS_LOCK = "mcs-lock";
        public final static String DEQUE = "chase-lev-deque-bugfix";

+       public final static String TREIBER_STACK = "treiber-stack";

 
 }
 
 }

diff --git a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
index f49911be2f51497a3268d79bc699fd6407d85974..b2e52a03d5b333626b5b014a8e433a91d4c22184 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
@@ -25,7 +25,14 @@ public class GlobalConstruct extends Construct {
        public final Code printState;
        public final ArrayList<CommutativityRule> commutativityRules;
 
        public final Code printState;
        public final ArrayList<CommutativityRule> commutativityRules;
 

+       // Whether the state declaration is empty
+       public final boolean emptyState;
+       // Whether we have auto-gen the state initialization code
+       public final boolean autoGenInitial;
+       // Whether we have auto-gen the state copying code

        public final boolean autoGenCopy;
        public final boolean autoGenCopy;

+       // Whether we have auto-gen the state printing code
+       public final boolean autoGenPrint;

 
        public GlobalConstruct(File file, int beginLineNum,
                        ArrayList<String> annotations) throws WrongAnnotationException {
 
        public GlobalConstruct(File file, int beginLineNum,
                        ArrayList<String> annotations) throws WrongAnnotationException {


@@ -39,13 +46,75 @@ public class GlobalConstruct extends Construct {
 
                processAnnotations(annotations);
 
 
                processAnnotations(annotations);
 

-               if (copyState.isEmpty()) {
+               emptyState = declState.isEmpty();
+               if (emptyState) {
+                       WrongAnnotationException.warning(file, beginLineNum,
+                                       "The state is empty. Make sure that's what you want!");
+               }
+
+               autoGenInitial = initState.isEmpty();
+               if (autoGenInitial) {
+                       Code code = generateAutoInitalFunction();
+                       initState.addLines(code);
+               }
+
+               autoGenCopy = copyState.isEmpty();
+               if (autoGenCopy) {

                        Code code = generateAutoCopyFunction();
                        copyState.addLines(code);
                        Code code = generateAutoCopyFunction();
                        copyState.addLines(code);

-                       autoGenCopy = true;
-               } else {
-                       autoGenCopy = false;

                }
                }

+
+               autoGenPrint = printState.isEmpty();
+               if (autoGenPrint) {
+                       Code code = generateAutoPrintFunction();
+                       printState.addLines(code);
+               }
+       }
+
+       /**
+        * <p>
+        * This function will automatically generate the initial statements for
+        * supported types if the user has not defined the "@Initial" primitive
+        * </p>
+        * 
+        * @return The auto-generated state intialization statements
+        * @throws WrongAnnotationException
+        */
+       private Code generateAutoInitalFunction() throws WrongAnnotationException {
+               Code code = new Code();
+               if (emptyState) // Empty state should have empty initial function
+                       return code;
+               for (VariableDeclaration decl : declState) {
+                       String type = decl.type;
+                       String name = decl.name;
+                       // Primitive types
+                       if (type.equals("int") || type.equals("unsigned")
+                                       || type.equals("unsigned int")
+                                       || type.equals("int unsigned") || type.equals("double")
+                                       || type.equals("double") || type.equals("bool")) {
+                               // x = 0;
+                               code.addLine(name + " = 0;");
+                       } else if (type.equals("IntList") || type.equals("IntSet")
+                                       || type.equals("IntMap")) {
+                               // Supported types
+                               // q = IntList();
+                               code.addLine(name + " = " + type + "();");
+                       } else if (type.equals("IntList *") || type.equals("IntSet *")
+                                       || type.equals("IntMap *")) {
+                               // Supported pointer types
+                               // q = new IntList;
+                               String originalType = SpecUtils.trimSpace(type
+                                               .replace('*', ' '));
+                               code.addLine(name + " = new " + originalType + "();");
+                       } else {
+                               WrongAnnotationException
+                                               .err(file,
+                                                               beginLineNum,
+                                                               "You have types in the state declaration that we do not support auto-gen initial function.");
+                       }
+               }
+
+               return code;

        }
 
        /**
        }
 
        /**


@@ -54,11 +123,13 @@ public class GlobalConstruct extends Construct {
         * supported types if the user has not defined the "@Copy" primitive
         * </p>
         * 
         * supported types if the user has not defined the "@Copy" primitive
         * </p>
         * 

-        * @return The auto-generated copy statements
+        * @return The auto-generated state copy statements

         * @throws WrongAnnotationException
         */
        private Code generateAutoCopyFunction() throws WrongAnnotationException {
                Code code = new Code();
         * @throws WrongAnnotationException
         */
        private Code generateAutoCopyFunction() throws WrongAnnotationException {
                Code code = new Code();

+               if (emptyState) // Empty state should have empty copy function
+                       return code;

                for (VariableDeclaration decl : declState) {
                        String type = decl.type;
                        String name = decl.name;
                for (VariableDeclaration decl : declState) {
                        String type = decl.type;
                        String name = decl.name;


@@ -97,6 +168,28 @@ public class GlobalConstruct extends Construct {
                return code;
        }
 
                return code;
        }
 

+       /**
+        * <p>
+        * This function will automatically generate the printing statements for
+        * supported types if the user has not defined the "@Print" primitive
+        * </p>
+        * 
+        * @return The auto-generated state printing statements
+        * @throws WrongAnnotationException
+        */
+       private Code generateAutoPrintFunction() throws WrongAnnotationException {
+               Code code = new Code();
+               if (emptyState) // Empty state should have empty printing function
+                       return code;
+               for (VariableDeclaration decl : declState) {
+                       String type = decl.type;
+                       String name = decl.name;
+                       code.addLines(SpecUtils.generatePrintStatement(type, name));
+               }
+
+               return code;
+       }
+

        /**
         * <p>
         * Assert that the global state primitive is valid; if not, throws an
        /**
         * <p>
         * Assert that the global state primitive is valid; if not, throws an

diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
index 2ed5367bb009df533d98b6c920eb9ffcd79d77e2..6afd5f127abd4261ec94b0285d23d56718209ae7 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
@@ -38,6 +38,8 @@ public class InterfaceConstruct extends Construct {
        // arguments of the interface
        private FunctionHeader funcHeader;
 
        // arguments of the interface
        private FunctionHeader funcHeader;
 

+       public final boolean autoGenPrint;
+

        public InterfaceConstruct(File file, int beginLineNum, int endLineNum,
                        ArrayList<String> annotations) throws WrongAnnotationException {
                super(file, beginLineNum);
        public InterfaceConstruct(File file, int beginLineNum, int endLineNum,
                        ArrayList<String> annotations) throws WrongAnnotationException {
                super(file, beginLineNum);


@@ -50,6 +52,8 @@ public class InterfaceConstruct extends Construct {
                this.print = new Code();
 
                processAnnotations(annotations);
                this.print = new Code();
 
                processAnnotations(annotations);

+
+               autoGenPrint = print.isEmpty();

        }
 
        public FunctionHeader getFunctionHeader() {
        }
 
        public FunctionHeader getFunctionHeader() {


@@ -71,6 +75,29 @@ public class InterfaceConstruct extends Construct {
                return this.name;
        }
 
                return this.name;
        }
 

+       /**
+        * <p>
+        * This function will automatically generate the printing statements for
+        * supported types if the user has not defined the "@Print" primitive
+        * </p>
+        * 
+        * @return The auto-generated state printing statements
+        * @throws WrongAnnotationException
+        */
+       private Code generateAutoPrintFunction() {
+               Code code = new Code();
+               // For RET
+               code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType,
+                               SpecNaming.RET));
+               // For arguments
+               for (VariableDeclaration decl : funcHeader.args) {
+                       String type = decl.type;
+                       String name = decl.name;
+                       code.addLines(SpecUtils.generatePrintStatement(type, name));
+               }
+               return code;
+       }
+

        /**
         * <p>
         * Assert that the interface primitive is valid; if not, throws an exception
        /**
         * <p>
         * Assert that the interface primitive is valid; if not, throws an exception


@@ -171,6 +198,12 @@ public class InterfaceConstruct extends Construct {
                funcHeader = UtilParser.parseFuncHeader(line);
                // Record the original declaration line
                funcHeader.setHeaderLine(line);
                funcHeader = UtilParser.parseFuncHeader(line);
                // Record the original declaration line
                funcHeader.setHeaderLine(line);

+
+               // Once we have the compelte function declaration, we can auto-gen the
+               // print-out statements if it's not defined
+               if (autoGenPrint) {
+                       print.addLines(generateAutoPrintFunction());
+               }

        }
 
        public String toString() {
        }
 
        public String toString() {

diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
index 959e51f2a7fda8cbcdbdc6edb1e3177d3a60c0c6..d3a2521223e3a3c5a9f918de46de5161fbaf8544 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
@@ -268,11 +268,12 @@ public class SpecExtractor {
                annotations.add(curLine);
                // System.out.println(curLine);
                // Initial settings for matching lines
                annotations.add(curLine);
                // System.out.println(curLine);
                // Initial settings for matching lines

-               // "\*/( |\t)*$"
-               Pattern regexpEnd = Pattern.compile("\\*/( |\\t)*$");
+               // "\*/\s*$"
+               Pattern regexpEnd = Pattern.compile("\\*/\\s*$");

                Matcher matcher = regexpEnd.matcher(curLine);
                Matcher matcher = regexpEnd.matcher(curLine);

-               if (matcher.find()) { // The beginning line is also the end line
-                       annotations.add(curLine);
+               if (matcher.find()) {
+                       // The beginning line is also the end line
+                       // In this case, we have already add the curLine

                        return annotations;
                } else {
                        try {
                        return annotations;
                } else {
                        try {

diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java
index aa021af99e463e08835630138eea05544de849f6..d60bf96c6f849fbb074c5fba50d50310bee3deb2 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecNaming.java
+++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java
@@ -176,6 +176,8 @@ public class SpecNaming {
        // Other CDSSpec functions
        public static final String AddInterfaceFunctions = "addInterfaceFunctions";
        public static final String CDSAnnotateFunc = "cdsannotate";
        // Other CDSSpec functions
        public static final String AddInterfaceFunctions = "addInterfaceFunctions";
        public static final String CDSAnnotateFunc = "cdsannotate";

+       public static final String PRINT = "PRINT";
+       public static final String PrintContainer = "printContainer";

 
        // Special instances
        public static final String Method1 = "_M";
 
        // Special instances
        public static final String Method1 = "_M";

diff --git a/src/edu/uci/eecs/specExtraction/SpecUtils.java b/src/edu/uci/eecs/specExtraction/SpecUtils.java
index 869b9ff81aff63566fbe77445851f7b360182977..71512d864cbb3c3ae55ac5174a9e647faab2977f 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecUtils.java
+++ b/src/edu/uci/eecs/specExtraction/SpecUtils.java
@@ -123,7 +123,8 @@ public class SpecUtils {
         *         annotations or the beginning line of the next primitive
         * @throws WrongAnnotationException
         */
         *         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
                        throws WrongAnnotationException {
                if (curIdx.getVal() == annotations.size()) // The current index points
                                                                                                        // to the end


@@ -146,8 +147,9 @@ public class SpecUtils {
                }
                // Assert that we must have found one primitive
                if (primitive == null) {
                }
                // 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"
                }
 
                // Process the current "primitive"


@@ -161,8 +163,9 @@ public class SpecUtils {
                                primitive.addLine(trimmedCode);
                        }
                } else {
                                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;
                }
 
                // Deal with other normal line. E.g. y = 1;


@@ -184,7 +187,8 @@ public class SpecUtils {
 
                if (primitive.contents.size() == 0) { // The content of the primitive is
                                                                                                // empty
 
                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;
        }
                }
                return primitive;
        }


@@ -229,8 +233,9 @@ public class SpecUtils {
                // FIXME: We only consider the type is either a one-level pointer or a
                // struct
                String bareType = trimSpace(type.replace('*', ' '));
                // 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")
+               return !bareType.equals("int") && !bareType.matches("unsigned\\s+int")
+                               && !bareType.equals("unsigned") && !bareType.equals("bool")
+                               && !bareType.equals("double") && !bareType.equals("float")

                                && !bareType.equals("void");
        }
 
                                && !bareType.equals("void");
        }
 


@@ -240,4 +245,67 @@ public class SpecUtils {
                String bareType = trimSpace(type.replace('*', ' '));
                return bareType;
        }
                String bareType = trimSpace(type.replace('*', ' '));
                return bareType;
        }

+
+       /**
+        * <p>
+        * This function will automatically generate the printing statements for
+        * supported types when given a type and a name of the declaration.
+        * </p>
+        * 
+        * @return The auto-generated state printing statements
+        */
+       public static Code generatePrintStatement(String type, String name) {
+               Code code = new Code();
+               // Primitive types
+               if (type.equals("int") || type.equals("unsigned")
+                               || type.equals("unsigned int") || type.equals("int unsigned")
+                               || type.equals("double") || type.equals("double")
+                               || type.equals("bool")) {
+                       // PRINT("\tx=%d\n", x);
+                       code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%d\\n\", "
+                                       + name + ");");
+               } else if (type.equals("int *") || type.equals("unsigned *")
+                               || type.equals("unsigned int *")
+                               || type.equals("int unsigned *") || type.equals("double *")
+                               || type.equals("double *") || type.equals("bool *")) {
+                       // Supported pointer types for primitive types
+                       // PRINT("\t*x=%d\n", *x);
+                       code.addLine(SpecNaming.PRINT + "(\"\\t*" + name + "=%d\\n\", *"
+                                       + name + ");");
+               } else if (type.equals("IntList") || type.equals("IntSet")
+                               || type.equals("IntMap")) {
+                       // Supported types
+                       // PRINT("\tq: ");
+                       // printContainer(&q);
+                       // model_print("\n");
+                       code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
+                       code.addLine(SpecNaming.PrintContainer + "(&" + name + ");");
+                       code.addLine(SpecNaming.PRINT + "(\"\\n\");");
+               } else if (type.equals("IntList *") || type.equals("IntSet *")
+                               || type.equals("IntMap *")) {
+                       // Supported pointer types
+                       // PRINT("\tq: ");
+                       // printContainer(q);
+                       // model_print("\n");
+                       code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
+                       code.addLine(SpecNaming.PrintContainer + "(" + name + ");");
+                       code.addLine(SpecNaming.PRINT + "(\"\\n\");");
+               } else if (type.equals("void")) {
+                       // Just do nothing!
+               } else {
+                       if (type.endsWith("*")) { // If it's an obvious pointer (with a STAR)
+                               // Weak support pointer types (just print out the address)
+                               // PRINT("\tmutex=%p\n", mutex);
+                               code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%p\\n\", "
+                                               + name + ");");
+                       } else {
+                               code.addLine("// We do not support auto-gen print-out for type: "
+                                               + type + ".");
+                       }
+                       
+               }
+
+               return code;
+       }
+

 }
 }