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 justifyingCondition;
34 public final Code transition;
35 public final Code postCondition;
36 public final Code print;
38 // The ending line number of the specification annotation construct
39 public final int endLineNum;
41 // The ending line number of the function definition
42 private int endLineNumFunction;
43 // The function header of the corresponding interface --- The list of
44 // variable declarations that represent the RETURN value and
45 // arguments of the interface
46 private FunctionHeader funcHeader;
48 public final boolean autoGenPrint;
50 public InterfaceConstruct(File file, int beginLineNum, int endLineNum,
51 ArrayList<String> annotations) throws WrongAnnotationException {
52 super(file, beginLineNum);
53 this.endLineNum = endLineNum;
55 this.structName = null;
56 this.preCondition = new Code();
57 this.justifyingCondition = new Code();
58 this.transition = new Code();
59 this.postCondition = new Code();
60 this.print = new Code();
62 processAnnotations(annotations);
64 autoGenPrint = print.isEmpty();
67 public FunctionHeader getFunctionHeader() {
68 return this.funcHeader;
71 public boolean equals(Object other) {
72 if (!(other instanceof InterfaceConstruct)) {
75 InterfaceConstruct o = (InterfaceConstruct) other;
76 if (o.name.equals(this.name))
82 public String getName() {
88 * This function will automatically generate the printing statements for
89 * supported types if the user has not defined the "@Print" primitive
92 * @return The auto-generated state printing statements
93 * @throws WrongAnnotationException
95 private Code generateAutoPrintFunction() {
96 Code code = new Code();
98 code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType,
101 for (VariableDeclaration decl : funcHeader.args) {
102 String type = decl.type;
103 String name = decl.name;
104 code.addLines(SpecUtils.generatePrintStatement(type, name));
111 * Assert that the interface primitive is valid; if not, throws an exception
117 * The primitive string that we have extracted earlier
118 * @throws WrongAnnotationException
120 private void assertValidPrimitive(File file, Primitive primitive)
121 throws WrongAnnotationException {
122 int lineNum = primitive.beginLineNum;
123 String name = primitive.name;
124 if (!name.equals(SpecNaming.Interface)
125 && !name.equals(SpecNaming.Transition)
126 && !name.equals(SpecNaming.PreCondition)
127 && !name.equals(SpecNaming.JustifyingCondition)
128 && !name.equals(SpecNaming.SideEffect)
129 && !name.equals(SpecNaming.PostCondition)
130 && !name.equals(SpecNaming.PrintValue)) {
131 WrongAnnotationException.err(file, lineNum, name
132 + " is NOT a valid CDSSpec interface primitive.");
138 * Assert that the "@Interface" primitive has correct syntax; if not, throws
139 * an exception. If so, it basically checks whether content of the primitive
140 * is a valid word and then return interface label name.
146 * Current line number
148 * The primitive string that we have extracted earlier
149 * @throws WrongAnnotationException
151 private String extractInterfaceName(File file, Primitive primitive)
152 throws WrongAnnotationException {
153 int lineNum = primitive.beginLineNum;
154 String name = primitive.name;
155 if (primitive.contents.size() != 1)
156 WrongAnnotationException.err(file, lineNum,
157 "The @Interface primitive: " + name + " has wrong syntax.");
158 String line = primitive.contents.get(0);
159 SpecUtils.matcherWord.reset(line);
160 if (!SpecUtils.matcherWord.find())
161 WrongAnnotationException.err(file, lineNum, name
162 + " is NOT a valid CDSSpec @Interface primitive.");
166 private void processAnnotations(ArrayList<String> annotations)
167 throws WrongAnnotationException {
168 IntObj curIdx = new IntObj(0);
169 Primitive primitive = null;
171 while ((primitive = SpecUtils.extractPrimitive(file, beginLineNum,
172 annotations, curIdx)) != null) {
173 String name = primitive.name;
174 assertValidPrimitive(file, primitive);
175 if (primitive.contents.size() == 0)
177 if (name.equals(SpecNaming.Interface)) {
178 String interName = extractInterfaceName(file, primitive);
180 } else if (name.equals(SpecNaming.Transition)) {
181 this.transition.addLines(primitive.contents);
182 } else if (name.equals(SpecNaming.PreCondition)) {
183 this.preCondition.addLines(primitive.contents);
184 } else if (name.equals(SpecNaming.JustifyingCondition)) {
185 this.justifyingCondition.addLines(primitive.contents);
186 } else if (name.equals(SpecNaming.PostCondition)) {
187 this.postCondition.addLines(primitive.contents);
188 } else if (name.equals(SpecNaming.PrintValue)) {
189 this.print.addLines(primitive.contents);
196 * This function is called to extract all the declarations that should go to
197 * the corresponding value struct --- a C++ struct to be generated for this
198 * interface that contains the information of the return value and the
203 * The line that represents the interface declaration line
204 * @throws ParseException
206 public void processFunctionDeclaration(String line) throws ParseException {
207 // FIXME: Currently we only allow the declaration to be one-liner
208 funcHeader = UtilParser.parseFuncHeader(line);
209 // Record the original declaration line
210 funcHeader.setHeaderLine(line);
212 // If users have not defined @Interface, we should use the function name
213 // as the interface label
215 setNames(funcHeader.funcName.bareName);
218 // Once we have the compelte function declaration, we can auto-gen the
219 // print-out statements if it's not defined
221 print.addLines(generateAutoPrintFunction());
225 public String toString() {
226 StringBuilder sb = new StringBuilder();
227 sb.append(super.toString() + "\n");
228 sb.append("@Interface: " + name + "\n");
229 if (!transition.isEmpty())
230 sb.append("@Transition:\n" + transition);
231 if (!preCondition.isEmpty())
232 sb.append("@PreCondition:\n" + preCondition);
233 if (!postCondition.isEmpty())
234 sb.append("@PostCondition:\n" + postCondition);
235 if (!print.isEmpty())
236 sb.append("@Print:\n" + print + "\n");
237 sb.append(funcHeader);
239 return sb.toString();
242 public int getEndLineNumFunction() {
243 return endLineNumFunction;
246 public void setEndLineNumFunction(int endLineNumFunction) {
247 this.endLineNumFunction = endLineNumFunction;
250 public String getStructName() {
254 private void setNames(String name) {
258 structName = createStructName(name);
261 static public String createStructName(String labelName) {
262 return "__struct_" + labelName + "__";