1 package edu.uci.eecs.specExtraction;
4 import java.util.ArrayList;
5 import java.util.HashMap;
6 import java.util.regex.Matcher;
7 import java.util.regex.Pattern;
9 import edu.uci.eecs.specExtraction.SpecUtils.IntObj;
10 import edu.uci.eecs.specExtraction.SpecUtils.Primitive;
11 import edu.uci.eecs.utilParser.ParseException;
12 import edu.uci.eecs.utilParser.UtilParser;
16 * This class is a subclass of Construct. It represents a complete interface
23 public class InterfaceConstruct extends Construct {
25 public final Code transition;
26 public final Code preCondition;
27 public final Code sideEffect;
28 public final Code postCondition;
29 public final Code print;
31 // The ending line number of the specification annotation construct
32 public final int endLineNum;
34 // The ending line number of the function definition
35 private int endLineNumFunction;
36 // The function header of the corresponding interface --- The list of
37 // variable declarations that represent the RETURN value and
38 // arguments of the interface
39 private FunctionHeader funcHeader;
41 public final boolean autoGenPrint;
43 public InterfaceConstruct(File file, int beginLineNum, int endLineNum,
44 ArrayList<String> annotations) throws WrongAnnotationException {
45 super(file, beginLineNum);
46 this.endLineNum = endLineNum;
48 this.transition = new Code();
49 this.preCondition = new Code();
50 this.sideEffect = new Code();
51 this.postCondition = new Code();
52 this.print = new Code();
54 processAnnotations(annotations);
56 autoGenPrint = print.isEmpty();
59 public FunctionHeader getFunctionHeader() {
60 return this.funcHeader;
63 public boolean equals(Object other) {
64 if (!(other instanceof InterfaceConstruct)) {
67 InterfaceConstruct o = (InterfaceConstruct) other;
68 if (o.name.equals(this.name))
74 public String getName() {
80 * This function will automatically generate the printing statements for
81 * supported types if the user has not defined the "@Print" primitive
84 * @return The auto-generated state printing statements
85 * @throws WrongAnnotationException
87 private Code generateAutoPrintFunction() {
88 Code code = new Code();
90 code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType,
93 for (VariableDeclaration decl : funcHeader.args) {
94 String type = decl.type;
95 String name = decl.name;
96 code.addLines(SpecUtils.generatePrintStatement(type, name));
103 * Assert that the interface primitive is valid; if not, throws an exception
109 * The primitive string that we have extracted earlier
110 * @throws WrongAnnotationException
112 private void assertValidPrimitive(File file, Primitive primitive)
113 throws WrongAnnotationException {
114 int lineNum = primitive.beginLineNum;
115 String name = primitive.name;
116 if (!name.equals(SpecNaming.Interface)
117 && !name.equals(SpecNaming.Transition)
118 && !name.equals(SpecNaming.PreCondition)
119 && !name.equals(SpecNaming.SideEffect)
120 && !name.equals(SpecNaming.PostCondition)
121 && !name.equals(SpecNaming.PrintValue)) {
122 WrongAnnotationException.err(file, lineNum, name
123 + " is NOT a valid CDSSpec interface primitive.");
129 * Assert that the "@Interface" primitive has correct syntax; if not, throws
130 * an exception. If so, it basically checks whether content of the primitive
131 * is a valid word and then return interface label name.
137 * Current line number
139 * The primitive string that we have extracted earlier
140 * @throws WrongAnnotationException
142 private String extractInterfaceName(File file, Primitive primitive)
143 throws WrongAnnotationException {
144 int lineNum = primitive.beginLineNum;
145 String name = primitive.name;
146 if (primitive.contents.size() != 1)
147 WrongAnnotationException.err(file, lineNum,
148 "The @Interface primitive: " + name + " has wrong syntax.");
149 String line = primitive.contents.get(0);
150 SpecUtils.matcherWord.reset(line);
151 if (!SpecUtils.matcherWord.find())
152 WrongAnnotationException.err(file, lineNum, name
153 + " is NOT a valid CDSSpec @Interface primitive.");
157 private void processAnnotations(ArrayList<String> annotations)
158 throws WrongAnnotationException {
159 IntObj curIdx = new IntObj(0);
160 Primitive primitive = null;
162 while ((primitive = SpecUtils.extractPrimitive(file, beginLineNum,
163 annotations, curIdx)) != null) {
164 String name = primitive.name;
165 assertValidPrimitive(file, primitive);
166 if (primitive.contents.size() == 0)
168 if (name.equals(SpecNaming.Interface)) {
169 this.name = extractInterfaceName(file, primitive);
170 } else if (name.equals(SpecNaming.Transition)) {
171 this.transition.addLines(primitive.contents);
172 } else if (name.equals(SpecNaming.PreCondition)) {
173 this.preCondition.addLines(primitive.contents);
174 } else if (name.equals(SpecNaming.SideEffect)) {
175 this.sideEffect.addLines(primitive.contents);
176 } else if (name.equals(SpecNaming.PostCondition)) {
177 this.postCondition.addLines(primitive.contents);
178 } else if (name.equals(SpecNaming.PrintValue)) {
179 this.print.addLines(primitive.contents);
186 * This function is called to extract all the declarations that should go to
187 * the corresponding value struct --- a C++ struct to be generated for this
188 * interface that contains the information of the return value and the
193 * The line that represents the interface declaration line
194 * @throws ParseException
196 public void processFunctionDeclaration(String line) throws ParseException {
197 // FIXME: Currently we only allow the declaration to be one-liner
198 funcHeader = UtilParser.parseFuncHeader(line);
199 // Record the original declaration line
200 funcHeader.setHeaderLine(line);
202 // Once we have the compelte function declaration, we can auto-gen the
203 // print-out statements if it's not defined
205 print.addLines(generateAutoPrintFunction());
209 public String toString() {
210 StringBuilder sb = new StringBuilder();
211 sb.append(super.toString() + "\n");
212 sb.append("@Interface: " + name + "\n");
213 if (!transition.isEmpty())
214 sb.append("@Transition:\n" + transition);
215 if (!preCondition.isEmpty())
216 sb.append("@PreCondition:\n" + preCondition);
217 if (!sideEffect.isEmpty())
218 sb.append("@SideEffect:\n" + sideEffect);
219 if (!postCondition.isEmpty())
220 sb.append("@PostCondition:\n" + postCondition);
221 if (!print.isEmpty())
222 sb.append("@Print:\n" + print + "\n");
223 sb.append(funcHeader);
225 return sb.toString();
228 public int getEndLineNumFunction() {
229 return endLineNumFunction;
232 public void setEndLineNumFunction(int endLineNumFunction) {
233 this.endLineNumFunction = endLineNumFunction;