edits

[cdsspec-compiler.git] / src / edu / uci / eecs / specExtraction / InterfaceConstruct.java

diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
index 2ed5367bb009df533d98b6c920eb9ffcd79d77e2..ddc26145f8f136c40576cb8ec00657d43f6a05ff 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
@@ -21,10 +21,18 @@ 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 sideEffect;
+       public final Code justifyingPrecondition;
+       public final Code transition;
+       public final Code justifyingPostcondition;
        public final Code postCondition;
        public final Code print;
 
@@ -38,18 +46,24 @@ public class InterfaceConstruct extends Construct {
        // 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);
                this.endLineNum = endLineNum;
                this.name = null;
-               this.transition = new Code();
+               this.structName = null;
                this.preCondition = new Code();
-               this.sideEffect = new Code();
+               this.justifyingPrecondition = new Code();
+               this.transition = new Code();
+               this.justifyingPostcondition = new Code();
                this.postCondition = new Code();
                this.print = new Code();
 
                processAnnotations(annotations);
+
+               autoGenPrint = print.isEmpty();
        }
 
        public FunctionHeader getFunctionHeader() {
@@ -71,6 +85,29 @@ public class InterfaceConstruct extends Construct {
                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 C_RET
+               code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType,
+                               SpecNaming.C_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
@@ -89,7 +126,9 @@ public class InterfaceConstruct extends Construct {
                if (!name.equals(SpecNaming.Interface)
                                && !name.equals(SpecNaming.Transition)
                                && !name.equals(SpecNaming.PreCondition)
+                               && !name.equals(SpecNaming.JustifyingPrecondition)
                                && !name.equals(SpecNaming.SideEffect)
+                               && !name.equals(SpecNaming.JustifyingPostcondition)
                                && !name.equals(SpecNaming.PostCondition)
                                && !name.equals(SpecNaming.PrintValue)) {
                        WrongAnnotationException.err(file, lineNum, name
@@ -139,13 +178,16 @@ 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)) {
                                this.preCondition.addLines(primitive.contents);
-                       } else if (name.equals(SpecNaming.SideEffect)) {
-                               this.sideEffect.addLines(primitive.contents);
+                       } else if (name.equals(SpecNaming.JustifyingPrecondition)) {
+                               this.justifyingPrecondition.addLines(primitive.contents);
+                       } else if (name.equals(SpecNaming.JustifyingPostcondition)) {
+                               this.justifyingPostcondition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PostCondition)) {
                                this.postCondition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PrintValue)) {
@@ -171,6 +213,18 @@ public class InterfaceConstruct extends Construct {
                funcHeader = UtilParser.parseFuncHeader(line);
                // 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) {
+                       print.addLines(generateAutoPrintFunction());
+               }
        }
 
        public String toString() {
@@ -181,8 +235,6 @@ public class InterfaceConstruct extends Construct {
                        sb.append("@Transition:\n" + transition);
                if (!preCondition.isEmpty())
                        sb.append("@PreCondition:\n" + preCondition);
-               if (!sideEffect.isEmpty())
-                       sb.append("@SideEffect:\n" + sideEffect);
                if (!postCondition.isEmpty())
                        sb.append("@PostCondition:\n" + postCondition);
                if (!print.isEmpty())
@@ -199,4 +251,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 + "__";
+       }
 }