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 {
24 // The interface label of the current interface; If not specified, we use
25 // the actual interface name to represent this interface
27 // Each interface interface will have an auto-generated struct that
28 // represents the return value and the arguments of that interface method
29 // call. We will mangle the interface label name to get this name in case we
30 // have other name conflict
31 private String structName;
32 public final Code preCondition;
33 public final Code justifyingPrecondition;
34 public final Code transition;
35 public final Code justifyingPostcondition;
36 public final Code postCondition;
37 public final Code print;
39 // The ending line number of the specification annotation construct
40 public final int endLineNum;
42 // The ending line number of the function definition
43 private int endLineNumFunction;
44 // The function header of the corresponding interface --- The list of
45 // variable declarations that represent the RETURN value and
46 // arguments of the interface
47 private FunctionHeader funcHeader;
49 public final boolean autoGenPrint;
51 public InterfaceConstruct(File file, int beginLineNum, int endLineNum,
52 ArrayList<String> annotations) throws WrongAnnotationException {
53 super(file, beginLineNum);
54 this.endLineNum = endLineNum;
56 this.structName = null;
57 this.preCondition = new Code();
58 this.justifyingPrecondition = new Code();
59 this.transition = new Code();
60 this.justifyingPostcondition = new Code();
61 this.postCondition = new Code();
62 this.print = new Code();
64 processAnnotations(annotations);
66 autoGenPrint = print.isEmpty();
69 public FunctionHeader getFunctionHeader() {
70 return this.funcHeader;
73 public boolean equals(Object other) {
74 if (!(other instanceof InterfaceConstruct)) {
77 InterfaceConstruct o = (InterfaceConstruct) other;
78 if (o.name.equals(this.name))
84 public String getName() {
90 * This function will automatically generate the printing statements for
91 * supported types if the user has not defined the "@Print" primitive
94 * @return The auto-generated state printing statements
95 * @throws WrongAnnotationException
97 private Code generateAutoPrintFunction() {
98 Code code = new Code();
100 code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType,
103 for (VariableDeclaration decl : funcHeader.args) {
104 String type = decl.type;
105 String name = decl.name;
106 code.addLines(SpecUtils.generatePrintStatement(type, name));
113 * Assert that the interface primitive is valid; if not, throws an exception
119 * The primitive string that we have extracted earlier
120 * @throws WrongAnnotationException
122 private void assertValidPrimitive(File file, Primitive primitive)
123 throws WrongAnnotationException {
124 int lineNum = primitive.beginLineNum;
125 String name = primitive.name;
126 if (!name.equals(SpecNaming.Interface)
127 && !name.equals(SpecNaming.Transition)
128 && !name.equals(SpecNaming.PreCondition)
129 && !name.equals(SpecNaming.JustifyingPrecondition)
130 && !name.equals(SpecNaming.SideEffect)
131 && !name.equals(SpecNaming.JustifyingPostcondition)
132 && !name.equals(SpecNaming.PostCondition)
133 && !name.equals(SpecNaming.PrintValue)) {
134 WrongAnnotationException.err(file, lineNum, name
135 + " is NOT a valid CDSSpec interface primitive.");
141 * Assert that the "@Interface" primitive has correct syntax; if not, throws
142 * an exception. If so, it basically checks whether content of the primitive
143 * is a valid word and then return interface label name.
149 * Current line number
151 * The primitive string that we have extracted earlier
152 * @throws WrongAnnotationException
154 private String extractInterfaceName(File file, Primitive primitive)
155 throws WrongAnnotationException {
156 int lineNum = primitive.beginLineNum;
157 String name = primitive.name;
158 if (primitive.contents.size() != 1)
159 WrongAnnotationException.err(file, lineNum,
160 "The @Interface primitive: " + name + " has wrong syntax.");
161 String line = primitive.contents.get(0);
162 SpecUtils.matcherWord.reset(line);
163 if (!SpecUtils.matcherWord.find())
164 WrongAnnotationException.err(file, lineNum, name
165 + " is NOT a valid CDSSpec @Interface primitive.");
169 private void processAnnotations(ArrayList<String> annotations)
170 throws WrongAnnotationException {
171 IntObj curIdx = new IntObj(0);
172 Primitive primitive = null;
174 while ((primitive = SpecUtils.extractPrimitive(file, beginLineNum,
175 annotations, curIdx)) != null) {
176 String name = primitive.name;
177 assertValidPrimitive(file, primitive);
178 if (primitive.contents.size() == 0)
180 if (name.equals(SpecNaming.Interface)) {
181 String interName = extractInterfaceName(file, primitive);
183 } else if (name.equals(SpecNaming.Transition)) {
184 this.transition.addLines(primitive.contents);
185 } else if (name.equals(SpecNaming.PreCondition)) {
186 this.preCondition.addLines(primitive.contents);
187 } else if (name.equals(SpecNaming.JustifyingPrecondition)) {
188 this.justifyingPrecondition.addLines(primitive.contents);
189 } else if (name.equals(SpecNaming.JustifyingPostcondition)) {
190 this.justifyingPostcondition.addLines(primitive.contents);
191 } else if (name.equals(SpecNaming.PostCondition)) {
192 this.postCondition.addLines(primitive.contents);
193 } else if (name.equals(SpecNaming.PrintValue)) {
194 this.print.addLines(primitive.contents);
201 * This function is called to extract all the declarations that should go to
202 * the corresponding value struct --- a C++ struct to be generated for this
203 * interface that contains the information of the return value and the
208 * The line that represents the interface declaration line
209 * @throws ParseException
211 public void processFunctionDeclaration(String line) throws ParseException {
212 // FIXME: Currently we only allow the declaration to be one-liner
213 funcHeader = UtilParser.parseFuncHeader(line);
214 // Record the original declaration line
215 funcHeader.setHeaderLine(line);
217 // If users have not defined @Interface, we should use the function name
218 // as the interface label
220 setNames(funcHeader.funcName.bareName);
223 // Once we have the compelte function declaration, we can auto-gen the
224 // print-out statements if it's not defined
226 print.addLines(generateAutoPrintFunction());
230 public String toString() {
231 StringBuilder sb = new StringBuilder();
232 sb.append(super.toString() + "\n");
233 sb.append("@Interface: " + name + "\n");
234 if (!transition.isEmpty())
235 sb.append("@Transition:\n" + transition);
236 if (!preCondition.isEmpty())
237 sb.append("@PreCondition:\n" + preCondition);
238 if (!postCondition.isEmpty())
239 sb.append("@PostCondition:\n" + postCondition);
240 if (!print.isEmpty())
241 sb.append("@Print:\n" + print + "\n");
242 sb.append(funcHeader);
244 return sb.toString();
247 public int getEndLineNumFunction() {
248 return endLineNumFunction;
251 public void setEndLineNumFunction(int endLineNumFunction) {
252 this.endLineNumFunction = endLineNumFunction;
255 public String getStructName() {
259 private void setNames(String name) {
263 structName = createStructName(name);
266 static public String createStructName(String labelName) {
267 return "__struct_" + labelName + "__";