add support for "C_RET, S_RET, JustifyingPre/Postconditions"

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

diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
index 0e470e0e5361bc9f476b6e69f06d21709faffcd2..8c478557139570708c7709d50717ad6694032d5c 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
@@ -30,6 +30,7 @@ import edu.uci.eecs.utilParser.ParseException;
  * 
  */
 public class SpecExtractor {
+       public final HashMap<File, ArrayList<DefineConstruct>> defineListMap;
        public final HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap;
        public final HashMap<File, ArrayList<OPConstruct>> OPListMap;
        public final HashSet<String> OPLabelSet;
@@ -38,17 +39,31 @@ public class SpecExtractor {
 
        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;
 
        public SpecExtractor() {
+               defineListMap = new HashMap<File, ArrayList<DefineConstruct>>();
                interfaceListMap = new HashMap<File, ArrayList<InterfaceConstruct>>();
                OPListMap = new HashMap<File, ArrayList<OPConstruct>>();
                OPLabelSet = new HashSet<String>();
                entryMap = new HashMap<File, EntryConstruct>();
                headerFiles = new HashSet<String>();
+               forwardClass = new HashSet<String>();
                globalConstruct = null;
        }
 
+       private void addDefineConstruct(DefineConstruct construct) {
+               ArrayList<DefineConstruct> list = defineListMap.get(construct.file);
+               if (list == null) {
+                       list = new ArrayList<DefineConstruct>();
+                       defineListMap.put(construct.file, list);
+               }
+               list.add(construct);
+       }
+
        private void addInterfaceConstruct(InterfaceConstruct construct) {
                ArrayList<InterfaceConstruct> list = interfaceListMap
                                .get(construct.file);
@@ -252,11 +267,12 @@ public class SpecExtractor {
                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);
-               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 {
@@ -369,6 +385,39 @@ public class SpecExtractor {
                return -1;
        }
 
+       /**
+        * <p>
+        * A sub-routine to extract the define construct. When called, we have
+        * already match the beginning of the construct, and we also need to find
+        * the ending line number of the anntotation.
+        * </p>
+        * 
+        * @param file
+        *            The file that we are processing
+        * @param lineReader
+        *            The LineNumberReader that we are using when processing the
+        *            current file.
+        * @param curLine
+        *            The current line that we are processing. It should be the
+        *            beginning line of the annotation construct.
+        * @param beginLineNum
+        *            The beginning line number of the interface construct
+        *            annotation
+        * @throws WrongAnnotationException
+        * @throws IOException
+        * @throws ParseException
+        */
+       private void extractDefineConstruct(File file, LineNumberReader lineReader,
+                       String curLine, int beginLineNum) throws WrongAnnotationException,
+                       IOException, ParseException {
+               ArrayList<String> annotations = extractTillConstructEnd(file,
+                               lineReader, curLine, beginLineNum);
+               int endLineNum = lineReader.getLineNumber();
+               DefineConstruct construct = new DefineConstruct(file, beginLineNum,
+                               endLineNum, annotations);
+               addDefineConstruct(construct);
+       }
+
        /**
         * <p>
         * A sub-routine to extract the interface construct. When called, we have
@@ -410,6 +459,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()
@@ -527,7 +588,9 @@ public class SpecExtractor {
                                extractEntryConstruct(file, beginLineNum, curLine);
                        else if (name.equals("OPDefine") || name.equals("PotentialOP")
                                        || name.equals("OPCheck") || name.equals("OPClear")
-                                       || name.equals("OPClearDefine"))
+                                       || name.equals("OPClearDefine")
+                                       || name.equals("OPDefineUnattached")
+                                       || name.equals("OPClearDefineUnattached"))
                                extractOPConstruct(file, beginLineNum, curLine,
                                                OPType.valueOf(name));
                }
@@ -561,7 +624,7 @@ public class SpecExtractor {
                        lineReader = new LineNumberReader(br);
                        // "/\*\*\s*@(DeclareState|Interface)"
                        Pattern regexpBegin = Pattern
-                                       .compile("/\\*\\*\\s*@(DeclareState|Interface)");
+                                       .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingPrecondition|Transition|JustifyingPostcondition|PostCondition|Define)");
                        Matcher matcher = regexpBegin.matcher("");
 
                        String line;
@@ -589,9 +652,17 @@ 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.JustifyingPrecondition)
+                                                       || constructName.equals(SpecNaming.Transition)
+                                                       || constructName.equals(SpecNaming.JustifyingPostcondition)
+                                                       || constructName.equals(SpecNaming.PostCondition)) {
                                                extractInterfaceConstruct(file, lineReader, line,
                                                                beginLineNum);
+                                       } else if (constructName.equals(SpecNaming.Define)) {
+                                               extractDefineConstruct(file, lineReader, line,
+                                                               beginLineNum);
                                        } else {
                                                WrongAnnotationException.err(file, beginLineNum,
                                                                constructName