src/edu/uci/eecs/specExtraction/SpecUtils.java

   1 package edu.uci.eecs.specExtraction;
   2
   3 import java.io.File;
   4 import java.util.ArrayList;
   5 import java.util.regex.Matcher;
   6 import java.util.regex.Pattern;
   7
   8 /**
   9  * <p>
  10  * This class contains a list of static utility functions for extracting
  11  * specification annotations more conveniently.
  12  * </p>
  13  *
  14  * @author Peizhao Ou
  15  *
  16  */
  17 public class SpecUtils {
  18
  19         /**
  20          * <p>
  21          * This inner class defines a primitive --- a sub-annotation. For example,
  22          * the "@DeclareState" in the global state is one primitive. We record the
  23          * beginning line number of that primitive, the name of the primitive and a
  24          * list of lines that belong to that primitive.
  25          * </p>
  26          *
  27          * @author Peizhao Ou
  28          *
  29          */
  30         public static class Primitive {
  31                 public final int beginLineNum;
  32                 public final String name;
  33                 public final ArrayList<String> contents;
  34
  35                 public Primitive(String name, int beginLineNum) {
  36                         this.name = name;
  37                         this.beginLineNum = beginLineNum;
  38                         contents = new ArrayList<String>();
  39                 }
  40
  41                 public void addLine(String line) {
  42                         contents.add(line);
  43                 }
  44
  45                 public String toString() {
  46                         return "@" + name + ":\n" + contents;
  47                 }
  48         };
  49
  50         /**
  51          * <p>
  52          * This is a customized wrap of integer so that we can use integer type as
  53          * if they were in a C/C++ pass-by-reference fashion. It basically wraps an
  54          * int primitive to allow read, write and increment its internal int value.
  55          * </p>
  56          *
  57          * @author Peizhao Ou
  58          *
  59          */
  60         public static class IntObj {
  61                 private int value;
  62
  63                 public IntObj(int value) {
  64                         this.value = value;
  65                 }
  66
  67                 public void setVal(int value) {
  68                         this.value = value;
  69                 }
  70
  71                 public int getVal() {
  72                         return this.value;
  73                 }
  74
  75                 public void dec() {
  76                         this.value--;
  77                 }
  78
  79                 public void inc() {
  80                         this.value++;
  81                 }
  82
  83                 public String toString() {
  84                         return Integer.toString(value);
  85                 }
  86         }
  87
  88         // A regular expression pattern that matches "@WORD:"
  89         public static final Pattern regexpPrimitive = Pattern.compile("@(\\w+):");
  90         // The matcher for the primitive regular expression
  91         public static final Matcher matcherPrimitive = regexpPrimitive.matcher("");
  92
  93         // Match code after colon: ":" + Code + "$"
  94         public static final Pattern regexpCode = Pattern.compile(":(.*)$");
  95         public static final Matcher matcherCode = regexpCode.matcher("");
  96
  97         // Match a valid word: "^\w+$"
  98         public static final Pattern regexpWord = Pattern.compile("^\\w+$");
  99         public static final Matcher matcherWord = regexpWord.matcher("");
 100
 101         /**
 102          * <p>
 103          * This function will look for the first line that contains a primitive from
 104          * the "curIdx", and then extracts all the non-empty lines of that primitive
 105          * until it gets to the end of the list or the beginning of the next
 106          * primitive. It returns a list of the actual code for that primitive. When
 107          * we are done with the function call, the curIdx either points to the next
 108          * primitive or the end of the annotation list.
 109          * </p>
 110          *
 111          * @param file
 112          *            The file begin processing
 113          * @param beginLineNum
 114          *            The beginning line number of the first annotation lines
 115          * @param annotations
 116          *            The list of annotations
 117          * @param curIdx
 118          *            The current index (the index of the line that we are
 119          *            processing). We will update the current index after calling
 120          *            this function. Keep in mind that this is a customized wrap of
 121          *            integer so that we can use it as if it is a C/C++ reference
 122          * @return The primitive starting from the curIdx till either the end of the
 123          *         annotations or the beginning line of the next primitive
 124          * @throws WrongAnnotationException
 125          */
 126         public static Primitive extractPrimitive(File file, int beginLineNum,
 127                         ArrayList<String> annotations, IntObj curIdx)
 128                         throws WrongAnnotationException {
 129                 if (curIdx.getVal() == annotations.size()) // The current index points
 130                                                                                                         // to the end
 131                         // of the list
 132                         return null;
 133
 134                 String line = null;
 135                 int curLineNum = -1;
 136                 Primitive primitive = null;
 137                 // Find the first primitive
 138                 for (; curIdx.getVal() < annotations.size(); curIdx.inc()) {
 139                         line = annotations.get(curIdx.getVal());
 140                         curLineNum = curIdx.getVal() + beginLineNum;
 141                         matcherPrimitive.reset(line);
 142                         if (matcherPrimitive.find()) {
 143                                 String name = matcherPrimitive.group(1);
 144                                 primitive = new Primitive(name, curLineNum);
 145                                 break;
 146                         }
 147                 }
 148                 // Assert that we must have found one primitive
 149                 if (primitive == null) {
 150                         WrongAnnotationException
 151                                         .err(file, curLineNum,
 152                                                         "Something is wrong! We must have found one primitve here!\n");
 153                 }
 154
 155                 // Process the current "primitive"
 156                 // Deal with the first special line. E.g. @DeclareState: int x;
 157                 String code = null;
 158                 matcherCode.reset(line);
 159                 if (matcherCode.find()) {
 160                         code = matcherCode.group(1);
 161                         String trimmedCode = trimSpace(trimTrailingCommentSymbol(code));
 162                         if (!trimmedCode.equals("")) {
 163                                 primitive.addLine(trimmedCode);
 164                         }
 165                 } else {
 166                         WrongAnnotationException
 167                                         .err(file, curLineNum,
 168                                                         "The state annotation should have correct primitive syntax (sub-annotations)");
 169                 }
 170
 171                 // Deal with other normal line. E.g. y = 1;
 172                 curIdx.inc();
 173                 ;
 174                 for (; curIdx.getVal() < annotations.size(); curIdx.inc()) {
 175                         curLineNum = beginLineNum + curIdx.getVal();
 176                         line = annotations.get(curIdx.getVal());
 177                         matcherPrimitive.reset(line);
 178                         if (!matcherPrimitive.find()) {
 179                                 // This is another line that we should add to the result
 180                                 code = trimSpace(trimTrailingCommentSymbol(line));
 181                                 if (!code.equals(""))
 182                                         primitive.addLine(code);
 183                         } else
 184                                 // We get to the end of the current primitive
 185                                 break;
 186                 }
 187
 188                 if (primitive.contents.size() == 0) { // The content of the primitive is
 189                                                                                                 // empty
 190                         WrongAnnotationException.warning(file, curLineNum, "Primitive "
 191                                         + primitive.name + " is empty.");
 192                 }
 193                 return primitive;
 194         }
 195
 196         /**
 197          *
 198          * @param line
 199          *            The line to be processed
 200          * @return The string whose beginning and ending space have been trimmed
 201          */
 202         public static String trimSpace(String line) {
 203                 // "^\s*(.*?)\s*$"
 204                 Pattern regexp = Pattern.compile("^\\s*(.*?)\\s*$");
 205                 Matcher matcher = regexp.matcher(line);
 206                 if (matcher.find()) {
 207                         return matcher.group(1);
 208                 } else {
 209                         return line;
 210                 }
 211         }
 212
 213         /**
 214          * <p>
 215          * It processed the line in a way that it removes the trailing C/C++ comment
 216          * symbols "STAR SLASH"
 217          * </p>
 218          *
 219          * @param line
 220          * @return
 221          */
 222         public static String trimTrailingCommentSymbol(String line) {
 223                 Pattern regexp = Pattern.compile("(.*?)\\s*(\\*/)?\\s*$");
 224                 Matcher matcher = regexp.matcher(line);
 225                 if (matcher.find()) {
 226                         return matcher.group(1);
 227                 } else {
 228                         return null;
 229                 }
 230         }
 231
 232         public static boolean isUserDefinedStruct(String type) {
 233                 // FIXME: We only consider the type is either a one-level pointer or a
 234                 // struct
 235                 String bareType = trimSpace(type.replace('*', ' '));
 236                 return !bareType.equals("int") && !bareType.matches("unsigned\\s+int")
 237                                 && !bareType.equals("unsigned") && !bareType.equals("bool")
 238                                 && !bareType.equals("double") && !bareType.equals("float")
 239                                 && !bareType.equals("void");
 240         }
 241
 242         public static String getPlainType(String type) {
 243                 // FIXME: We only consider the type is either a one-level pointer or a
 244                 // struct
 245                 String bareType = trimSpace(type.replace('*', ' '));
 246                 return bareType;
 247         }
 248
 249         /**
 250          * <p>
 251          * This function will automatically generate the printing statements for
 252          * supported types when given a type and a name of the declaration.
 253          * </p>
 254          *
 255          * @return The auto-generated state printing statements
 256          */
 257         public static Code generatePrintStatement(String type, String name) {
 258                 Code code = new Code();
 259                 // Primitive types
 260                 if (type.equals("int") || type.equals("unsigned")
 261                                 || type.equals("unsigned int") || type.equals("int unsigned")
 262                                 || type.equals("double") || type.equals("double")
 263                                 || type.equals("bool")) {
 264                         // PRINT("\tx=%d\n", x);
 265                         code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%d\\n\", "
 266                                         + name + ");");
 267                 } else if (type.equals("int *") || type.equals("unsigned *")
 268                                 || type.equals("unsigned int *")
 269                                 || type.equals("int unsigned *") || type.equals("double *")
 270                                 || type.equals("double *") || type.equals("bool *")) {
 271                         // Supported pointer types for primitive types
 272                         // PRINT("\t*x=%d\n", *x);
 273                         code.addLine(SpecNaming.PRINT + "(\"\\t*" + name + "=%d\\n\", *"
 274                                         + name + ");");
 275                 } else if (type.equals("IntList") || type.equals("IntSet")
 276                                 || type.equals("IntMap")) {
 277                         // Supported types
 278                         // PRINT("\tq: ");
 279                         // printContainer(&q);
 280                         // model_print("\n");
 281                         code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
 282                         code.addLine(SpecNaming.PrintContainer + "(&" + name + ");");
 283                         code.addLine(SpecNaming.PRINT + "(\"\\n\");");
 284                 } else if (type.equals("IntList *") || type.equals("IntSet *")
 285                                 || type.equals("IntMap *")) {
 286                         // Supported pointer types
 287                         // PRINT("\tq: ");
 288                         // printContainer(q);
 289                         // model_print("\n");
 290                         code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
 291                         code.addLine(SpecNaming.PrintContainer + "(" + name + ");");
 292                         code.addLine(SpecNaming.PRINT + "(\"\\n\");");
 293                 } else if (type.equals("void")) {
 294                         // Just do nothing!
 295                 } else {
 296                         if (type.endsWith("*")) { // If it's an obvious pointer (with a STAR)
 297                                 // Weak support pointer types (just print out the address)
 298                                 // PRINT("\tmutex=%p\n", mutex);
 299                                 code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%p\\n\", "
 300                                                 + name + ");");
 301                         } else {
 302                                 code.addLine("// We do not support auto-gen print-out for type: "
 303                                                 + type + ".");
 304                         }
 305
 306                 }
 307
 308                 return code;
 309         }
 310
 311 }