allow shorter spec --- @Interface is not mandatory

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 99c4f2e17ca038260ad55f0e10ff0a6c01c44cea..4100a0a3d5acddb338b9b1ee87605d63ac5e3a63 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -197,9 +197,10 @@ public class CodeGeneratorUtils {
                        for (InterfaceConstruct construct : list) {
                                // Declare custom value struct for the interface
                                String name = construct.getName();
+                               String structName = construct.getStructName();
                                code.addLine(ShortComment("Declare custom value struct for "
                                                + name));
-                               code.addLine("typedef struct " + name + " {");
+                               code.addLine("typedef struct " + structName + " {");
                                FunctionHeader funcHeader = construct.getFunctionHeader();
                                // RET
                                if (!funcHeader.returnType.equals("void"))
@@ -209,7 +210,7 @@ public class CodeGeneratorUtils {
                                for (VariableDeclaration decl : funcHeader.args) {
                                        code.addLine(TabbedLine(Declare(decl)));
                                }
-                               code.addLine("} " + name + ";");
+                               code.addLine("} " + structName + ";");
                                code.addLine("");
                        }
                }
@@ -498,11 +499,15 @@ public class CodeGeneratorUtils {
                                        + SpecNaming.AppendStr(rule.method2) + ") {"));
                        // Initialize M1 & M2 in commutativity rule
                        // e.g. ENQ *M1 = (ENQ*) m1->value;
+                       String structName1 = InterfaceConstruct
+                                       .createStructName(rule.method1);
+                       String structName2 = InterfaceConstruct
+                                       .createStructName(rule.method2);
                        code.addLine(TabbedLine(
-                                       DeclareDefine(rule.method1, "*M1", "(" + rule.method1
+                                       DeclareDefine(structName1, "*M1", "(" + structName1
                                                        + "*) m1->value"), 2));
                        code.addLine(TabbedLine(
-                                       DeclareDefine(rule.method2, "*M2", "(" + rule.method2
+                                       DeclareDefine(structName2, "*M2", "(" + structName2
                                                        + "*) m2->value"), 2));
                        code.addLine(TabbedLine("return " + rule.condition + ";", 2));
                        code.addLine(TabbedLine("}"));
@@ -520,6 +525,7 @@ public class CodeGeneratorUtils {
 
                                // Define interface functions
                                String name = construct.getName();
+                               String structName = construct.getStructName();
                                code.addLine("/**********    " + name
                                                + " functions    **********/");
                                // Define @Transition for INTERFACE
@@ -861,10 +867,11 @@ public class CodeGeneratorUtils {
                        String inst, InterfaceConstruct construct) {
                Code res = new Code();
                String name = construct.getName();
+               String structName = construct.getStructName();
                res.addLine(ShortComment("Initialize fields for " + name));
                // The very first assignment "
-               res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) "
-                               + methodInst + "->" + SpecNaming.MethodValueField));
+               res.addLine(DeclareDefine(structName, "*" + inst, "(" + structName
+                               + "*) " + methodInst + "->" + SpecNaming.MethodValueField));
                // Don't leave out the RET field
                if (!construct.getFunctionHeader().isReturnVoid()) {
                        res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
@@ -975,6 +982,7 @@ public class CodeGeneratorUtils {
                Code code = new Code();
 
                String name = construct.getName();
+               String structName = construct.getStructName();
                String beginLine = construct.getFunctionHeader().getHeaderLine();
                Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
                Matcher matcherSpace = regexpSpace.matcher(beginLine);
@@ -1017,8 +1025,9 @@ public class CodeGeneratorUtils {
                // The very first assignment "
                code.addLine(prefixTabs
                                + "\t"
-                               + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst,
-                                               SpecNaming.New + Brace(name)));
+                               + DeclareDefine(structName,
+                                               "*" + SpecNaming.InterfaceValueInst, SpecNaming.New
+                                                               + Brace(structName)));
                // Don't leave out the RET field
                if (!construct.getFunctionHeader().isReturnVoid())
                        code.addLine(prefixTabs

diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
index 232acaf2b34bc5529db9d64bb10af8547059f1ca..1ff0cb05514cc3c8e7c01d56587cee307c6bcd03 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
@@ -21,9 +21,16 @@ import edu.uci.eecs.utilParser.UtilParser;
  * 
  */
 public class InterfaceConstruct extends Construct {
+       // The interface label of the current interface; If not specified, we use
+       // the actual interface name to represent this interface
        private String name;
-       public final Code transition;
+       // Each interface interface will have an auto-generated struct that
+       // represents the return value and the arguments of that interface method
+       // call. We will mangle the interface label name to get this name in case we
+       // have other name conflict
+       private String structName;
        public final Code preCondition;
+       public final Code transition;
        public final Code postCondition;
        public final Code print;
 
@@ -44,8 +51,9 @@ public class InterfaceConstruct extends Construct {
                super(file, beginLineNum);
                this.endLineNum = endLineNum;
                this.name = null;
-               this.transition = new Code();
+               this.structName = null;
                this.preCondition = new Code();
+               this.transition = new Code();
                this.postCondition = new Code();
                this.print = new Code();
 
@@ -164,7 +172,8 @@ public class InterfaceConstruct extends Construct {
                        if (primitive.contents.size() == 0)
                                continue;
                        if (name.equals(SpecNaming.Interface)) {
-                               this.name = extractInterfaceName(file, primitive);
+                               String interName = extractInterfaceName(file, primitive); 
+                               setNames(interName);
                        } else if (name.equals(SpecNaming.Transition)) {
                                this.transition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PreCondition)) {
@@ -195,6 +204,12 @@ public class InterfaceConstruct extends Construct {
                // Record the original declaration line
                funcHeader.setHeaderLine(line);
 
+               // If users have not defined @Interface, we should use the function name
+               // as the interface label
+               if (name == null) {
+                       setNames(funcHeader.funcName.bareName);
+               }
+
                // Once we have the compelte function declaration, we can auto-gen the
                // print-out statements if it's not defined
                if (autoGenPrint) {
@@ -226,4 +241,19 @@ public class InterfaceConstruct extends Construct {
        public void setEndLineNumFunction(int endLineNumFunction) {
                this.endLineNumFunction = endLineNumFunction;
        }
+
+       public String getStructName() {
+               return structName;
+       }
+
+       private void setNames(String name) {
+               this.name = name;
+               if (name == null)
+                       return;
+               structName = createStructName(name);
+       }
+       
+       static public String createStructName(String labelName) {
+               return "__struct_" + labelName + "__";
+       }
 }

diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
index d3a2521223e3a3c5a9f918de46de5161fbaf8544..afa42f78033b5d34475c38c5601fa251950563fc 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
@@ -624,7 +624,7 @@ public class SpecExtractor {
                        lineReader = new LineNumberReader(br);
                        // "/\*\*\s*@(DeclareState|Interface)"
                        Pattern regexpBegin = Pattern
-                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|Define)");
+                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|Transition|PostCondition|Define)");
                        Matcher matcher = regexpBegin.matcher("");
 
                        String line;
@@ -652,7 +652,10 @@ public class SpecExtractor {
                                        if (constructName.equals(SpecNaming.DeclareState)) {
                                                extractGlobalConstruct(file, lineReader, line,
                                                                beginLineNum);
-                                       } else if (constructName.equals(SpecNaming.Interface)) {
+                                       } else if (constructName.equals(SpecNaming.Interface)
+                                                       || constructName.equals(SpecNaming.PreCondition)
+                                                       || constructName.equals(SpecNaming.Transition)
+                                                       || constructName.equals(SpecNaming.PostCondition)) {
                                                extractInterfaceConstruct(file, lineReader, line,
                                                                beginLineNum);
                                        } else if (constructName.equals(SpecNaming.Define)) {