edits
[cdsspec-compiler.git] / src / edu / uci / eecs / codeGenerator / CodeGeneratorUtils.java
1 package edu.uci.eecs.codeGenerator;
2
3 import java.util.ArrayList;
4 import java.util.HashMap;
5 import java.util.HashSet;
6 import java.util.regex.Matcher;
7 import java.util.regex.Pattern;
8 import java.io.BufferedWriter;
9 import java.io.File;
10 import java.io.FileWriter;
11 import java.io.IOException;
12
13 import edu.uci.eecs.specExtraction.Code;
14 import edu.uci.eecs.specExtraction.CommutativityRule;
15 import edu.uci.eecs.specExtraction.DefineConstruct;
16 import edu.uci.eecs.specExtraction.EntryConstruct;
17 import edu.uci.eecs.specExtraction.FunctionHeader;
18 import edu.uci.eecs.specExtraction.GlobalConstruct;
19 import edu.uci.eecs.specExtraction.InterfaceConstruct;
20 import edu.uci.eecs.specExtraction.OPConstruct;
21 import edu.uci.eecs.specExtraction.SpecExtractor;
22 import edu.uci.eecs.specExtraction.SpecNaming;
23 import edu.uci.eecs.specExtraction.VariableDeclaration;
24
25 /**
26  * <p>
27  * Some utility functions for generating specification checking code.
28  * </p>
29  * 
30  * @author Peizhao Ou
31  * 
32  */
33 public class CodeGeneratorUtils {
34
35         public static void PrintCode(ArrayList<String> code) {
36                 for (int i = 0; i < code.size(); i++) {
37                         System.out.println(code.get(i));
38                 }
39         }
40
41         public static String Comment(String comment) {
42                 return "/** " + comment + " */";
43         }
44
45         public static String ShortComment(String comment) {
46                 return "// " + comment;
47         }
48
49         public static String IncludeHeader(String header) {
50                 return "#include " + header;
51         }
52
53         public static String Brace(String val) {
54                 return "(" + val + ")";
55         }
56
57         public static String Quote(String val) {
58                 return "\"" + val + "\"";
59         }
60
61         public static String Assign(String varName, String val) {
62                 return varName + " = " + val + ";";
63         }
64
65         public static String AssignToPtr(String structName, String field, String val) {
66                 return structName + "->" + field + " = " + val + ";";
67         }
68
69         public static String Declare(String type, String name) {
70                 return type + " " + name + ";";
71         }
72
73         public static String Declare(VariableDeclaration varDecl) {
74                 return Declare(varDecl.type, varDecl.name);
75         }
76
77         public static String DeclareDefine(String type, String var, String val) {
78                 return type + " " + var + " = " + val + ";";
79         }
80
81         /**
82          * <p>
83          * Insert a number of tabs at the beginning of the line.
84          * </p>
85          * 
86          * @param line
87          *            Input line
88          * @param tabCnt
89          *            The number of tabs to be inserted
90          * @return A line that starts with the specific inserted tabs
91          */
92         public static String TabbedLine(String line, int tabCnt) {
93                 String res = "";
94                 for (int i = 0; i < tabCnt; i++)
95                         res = "\t" + res;
96                 res = res + line;
97                 return res;
98         }
99
100         /**
101          * <p>
102          * Insert a tab at the beginning of the line.
103          * </p>
104          * 
105          * @param line
106          *            Input line
107          * @return A line that starts with one inserted tab
108          */
109         public static String TabbedLine(String line) {
110                 return "\t" + line;
111         }
112
113         /**
114          * <p>
115          * This function generates the code for the header file that our
116          * specification generates automatically --- cdsspec-generated.h.
117          * </p>
118          * 
119          * @param extractor
120          *            The SpecExtractor that contains the extracted information
121          * @return The generated code
122          */
123         public static Code GenerateCDSSpecHeaderFile(SpecExtractor extractor) {
124                 HashSet<String> headerFiles = extractor.headerFiles;
125                 GlobalConstruct globalConstruct = extractor.getGlobalConstruct();
126                 HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap = extractor.interfaceListMap;
127                 HashSet<String> OPLabelSet = extractor.OPLabelSet;
128
129                 Code code = new Code();
130
131                 // Add auto-generated comments
132                 code.addLine("/**");
133                 code.addLine(TabbedLine("This is a header file auto-generated by CDSSpec compiler; together, CDSSpec"));
134                 code.addLine(TabbedLine("compiler should have generated the accompanying implementation file that"));
135                 code.addLine(TabbedLine("implements the some functions declared in this file. In order to instrument"));
136                 code.addLine(TabbedLine("your benchmark for CDSSpec checker to check, you should include this header"));
137                 code.addLine(TabbedLine("file in every file you use an CDSSpec annotation. Note that it should be"));
138                 code.addLine(TabbedLine("placed in the end of all other header files. Currently we require a C++"));
139                 code.addLine(TabbedLine("compiler that supports C++11."));
140                 code.addLine("*/");
141                 code.addLine("");
142
143                 code.addLine("#ifndef _"
144                                 + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
145                                                 '_') + "_H");
146                 code.addLine("#define _"
147                                 + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
148                                                 '_') + "_H");
149                 code.addLine("");
150
151                 // FIXME: We have included ad-hoc header files here
152                 // System included headers
153                 code.addLine(ShortComment("System included headers go here"));
154                 code.addLine(IncludeHeader(SpecNaming.SPECANNOTATION_API));
155                 code.addLine(IncludeHeader(SpecNaming.STDLIB));
156
157                 code.addLine("");
158
159                 // Users included headers
160                 code.addLine(ShortComment("User included headers go here"));
161                 for (String header : headerFiles) {
162                         code.addLine(IncludeHeader(header));
163                 }
164                 code.addLine("");
165
166                 // Decalre extern "C" --- begin
167                 code.addLine("#ifdef __cplusplus");
168                 code.addLine("extern \"C\" {");
169                 code.addLine("#endif");
170                 code.addLine("");
171
172                 code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
173
174                 // Interface name strings
175                 code.addLine(ShortComment("Interface name strings"));
176                 for (File file : interfaceListMap.keySet()) {
177                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
178                         for (InterfaceConstruct construct : list) {
179                                 String name = construct.getName();
180                                 code.addLine(Declare("extern " + SpecNaming.CString,
181                                                 SpecNaming.AppendStr(name)));
182                         }
183                 }
184                 code.addLine("");
185
186                 // Ordering points label strings
187                 code.addLine(ShortComment("Ordering points label strings"));
188                 for (String label : OPLabelSet) {
189                         code.addLine(Declare("extern " + SpecNaming.CString,
190                                         SpecNaming.AppendStr(label)));
191                 }
192                 code.addLine("");
193
194                 // Declare customized value struct
195                 for (File file : interfaceListMap.keySet()) {
196                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
197                         for (InterfaceConstruct construct : list) {
198                                 // Declare custom value struct for the interface
199                                 String name = construct.getName();
200                                 code.addLine(ShortComment("Declare custom value struct for "
201                                                 + name));
202                                 code.addLine("typedef struct " + name + " {");
203                                 FunctionHeader funcHeader = construct.getFunctionHeader();
204                                 // RET
205                                 if (!funcHeader.returnType.equals("void"))
206                                         code.addLine(TabbedLine(Declare(funcHeader.returnType,
207                                                         SpecNaming.RET)));
208                                 // Arguments
209                                 for (VariableDeclaration decl : funcHeader.args) {
210                                         code.addLine(TabbedLine(Declare(decl)));
211                                 }
212                                 code.addLine("} " + name + ";");
213                                 code.addLine("");
214                         }
215                 }
216
217                 // Declare INIT annotation instrumentation function
218                 code.addLine(ShortComment("Declare INIT annotation instrumentation function"));
219                 code.addLine("void _createInitAnnotation();");
220                 code.addLine("");
221
222                 // Decalre extern "C" --- begin
223                 code.addLine("#ifdef __cplusplus");
224                 code.addLine("};");
225                 code.addLine("#endif");
226                 code.addLine("");
227
228                 // Declare #endif
229                 code.addLine("#endif");
230
231                 return code;
232         }
233
234         /**
235          * <p>
236          * This function generates the code for the CPP file that our specification
237          * generates automatically --- cdsspec-generated.cc.
238          * </p>
239          * 
240          * @param extractor
241          *            The SpecExtractor that contains the extracted information
242          * @return The generated code
243          */
244         public static Code GenerateCDSSpecCPPFile(SpecExtractor extractor) {
245                 GlobalConstruct globalConstruct = extractor.getGlobalConstruct();
246                 HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap = extractor.interfaceListMap;
247                 HashSet<String> OPLabelSet = extractor.OPLabelSet;
248
249                 Code code = new Code();
250                 String line = null;
251                 Code fieldsInit = null;
252
253                 // Add auto-generated comments
254                 code.addLine("/**");
255                 code.addLine(TabbedLine("This is an implementation file auto-generated by CDSSpec compiler to"));
256                 code.addLine(TabbedLine("instrument your benchmark for CDSSpec checker to check. Currently we require"));
257                 code.addLine(TabbedLine("a C++ compiler that supports C++11."));
258                 code.addLine("*/");
259                 code.addLine("");
260
261                 code.addLine("#include " + SpecNaming.CDSSpecGeneratedHeader);
262                 code.addLine("#include " + SpecNaming.CDSANNOTATE);
263                 code.addLine("#include " + SpecNaming.SPEC_COMMON);
264                 code.addLine("#include " + SpecNaming.METHODCALL);
265                 code.addLine("#include " + SpecNaming.CDSSPEC);
266                 code.addLine("#include " + SpecNaming.SPECANNOTATION);
267                 code.addLine("");
268                 code.addLine("");
269
270                 // Declare customized StateStruct
271                 code.addLine(ShortComment("Declare customized StateStruct"));
272                 code.addLine("typedef struct " + SpecNaming.StateStruct + " {");
273                 for (VariableDeclaration decl : globalConstruct.declState) {
274                         code.addLine(TabbedLine(Declare(decl)));
275                 }
276                 code.addLine("");
277                 // Define state destructor
278                 code.addLine(TabbedLine(ShortComment("Define state destructor")));
279                 code.addLine(TabbedLine("~" + SpecNaming.StateStruct + "() {"));
280                 if (!globalConstruct.autoGenClear) {
281                         code.addLine(TabbedLine(
282                                         ShortComment("Execute user-defined state clear code"), 2));
283                 } else {
284                         code.addLine(TabbedLine(
285                                         ShortComment("Execute auto-generated state clear code"), 2));
286                 }
287                 globalConstruct.clearState.align(2);
288                 code.addLines(globalConstruct.clearState);
289                 code.addLine(TabbedLine("}"));
290                 code.addLine("");
291
292                 code.addLine(TabbedLine("SNAPSHOTALLOC"));
293                 code.addLine("");
294                 code.addLine("} " + SpecNaming.StateStruct + ";");
295                 code.addLine("");
296                 code.addLine("");
297
298                 code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
299                 code.addLine(ShortComment("A special empty string"));
300                 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,
301                                 "\"\""));
302                 code.addLine("");
303
304                 // Interface name strings
305                 code.addLine(ShortComment("Interface name strings"));
306                 for (File file : interfaceListMap.keySet()) {
307                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
308                         for (InterfaceConstruct construct : list) {
309                                 String name = construct.getName();
310                                 code.addLine(DeclareDefine(SpecNaming.CString,
311                                                 SpecNaming.AppendStr(name), Quote(name)));
312                         }
313                 }
314                 code.addLine("");
315
316                 // Commutativity rule strings
317                 code.addLine(ShortComment("Commutativity rule strings"));
318                 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
319                         CommutativityRule rule = globalConstruct.commutativityRules
320                                         .get(i - 1);
321                         code.addLine(DeclareDefine(SpecNaming.CString,
322                                         SpecNaming.AppendStr(SpecNaming.Commutativity + i),
323                                         Quote(rule.toString())));
324                 }
325                 code.addLine("");
326
327                 // Ordering points label strings
328                 code.addLine(ShortComment("Ordering points label strings"));
329                 for (String label : OPLabelSet) {
330                         code.addLine(DeclareDefine(SpecNaming.CString,
331                                         SpecNaming.AppendStr(label), Quote(label)));
332                 }
333                 code.addLine("");
334
335                 // Special function name strings
336                 code.addLine(ShortComment("Special function name strings"));
337                 code.addLine(DeclareDefine(SpecNaming.CString,
338                                 SpecNaming.AppendStr(SpecNaming.InitalState), Quote("_"
339                                                 + SpecNaming.InitalState.toLowerCase())));
340                 code.addLine(DeclareDefine(SpecNaming.CString,
341                                 SpecNaming.AppendStr(SpecNaming.CopyState), Quote("_"
342                                                 + SpecNaming.CopyState.toLowerCase())));
343                 code.addLine(DeclareDefine(SpecNaming.CString,
344                                 SpecNaming.AppendStr(SpecNaming.ClearState), Quote("_"
345                                                 + SpecNaming.ClearState.toLowerCase())));
346                 code.addLine(DeclareDefine(SpecNaming.CString,
347                                 SpecNaming.AppendStr(SpecNaming.FinalState), Quote("_"
348                                                 + SpecNaming.FinalState.toLowerCase())));
349                 code.addLine(DeclareDefine(SpecNaming.CString,
350                                 SpecNaming.AppendStr(SpecNaming.PrintState), Quote("_"
351                                                 + SpecNaming.PrintState.toLowerCase())));
352                 code.addLine("");
353
354                 // Interface name strings
355                 for (File file : interfaceListMap.keySet()) {
356                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
357                         for (InterfaceConstruct construct : list) {
358                                 String name = construct.getName();
359                                 code.addLine(ShortComment(name + " function strings"));
360                                 // Transition
361                                 String tmpFunc = name + "_" + SpecNaming.Transition;
362                                 code.addLine(DeclareDefine(SpecNaming.CString,
363                                                 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
364                                 // PreCondition
365                                 tmpFunc = name + "_" + SpecNaming.PreCondition;
366                                 if (!construct.preCondition.isEmpty())
367                                         code.addLine(DeclareDefine(SpecNaming.CString,
368                                                         SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
369                                 else
370                                         code.addLine(DeclareDefine(SpecNaming.CString,
371                                                         SpecNaming.AppendStr(tmpFunc),
372                                                         SpecNaming.EmptyCString));
373                                 // PostCondition
374                                 tmpFunc = name + "_" + SpecNaming.PostCondition;
375                                 if (!construct.postCondition.isEmpty())
376                                         code.addLine(DeclareDefine(SpecNaming.CString,
377                                                         SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
378                                 else
379                                         code.addLine(DeclareDefine(SpecNaming.CString,
380                                                         SpecNaming.AppendStr(tmpFunc),
381                                                         SpecNaming.EmptyCString));
382                                 // Print
383                                 tmpFunc = name + "_" + SpecNaming.PrintValue;
384                                 if (!construct.print.isEmpty())
385                                         code.addLine(DeclareDefine(SpecNaming.CString,
386                                                         SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
387                                 else
388                                         code.addLine(DeclareDefine(SpecNaming.CString,
389                                                         SpecNaming.AppendStr(tmpFunc),
390                                                         SpecNaming.EmptyCString));
391                                 code.addLine("");
392                         }
393                 }
394
395                 // Define @Initial
396                 code.addLine(ShortComment("Define @" + SpecNaming.InitalState));
397                 code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
398                                 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
399                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
400                                 + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
401                 // Define macros
402                 for (VariableDeclaration decl : globalConstruct.declState) {
403                         code.addLine(TabbedLine("#define " + decl.name + " "
404                                         + SpecNaming.StateInst + "->" + decl.name));
405                 }
406                 if (!globalConstruct.autoGenInitial)
407                         code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
408                 else
409                         // Auto-generated the initialization function
410                         code.addLine(TabbedLine(ShortComment("Auto-generated state intialization code")));
411                 // Align the code with one tab
412                 globalConstruct.initState.align(1);
413                 code.addLines(globalConstruct.initState);
414                 // Undefine macros
415                 for (VariableDeclaration decl : globalConstruct.declState) {
416                         code.addLine(TabbedLine("#undef " + decl.name));
417                 }
418                 code.addLine("");
419                 code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1,
420                                 SpecNaming.StateInst, SpecNaming.StateInst)));
421                 code.addLine("}");
422                 code.addLine("");
423
424                 // Define @Copy
425                 code.addLine(ShortComment("Define @" + SpecNaming.CopyState));
426                 code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
427                                 + SpecNaming.Method + " " + "dest, " + SpecNaming.Method
428                                 + " src) {");
429                 // StateStruct *OLD = (StateStruct*) src->state;
430                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
431                                 + SpecNaming.OldStateInst, Brace(SpecNaming.StateStruct + "*")
432                                 + " src->" + SpecNaming.StateInst)));
433                 // StateStruct *NEW = new StateStruct;
434                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
435                                 + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
436                 if (!globalConstruct.autoGenCopy)
437                         code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
438                 else
439                         // Auto-generated the copy function
440                         code.addLine(TabbedLine(ShortComment("Auto-generated state copy statements")));
441                 globalConstruct.copyState.align(1);
442                 code.addLines(globalConstruct.copyState);
443                 code.addLine("");
444                 code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst,
445                                 SpecNaming.NewStateInst)));
446                 code.addLine("}");
447                 code.addLine("");
448
449                 // Define @Clear
450                 code.addLine(ShortComment("Define @" + SpecNaming.ClearState));
451                 code.addLine("void _" + SpecNaming.ClearState.toLowerCase() + "("
452                                 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
453                 // Retrieve the state
454                 code.addLine(TabbedLine(ShortComment("Retrieve the state")));
455                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
456                                 + SpecNaming.StateInst, "(" + SpecNaming.StateStruct + "*) "
457                                 + SpecNaming.Method1 + "->state")));
458                 // Explicitly call the state destructor
459                 code.addLine(TabbedLine(ShortComment("Explicitly call the state destructor")));
460                 code.addLine(TabbedLine("delete " + SpecNaming.StateInst + ";"));
461                 code.addLine("}");
462                 code.addLine("");
463
464                 // Define @Print
465                 code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
466                 code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
467                                 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
468
469                 // Initialize state struct fields
470                 fieldsInit = GenerateStateFieldsInitialization(SpecNaming.Method1,
471                                 SpecNaming.StateInst, globalConstruct);
472                 fieldsInit.align(1);
473                 code.addLines(fieldsInit);
474                 code.addLine("");
475                 if (!globalConstruct.autoGenPrint)
476                         code.addLine(TabbedLine(ShortComment("Execute user-defined state printing code")));
477                 else
478                         // Auto-generated the copy function
479                         code.addLine(TabbedLine(ShortComment("Execute auto-generated state printing code")));
480
481                 // Align the code with one tab
482                 globalConstruct.printState.align(1);
483                 code.addLines(globalConstruct.printState);
484                 code.addLine("}");
485                 code.addLine("");
486
487                 // Define @Commutativity
488                 code.addLine(ShortComment("Define commutativity checking functions"));
489                 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
490                         CommutativityRule rule = globalConstruct.commutativityRules
491                                         .get(i - 1);
492                         code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
493                                         + SpecNaming.Method + " m1, " + SpecNaming.Method
494                                         + " m2) {");
495                         // if (m1->name == _ENQ_str && m2->name == _DEQ_str) {
496                         code.addLine(TabbedLine("if (m1->name == "
497                                         + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
498                                         + SpecNaming.AppendStr(rule.method2) + ") {"));
499                         // Initialize M1 & M2 in commutativity rule
500                         // e.g. ENQ *M1 = (ENQ*) m1->value;
501                         code.addLine(TabbedLine(
502                                         DeclareDefine(rule.method1, "*M1", "(" + rule.method1
503                                                         + "*) m1->value"), 2));
504                         code.addLine(TabbedLine(
505                                         DeclareDefine(rule.method2, "*M2", "(" + rule.method2
506                                                         + "*) m2->value"), 2));
507                         code.addLine(TabbedLine("return " + rule.condition + ";", 2));
508                         code.addLine(TabbedLine("}"));
509                         code.addLine(TabbedLine("return false;"));
510
511                         code.addLine("}");
512                         code.addLine("");
513                 }
514
515                 // Define customized interface functions
516                 for (File file : interfaceListMap.keySet()) {
517                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
518                         for (InterfaceConstruct construct : list) {
519                                 fieldsInit = null;
520
521                                 // Define interface functions
522                                 String name = construct.getName();
523                                 code.addLine("/**********    " + name
524                                                 + " functions    **********/");
525                                 // Define @Transition for INTERFACE
526                                 code.addLine(ShortComment("Define @" + SpecNaming.Transition
527                                                 + " for " + name));
528                                 code.addLine("bool _" + name + "_" + SpecNaming.Transition
529                                                 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
530                                                 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
531                                                 + ") {");
532
533                                 // Initialize value struct fields
534                                 fieldsInit = GenerateInterfaceFieldsInitialization(
535                                                 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
536                                                 construct);
537                                 fieldsInit.align(1);
538                                 code.addLines(fieldsInit);
539
540                                 construct.transition.align(1);
541                                 code.addLine(TabbedLine(ShortComment("Execute Transition")));
542                                 code.addLines(construct.transition);
543
544                                 // By default, we will return true for state transition
545                                 code.addLine(TabbedLine(ShortComment("By default @Transition returns true")));
546                                 code.addLine(TabbedLine("return true;"));
547                                 code.addLine("}");
548                                 code.addLine("");
549
550                                 // Define @PreCondition
551                                 if (!construct.preCondition.isEmpty()) {
552                                         code.addLine(ShortComment("Define @"
553                                                         + SpecNaming.PreCondition + " for " + name));
554                                         code.addLine("bool _" + name + "_"
555                                                         + SpecNaming.PreCondition + "(" + SpecNaming.Method
556                                                         + " " + SpecNaming.Method1 + ") {");
557
558                                         // Initialize value struct fields
559                                         fieldsInit = GenerateInterfaceFieldsInitialization(
560                                                         SpecNaming.Method1, SpecNaming.InterfaceValueInst,
561                                                         construct);
562                                         fieldsInit.align(1);
563                                         code.addLines(fieldsInit);
564
565                                         construct.preCondition.align(1);
566                                         code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
567                                         code.addLines(construct.preCondition);
568
569                                         code.addLine("}");
570                                         code.addLine("");
571
572                                 }
573                                 // Define @PostCondition
574                                 if (!construct.postCondition.isEmpty()) {
575                                         code.addLine(ShortComment("Define @"
576                                                         + SpecNaming.PostCondition + " for " + name));
577                                         code.addLine("bool _" + name + "_"
578                                                         + SpecNaming.PostCondition + "("
579                                                         + SpecNaming.Method + " " + SpecNaming.Method1
580                                                         + ") {");
581
582                                         // Initialize value struct fields
583                                         fieldsInit = GenerateInterfaceFieldsInitialization(
584                                                         SpecNaming.Method1, SpecNaming.InterfaceValueInst,
585                                                         construct);
586                                         fieldsInit.align(1);
587                                         code.addLines(fieldsInit);
588
589                                         construct.postCondition.align(1);
590                                         code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
591                                         code.addLines(construct.postCondition);
592
593                                         code.addLine("}");
594                                         code.addLine("");
595                                 }
596                                 // Define @Print
597                                 if (!construct.print.isEmpty()) {
598                                         code.addLine(ShortComment("Define @"
599                                                         + SpecNaming.PrintValue + " for " + name));
600                                         code.addLine("void _" + name + "_" + SpecNaming.PrintValue
601                                                         + "(" + SpecNaming.Method + " "
602                                                         + SpecNaming.Method1 + ") {");
603                                         // Initialize value struct fields
604                                         fieldsInit = GenerateInterfaceFieldsInitialization(
605                                                         SpecNaming.Method1, SpecNaming.InterfaceValueInst,
606                                                         construct);
607                                         fieldsInit.align(1);
608                                         code.addLines(fieldsInit);
609
610                                         construct.print.align(1);
611                                         if (!construct.autoGenPrint)
612                                                 code.addLine(TabbedLine(ShortComment("Execute user-defined value printing code")));
613                                         else
614                                                 // Auto-generated the value printing function
615                                                 code.addLine(TabbedLine(ShortComment("Execute auto-generated value printing code")));
616                                         code.addLines(construct.print);
617
618                                         code.addLine("}");
619                                         code.addLine("");
620                                 }
621                         }
622                 }
623
624                 // Define INIT annotation instrumentation function
625                 code.addLine(ShortComment("Define INIT annotation instrumentation function"));
626                 code.addLine("void _createInitAnnotation() {");
627
628                 // Init commutativity rules
629                 code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
630                 code.addLine(TabbedLine(DeclareDefine("int",
631                                 SpecNaming.CommutativityRuleSizeInst,
632                                 Integer.toString(globalConstruct.commutativityRules.size()))));
633                 String tmp = SpecNaming.NewSize
634                                 + Brace(SpecNaming.CommutativityRule + ", sizeof"
635                                                 + Brace(SpecNaming.CommutativityRule) + " * "
636                                                 + SpecNaming.CommutativityRuleSizeInst);
637                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*"
638                                 + SpecNaming.CommutativityRuleInst, tmp)));
639                 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
640                         CommutativityRule rule = globalConstruct.commutativityRules
641                                         .get(i - 1);
642                         code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ")
643                                         + i));
644                         // new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
645                         // _Commutativity1_str, _checkCommutativity1)
646                         line = "new"
647                                         + Brace(" &" + SpecNaming.CommutativityRuleInst + "["
648                                                         + (i - 1) + "] ") + SpecNaming.CommutativityRule
649                                         + "(" + SpecNaming.AppendStr(rule.method1) + ", "
650                                         + SpecNaming.AppendStr(rule.method2) + ", "
651                                         + SpecNaming.AppendStr(SpecNaming.Commutativity + i) + ", "
652                                         + "_check" + SpecNaming.Commutativity + i + ");";
653                         code.addLine(TabbedLine(line));
654                 }
655
656                 // Initialize AnnoInit
657                 code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
658                 // AnnoInit *init = new AnnoInit(
659                 code.addLine(TabbedLine(SpecNaming.AnnoInit + " *"
660                                 + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit
661                                 + "("));
662                 // new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
663                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
664                                 + SpecNaming.AppendStr(SpecNaming.InitalState) + ", "
665                                 + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
666                                 + SpecNaming.InitalState.toLowerCase() + "),", 2));
667                 // new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
668                 line = "new " + SpecNaming.NamedFunction + "("
669                                 + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
670                                 + SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
671                 if (globalConstruct.finalState.isEmpty()) {
672                         line = line + SpecNaming.NullFunc + "),";
673                 } else {
674                         line = line + "_" + SpecNaming.FinalState.toUpperCase();
675                 }
676                 code.addLine(TabbedLine(line, 2));
677                 // new NamedFunction(_Copy_str, COPY, (void*) _copy),
678                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
679                                 + SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
680                                 + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
681                                 + SpecNaming.CopyState.toLowerCase() + "),", 2));
682                 // new NamedFunction(_Clear_str, CLEAR, (void*) _clear),
683                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
684                                 + SpecNaming.AppendStr(SpecNaming.ClearState) + ", "
685                                 + SpecNaming.ClearState.toUpperCase() + ", " + "(void*) _"
686                                 + SpecNaming.ClearState.toLowerCase() + "),", 2));
687                 // new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
688                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
689                                 + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
690                                 + SpecNaming.PrintStateType + ", " + "(void*) _"
691                                 + SpecNaming.PrintState.toLowerCase() + "),", 2));
692                 // commuteRules, CommuteRuleSize);
693                 code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
694                                 + SpecNaming.CommutativityRuleSizeInst + ");", 2));
695                 code.addLine("");
696
697                 // Declare StateFunctions map
698                 code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
699                 code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*"
700                                 + SpecNaming.StateFunctionsInst)));
701                 code.addLine("");
702
703                 // StateFunction for interface
704                 for (File file : interfaceListMap.keySet()) {
705                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
706                         for (InterfaceConstruct construct : list) {
707                                 String name = construct.getName();
708                                 code.addLine(TabbedLine(ShortComment("StateFunction for "
709                                                 + name)));
710                                 // stateFuncs = new StateFunctions(
711                                 code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
712                                                 + " = new " + SpecNaming.StateFunctions + "("));
713                                 // new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
714                                 // _ENQ_Transition),
715                                 // Transition
716                                 code.addLine(TabbedLine(
717                                                 "new "
718                                                                 + SpecNaming.NamedFunction
719                                                                 + "("
720                                                                 + SpecNaming.AppendStr(name + "_"
721                                                                                 + SpecNaming.Transition) + ", "
722                                                                 + SpecNaming.TransitionType + ", (void*) _"
723                                                                 + name + "_" + SpecNaming.Transition + "),", 2));
724                                 // PreCondition
725                                 line = "new "
726                                                 + SpecNaming.NamedFunction
727                                                 + "("
728                                                 + SpecNaming.AppendStr(name + "_"
729                                                                 + SpecNaming.PreCondition) + ", "
730                                                 + SpecNaming.PreConditionType + ", (void*) ";
731                                 if (construct.preCondition.isEmpty()) {
732                                         line = line + SpecNaming.NullFunc + "),";
733                                 } else {
734                                         line = line + "_" + name + "_" + SpecNaming.PreCondition
735                                                         + "),";
736                                 }
737                                 code.addLine(TabbedLine(line, 2));
738                                 // PostCondition
739                                 line = "new "
740                                                 + SpecNaming.NamedFunction
741                                                 + "("
742                                                 + SpecNaming.AppendStr(name + "_"
743                                                                 + SpecNaming.PostCondition) + ", "
744                                                 + SpecNaming.PostConditionType + ", (void*) ";
745                                 if (construct.postCondition.isEmpty()) {
746                                         line = line + SpecNaming.NullFunc + "),";
747                                 } else {
748                                         line = line + "_" + name + "_" + SpecNaming.PostCondition
749                                                         + "),";
750                                 }
751                                 code.addLine(TabbedLine(line, 2));
752                                 // Print (PrintValue
753                                 line = "new "
754                                                 + SpecNaming.NamedFunction
755                                                 + "("
756                                                 + SpecNaming.AppendStr(name + "_"
757                                                                 + SpecNaming.PrintValue) + ", "
758                                                 + SpecNaming.PrintValueType + ", (void*) ";
759                                 if (construct.print.isEmpty()) {
760                                         line = line + SpecNaming.NullFunc + ")";
761                                 } else {
762                                         line = line + "_" + name + "_" + SpecNaming.PrintValue
763                                                         + ")";
764                                 }
765                                 code.addLine(TabbedLine(line, 2));
766                                 code.addLine(TabbedLine(");"));
767
768                                 // init->addInterfaceFunctions(_ENQ_str, stateFuncs);
769                                 code.addLine(TabbedLine(SpecNaming.AnnoInitInst
770                                                 + "->"
771                                                 + SpecNaming.AddInterfaceFunctions
772                                                 + Brace(SpecNaming.AppendStr(name) + ", "
773                                                                 + SpecNaming.StateFunctionsInst) + ";"));
774                                 code.addLine("");
775                         }
776                 }
777
778                 // Create and instrument with the INIT annotation
779                 code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
780                 // cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
781                 code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc
782                                 + Brace(SpecNaming.SPEC_ANALYSIS
783                                                 + ", new "
784                                                 + SpecNaming.SpecAnnotation
785                                                 + Brace(SpecNaming.AnnoTypeInit + ", "
786                                                                 + SpecNaming.AnnoInitInst)) + ";"));
787
788                 code.addLine("}");
789                 code.addLine("");
790
791                 return code;
792         }
793
794         /**
795          * <p>
796          * This function generates a list of lines that initialize the fields of the
797          * global state struct. See below.
798          * </p>
799          * 
800          * <p>
801          * <code>
802          * StateStruct *state = (StateStruct*) _M->state;
803          * <br>
804          * IntList * q = state->q;
805          * </code>
806          * </p>
807          * 
808          * <p>
809          * In this example, _M --> methodInst, state --> inst.
810          * </p>
811          * 
812          * @param methodInst
813          *            See description
814          * @param inst
815          *            See description
816          * @param construct
817          *            The global state construct
818          * @return The generated code
819          */
820         public static Code GenerateStateFieldsInitialization(String methodInst,
821                         String inst, GlobalConstruct construct) {
822                 Code res = new Code();
823                 res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct
824                                 + " fields"));
825                 res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst, "("
826                                 + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
827                 for (VariableDeclaration decl : construct.declState) {
828                         res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
829                                         + decl.name));
830                 }
831                 return res;
832         }
833
834         /**
835          * <p>
836          * This function generates a list of lines that initialize the fields of a
837          * specific interface struct. See below.
838          * </p>
839          * 
840          * <p>
841          * <code>
842          * ENQ *info = (ENQ*) _M->value;
843          * <br>
844          * IntList * q = info->q;
845          * </code>
846          * </p>
847          * 
848          * <p>
849          * In this example, ENQ --> structType, _M --> methodInst, info --> inst
850          * </p>
851          * 
852          * @param methodInst
853          *            See description
854          * @param inst
855          *            See description
856          * @param construct
857          *            The corresponding interface construct
858          * @return The generated code
859          */
860         public static Code GenerateInterfaceFieldsInitialization(String methodInst,
861                         String inst, InterfaceConstruct construct) {
862                 Code res = new Code();
863                 String name = construct.getName();
864                 res.addLine(ShortComment("Initialize fields for " + name));
865                 // The very first assignment "
866                 res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) "
867                                 + methodInst + "->" + SpecNaming.MethodValueField));
868                 // Don't leave out the RET field
869                 if (!construct.getFunctionHeader().isReturnVoid()) {
870                         res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
871                                         SpecNaming.RET, inst + "->" + SpecNaming.RET));
872                 }
873                 // For arguments
874                 for (VariableDeclaration decl : construct.getFunctionHeader().args) {
875                         res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
876                                         + decl.name));
877                 }
878                 return res;
879         }
880
881         /**
882          * <p>
883          * This function generates the code to be inserted right after the ordering
884          * point construct (instrumentation code)
885          * </p>
886          * 
887          * @param construct
888          *            The corresponding ordering point construct
889          * @return The generated code
890          */
891         public static Code Generate4OPConstruct(OPConstruct construct) {
892                 Code code = new Code();
893                 String curLine = construct.annotation;
894                 String label = construct.label;
895                 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
896                 if (!construct.condition.equals("true")) {
897                         code.addLine(prefixTabs + "if (" + construct.condition + ")");
898                         prefixTabs = prefixTabs + "\t";
899                 }
900
901                 switch (construct.type) {
902                 case OPDefine:
903                         code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
904                         break;
905                 case PotentialOP:
906                         code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
907                                         + "(" + SpecNaming.AppendStr(label) + ");");
908                         break;
909                 case OPCheck:
910                         code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "("
911                                         + SpecNaming.AppendStr(label) + ");");
912                         break;
913                 case OPClear:
914                         code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();");
915                         break;
916                 case OPClearDefine:
917                         code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
918                                         + "();");
919                         break;
920                 default:
921                         break;
922                 }
923                 return code;
924         }
925
926         /**
927          * <p>
928          * This function generates the code to be inserted right after the entry
929          * construct (instrumentation code)
930          * </p>
931          * 
932          * @param construct
933          *            The corresponding entry construct
934          * @return
935          */
936         public static Code Generate4Entry(EntryConstruct construct) {
937                 Code res = new Code();
938                 String curLine = construct.annotation;
939                 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
940                 // _createInitAnnotation();
941                 res.addLine(prefixTabs + SpecNaming.CreateInitAnnoFunc + "();");
942                 return res;
943         }
944
945         /**
946          * <p>
947          * This function generates the code to be inserted right after the "@Define"
948          * construct (instrumentation code)
949          * </p>
950          * 
951          * @param construct
952          *            The corresponding entry construct
953          * @return
954          */
955         public static Code Generate4Define(DefineConstruct construct) {
956                 Code code = new Code();
957                 code.addLine("");
958                 code.addLine("/**********    User-defined code in annotation (BEGIN)    **********/");
959                 code.addLines(construct.code);
960                 code.addLine("/**********    User-defined code in annotation (END)    **********/");
961                 return code;
962         }
963
964         /**
965          * <p>
966          * This function generates the new interface wrapper code to be inserted
967          * right after the end of the interface definition
968          * </p>
969          * 
970          * @param construct
971          *            The corresponding interface construct
972          * @return The generated code
973          */
974         public static Code GenerateInterfaceWrapper(InterfaceConstruct construct) {
975                 Code code = new Code();
976
977                 String name = construct.getName();
978                 String beginLine = construct.getFunctionHeader().getHeaderLine();
979                 Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
980                 Matcher matcherSpace = regexpSpace.matcher(beginLine);
981                 String prefixTabs = "";
982                 if (matcherSpace.find())
983                         prefixTabs = matcherSpace.group(1);
984
985                 // Add one line to separate
986                 code.addLine("");
987                 code.addLine(prefixTabs
988                                 + ShortComment("Generated wrapper interface for " + name));
989                 if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
990                                                                                         // of the line
991                         code.addLine(beginLine + " {");
992                 } else {
993                         code.addLine(beginLine);
994                 }
995                 // Instrument with the INTERFACE_BEGIN annotations
996                 code.addLine(prefixTabs
997                                 + "\t"
998                                 + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
999                 // CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
1000                 code.addLine(prefixTabs
1001                                 + "\t"
1002                                 + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
1003                                                 + SpecNaming.AnnoInterfaceInfoInst,
1004                                                 SpecNaming.CreateInterfaceBeginAnnoFunc
1005                                                                 + Brace(SpecNaming.AppendStr(name))));
1006                 // Call the actual function
1007                 code.addLine(prefixTabs + "\t"
1008                                 + ShortComment("Call the actual function"));
1009                 // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
1010                 code.addLine(prefixTabs + "\t"
1011                                 + construct.getFunctionHeader().getRenamedCall() + ";");
1012                 code.addLine("");
1013
1014                 // Initialize the value struct
1015                 code.addLine(prefixTabs + "\t"
1016                                 + ShortComment("Initialize the value struct"));
1017                 // The very first assignment "
1018                 code.addLine(prefixTabs
1019                                 + "\t"
1020                                 + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst,
1021                                                 SpecNaming.New + Brace(name)));
1022                 // Don't leave out the RET field
1023                 if (!construct.getFunctionHeader().isReturnVoid())
1024                         code.addLine(prefixTabs
1025                                         + "\t"
1026                                         + AssignToPtr(SpecNaming.InterfaceValueInst,
1027                                                         SpecNaming.RET, SpecNaming.RET));
1028                 // For arguments
1029                 for (VariableDeclaration decl : construct.getFunctionHeader().args)
1030                         code.addLine(prefixTabs
1031                                         + "\t"
1032                                         + AssignToPtr(SpecNaming.InterfaceValueInst, decl.name,
1033                                                         decl.name));
1034                 code.addLine("");
1035
1036                 // Store the value info into the current MethodCall
1037                 // _setInterfaceBeginAnnotationValue(info, value);
1038                 code.addLine(prefixTabs
1039                                 + "\t"
1040                                 + ShortComment("Store the value info into the current MethodCall"));
1041                 code.addLine(prefixTabs
1042                                 + "\t"
1043                                 + SpecNaming.SetInterfaceBeginAnnoValueFunc
1044                                 + Brace(SpecNaming.AnnoInterfaceInfoInst + ", "
1045                                                 + SpecNaming.InterfaceValueInst) + ";");
1046                 code.addLine("");
1047
1048                 // Return if necessary
1049                 if (!construct.getFunctionHeader().isReturnVoid())
1050                         code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");
1051                 code.addLine(prefixTabs + "}");
1052
1053                 return code;
1054         }
1055
1056         /**
1057          * <p>
1058          * Write a list of lines (as the whole of the file) to a file ---
1059          * newFileName. If that file does not exist, we create that file and then
1060          * write the lines.
1061          * </p>
1062          * 
1063          * @param newFileName
1064          *            The name of the file to be written
1065          * @param content
1066          *            The list of lines that as a whole become the content of the
1067          *            file
1068          */
1069         public static void write2File(String newFileName, ArrayList<String> content) {
1070                 File newFile = new File(newFileName);
1071                 newFile.getParentFile().mkdirs();
1072                 if (!newFile.exists()) {
1073                         try {
1074                                 newFile.createNewFile();
1075                         } catch (IOException e) {
1076                                 e.printStackTrace();
1077                         }
1078                 }
1079                 BufferedWriter bw = null;
1080                 try {
1081                         bw = new BufferedWriter(new FileWriter(newFile));
1082                         for (int i = 0; i < content.size(); i++) {
1083                                 bw.write(content.get(i) + "\n");
1084                         }
1085                         bw.flush();
1086                 } catch (IOException e) {
1087                         e.printStackTrace();
1088                 } finally {
1089                         if (bw != null)
1090                                 try {
1091                                         bw.close();
1092                                 } catch (IOException e) {
1093                                         e.printStackTrace();
1094                                 }
1095                 }
1096         }
1097 }