1 package edu.uci.eecs.specExtraction;
4 import java.util.ArrayList;
5 import java.util.regex.Matcher;
6 import java.util.regex.Pattern;
10 * This class contains a list of static utility functions for extracting
11 * specification annotations more conveniently.
17 public class SpecUtils {
21 * This inner class defines a primitive --- a sub-annotation. For example,
22 * the "@DeclareState" in the global state is one primitive. We record the
23 * beginning line number of that primitive, the name of the primitive and a
24 * list of lines that belong to that primitive.
30 public static class Primitive {
31 public final int beginLineNum;
32 public final String name;
33 public final ArrayList<String> contents;
35 public Primitive(String name, int beginLineNum) {
37 this.beginLineNum = beginLineNum;
38 contents = new ArrayList<String>();
41 public void addLine(String line) {
45 public String toString() {
46 return "@" + name + ":\n" + contents;
52 * This is a customized wrap of integer so that we can use integer type as
53 * if they were in a C/C++ pass-by-reference fashion. It basically wraps an
54 * int primitive to allow read, write and increment its internal int value.
60 public static class IntObj {
63 public IntObj(int value) {
67 public void setVal(int value) {
83 public String toString() {
84 return Integer.toString(value);
88 // A regular expression pattern that matches "@WORD:"
89 public static final Pattern regexpPrimitive = Pattern.compile("@(\\w+):");
90 // The matcher for the primitive regular expression
91 public static final Matcher matcherPrimitive = regexpPrimitive.matcher("");
93 // Match code after colon: ":" + Code + "$"
94 public static final Pattern regexpCode = Pattern.compile(":(.*)$");
95 public static final Matcher matcherCode = regexpCode.matcher("");
97 // Match a valid word: "^\w+$"
98 public static final Pattern regexpWord = Pattern.compile("^\\w+$");
99 public static final Matcher matcherWord = regexpWord.matcher("");
103 * This function will look for the first line that contains a primitive from
104 * the "curIdx", and then extracts all the non-empty lines of that primitive
105 * until it gets to the end of the list or the beginning of the next
106 * primitive. It returns a list of the actual code for that primitive. When
107 * we are done with the function call, the curIdx either points to the next
108 * primitive or the end of the annotation list.
112 * The file begin processing
113 * @param beginLineNum
114 * The beginning line number of the first annotation lines
116 * The list of annotations
118 * The current index (the index of the line that we are
119 * processing). We will update the current index after calling
120 * this function. Keep in mind that this is a customized wrap of
121 * integer so that we can use it as if it is a C/C++ reference
122 * @return The primitive starting from the curIdx till either the end of the
123 * annotations or the beginning line of the next primitive
124 * @throws WrongAnnotationException
126 public static Primitive extractPrimitive(File file, int beginLineNum,
127 ArrayList<String> annotations, IntObj curIdx)
128 throws WrongAnnotationException {
129 if (curIdx.getVal() == annotations.size()) // The current index points
136 Primitive primitive = null;
137 // Find the first primitive
138 for (; curIdx.getVal() < annotations.size(); curIdx.inc()) {
139 line = annotations.get(curIdx.getVal());
140 curLineNum = curIdx.getVal() + beginLineNum;
141 matcherPrimitive.reset(line);
142 if (matcherPrimitive.find()) {
143 String name = matcherPrimitive.group(1);
144 primitive = new Primitive(name, curLineNum);
148 // Assert that we must have found one primitive
149 if (primitive == null) {
150 WrongAnnotationException
151 .err(file, curLineNum,
152 "Something is wrong! We must have found one primitve here!\n");
155 // Process the current "primitive"
156 // Deal with the first special line. E.g. @DeclareState: int x;
158 matcherCode.reset(line);
159 if (matcherCode.find()) {
160 code = matcherCode.group(1);
161 String trimmedCode = trimSpace(trimTrailingCommentSymbol(code));
162 if (!trimmedCode.equals("")) {
163 primitive.addLine(trimmedCode);
166 WrongAnnotationException
167 .err(file, curLineNum,
168 "The state annotation should have correct primitive syntax (sub-annotations)");
171 // Deal with other normal line. E.g. y = 1;
174 for (; curIdx.getVal() < annotations.size(); curIdx.inc()) {
175 curLineNum = beginLineNum + curIdx.getVal();
176 line = annotations.get(curIdx.getVal());
177 matcherPrimitive.reset(line);
178 if (!matcherPrimitive.find()) {
179 // This is another line that we should add to the result
180 code = trimSpace(trimTrailingCommentSymbol(line));
181 if (!code.equals(""))
182 primitive.addLine(code);
184 // We get to the end of the current primitive
188 if (primitive.contents.size() == 0) { // The content of the primitive is
190 WrongAnnotationException.warning(file, curLineNum, "Primitive "
191 + primitive.name + " is empty.");
199 * The line to be processed
200 * @return The string whose beginning and ending space have been trimmed
202 public static String trimSpace(String line) {
204 Pattern regexp = Pattern.compile("^\\s*(.*?)\\s*$");
205 Matcher matcher = regexp.matcher(line);
206 if (matcher.find()) {
207 return matcher.group(1);
215 * It processed the line in a way that it removes the trailing C/C++ comment
216 * symbols "STAR SLASH"
222 public static String trimTrailingCommentSymbol(String line) {
223 Pattern regexp = Pattern.compile("(.*?)\\s*(\\*/)?\\s*$");
224 Matcher matcher = regexp.matcher(line);
225 if (matcher.find()) {
226 return matcher.group(1);
232 public static boolean isUserDefinedStruct(String type) {
233 // FIXME: We only consider the type is either a one-level pointer or a
235 String bareType = trimSpace(type.replace('*', ' '));
236 return !bareType.equals("int") && !bareType.matches("unsigned\\s+int")
237 && !bareType.equals("unsigned") && !bareType.equals("bool")
238 && !bareType.equals("double") && !bareType.equals("float")
239 && !bareType.equals("void");
242 public static String getPlainType(String type) {
243 // FIXME: We only consider the type is either a one-level pointer or a
245 String bareType = trimSpace(type.replace('*', ' '));
251 * This function will automatically generate the printing statements for
252 * supported types when given a type and a name of the declaration.
255 * @return The auto-generated state printing statements
257 public static Code generatePrintStatement(String type, String name) {
258 Code code = new Code();
260 if (type.equals("int") || type.equals("unsigned")
261 || type.equals("unsigned int") || type.equals("int unsigned")
262 || type.equals("double") || type.equals("double")
263 || type.equals("bool")) {
264 // PRINT("\tx=%d\n", x);
265 code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%d\\n\", "
267 } else if (type.equals("int *") || type.equals("unsigned *")
268 || type.equals("unsigned int *")
269 || type.equals("int unsigned *") || type.equals("double *")
270 || type.equals("double *") || type.equals("bool *")) {
271 // Supported pointer types for primitive types
272 // PRINT("\t*x=%d\n", *x);
273 code.addLine(SpecNaming.PRINT + "(\"\\t*" + name + "=%d\\n\", *"
275 } else if (type.equals("IntList") || type.equals("IntSet")
276 || type.equals("IntMap")) {
279 // printContainer(&q);
280 // model_print("\n");
281 code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
282 if (type.equals("IntMap")) {
283 code.addLine(SpecNaming.PrintMap + "(&" + name + ");");
285 code.addLine(SpecNaming.PrintContainer + "(&" + name + ");");
287 code.addLine(SpecNaming.PRINT + "(\"\\n\");");
288 } else if (type.equals("IntList *") || type.equals("IntSet *")
289 || type.equals("IntMap *")) {
290 // Supported pointer types
292 // printContainer(q);
293 // model_print("\n");
294 code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
295 if (type.equals("IntMap *")) {
296 code.addLine(SpecNaming.PrintMap + "(" + name + ");");
298 code.addLine(SpecNaming.PrintContainer + "(" + name + ");");
300 code.addLine(SpecNaming.PRINT + "(\"\\n\");");
301 } else if (type.equals("void")) {
304 if (type.endsWith("*")) { // If it's an obvious pointer (with a STAR)
305 // Weak support pointer types (just print out the address)
306 // PRINT("\tmutex=%p\n", mutex);
307 code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%p\\n\", "
310 code.addLine("// We do not support auto-gen print-out for type: "