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("\\*/( |\\t)*$");
273 Matcher matcher = regexpEnd.matcher(curLine);
274 if (matcher.find()) { // The beginning line is also the end line
275 annotations.add(curLine);
280 while ((line = lineReader.readLine()) != null) {
282 // System.out.println(line);
284 matcher.reset(line); // reset the input
285 annotations.add(line);
289 WrongAnnotationException
292 "The interface annotation should have the matching closing symbol closing \"*/\"");
293 } catch (IOException e) {
302 * A sub-routine to extract the global construct. When called, we have
303 * already match the beginning of the construct.
307 * The file that we are processing
309 * The LineNumberReader that we are using when processing the
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
317 * @throws WrongAnnotationException
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,
325 if (globalConstruct != null) { // Check if we have seen a global state
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);
335 globalConstruct = construct;
340 * The current file we are processing
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
349 * @throws WrongAnnotationException
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 '{' & '{'
357 boolean foundFirstCurl = false;
358 int unmatchedCnt = 0;
361 // System.out.println(line);
363 // Extract the one-liner construct first
364 extractOneLineConstruct(file, lineReader.getLineNumber(), line);
366 for (int i = 0; i < line.length(); i++) {
367 char ch = line.charAt(i);
369 foundFirstCurl = true;
371 } else if (ch == '}') {
374 // The current line is the end of the function
375 if (foundFirstCurl && unmatchedCnt == 0) {
376 int endLineNumFunction = lineReader.getLineNumber();
377 return endLineNumFunction;
380 } while ((line = lineReader.readLine()) != null);
381 } catch (IOException e) {
384 // -1 means the curl symbols in the interface do not match
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.
396 * The file that we are processing
398 * The LineNumberReader that we are using when processing the
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
406 * @throws WrongAnnotationException
407 * @throws IOException
408 * @throws ParseException
410 private void extractDefineConstruct(File file,
411 LineNumberReader lineReader, String curLine, int beginLineNum)
412 throws WrongAnnotationException, IOException, ParseException {
413 ArrayList<String> annotations = extractTillConstructEnd(file,
414 lineReader, curLine, beginLineNum);
415 int endLineNum = lineReader.getLineNumber();
416 DefineConstruct construct = new DefineConstruct(file,
417 beginLineNum, endLineNum, annotations);
418 addDefineConstruct(construct);
424 * A sub-routine to extract the interface construct. When called, we have
425 * already match the beginning of the construct, and we also need to find
426 * the ending line number of the closing brace of the corresponding
431 * The file that we are processing
433 * The LineNumberReader that we are using when processing the
436 * The current line that we are processing. It should be the
437 * beginning line of the annotation construct.
438 * @param beginLineNum
439 * The beginning line number of the interface construct
441 * @throws WrongAnnotationException
442 * @throws IOException
443 * @throws ParseException
445 private void extractInterfaceConstruct(File file,
446 LineNumberReader lineReader, String curLine, int beginLineNum)
447 throws WrongAnnotationException, IOException, ParseException {
448 ArrayList<String> annotations = extractTillConstructEnd(file,
449 lineReader, curLine, beginLineNum);
450 int endLineNum = lineReader.getLineNumber();
451 InterfaceConstruct construct = new InterfaceConstruct(file,
452 beginLineNum, endLineNum, annotations);
453 addInterfaceConstruct(construct);
455 // Process the corresponding interface function declaration header
460 line = lineReader.readLine();
461 lineNum = lineReader.getLineNumber();
462 construct.processFunctionDeclaration(line);
464 // Record those user-defined struct
466 String returnType = construct.getFunctionHeader().returnType;
467 if (SpecUtils.isUserDefinedStruct(returnType))
468 forwardClass.add(SpecUtils.getPlainType(returnType));
470 for (VariableDeclaration decl : construct.getFunctionHeader().args) {
471 if (SpecUtils.isUserDefinedStruct(decl.type))
472 forwardClass.add(SpecUtils.getPlainType(decl.type));
475 } catch (IOException e) {
476 errMsg = "Spec error in file \""
480 + " :\n\tThe function declaration should take only one line and have the correct syntax (follow the annotations immediately)\n";
481 System.out.println(errMsg);
483 } catch (ParseException e) {
484 errMsg = "Spec error in file \""
488 + " :\n\tThe function declaration should take only one line and have the correct syntax (follow the annotations immediately)\n";
489 System.out.println(errMsg);
493 // Now we find the end of the interface definition
494 int endLineNumFunction = findEndLineNumFunction(file, lineReader, line);
495 construct.setEndLineNumFunction(endLineNumFunction);
496 if (endLineNumFunction == -1) {
497 WrongAnnotationException
498 .err(file, beginLineNum,
499 "The interface definition does NOT have matching curls '}'");
505 * A sub-routine to extract the ordering point construct. When called, we
506 * have already match the beginning of the construct.
510 * The file that we are processing
511 * @param beginLineNum
512 * The beginning line number of the interface construct
515 * The current line that we are processing. It should be the
516 * beginning line of the annotation construct.
518 * The type of ordering point construct we are processing
519 * @throws WrongAnnotationException
521 private void extractOPConstruct(File file, int beginLineNum,
522 String curLine, OPType type) throws WrongAnnotationException {
523 String condition = null;
526 // "(\(\s?(\w+)\s?\))?\s:\s?(.+)\*/\s?$"
527 Pattern regexp = Pattern
528 .compile("(\\(\\s*(\\w+)\\s*\\))?\\s*:\\s*(.+)\\*/\\s*$");
529 Matcher matcher = regexp.matcher(curLine);
530 if (matcher.find()) {
531 label = matcher.group(2);
532 condition = matcher.group(3);
534 WrongAnnotationException
537 "Wrong syntax for the ordering point construct. You might need a colon before the condition.");
539 OPConstruct op = new OPConstruct(file, beginLineNum, type, label,
546 * A sub-routine to extract the entry construct. When called, we have
547 * already match the beginning of the construct.
551 * The file that we are processing
552 * @param beginLineNum
553 * The beginning line number of the interface construct
556 * Current line being processed
557 * @throws WrongAnnotationException
559 public void extractEntryConstruct(File file, int beginLineNum,
560 String curLine) throws WrongAnnotationException {
561 addEntryConstruct(file, new EntryConstruct(file, beginLineNum, curLine));
566 * A sub-routine to extract those annotation constructs that take only one
567 * line --- Entry, OPDefine, PotentialOP, OPCheck, OPClear and OPClearDefin.
571 * The file that we are processing
572 * @param beginLineNum
573 * The beginning line number of the interface construct
576 * The current line that we are processing. It should be the
577 * beginning line of the annotation construct.
578 * @throws WrongAnnotationException
580 private void extractOneLineConstruct(File file, int beginLineNum,
581 String curLine) throws WrongAnnotationException {
582 // "/\*\*\s*@(Entry|OPDefine|PotentialOP|OPCheck|OPClear|OPClearDefine)"
583 Pattern regexpBegin = Pattern.compile("/\\*\\*\\s*@(\\w+)");
584 Matcher matcher = regexpBegin.matcher(curLine);
585 matcher.reset(curLine);
586 if (matcher.find()) {
587 String name = matcher.group(1);
588 if (name.equals("Entry"))
589 extractEntryConstruct(file, beginLineNum, curLine);
590 else if (name.equals("OPDefine") || name.equals("PotentialOP")
591 || name.equals("OPCheck") || name.equals("OPClear")
592 || name.equals("OPClearDefine"))
593 extractOPConstruct(file, beginLineNum, curLine,
594 OPType.valueOf(name));
600 * This function will process a given C/C++ file ( .h, .c or .cc). It will
601 * extract all the headers included in that file, and all the annotation
602 * constructs specified in that file. We then will store the information in
603 * the corresponding containers.
607 * The basic idea is to read the file line by line, and then use regular
608 * expression to match the specific annotations or the header files.
612 * The file object of the corresponding file to be processed
613 * @throws WrongAnnotationException
614 * @throws ParseException
616 public void extractConstruct(File file) throws WrongAnnotationException,
618 BufferedReader br = null;
619 LineNumberReader lineReader = null;
621 // Initial settings for processing the lines
622 br = new BufferedReader(new FileReader(file));
623 lineReader = new LineNumberReader(br);
624 // "/\*\*\s*@(DeclareState|Interface)"
625 Pattern regexpBegin = Pattern
626 .compile("/\\*\\*\\s*@(DeclareState|Interface|Define)");
627 Matcher matcher = regexpBegin.matcher("");
630 while ((line = lineReader.readLine()) != null) {
631 // Start to process the line
633 // First try to process the line to see if it's a header file
635 boolean succ = extractHeaders(line);
636 if (succ) // It's a header line and we successfully extract it
639 int beginLineNum = lineReader.getLineNumber();
640 // Extract the one-liner construct first
641 extractOneLineConstruct(file, beginLineNum, line);
643 // Now we process the line to see if it's an annotation (State
645 matcher.reset(line); // reset the input
646 if (matcher.find()) { // Found the beginning line
647 // The matching annotation name
648 String constructName = matcher.group(1);
650 // Process each annotation accordingly
651 if (constructName.equals(SpecNaming.DeclareState)) {
652 extractGlobalConstruct(file, lineReader, line,
654 } else if (constructName.equals(SpecNaming.Interface)) {
655 extractInterfaceConstruct(file, lineReader, line,
657 } else if (constructName.equals(SpecNaming.Define)) {
658 extractDefineConstruct(file, lineReader, line,
661 WrongAnnotationException.err(file, beginLineNum,
663 + " is not a supported annotation.");
668 } catch (FileNotFoundException e) {
670 } catch (IOException e) {
675 } catch (IOException e) {
683 * Given a list of files, it scans each file and add found SpecConstrcut to
684 * the _constructs list.
688 * The list of files that needs to be processed. In general, this
689 * list only need to contain those that have specification
691 * @throws WrongAnnotationException
692 * @throws ParseException
694 public void extract(File[] files) throws WrongAnnotationException,
696 for (int i = 0; i < files.length; i++)
699 // Check basic specification semantics
703 public void extract(ArrayList<File> files) throws WrongAnnotationException,
705 for (int i = 0; i < files.size(); i++)
706 extract(files.get(i));
708 // Check basic specification semantics
714 * Extract the specification annotations and header files in the current
715 * file. This function should generally be called by extractFiles.
719 * The list of files that needs to be processed. In general, this
720 * list only need to contain those that have specification
722 * @throws WrongAnnotationException
723 * @throws ParseException
725 public void extract(File file) throws WrongAnnotationException,
727 extractConstruct(file);