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("void _" + 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                                 code.addLine("}");
545                                 code.addLine("");
546
547                                 // Define @PreCondition
548                                 if (!construct.preCondition.isEmpty()) {
549                                         code.addLine(ShortComment("Define @"
550                                                         + SpecNaming.PreCondition + " for " + name));
551                                         code.addLine("bool _" + name + "_"
552                                                         + SpecNaming.PreCondition + "(" + SpecNaming.Method
553                                                         + " " + SpecNaming.Method1 + ") {");
554
555                                         // Initialize value struct fields
556                                         fieldsInit = GenerateInterfaceFieldsInitialization(
557                                                         SpecNaming.Method1, SpecNaming.InterfaceValueInst,
558                                                         construct);
559                                         fieldsInit.align(1);
560                                         code.addLines(fieldsInit);
561
562                                         construct.preCondition.align(1);
563                                         code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
564                                         code.addLines(construct.preCondition);
565
566                                         code.addLine("}");
567                                         code.addLine("");
568
569                                 }
570                                 // Define @PostCondition
571                                 if (!construct.postCondition.isEmpty()) {
572                                         code.addLine(ShortComment("Define @"
573                                                         + SpecNaming.PostCondition + " for " + name));
574                                         code.addLine("bool _" + name + "_"
575                                                         + SpecNaming.PostCondition + "("
576                                                         + SpecNaming.Method + " " + SpecNaming.Method1
577                                                         + ") {");
578
579                                         // Initialize value struct fields
580                                         fieldsInit = GenerateInterfaceFieldsInitialization(
581                                                         SpecNaming.Method1, SpecNaming.InterfaceValueInst,
582                                                         construct);
583                                         fieldsInit.align(1);
584                                         code.addLines(fieldsInit);
585
586                                         construct.postCondition.align(1);
587                                         code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
588                                         code.addLines(construct.postCondition);
589
590                                         code.addLine("}");
591                                         code.addLine("");
592                                 }
593                                 // Define @Print
594                                 if (!construct.print.isEmpty()) {
595                                         code.addLine(ShortComment("Define @"
596                                                         + SpecNaming.PrintValue + " for " + name));
597                                         code.addLine("void _" + name + "_" + SpecNaming.PrintValue
598                                                         + "(" + SpecNaming.Method + " "
599                                                         + SpecNaming.Method1 + ") {");
600                                         // Initialize value struct fields
601                                         fieldsInit = GenerateInterfaceFieldsInitialization(
602                                                         SpecNaming.Method1, SpecNaming.InterfaceValueInst,
603                                                         construct);
604                                         fieldsInit.align(1);
605                                         code.addLines(fieldsInit);
606
607                                         construct.print.align(1);
608                                         if (!construct.autoGenPrint)
609                                                 code.addLine(TabbedLine(ShortComment("Execute user-defined value printing code")));
610                                         else
611                                                 // Auto-generated the value printing function
612                                                 code.addLine(TabbedLine(ShortComment("Execute auto-generated value printing code")));
613                                         code.addLines(construct.print);
614
615                                         code.addLine("}");
616                                         code.addLine("");
617                                 }
618                         }
619                 }
620
621                 // Define INIT annotation instrumentation function
622                 code.addLine(ShortComment("Define INIT annotation instrumentation function"));
623                 code.addLine("void _createInitAnnotation() {");
624
625                 // Init commutativity rules
626                 code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
627                 code.addLine(TabbedLine(DeclareDefine("int",
628                                 SpecNaming.CommutativityRuleSizeInst,
629                                 Integer.toString(globalConstruct.commutativityRules.size()))));
630                 String tmp = SpecNaming.NewSize
631                                 + Brace(SpecNaming.CommutativityRule + ", sizeof"
632                                                 + Brace(SpecNaming.CommutativityRule) + " * "
633                                                 + SpecNaming.CommutativityRuleSizeInst);
634                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*"
635                                 + SpecNaming.CommutativityRuleInst, tmp)));
636                 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
637                         CommutativityRule rule = globalConstruct.commutativityRules
638                                         .get(i - 1);
639                         code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ")
640                                         + i));
641                         // new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
642                         // _Commutativity1_str, _checkCommutativity1)
643                         line = "new"
644                                         + Brace(" &" + SpecNaming.CommutativityRuleInst + "["
645                                                         + (i - 1) + "] ") + SpecNaming.CommutativityRule
646                                         + "(" + SpecNaming.AppendStr(rule.method1) + ", "
647                                         + SpecNaming.AppendStr(rule.method2) + ", "
648                                         + SpecNaming.AppendStr(SpecNaming.Commutativity + i) + ", "
649                                         + "_check" + SpecNaming.Commutativity + i + ");";
650                         code.addLine(TabbedLine(line));
651                 }
652
653                 // Initialize AnnoInit
654                 code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
655                 // AnnoInit *init = new AnnoInit(
656                 code.addLine(TabbedLine(SpecNaming.AnnoInit + " *"
657                                 + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit
658                                 + "("));
659                 // new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
660                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
661                                 + SpecNaming.AppendStr(SpecNaming.InitalState) + ", "
662                                 + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
663                                 + SpecNaming.InitalState.toLowerCase() + "),", 2));
664                 // new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
665                 line = "new " + SpecNaming.NamedFunction + "("
666                                 + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
667                                 + SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
668                 if (globalConstruct.finalState.isEmpty()) {
669                         line = line + SpecNaming.NullFunc + "),";
670                 } else {
671                         line = line + "_" + SpecNaming.FinalState.toUpperCase();
672                 }
673                 code.addLine(TabbedLine(line, 2));
674                 // new NamedFunction(_Copy_str, COPY, (void*) _copy),
675                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
676                                 + SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
677                                 + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
678                                 + SpecNaming.CopyState.toLowerCase() + "),", 2));
679                 // new NamedFunction(_Clear_str, CLEAR, (void*) _clear),
680                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
681                                 + SpecNaming.AppendStr(SpecNaming.ClearState) + ", "
682                                 + SpecNaming.ClearState.toUpperCase() + ", " + "(void*) _"
683                                 + SpecNaming.ClearState.toLowerCase() + "),", 2));
684                 // new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
685                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
686                                 + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
687                                 + SpecNaming.PrintStateType + ", " + "(void*) _"
688                                 + SpecNaming.PrintState.toLowerCase() + "),", 2));
689                 // commuteRules, CommuteRuleSize);
690                 code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
691                                 + SpecNaming.CommutativityRuleSizeInst + ");", 2));
692                 code.addLine("");
693
694                 // Declare StateFunctions map
695                 code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
696                 code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*"
697                                 + SpecNaming.StateFunctionsInst)));
698                 code.addLine("");
699
700                 // StateFunction for interface
701                 for (File file : interfaceListMap.keySet()) {
702                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
703                         for (InterfaceConstruct construct : list) {
704                                 String name = construct.getName();
705                                 code.addLine(TabbedLine(ShortComment("StateFunction for "
706                                                 + name)));
707                                 // stateFuncs = new StateFunctions(
708                                 code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
709                                                 + " = new " + SpecNaming.StateFunctions + "("));
710                                 // new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
711                                 // _ENQ_Transition),
712                                 // Transition
713                                 code.addLine(TabbedLine(
714                                                 "new "
715                                                                 + SpecNaming.NamedFunction
716                                                                 + "("
717                                                                 + SpecNaming.AppendStr(name + "_"
718                                                                                 + SpecNaming.Transition) + ", "
719                                                                 + SpecNaming.TransitionType + ", (void*) _"
720                                                                 + name + "_" + SpecNaming.Transition + "),", 2));
721                                 // PreCondition
722                                 line = "new "
723                                                 + SpecNaming.NamedFunction
724                                                 + "("
725                                                 + SpecNaming.AppendStr(name + "_"
726                                                                 + SpecNaming.PreCondition) + ", "
727                                                 + SpecNaming.PreConditionType + ", (void*) ";
728                                 if (construct.preCondition.isEmpty()) {
729                                         line = line + SpecNaming.NullFunc + "),";
730                                 } else {
731                                         line = line + "_" + name + "_" + SpecNaming.PreCondition
732                                                         + "),";
733                                 }
734                                 code.addLine(TabbedLine(line, 2));
735                                 // PostCondition
736                                 line = "new "
737                                                 + SpecNaming.NamedFunction
738                                                 + "("
739                                                 + SpecNaming.AppendStr(name + "_"
740                                                                 + SpecNaming.PostCondition) + ", "
741                                                 + SpecNaming.PostConditionType + ", (void*) ";
742                                 if (construct.postCondition.isEmpty()) {
743                                         line = line + SpecNaming.NullFunc + "),";
744                                 } else {
745                                         line = line + "_" + name + "_" + SpecNaming.PostCondition
746                                                         + "),";
747                                 }
748                                 code.addLine(TabbedLine(line, 2));
749                                 // Print (PrintValue
750                                 line = "new "
751                                                 + SpecNaming.NamedFunction
752                                                 + "("
753                                                 + SpecNaming.AppendStr(name + "_"
754                                                                 + SpecNaming.PrintValue) + ", "
755                                                 + SpecNaming.PrintValueType + ", (void*) ";
756                                 if (construct.print.isEmpty()) {
757                                         line = line + SpecNaming.NullFunc + ")";
758                                 } else {
759                                         line = line + "_" + name + "_" + SpecNaming.PrintValue
760                                                         + ")";
761                                 }
762                                 code.addLine(TabbedLine(line, 2));
763                                 code.addLine(TabbedLine(");"));
764
765                                 // init->addInterfaceFunctions(_ENQ_str, stateFuncs);
766                                 code.addLine(TabbedLine(SpecNaming.AnnoInitInst
767                                                 + "->"
768                                                 + SpecNaming.AddInterfaceFunctions
769                                                 + Brace(SpecNaming.AppendStr(name) + ", "
770                                                                 + SpecNaming.StateFunctionsInst) + ";"));
771                                 code.addLine("");
772                         }
773                 }
774
775                 // Create and instrument with the INIT annotation
776                 code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
777                 // cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
778                 code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc
779                                 + Brace(SpecNaming.SPEC_ANALYSIS
780                                                 + ", new "
781                                                 + SpecNaming.SpecAnnotation
782                                                 + Brace(SpecNaming.AnnoTypeInit + ", "
783                                                                 + SpecNaming.AnnoInitInst)) + ";"));
784
785                 code.addLine("}");
786                 code.addLine("");
787
788                 return code;
789         }
790
791         /**
792          * <p>
793          * This function generates a list of lines that initialize the fields of the
794          * global state struct. See below.
795          * </p>
796          * 
797          * <p>
798          * <code>
799          * StateStruct *state = (StateStruct*) _M->state;
800          * <br>
801          * IntList * q = state->q;
802          * </code>
803          * </p>
804          * 
805          * <p>
806          * In this example, _M --> methodInst, state --> inst.
807          * </p>
808          * 
809          * @param methodInst
810          *            See description
811          * @param inst
812          *            See description
813          * @param construct
814          *            The global state construct
815          * @return The generated code
816          */
817         public static Code GenerateStateFieldsInitialization(String methodInst,
818                         String inst, GlobalConstruct construct) {
819                 Code res = new Code();
820                 res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct
821                                 + " fields"));
822                 res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst, "("
823                                 + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
824                 for (VariableDeclaration decl : construct.declState) {
825                         res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
826                                         + decl.name));
827                 }
828                 return res;
829         }
830
831         /**
832          * <p>
833          * This function generates a list of lines that initialize the fields of a
834          * specific interface struct. See below.
835          * </p>
836          * 
837          * <p>
838          * <code>
839          * ENQ *info = (ENQ*) _M->value;
840          * <br>
841          * IntList * q = info->q;
842          * </code>
843          * </p>
844          * 
845          * <p>
846          * In this example, ENQ --> structType, _M --> methodInst, info --> inst
847          * </p>
848          * 
849          * @param methodInst
850          *            See description
851          * @param inst
852          *            See description
853          * @param construct
854          *            The corresponding interface construct
855          * @return The generated code
856          */
857         public static Code GenerateInterfaceFieldsInitialization(String methodInst,
858                         String inst, InterfaceConstruct construct) {
859                 Code res = new Code();
860                 String name = construct.getName();
861                 res.addLine(ShortComment("Initialize fields for " + name));
862                 // The very first assignment "
863                 res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) "
864                                 + methodInst + "->" + SpecNaming.MethodValueField));
865                 // Don't leave out the RET field
866                 if (!construct.getFunctionHeader().isReturnVoid()) {
867                         res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
868                                         SpecNaming.RET, inst + "->" + SpecNaming.RET));
869                 }
870                 // For arguments
871                 for (VariableDeclaration decl : construct.getFunctionHeader().args) {
872                         res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
873                                         + decl.name));
874                 }
875                 return res;
876         }
877
878         /**
879          * <p>
880          * This function generates the code to be inserted right after the ordering
881          * point construct (instrumentation code)
882          * </p>
883          * 
884          * @param construct
885          *            The corresponding ordering point construct
886          * @return The generated code
887          */
888         public static Code Generate4OPConstruct(OPConstruct construct) {
889                 Code code = new Code();
890                 String curLine = construct.annotation;
891                 String label = construct.label;
892                 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
893                 if (!construct.condition.equals("true")) {
894                         code.addLine(prefixTabs + "if (" + construct.condition + ")");
895                         prefixTabs = prefixTabs + "\t";
896                 }
897
898                 switch (construct.type) {
899                 case OPDefine:
900                         code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
901                         break;
902                 case PotentialOP:
903                         code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
904                                         + "(" + SpecNaming.AppendStr(label) + ");");
905                         break;
906                 case OPCheck:
907                         code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "("
908                                         + SpecNaming.AppendStr(label) + ");");
909                         break;
910                 case OPClear:
911                         code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();");
912                         break;
913                 case OPClearDefine:
914                         code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
915                                         + "();");
916                         break;
917                 default:
918                         break;
919                 }
920                 return code;
921         }
922
923         /**
924          * <p>
925          * This function generates the code to be inserted right after the entry
926          * construct (instrumentation code)
927          * </p>
928          * 
929          * @param construct
930          *            The corresponding entry construct
931          * @return
932          */
933         public static Code Generate4Entry(EntryConstruct construct) {
934                 Code res = new Code();
935                 String curLine = construct.annotation;
936                 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
937                 // _createInitAnnotation();
938                 res.addLine(prefixTabs + SpecNaming.CreateInitAnnoFunc + "();");
939                 return res;
940         }
941
942         /**
943          * <p>
944          * This function generates the code to be inserted right after the "@Define"
945          * construct (instrumentation code)
946          * </p>
947          * 
948          * @param construct
949          *            The corresponding entry construct
950          * @return
951          */
952         public static Code Generate4Define(DefineConstruct construct) {
953                 Code code = new Code();
954                 code.addLine("");
955                 code.addLine("/**********    User-defined code in annotation (BEGIN)    **********/");
956                 code.addLines(construct.code);
957                 code.addLine("/**********    User-defined code in annotation (END)    **********/");
958                 return code;
959         }
960
961         /**
962          * <p>
963          * This function generates the new interface wrapper code to be inserted
964          * right after the end of the interface definition
965          * </p>
966          * 
967          * @param construct
968          *            The corresponding interface construct
969          * @return The generated code
970          */
971         public static Code GenerateInterfaceWrapper(InterfaceConstruct construct) {
972                 Code code = new Code();
973
974                 String name = construct.getName();
975                 String beginLine = construct.getFunctionHeader().getHeaderLine();
976                 Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
977                 Matcher matcherSpace = regexpSpace.matcher(beginLine);
978                 String prefixTabs = "";
979                 if (matcherSpace.find())
980                         prefixTabs = matcherSpace.group(1);
981
982                 // Add one line to separate
983                 code.addLine("");
984                 code.addLine(prefixTabs
985                                 + ShortComment("Generated wrapper interface for " + name));
986                 if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
987                                                                                         // of the line
988                         code.addLine(beginLine + " {");
989                 } else {
990                         code.addLine(beginLine);
991                 }
992                 // Instrument with the INTERFACE_BEGIN annotations
993                 code.addLine(prefixTabs
994                                 + "\t"
995                                 + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
996                 // CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
997                 code.addLine(prefixTabs
998                                 + "\t"
999                                 + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
1000                                                 + SpecNaming.AnnoInterfaceInfoInst,
1001                                                 SpecNaming.CreateInterfaceBeginAnnoFunc
1002                                                                 + Brace(SpecNaming.AppendStr(name))));
1003                 // Call the actual function
1004                 code.addLine(prefixTabs + "\t"
1005                                 + ShortComment("Call the actual function"));
1006                 // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
1007                 code.addLine(prefixTabs + "\t"
1008                                 + construct.getFunctionHeader().getRenamedCall() + ";");
1009                 code.addLine("");
1010
1011                 // Initialize the value struct
1012                 code.addLine(prefixTabs + "\t"
1013                                 + ShortComment("Initialize the value struct"));
1014                 // The very first assignment "
1015                 code.addLine(prefixTabs
1016                                 + "\t"
1017                                 + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst,
1018                                                 SpecNaming.New + Brace(name)));
1019                 // Don't leave out the RET field
1020                 if (!construct.getFunctionHeader().isReturnVoid())
1021                         code.addLine(prefixTabs
1022                                         + "\t"
1023                                         + AssignToPtr(SpecNaming.InterfaceValueInst,
1024                                                         SpecNaming.RET, SpecNaming.RET));
1025                 // For arguments
1026                 for (VariableDeclaration decl : construct.getFunctionHeader().args)
1027                         code.addLine(prefixTabs
1028                                         + "\t"
1029                                         + AssignToPtr(SpecNaming.InterfaceValueInst, decl.name,
1030                                                         decl.name));
1031                 code.addLine("");
1032
1033                 // Store the value info into the current MethodCall
1034                 // _setInterfaceBeginAnnotationValue(info, value);
1035                 code.addLine(prefixTabs
1036                                 + "\t"
1037                                 + ShortComment("Store the value info into the current MethodCall"));
1038                 code.addLine(prefixTabs
1039                                 + "\t"
1040                                 + SpecNaming.SetInterfaceBeginAnnoValueFunc
1041                                 + Brace(SpecNaming.AnnoInterfaceInfoInst + ", "
1042                                                 + SpecNaming.InterfaceValueInst) + ";");
1043                 code.addLine("");
1044
1045                 // Return if necessary
1046                 if (!construct.getFunctionHeader().isReturnVoid())
1047                         code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");
1048                 code.addLine(prefixTabs + "}");
1049
1050                 return code;
1051         }
1052
1053         /**
1054          * <p>
1055          * Write a list of lines (as the whole of the file) to a file ---
1056          * newFileName. If that file does not exist, we create that file and then
1057          * write the lines.
1058          * </p>
1059          * 
1060          * @param newFileName
1061          *            The name of the file to be written
1062          * @param content
1063          *            The list of lines that as a whole become the content of the
1064          *            file
1065          */
1066         public static void write2File(String newFileName, ArrayList<String> content) {
1067                 File newFile = new File(newFileName);
1068                 newFile.getParentFile().mkdirs();
1069                 if (!newFile.exists()) {
1070                         try {
1071                                 newFile.createNewFile();
1072                         } catch (IOException e) {
1073                                 e.printStackTrace();
1074                         }
1075                 }
1076                 BufferedWriter bw = null;
1077                 try {
1078                         bw = new BufferedWriter(new FileWriter(newFile));
1079                         for (int i = 0; i < content.size(); i++) {
1080                                 bw.write(content.get(i) + "\n");
1081                         }
1082                         bw.flush();
1083                 } catch (IOException e) {
1084                         e.printStackTrace();
1085                 } finally {
1086                         if (bw != null)
1087                                 try {
1088                                         bw.close();
1089                                 } catch (IOException e) {
1090                                         e.printStackTrace();
1091                                 }
1092                 }
1093         }
1094 }