1 package edu.uci.eecs.specExtraction;
3 import java.io.BufferedReader;
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;
16 import edu.uci.eecs.codeGenerator.CodeGeneratorUtils;
17 import edu.uci.eecs.codeGenerator.Environment;
18 import edu.uci.eecs.utilParser.ParseException;
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
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;
40 public final HashSet<String> headerFiles;
42 // In the generated header file, we need to forward the user-defined
43 public final HashSet<String> forwardClass;
45 private GlobalConstruct globalConstruct;
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;
58 private void addDefineConstruct(DefineConstruct construct) {
59 ArrayList<DefineConstruct> list = defineListMap
62 list = new ArrayList<DefineConstruct>();
63 defineListMap.put(construct.file, list);
68 private void addInterfaceConstruct(InterfaceConstruct construct) {
69 ArrayList<InterfaceConstruct> list = interfaceListMap
72 list = new ArrayList<InterfaceConstruct>();
73 interfaceListMap.put(construct.file, list);
78 private void addOPConstruct(OPConstruct construct) {
79 ArrayList<OPConstruct> list = OPListMap.get(construct.file);
81 list = new ArrayList<OPConstruct>();
82 OPListMap.put(construct.file, list);
87 private void addEntryConstruct(File file, EntryConstruct construct)
88 throws WrongAnnotationException {
89 EntryConstruct old = entryMap.get(file);
91 entryMap.put(file, construct);
92 else { // Error processing
93 String errMsg = "Multiple @Entry annotations in the same file.\n\t Other @Entry at Line "
94 + old.beginLineNum + ".";
95 WrongAnnotationException.err(file, construct.beginLineNum, errMsg);
99 public GlobalConstruct getGlobalConstruct() {
100 return this.globalConstruct;
105 * A print out function for the purpose of debugging. Note that we better
106 * call this function after having called the checkSemantics() function to
107 * check annotation consistency.
110 public void printAnnotations() {
112 .println("/********** Print out of specification extraction **********/");
113 System.out.println("// Extracted header files");
114 for (String header : headerFiles)
115 System.out.println(header);
117 System.out.println("// Global State Construct");
118 if (globalConstruct != null)
119 System.out.println(globalConstruct);
121 for (File file : interfaceListMap.keySet()) {
122 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
123 System.out.println("// Interface in file: " + file.getName());
124 for (InterfaceConstruct construct : list) {
125 System.out.println(construct);
126 System.out.println("EndLineNumFunc: "
127 + construct.getEndLineNumFunction());
131 for (File file : OPListMap.keySet()) {
132 System.out.println("// Ordering points in file: " + file.getName());
133 ArrayList<OPConstruct> list = OPListMap.get(file);
134 for (OPConstruct construct : list)
135 System.out.println(construct);
138 for (File file : entryMap.keySet()) {
139 System.out.println("// Entry in file: " + file.getName());
140 System.out.println(entryMap.get(file));
146 * Perform basic semantics checking of the extracted specification.
150 * @throws WrongAnnotationException
152 public void checkSemantics() throws WrongAnnotationException {
153 String errMsg = null;
155 // Assert that we have defined and only defined one global state
157 if (globalConstruct == null) {
158 errMsg = "Spec error: There should be one global state annotation.\n";
159 throw new WrongAnnotationException(errMsg);
162 // Assert that the interface constructs have unique label name
163 HashMap<String, InterfaceConstruct> interfaceMap = new HashMap<String, InterfaceConstruct>();
164 for (File f : interfaceListMap.keySet()) {
165 ArrayList<InterfaceConstruct> list = interfaceListMap.get(f);
167 for (InterfaceConstruct construct : list) {
168 InterfaceConstruct existingConstruct = interfaceMap
169 .get(construct.getName());
170 if (existingConstruct != null) { // Error
171 errMsg = "Interface labels duplication with: \""
172 + construct.getName() + "\" in File \""
173 + existingConstruct.file.getName()
174 + "\", Line " + existingConstruct.beginLineNum
176 WrongAnnotationException.err(construct.file,
177 construct.beginLineNum, errMsg);
179 interfaceMap.put(construct.getName(), construct);
185 // Process ordering point labels
186 for (File file : OPListMap.keySet()) {
187 ArrayList<OPConstruct> list = OPListMap.get(file);
188 for (OPConstruct construct : list) {
189 if (construct.type == OPType.OPCheck
190 || construct.type == OPType.PotentialOP) {
191 String label = construct.label;
192 OPLabelSet.add(label);
201 * This function applies on a String (a plain line of text) to check whether
202 * the current line is a C/C++ header include statement. If it is, it
203 * extracts the header file name and store it, and returns true; otherwise,
208 * The line of text to be processed
209 * @return Returns true if the current line is a C/C++ header include
212 public boolean extractHeaders(String line) {
213 // "^( |\t)*#include( |\t)+("|<)([a-zA-Z_0-9\-\.])+("|>)"
214 Pattern regexp = Pattern
215 .compile("^( |\\t)*(#include)( |\\t)+(\"|<)([a-zA-Z_0-9\\-\\.]+)(\"|>)");
216 Matcher matcher = regexp.matcher(line);
219 if (matcher.find()) {
220 String header = null;
221 String braceSymbol = matcher.group(4);
222 if (braceSymbol.equals("<"))
223 header = "<" + matcher.group(5) + ">";
225 header = "\"" + matcher.group(5) + "\"";
226 if (!SpecNaming.isPreIncludedHeader(header)) {
227 headerFiles.add(header);
236 * A sub-routine to extract the construct from beginning till end. When
237 * called, we have already match the beginning of the construct. We will
238 * call this sub-routine when we extract the interface construct and the
239 * global state construct.
243 * The side effect of this function is that the lineReader has just read the
244 * end of the construct, meaning that the caller can get the end line number
245 * by calling lineReader.getLineNumber().
249 * The file that we are processing
251 * The LineNumberReader that we are using when processing the
254 * The file that we are processing
256 * The current line that we are processing. It should be the
257 * beginning line of the annotation construct.
258 * @param beginLineNum
259 * The beginning line number of the interface construct
261 * @return Returns the annotation string list of the current construct
262 * @throws WrongAnnotationException
264 private ArrayList<String> extractTillConstructEnd(File file,
265 LineNumberReader lineReader, String curLine, int beginLineNum)
266 throws WrongAnnotationException {
267 ArrayList<String> annotations = new ArrayList<String>();
268 annotations.add(curLine);
269 // System.out.println(curLine);
270 // Initial settings for matching lines
272 Pattern regexpEnd = Pattern.compile("\\*/\\s*$");
273 Matcher matcher = regexpEnd.matcher(curLine);
274 if (matcher.find()) {
275 // The beginning line is also the end line
276 // In this case, we have already add the curLine
281 while ((line = lineReader.readLine()) != null) {
283 // System.out.println(line);
285 matcher.reset(line); // reset the input
286 annotations.add(line);
290 WrongAnnotationException
293 "The interface annotation should have the matching closing symbol closing \"*/\"");
294 } catch (IOException e) {
303 * A sub-routine to extract the global construct. When called, we have
304 * already match the beginning of the construct.
308 * The file that we are processing
310 * The LineNumberReader that we are using when processing the
313 * The current line that we are processing. It should be the
314 * beginning line of the annotation construct.
315 * @param beginLineNum
316 * The beginning line number of the interface construct
318 * @throws WrongAnnotationException
320 private void extractGlobalConstruct(File file, LineNumberReader lineReader,
321 String curLine, int beginLineNum) throws WrongAnnotationException {
322 ArrayList<String> annotations = extractTillConstructEnd(file,
323 lineReader, curLine, beginLineNum);
324 GlobalConstruct construct = new GlobalConstruct(file, beginLineNum,
326 if (globalConstruct != null) { // Check if we have seen a global state
328 File otherDefinitionFile = globalConstruct.file;
329 int otherDefinitionLine = globalConstruct.beginLineNum;
330 String errMsg = "Multiple definition of global state.\n"
331 + "\tAnother definition is in File \""
332 + otherDefinitionFile.getName() + "\" (Line "
333 + otherDefinitionLine + ").";
334 WrongAnnotationException.err(file, beginLineNum, errMsg);
336 globalConstruct = construct;
341 * The current file we are processing
343 * Call this function when the lineReader will read the beginning
344 * of the definition right away
345 * @param startingLine
346 * The line that we should start processing
347 * @return The line number of the ending line of the interfae definition. If
348 * returning -1, it means the curl symbols in the interface do not
350 * @throws WrongAnnotationException
352 private int findEndLineNumFunction(File file, LineNumberReader lineReader,
353 String startingLine) throws WrongAnnotationException {
354 String line = startingLine;
355 // FIXME: We assume that in the string of the code, there does not exist
356 // the symbol '{' & '{'
358 boolean foundFirstCurl = false;
359 int unmatchedCnt = 0;
362 // System.out.println(line);
364 // Extract the one-liner construct first
365 extractOneLineConstruct(file, lineReader.getLineNumber(), line);
367 for (int i = 0; i < line.length(); i++) {
368 char ch = line.charAt(i);
370 foundFirstCurl = true;
372 } else if (ch == '}') {
375 // The current line is the end of the function
376 if (foundFirstCurl && unmatchedCnt == 0) {
377 int endLineNumFunction = lineReader.getLineNumber();
378 return endLineNumFunction;
381 } while ((line = lineReader.readLine()) != null);
382 } catch (IOException e) {
385 // -1 means the curl symbols in the interface do not match
391 * A sub-routine to extract the define construct. When called, we have
392 * already match the beginning of the construct, and we also need to find
393 * the ending line number of the anntotation.
397 * The file that we are processing
399 * The LineNumberReader that we are using when processing the
402 * The current line that we are processing. It should be the
403 * beginning line of the annotation construct.
404 * @param beginLineNum
405 * The beginning line number of the interface construct
407 * @throws WrongAnnotationException
408 * @throws IOException
409 * @throws ParseException
411 private void extractDefineConstruct(File file,
412 LineNumberReader lineReader, String curLine, int beginLineNum)
413 throws WrongAnnotationException, IOException, ParseException {
414 ArrayList<String> annotations = extractTillConstructEnd(file,
415 lineReader, curLine, beginLineNum);
416 int endLineNum = lineReader.getLineNumber();
417 DefineConstruct construct = new DefineConstruct(file,
418 beginLineNum, endLineNum, annotations);
419 addDefineConstruct(construct);
425 * A sub-routine to extract the interface construct. When called, we have
426 * already match the beginning of the construct, and we also need to find
427 * the ending line number of the closing brace of the corresponding
432 * The file that we are processing
434 * The LineNumberReader that we are using when processing the
437 * The current line that we are processing. It should be the
438 * beginning line of the annotation construct.
439 * @param beginLineNum
440 * The beginning line number of the interface construct
442 * @throws WrongAnnotationException
443 * @throws IOException
444 * @throws ParseException
446 private void extractInterfaceConstruct(File file,
447 LineNumberReader lineReader, String curLine, int beginLineNum)
448 throws WrongAnnotationException, IOException, ParseException {
449 ArrayList<String> annotations = extractTillConstructEnd(file,
450 lineReader, curLine, beginLineNum);
451 int endLineNum = lineReader.getLineNumber();
452 InterfaceConstruct construct = new InterfaceConstruct(file,
453 beginLineNum, endLineNum, annotations);
454 addInterfaceConstruct(construct);
456 // Process the corresponding interface function declaration header
461 line = lineReader.readLine();
462 lineNum = lineReader.getLineNumber();
463 construct.processFunctionDeclaration(line);
465 // Record those user-defined struct
467 String returnType = construct.getFunctionHeader().returnType;
468 if (SpecUtils.isUserDefinedStruct(returnType))
469 forwardClass.add(SpecUtils.getPlainType(returnType));
471 for (VariableDeclaration decl : construct.getFunctionHeader().args) {
472 if (SpecUtils.isUserDefinedStruct(decl.type))
473 forwardClass.add(SpecUtils.getPlainType(decl.type));
476 } catch (IOException e) {
477 errMsg = "Spec error in file \""
481 + " :\n\tThe function declaration should take only one line and have the correct syntax (follow the annotations immediately)\n";
482 System.out.println(errMsg);
484 } catch (ParseException e) {
485 errMsg = "Spec error in file \""
489 + " :\n\tThe function declaration should take only one line and have the correct syntax (follow the annotations immediately)\n";
490 System.out.println(errMsg);
494 // Now we find the end of the interface definition
495 int endLineNumFunction = findEndLineNumFunction(file, lineReader, line);
496 construct.setEndLineNumFunction(endLineNumFunction);
497 if (endLineNumFunction == -1) {
498 WrongAnnotationException
499 .err(file, beginLineNum,
500 "The interface definition does NOT have matching curls '}'");
506 * A sub-routine to extract the ordering point construct. When called, we
507 * have already match the beginning of the construct.
511 * The file that we are processing
512 * @param beginLineNum
513 * The beginning line number of the interface construct
516 * The current line that we are processing. It should be the
517 * beginning line of the annotation construct.
519 * The type of ordering point construct we are processing
520 * @throws WrongAnnotationException
522 private void extractOPConstruct(File file, int beginLineNum,
523 String curLine, OPType type) throws WrongAnnotationException {
524 String condition = null;
527 // "(\(\s?(\w+)\s?\))?\s:\s?(.+)\*/\s?$"
528 Pattern regexp = Pattern
529 .compile("(\\(\\s*(\\w+)\\s*\\))?\\s*:\\s*(.+)\\*/\\s*$");
530 Matcher matcher = regexp.matcher(curLine);
531 if (matcher.find()) {
532 label = matcher.group(2);
533 condition = matcher.group(3);
535 WrongAnnotationException
538 "Wrong syntax for the ordering point construct. You might need a colon before the condition.");
540 OPConstruct op = new OPConstruct(file, beginLineNum, type, label,
547 * A sub-routine to extract the entry construct. When called, we have
548 * already match the beginning of the construct.
552 * The file that we are processing
553 * @param beginLineNum
554 * The beginning line number of the interface construct
557 * Current line being processed
558 * @throws WrongAnnotationException
560 public void extractEntryConstruct(File file, int beginLineNum,
561 String curLine) throws WrongAnnotationException {
562 addEntryConstruct(file, new EntryConstruct(file, beginLineNum, curLine));
567 * A sub-routine to extract those annotation constructs that take only one
568 * line --- Entry, OPDefine, PotentialOP, OPCheck, OPClear and OPClearDefin.
572 * The file that we are processing
573 * @param beginLineNum
574 * The beginning line number of the interface construct
577 * The current line that we are processing. It should be the
578 * beginning line of the annotation construct.
579 * @throws WrongAnnotationException
581 private void extractOneLineConstruct(File file, int beginLineNum,
582 String curLine) throws WrongAnnotationException {
583 // "/\*\*\s*@(Entry|OPDefine|PotentialOP|OPCheck|OPClear|OPClearDefine)"
584 Pattern regexpBegin = Pattern.compile("/\\*\\*\\s*@(\\w+)");
585 Matcher matcher = regexpBegin.matcher(curLine);
586 matcher.reset(curLine);
587 if (matcher.find()) {
588 String name = matcher.group(1);
589 if (name.equals("Entry"))
590 extractEntryConstruct(file, beginLineNum, curLine);
591 else if (name.equals("OPDefine") || name.equals("PotentialOP")
592 || name.equals("OPCheck") || name.equals("OPClear")
593 || name.equals("OPClearDefine"))
594 extractOPConstruct(file, beginLineNum, curLine,
595 OPType.valueOf(name));
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.
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.
613 * The file object of the corresponding file to be processed
614 * @throws WrongAnnotationException
615 * @throws ParseException
617 public void extractConstruct(File file) throws WrongAnnotationException,
619 BufferedReader br = null;
620 LineNumberReader lineReader = null;
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|Transition|PostCondition|Define)");
628 Matcher matcher = regexpBegin.matcher("");
631 while ((line = lineReader.readLine()) != null) {
632 // Start to process the line
634 // First try to process the line to see if it's a header file
636 boolean succ = extractHeaders(line);
637 if (succ) // It's a header line and we successfully extract it
640 int beginLineNum = lineReader.getLineNumber();
641 // Extract the one-liner construct first
642 extractOneLineConstruct(file, beginLineNum, line);
644 // Now we process the line to see if it's an annotation (State
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);
651 // Process each annotation accordingly
652 if (constructName.equals(SpecNaming.DeclareState)) {
653 extractGlobalConstruct(file, lineReader, line,
655 } else if (constructName.equals(SpecNaming.Interface)
656 || constructName.equals(SpecNaming.PreCondition)
657 || constructName.equals(SpecNaming.Transition)
658 || constructName.equals(SpecNaming.PostCondition)) {
659 extractInterfaceConstruct(file, lineReader, line,
661 } else if (constructName.equals(SpecNaming.Define)) {
662 extractDefineConstruct(file, lineReader, line,
665 WrongAnnotationException.err(file, beginLineNum,
667 + " is not a supported annotation.");
672 } catch (FileNotFoundException e) {
674 } catch (IOException e) {
679 } catch (IOException e) {
687 * Given a list of files, it scans each file and add found SpecConstrcut to
688 * the _constructs list.
692 * The list of files that needs to be processed. In general, this
693 * list only need to contain those that have specification
695 * @throws WrongAnnotationException
696 * @throws ParseException
698 public void extract(File[] files) throws WrongAnnotationException,
700 for (int i = 0; i < files.length; i++)
703 // Check basic specification semantics
707 public void extract(ArrayList<File> files) throws WrongAnnotationException,
709 for (int i = 0; i < files.size(); i++)
710 extract(files.get(i));
712 // Check basic specification semantics
718 * Extract the specification annotations and header files in the current
719 * file. This function should generally be called by extractFiles.
723 * The list of files that needs to be processed. In general, this
724 * list only need to contain those that have specification
726 * @throws WrongAnnotationException
727 * @throws ParseException
729 public void extract(File file) throws WrongAnnotationException,
731 extractConstruct(file);