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

   1 package edu.uci.eecs.specExtraction;
   2
   3 import java.io.BufferedReader;
   4 import java.io.File;
   5 import java.io.FileNotFoundException;
   6 import java.io.FileReader;
   7 import java.io.IOException;
   8 import java.io.LineNumberReader;
   9 import java.util.ArrayList;
  10 import java.util.Collections;
  11 import java.util.HashMap;
  12 import java.util.HashSet;
  13 import java.util.regex.Matcher;
  14 import java.util.regex.Pattern;
  15
  16 import edu.uci.eecs.codeGenerator.CodeGeneratorUtils;
  17 import edu.uci.eecs.codeGenerator.Environment;
  18 import edu.uci.eecs.utilParser.ParseException;
  19
  20 /**
  21  * <p>
  22  * This class represents the specification extractor of the specification. The
  23  * main function of this class is to read C/C++11 source files and extract the
  24  * corresponding specifications, and record corresponding information such as
  25  * location, e.g., the file name and the line number, to help the code
  26  * generation process.
  27  * </p>
  28  *
  29  * @author Peizhao Ou
  30  *
  31  */
  32 public class SpecExtractor {
  33         public final HashMap<File, ArrayList<DefineConstruct>> defineListMap;
  34         public final HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap;
  35         public final HashMap<File, ArrayList<OPConstruct>> OPListMap;
  36         public final HashSet<String> OPLabelSet;
  37         // Note that we only allow one entry per file at most
  38         public final HashMap<File, EntryConstruct> entryMap;
  39
  40         public final HashSet<String> headerFiles;
  41
  42         // In the generated header file, we need to forward the user-defined
  43         public final HashSet<String> forwardClass;
  44
  45         private GlobalConstruct globalConstruct;
  46
  47         public SpecExtractor() {
  48                 defineListMap = new HashMap<File, ArrayList<DefineConstruct>>();
  49                 interfaceListMap = new HashMap<File, ArrayList<InterfaceConstruct>>();
  50                 OPListMap = new HashMap<File, ArrayList<OPConstruct>>();
  51                 OPLabelSet = new HashSet<String>();
  52                 entryMap = new HashMap<File, EntryConstruct>();
  53                 headerFiles = new HashSet<String>();
  54                 forwardClass = new HashSet<String>();
  55                 globalConstruct = null;
  56         }
  57
  58         private void addDefineConstruct(DefineConstruct construct) {
  59                 ArrayList<DefineConstruct> list = defineListMap.get(construct.file);
  60                 if (list == null) {
  61                         list = new ArrayList<DefineConstruct>();
  62                         defineListMap.put(construct.file, list);
  63                 }
  64                 list.add(construct);
  65         }
  66
  67         private void addInterfaceConstruct(InterfaceConstruct construct) {
  68                 ArrayList<InterfaceConstruct> list = interfaceListMap
  69                                 .get(construct.file);
  70                 if (list == null) {
  71                         list = new ArrayList<InterfaceConstruct>();
  72                         interfaceListMap.put(construct.file, list);
  73                 }
  74                 list.add(construct);
  75         }
  76
  77         private void addOPConstruct(OPConstruct construct) {
  78                 ArrayList<OPConstruct> list = OPListMap.get(construct.file);
  79                 if (list == null) {
  80                         list = new ArrayList<OPConstruct>();
  81                         OPListMap.put(construct.file, list);
  82                 }
  83                 list.add(construct);
  84         }
  85
  86         private void addEntryConstruct(File file, EntryConstruct construct)
  87                         throws WrongAnnotationException {
  88                 EntryConstruct old = entryMap.get(file);
  89                 if (old == null)
  90                         entryMap.put(file, construct);
  91                 else { // Error processing
  92                         String errMsg = "Multiple @Entry annotations in the same file.\n\t Other @Entry at Line "
  93                                         + old.beginLineNum + ".";
  94                         WrongAnnotationException.err(file, construct.beginLineNum, errMsg);
  95                 }
  96         }
  97
  98         public GlobalConstruct getGlobalConstruct() {
  99                 return this.globalConstruct;
 100         }
 101
 102         /**
 103          * <p>
 104          * A print out function for the purpose of debugging. Note that we better
 105          * call this function after having called the checkSemantics() function to
 106          * check annotation consistency.
 107          * </p>
 108          */
 109         public void printAnnotations() {
 110                 System.out
 111                                 .println("/**********    Print out of specification extraction    **********/");
 112                 System.out.println("// Extracted header files");
 113                 for (String header : headerFiles)
 114                         System.out.println(header);
 115
 116                 System.out.println("// Global State Construct");
 117                 if (globalConstruct != null)
 118                         System.out.println(globalConstruct);
 119
 120                 for (File file : interfaceListMap.keySet()) {
 121                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
 122                         System.out.println("// Interface in file: " + file.getName());
 123                         for (InterfaceConstruct construct : list) {
 124                                 System.out.println(construct);
 125                                 System.out.println("EndLineNumFunc: "
 126                                                 + construct.getEndLineNumFunction());
 127                         }
 128                 }
 129
 130                 for (File file : OPListMap.keySet()) {
 131                         System.out.println("// Ordering points in file: " + file.getName());
 132                         ArrayList<OPConstruct> list = OPListMap.get(file);
 133                         for (OPConstruct construct : list)
 134                                 System.out.println(construct);
 135                 }
 136
 137                 for (File file : entryMap.keySet()) {
 138                         System.out.println("// Entry in file: " + file.getName());
 139                         System.out.println(entryMap.get(file));
 140                 }
 141         }
 142
 143         /**
 144          * <p>
 145          * Perform basic semantics checking of the extracted specification.
 146          * </p>
 147          *
 148          * @return
 149          * @throws WrongAnnotationException
 150          */
 151         public void checkSemantics() throws WrongAnnotationException {
 152                 String errMsg = null;
 153
 154                 // Assert that we have defined and only defined one global state
 155                 // annotation
 156                 if (globalConstruct == null) {
 157                         errMsg = "Spec error: There should be one global state annotation.\n";
 158                         throw new WrongAnnotationException(errMsg);
 159                 }
 160
 161                 // Assert that the interface constructs have unique label name
 162                 HashMap<String, InterfaceConstruct> interfaceMap = new HashMap<String, InterfaceConstruct>();
 163                 for (File f : interfaceListMap.keySet()) {
 164                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(f);
 165                         if (list != null) {
 166                                 for (InterfaceConstruct construct : list) {
 167                                         InterfaceConstruct existingConstruct = interfaceMap
 168                                                         .get(construct.getName());
 169                                         if (existingConstruct != null) { // Error
 170                                                 errMsg = "Interface labels duplication with: \""
 171                                                                 + construct.getName() + "\" in File \""
 172                                                                 + existingConstruct.file.getName()
 173                                                                 + "\", Line " + existingConstruct.beginLineNum
 174                                                                 + ".";
 175                                                 WrongAnnotationException.err(construct.file,
 176                                                                 construct.beginLineNum, errMsg);
 177                                         } else {
 178                                                 interfaceMap.put(construct.getName(), construct);
 179                                         }
 180                                 }
 181                         }
 182                 }
 183
 184                 // Process ordering point labels
 185                 for (File file : OPListMap.keySet()) {
 186                         ArrayList<OPConstruct> list = OPListMap.get(file);
 187                         for (OPConstruct construct : list) {
 188                                 if (construct.type == OPType.OPCheck
 189                                                 || construct.type == OPType.PotentialOP) {
 190                                         String label = construct.label;
 191                                         OPLabelSet.add(label);
 192                                 }
 193                         }
 194                 }
 195
 196         }
 197
 198         /**
 199          * <p>
 200          * This function applies on a String (a plain line of text) to check whether
 201          * the current line is a C/C++ header include statement. If it is, it
 202          * extracts the header file name and store it, and returns true; otherwise,
 203          * it returns false.
 204          * </p>
 205          *
 206          * @param line
 207          *            The line of text to be processed
 208          * @return Returns true if the current line is a C/C++ header include
 209          *         statement
 210          */
 211         public boolean extractHeaders(String line) {
 212                 // "^( |\t)*#include( |\t)+("|<)([a-zA-Z_0-9\-\.])+("|>)"
 213                 Pattern regexp = Pattern
 214                                 .compile("^( |\\t)*(#include)( |\\t)+(\"|<)([a-zA-Z_0-9\\-\\.]+)(\"|>)");
 215                 Matcher matcher = regexp.matcher(line);
 216
 217                 // process the line.
 218                 if (matcher.find()) {
 219                         String header = null;
 220                         String braceSymbol = matcher.group(4);
 221                         if (braceSymbol.equals("<"))
 222                                 header = "<" + matcher.group(5) + ">";
 223                         else
 224                                 header = "\"" + matcher.group(5) + "\"";
 225                         if (!SpecNaming.isPreIncludedHeader(header)) {
 226                                 headerFiles.add(header);
 227                         }
 228                         return true;
 229                 } else
 230                         return false;
 231         }
 232
 233         /**
 234          * <p>
 235          * A sub-routine to extract the construct from beginning till end. When
 236          * called, we have already match the beginning of the construct. We will
 237          * call this sub-routine when we extract the interface construct and the
 238          * global state construct.
 239          * </p>
 240          *
 241          * <p>
 242          * The side effect of this function is that the lineReader has just read the
 243          * end of the construct, meaning that the caller can get the end line number
 244          * by calling lineReader.getLineNumber().
 245          * </p>
 246          *
 247          * @param file
 248          *            The file that we are processing
 249          * @param lineReader
 250          *            The LineNumberReader that we are using when processing the
 251          *            current file.
 252          * @param file
 253          *            The file that we are processing
 254          * @param curLine
 255          *            The current line that we are processing. It should be the
 256          *            beginning line of the annotation construct.
 257          * @param beginLineNum
 258          *            The beginning line number of the interface construct
 259          *            annotation
 260          * @return Returns the annotation string list of the current construct
 261          * @throws WrongAnnotationException
 262          */
 263         private ArrayList<String> extractTillConstructEnd(File file,
 264                         LineNumberReader lineReader, String curLine, int beginLineNum)
 265                         throws WrongAnnotationException {
 266                 ArrayList<String> annotations = new ArrayList<String>();
 267                 annotations.add(curLine);
 268                 // System.out.println(curLine);
 269                 // Initial settings for matching lines
 270                 // "\*/\s*$"
 271                 Pattern regexpEnd = Pattern.compile("\\*/\\s*$");
 272                 Matcher matcher = regexpEnd.matcher(curLine);
 273                 if (matcher.find()) {
 274                         // The beginning line is also the end line
 275                         // In this case, we have already add the curLine
 276                         return annotations;
 277                 } else {
 278                         try {
 279                                 String line;
 280                                 while ((line = lineReader.readLine()) != null) {
 281                                         // process the line.
 282                                         // System.out.println(line);
 283
 284                                         matcher.reset(line); // reset the input
 285                                         annotations.add(line);
 286                                         if (matcher.find())
 287                                                 return annotations;
 288                                 }
 289                                 WrongAnnotationException
 290                                                 .err(file,
 291                                                                 beginLineNum,
 292                                                                 "The interface annotation should have the matching closing symbol closing \"*/\"");
 293                         } catch (IOException e) {
 294                                 e.printStackTrace();
 295                         }
 296                 }
 297                 return null;
 298         }
 299
 300         /**
 301          * <p>
 302          * A sub-routine to extract the global construct. When called, we have
 303          * already match the beginning of the construct.
 304          * </p>
 305          *
 306          * @param file
 307          *            The file that we are processing
 308          * @param lineReader
 309          *            The LineNumberReader that we are using when processing the
 310          *            current file.
 311          * @param curLine
 312          *            The current line that we are processing. It should be the
 313          *            beginning line of the annotation construct.
 314          * @param beginLineNum
 315          *            The beginning line number of the interface construct
 316          *            annotation
 317          * @throws WrongAnnotationException
 318          */
 319         private void extractGlobalConstruct(File file, LineNumberReader lineReader,
 320                         String curLine, int beginLineNum) throws WrongAnnotationException {
 321                 ArrayList<String> annotations = extractTillConstructEnd(file,
 322                                 lineReader, curLine, beginLineNum);
 323                 GlobalConstruct construct = new GlobalConstruct(file, beginLineNum,
 324                                 annotations);
 325                 if (globalConstruct != null) { // Check if we have seen a global state
 326                                                                                 // construct earlier
 327                         File otherDefinitionFile = globalConstruct.file;
 328                         int otherDefinitionLine = globalConstruct.beginLineNum;
 329                         String errMsg = "Multiple definition of global state.\n"
 330                                         + "\tAnother definition is in File \""
 331                                         + otherDefinitionFile.getName() + "\" (Line "
 332                                         + otherDefinitionLine + ").";
 333                         WrongAnnotationException.err(file, beginLineNum, errMsg);
 334                 }
 335                 globalConstruct = construct;
 336         }
 337
 338         /**
 339          * @param file
 340          *            The current file we are processing
 341          * @param lineReader
 342          *            Call this function when the lineReader will read the beginning
 343          *            of the definition right away
 344          * @param startingLine
 345          *            The line that we should start processing
 346          * @return The line number of the ending line of the interfae definition. If
 347          *         returning -1, it means the curl symbols in the interface do not
 348          *         match
 349          * @throws WrongAnnotationException
 350          */
 351         private int findEndLineNumFunction(File file, LineNumberReader lineReader,
 352                         String startingLine) throws WrongAnnotationException {
 353                 String line = startingLine;
 354                 // FIXME: We assume that in the string of the code, there does not exist
 355                 // the symbol '{' & '{'
 356                 try {
 357                         boolean foundFirstCurl = false;
 358                         int unmatchedCnt = 0;
 359                         do {
 360                                 // process the line.
 361                                 // System.out.println(line);
 362
 363                                 // Extract the one-liner construct first
 364                                 extractOneLineConstruct(file, lineReader.getLineNumber(), line);
 365
 366                                 for (int i = 0; i < line.length(); i++) {
 367                                         char ch = line.charAt(i);
 368                                         if (ch == '{') {
 369                                                 foundFirstCurl = true;
 370                                                 unmatchedCnt++;
 371                                         } else if (ch == '}') {
 372                                                 unmatchedCnt--;
 373                                         }
 374                                         // The current line is the end of the function
 375                                         if (foundFirstCurl && unmatchedCnt == 0) {
 376                                                 int endLineNumFunction = lineReader.getLineNumber();
 377                                                 return endLineNumFunction;
 378                                         }
 379                                 }
 380                         } while ((line = lineReader.readLine()) != null);
 381                 } catch (IOException e) {
 382                         e.printStackTrace();
 383                 }
 384                 // -1 means the curl symbols in the interface do not match
 385                 return -1;
 386         }
 387
 388         /**
 389          * <p>
 390          * A sub-routine to extract the define construct. When called, we have
 391          * already match the beginning of the construct, and we also need to find
 392          * the ending line number of the anntotation.
 393          * </p>
 394          *
 395          * @param file
 396          *            The file that we are processing
 397          * @param lineReader
 398          *            The LineNumberReader that we are using when processing the
 399          *            current file.
 400          * @param curLine
 401          *            The current line that we are processing. It should be the
 402          *            beginning line of the annotation construct.
 403          * @param beginLineNum
 404          *            The beginning line number of the interface construct
 405          *            annotation
 406          * @throws WrongAnnotationException
 407          * @throws IOException
 408          * @throws ParseException
 409          */
 410         private void extractDefineConstruct(File file, LineNumberReader lineReader,
 411                         String curLine, int beginLineNum) throws WrongAnnotationException,
 412                         IOException, ParseException {
 413                 ArrayList<String> annotations = extractTillConstructEnd(file,
 414                                 lineReader, curLine, beginLineNum);
 415                 int endLineNum = lineReader.getLineNumber();
 416                 DefineConstruct construct = new DefineConstruct(file, beginLineNum,
 417                                 endLineNum, annotations);
 418                 addDefineConstruct(construct);
 419         }
 420
 421         /**
 422          * <p>
 423          * A sub-routine to extract the interface construct. When called, we have
 424          * already match the beginning of the construct, and we also need to find
 425          * the ending line number of the closing brace of the corresponding
 426          * function.
 427          * </p>
 428          *
 429          * @param file
 430          *            The file that we are processing
 431          * @param lineReader
 432          *            The LineNumberReader that we are using when processing the
 433          *            current file.
 434          * @param curLine
 435          *            The current line that we are processing. It should be the
 436          *            beginning line of the annotation construct.
 437          * @param beginLineNum
 438          *            The beginning line number of the interface construct
 439          *            annotation
 440          * @throws WrongAnnotationException
 441          * @throws IOException
 442          * @throws ParseException
 443          */
 444         private void extractInterfaceConstruct(File file,
 445                         LineNumberReader lineReader, String curLine, int beginLineNum)
 446                         throws WrongAnnotationException, IOException, ParseException {
 447                 ArrayList<String> annotations = extractTillConstructEnd(file,
 448                                 lineReader, curLine, beginLineNum);
 449                 int endLineNum = lineReader.getLineNumber();
 450                 InterfaceConstruct construct = new InterfaceConstruct(file,
 451                                 beginLineNum, endLineNum, annotations);
 452                 addInterfaceConstruct(construct);
 453
 454                 // Process the corresponding interface function declaration header
 455                 String line = null;
 456                 int lineNum = -1;
 457                 String errMsg;
 458                 try {
 459                         line = lineReader.readLine();
 460                         lineNum = lineReader.getLineNumber();
 461                         construct.processFunctionDeclaration(line);
 462
 463                         // Record those user-defined struct
 464                         // RET
 465                         String returnType = construct.getFunctionHeader().returnType;
 466                         if (SpecUtils.isUserDefinedStruct(returnType))
 467                                 forwardClass.add(SpecUtils.getPlainType(returnType));
 468                         // Arguments
 469                         for (VariableDeclaration decl : construct.getFunctionHeader().args) {
 470                                 if (SpecUtils.isUserDefinedStruct(decl.type))
 471                                         forwardClass.add(SpecUtils.getPlainType(decl.type));
 472                         }
 473
 474                 } catch (IOException e) {
 475                         errMsg = "Spec error in file \""
 476                                         + file.getName()
 477                                         + "\", Line "
 478                                         + lineNum
 479                                         + " :\n\tThe function declaration should take only one line and have the correct syntax (follow the annotations immediately)\n";
 480                         System.out.println(errMsg);
 481                         throw e;
 482                 } catch (ParseException e) {
 483                         errMsg = "Spec error in file \""
 484                                         + file.getName()
 485                                         + "\", Line "
 486                                         + lineNum
 487                                         + " :\n\tThe function declaration should take only one line and have the correct syntax (follow the annotations immediately)\n";
 488                         System.out.println(errMsg);
 489                         throw e;
 490                 }
 491
 492                 // Now we find the end of the interface definition
 493                 int endLineNumFunction = findEndLineNumFunction(file, lineReader, line);
 494                 construct.setEndLineNumFunction(endLineNumFunction);
 495                 if (endLineNumFunction == -1) {
 496                         WrongAnnotationException
 497                                         .err(file, beginLineNum,
 498                                                         "The interface definition does NOT have matching curls '}'");
 499                 }
 500         }
 501
 502         /**
 503          * <p>
 504          * A sub-routine to extract the ordering point construct. When called, we
 505          * have already match the beginning of the construct.
 506          * </p>
 507          *
 508          * @param file
 509          *            The file that we are processing
 510          * @param beginLineNum
 511          *            The beginning line number of the interface construct
 512          *            annotation
 513          * @param curLine
 514          *            The current line that we are processing. It should be the
 515          *            beginning line of the annotation construct.
 516          * @param type
 517          *            The type of ordering point construct we are processing
 518          * @throws WrongAnnotationException
 519          */
 520         private void extractOPConstruct(File file, int beginLineNum,
 521                         String curLine, OPType type) throws WrongAnnotationException {
 522                 String condition = null;
 523                 String label = null;
 524
 525                 // "(\(\s?(\w+)\s?\))?\s:\s?(.+)\*/\s?$"
 526                 Pattern regexp = Pattern
 527                                 .compile("(\\(\\s*(\\w+)\\s*\\))?\\s*:\\s*(.+)\\*/\\s*$");
 528                 Matcher matcher = regexp.matcher(curLine);
 529                 if (matcher.find()) {
 530                         label = matcher.group(2);
 531                         condition = matcher.group(3);
 532                 } else {
 533                         WrongAnnotationException
 534                                         .err(file,
 535                                                         beginLineNum,
 536                                                         "Wrong syntax for the ordering point construct. You might need a colon before the condition.");
 537                 }
 538                 OPConstruct op = new OPConstruct(file, beginLineNum, type, label,
 539                                 condition, curLine);
 540                 addOPConstruct(op);
 541         }
 542
 543         /**
 544          * <p>
 545          * A sub-routine to extract the entry construct. When called, we have
 546          * already match the beginning of the construct.
 547          * </p>
 548          *
 549          * @param file
 550          *            The file that we are processing
 551          * @param beginLineNum
 552          *            The beginning line number of the interface construct
 553          *            annotation
 554          * @param curLine
 555          *            Current line being processed
 556          * @throws WrongAnnotationException
 557          */
 558         public void extractEntryConstruct(File file, int beginLineNum,
 559                         String curLine) throws WrongAnnotationException {
 560                 addEntryConstruct(file, new EntryConstruct(file, beginLineNum, curLine));
 561         }
 562
 563         /**
 564          * <p>
 565          * A sub-routine to extract those annotation constructs that take only one
 566          * line --- Entry, OPDefine, PotentialOP, OPCheck, OPClear and OPClearDefin.
 567          * </p>
 568          *
 569          * @param file
 570          *            The file that we are processing
 571          * @param beginLineNum
 572          *            The beginning line number of the interface construct
 573          *            annotation
 574          * @param curLine
 575          *            The current line that we are processing. It should be the
 576          *            beginning line of the annotation construct.
 577          * @throws WrongAnnotationException
 578          */
 579         private void extractOneLineConstruct(File file, int beginLineNum,
 580                         String curLine) throws WrongAnnotationException {
 581                 // "/\*\*\s*@(Entry|OPDefine|PotentialOP|OPCheck|OPClear|OPClearDefine)"
 582                 Pattern regexpBegin = Pattern.compile("/\\*\\*\\s*@(\\w+)");
 583                 Matcher matcher = regexpBegin.matcher(curLine);
 584                 matcher.reset(curLine);
 585                 if (matcher.find()) {
 586                         String name = matcher.group(1);
 587                         if (name.equals("Entry"))
 588                                 extractEntryConstruct(file, beginLineNum, curLine);
 589                         else if (name.equals("OPDefine") || name.equals("PotentialOP")
 590                                         || name.equals("OPCheck") || name.equals("OPClear")
 591                                         || name.equals("OPClearDefine")
 592                                         || name.equals("OPDefineUnattached")
 593                                         || name.equals("OPClearDefineUnattached"))
 594                                 extractOPConstruct(file, beginLineNum, curLine,
 595                                                 OPType.valueOf(name));
 596                 }
 597         }
 598
 599         /**
 600          * <p>
 601          * This function will process a given C/C++ file ( .h, .c or .cc). It will
 602          * extract all the headers included in that file, and all the annotation
 603          * constructs specified in that file. We then will store the information in
 604          * the corresponding containers.
 605          * </p>
 606          *
 607          * <p>
 608          * The basic idea is to read the file line by line, and then use regular
 609          * expression to match the specific annotations or the header files.
 610          * </p>
 611          *
 612          * @param file
 613          *            The file object of the corresponding file to be processed
 614          * @throws WrongAnnotationException
 615          * @throws ParseException
 616          */
 617         public void extractConstruct(File file) throws WrongAnnotationException,
 618                         ParseException {
 619                 BufferedReader br = null;
 620                 LineNumberReader lineReader = null;
 621                 try {
 622                         // Initial settings for processing the lines
 623                         br = new BufferedReader(new FileReader(file));
 624                         lineReader = new LineNumberReader(br);
 625                         // "/\*\*\s*@(DeclareState|Interface)"
 626                         Pattern regexpBegin = Pattern
 627                                         .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingCondition|Transition|PostCondition|Define)");
 628                         Matcher matcher = regexpBegin.matcher("");
 629
 630                         String line;
 631                         while ((line = lineReader.readLine()) != null) {
 632                                 // Start to process the line
 633
 634                                 // First try to process the line to see if it's a header file
 635                                 // include
 636                                 boolean succ = extractHeaders(line);
 637                                 if (succ) // It's a header line and we successfully extract it
 638                                         continue;
 639
 640                                 int beginLineNum = lineReader.getLineNumber();
 641                                 // Extract the one-liner construct first
 642                                 extractOneLineConstruct(file, beginLineNum, line);
 643
 644                                 // Now we process the line to see if it's an annotation (State
 645                                 // or Interface)
 646                                 matcher.reset(line); // reset the input
 647                                 if (matcher.find()) { // Found the beginning line
 648                                         // The matching annotation name
 649                                         String constructName = matcher.group(1);
 650
 651                                         // Process each annotation accordingly
 652                                         if (constructName.equals(SpecNaming.DeclareState)) {
 653                                                 extractGlobalConstruct(file, lineReader, line,
 654                                                                 beginLineNum);
 655                                         } else if (constructName.equals(SpecNaming.Interface)
 656                                                         || constructName.equals(SpecNaming.PreCondition)
 657                                                         || constructName.equals(SpecNaming.JustifyingCondition)
 658                                                         || constructName.equals(SpecNaming.Transition)
 659                                                         || constructName.equals(SpecNaming.PostCondition)) {
 660                                                 extractInterfaceConstruct(file, lineReader, line,
 661                                                                 beginLineNum);
 662                                         } else if (constructName.equals(SpecNaming.Define)) {
 663                                                 extractDefineConstruct(file, lineReader, line,
 664                                                                 beginLineNum);
 665                                         } else {
 666                                                 WrongAnnotationException.err(file, beginLineNum,
 667                                                                 constructName
 668                                                                                 + " is not a supported annotation.");
 669                                         }
 670
 671                                 }
 672                         }
 673                 } catch (FileNotFoundException e) {
 674                         e.printStackTrace();
 675                 } catch (IOException e) {
 676                         e.printStackTrace();
 677                 } finally {
 678                         try {
 679                                 lineReader.close();
 680                         } catch (IOException e) {
 681                                 e.printStackTrace();
 682                         }
 683                 }
 684         }
 685
 686         /**
 687          * <p>
 688          * Given a list of files, it scans each file and add found SpecConstrcut to
 689          * the _constructs list.
 690          * </p>
 691          *
 692          * @param files
 693          *            The list of files that needs to be processed. In general, this
 694          *            list only need to contain those that have specification
 695          *            annotations
 696          * @throws WrongAnnotationException
 697          * @throws ParseException
 698          */
 699         public void extract(File[] files) throws WrongAnnotationException,
 700                         ParseException {
 701                 for (int i = 0; i < files.length; i++)
 702                         extract(files[i]);
 703
 704                 // Check basic specification semantics
 705                 checkSemantics();
 706         }
 707
 708         public void extract(ArrayList<File> files) throws WrongAnnotationException,
 709                         ParseException {
 710                 for (int i = 0; i < files.size(); i++)
 711                         extract(files.get(i));
 712
 713                 // Check basic specification semantics
 714                 checkSemantics();
 715         }
 716
 717         /**
 718          * <p>
 719          * Extract the specification annotations and header files in the current
 720          * file. This function should generally be called by extractFiles.
 721          * </p>
 722          *
 723          * @param files
 724          *            The list of files that needs to be processed. In general, this
 725          *            list only need to contain those that have specification
 726          *            annotations
 727          * @throws WrongAnnotationException
 728          * @throws ParseException
 729          */
 730         public void extract(File file) throws WrongAnnotationException,
 731                         ParseException {
 732                 extractConstruct(file);
 733         }
 734 }