add destructors
[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
252                 // Add auto-generated comments
253                 code.addLine("/**");
254                 code.addLine(TabbedLine("This is an implementation file auto-generated by CDSSpec compiler to"));
255                 code.addLine(TabbedLine("instrument your benchmark for CDSSpec checker to check. Currently we require"));
256                 code.addLine(TabbedLine("a C++ compiler that supports C++11."));
257                 code.addLine("*/");
258                 code.addLine("");
259
260                 code.addLine("#include " + SpecNaming.CDSSpecGeneratedHeader);
261                 code.addLine("#include " + SpecNaming.CDSANNOTATE);
262                 code.addLine("#include " + SpecNaming.SPEC_COMMON);
263                 code.addLine("#include " + SpecNaming.METHODCALL);
264                 code.addLine("#include " + SpecNaming.CDSSPEC);
265                 code.addLine("#include " + SpecNaming.SPECANNOTATION);
266                 code.addLine("");
267                 code.addLine("");
268
269                 // Declare customized StateStruct
270                 code.addLine(ShortComment("Declare customized StateStruct"));
271                 code.addLine("typedef struct " + SpecNaming.StateStruct + " {");
272                 for (VariableDeclaration decl : globalConstruct.declState) {
273                         code.addLine(TabbedLine(Declare(decl)));
274                 }
275                 code.addLine("");
276                 // Define state destructor
277                 code.addLine(TabbedLine(ShortComment("Define state destructor")));
278                 code.addLine(TabbedLine("~" + SpecNaming.StateStruct + "() {"));
279                 if (!globalConstruct.autoGenClear) {
280                         code.addLine(TabbedLine(
281                                         ShortComment("Execute user-defined state clear code"), 2));
282                 } else {
283                         code.addLine(TabbedLine(
284                                         ShortComment("Execute auto-generated state clear code"), 2));
285                 }
286                 globalConstruct.clearState.align(2);
287                 code.addLines(globalConstruct.clearState);
288                 code.addLine(TabbedLine("}"));
289                 code.addLine("");
290
291                 code.addLine(TabbedLine("SNAPSHOTALLOC"));
292                 code.addLine("");
293                 code.addLine("} " + SpecNaming.StateStruct + ";");
294                 code.addLine("");
295                 code.addLine("");
296
297                 code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
298                 code.addLine(ShortComment("A special empty string"));
299                 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,
300                                 "\"\""));
301                 code.addLine("");
302
303                 // Interface name strings
304                 code.addLine(ShortComment("Interface name strings"));
305                 for (File file : interfaceListMap.keySet()) {
306                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
307                         for (InterfaceConstruct construct : list) {
308                                 String name = construct.getName();
309                                 code.addLine(DeclareDefine(SpecNaming.CString,
310                                                 SpecNaming.AppendStr(name), Quote(name)));
311                         }
312                 }
313                 code.addLine("");
314
315                 // Commutativity rule strings
316                 code.addLine(ShortComment("Commutativity rule strings"));
317                 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
318                         CommutativityRule rule = globalConstruct.commutativityRules
319                                         .get(i - 1);
320                         code.addLine(DeclareDefine(SpecNaming.CString,
321                                         SpecNaming.AppendStr(SpecNaming.Commutativity + i),
322                                         Quote(rule.toString())));
323                 }
324                 code.addLine("");
325
326                 // Ordering points label strings
327                 code.addLine(ShortComment("Ordering points label strings"));
328                 for (String label : OPLabelSet) {
329                         code.addLine(DeclareDefine(SpecNaming.CString,
330                                         SpecNaming.AppendStr(label), Quote(label)));
331                 }
332                 code.addLine("");
333
334                 // Special function name strings
335                 code.addLine(ShortComment("Special function name strings"));
336                 code.addLine(DeclareDefine(SpecNaming.CString,
337                                 SpecNaming.AppendStr(SpecNaming.InitalState), Quote("_"
338                                                 + SpecNaming.InitalState.toLowerCase())));
339                 code.addLine(DeclareDefine(SpecNaming.CString,
340                                 SpecNaming.AppendStr(SpecNaming.CopyState), Quote("_"
341                                                 + SpecNaming.CopyState.toLowerCase())));
342                 code.addLine(DeclareDefine(SpecNaming.CString,
343                                 SpecNaming.AppendStr(SpecNaming.ClearState), Quote("_"
344                                                 + SpecNaming.ClearState.toLowerCase())));
345                 code.addLine(DeclareDefine(SpecNaming.CString,
346                                 SpecNaming.AppendStr(SpecNaming.FinalState), Quote("_"
347                                                 + SpecNaming.FinalState.toLowerCase())));
348                 code.addLine(DeclareDefine(SpecNaming.CString,
349                                 SpecNaming.AppendStr(SpecNaming.PrintState), Quote("_"
350                                                 + SpecNaming.PrintState.toLowerCase())));
351                 code.addLine("");
352
353                 // Interface name strings
354                 for (File file : interfaceListMap.keySet()) {
355                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
356                         for (InterfaceConstruct construct : list) {
357                                 String name = construct.getName();
358                                 code.addLine(ShortComment(name + " function strings"));
359                                 // Transition
360                                 String tmpFunc = name + "_" + SpecNaming.Transition;
361                                 code.addLine(DeclareDefine(SpecNaming.CString,
362                                                 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
363                                 // PreCondition
364                                 tmpFunc = name + "_" + SpecNaming.PreCondition;
365                                 if (!construct.preCondition.isEmpty())
366                                         code.addLine(DeclareDefine(SpecNaming.CString,
367                                                         SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
368                                 else
369                                         code.addLine(DeclareDefine(SpecNaming.CString,
370                                                         SpecNaming.AppendStr(tmpFunc),
371                                                         SpecNaming.EmptyCString));
372                                 // PostCondition
373                                 tmpFunc = name + "_" + SpecNaming.PostCondition;
374                                 if (!construct.postCondition.isEmpty())
375                                         code.addLine(DeclareDefine(SpecNaming.CString,
376                                                         SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
377                                 else
378                                         code.addLine(DeclareDefine(SpecNaming.CString,
379                                                         SpecNaming.AppendStr(tmpFunc),
380                                                         SpecNaming.EmptyCString));
381                                 // Print
382                                 tmpFunc = name + "_" + SpecNaming.PrintValue;
383                                 if (!construct.print.isEmpty())
384                                         code.addLine(DeclareDefine(SpecNaming.CString,
385                                                         SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
386                                 else
387                                         code.addLine(DeclareDefine(SpecNaming.CString,
388                                                         SpecNaming.AppendStr(tmpFunc),
389                                                         SpecNaming.EmptyCString));
390                                 code.addLine("");
391                         }
392                 }
393
394                 // Define @Initial
395                 code.addLine(ShortComment("Define @" + SpecNaming.InitalState));
396                 code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
397                                 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
398                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
399                                 + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
400                 // Define macros
401                 for (VariableDeclaration decl : globalConstruct.declState) {
402                         code.addLine(TabbedLine("#define " + decl.name + " "
403                                         + SpecNaming.StateInst + "->" + decl.name));
404                 }
405                 if (!globalConstruct.autoGenInitial)
406                         code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
407                 else
408                         // Auto-generated the initialization function
409                         code.addLine(TabbedLine(ShortComment("Auto-generated state intialization code")));
410                 // Align the code with one tab
411                 globalConstruct.initState.align(1);
412                 code.addLines(globalConstruct.initState);
413                 // Undefine macros
414                 for (VariableDeclaration decl : globalConstruct.declState) {
415                         code.addLine(TabbedLine("#undef " + decl.name));
416                 }
417                 code.addLine("");
418                 code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1,
419                                 SpecNaming.StateInst, SpecNaming.StateInst)));
420                 code.addLine("}");
421                 code.addLine("");
422
423                 // Define @Copy
424                 code.addLine(ShortComment("Define @" + SpecNaming.CopyState));
425                 code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
426                                 + SpecNaming.Method + " " + "dest, " + SpecNaming.Method
427                                 + " src) {");
428                 // StateStruct *OLD = (StateStruct*) src->state;
429                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
430                                 + SpecNaming.OldStateInst, Brace(SpecNaming.StateStruct + "*")
431                                 + " src->" + SpecNaming.StateInst)));
432                 // StateStruct *NEW = new StateStruct;
433                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
434                                 + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
435                 if (!globalConstruct.autoGenCopy)
436                         code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
437                 else
438                         // Auto-generated the copy function
439                         code.addLine(TabbedLine(ShortComment("Auto-generated state copy statements")));
440                 globalConstruct.copyState.align(1);
441                 code.addLines(globalConstruct.copyState);
442                 code.addLine("");
443                 code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst,
444                                 SpecNaming.NewStateInst)));
445                 code.addLine("}");
446                 code.addLine("");
447
448                 // Define @Clear
449                 code.addLine(ShortComment("Define @" + SpecNaming.ClearState));
450                 code.addLine("void _" + SpecNaming.ClearState.toLowerCase() + "("
451                                 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
452                 // Retrieve the state
453                 code.addLine(TabbedLine(ShortComment("Retrieve the state")));
454                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
455                                 + SpecNaming.StateInst, "(" + SpecNaming.StateStruct + "*) "
456                                 + SpecNaming.Method1 + "->state")));
457                 // Explicitly call the state destructor
458                 code.addLine(TabbedLine(ShortComment("Explicitly call the state destructor")));
459                 code.addLine(TabbedLine("delete " + SpecNaming.StateInst + ";"));
460                 code.addLine("}");
461                 code.addLine("");
462
463                 // Define @Print
464                 if (!globalConstruct.printState.isEmpty()) {
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                         Code fieldsInit = GenerateStateFieldsInitialization(
471                                         SpecNaming.Method1, 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
488                 // Define @Commutativity
489                 code.addLine(ShortComment("Define commutativity checking functions"));
490                 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
491                         CommutativityRule rule = globalConstruct.commutativityRules
492                                         .get(i - 1);
493                         code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
494                                         + SpecNaming.Method + " m1, " + SpecNaming.Method
495                                         + " m2) {");
496                         // if (m1->name == _ENQ_str && m2->name == _DEQ_str) {
497                         code.addLine(TabbedLine("if (m1->name == "
498                                         + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
499                                         + SpecNaming.AppendStr(rule.method2) + ") {"));
500                         // Initialize M1 & M2 in commutativity rule
501                         // e.g. ENQ *M1 = (ENQ*) m1->value;
502                         code.addLine(TabbedLine(
503                                         DeclareDefine(rule.method1, "*M1", "(" + rule.method1
504                                                         + "*) m1->value"), 2));
505                         code.addLine(TabbedLine(
506                                         DeclareDefine(rule.method2, "*M2", "(" + rule.method2
507                                                         + "*) m2->value"), 2));
508                         code.addLine(TabbedLine("return " + rule.condition + ";", 2));
509                         code.addLine(TabbedLine("}"));
510                         code.addLine(TabbedLine("return false;"));
511
512                         code.addLine("}");
513                         code.addLine("");
514                 }
515
516                 // Define customized interface functions
517                 for (File file : interfaceListMap.keySet()) {
518                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
519                         for (InterfaceConstruct construct : list) {
520                                 Code fieldsInit = null;
521
522                                 // Define interface functions
523                                 String name = construct.getName();
524                                 code.addLine("/**********    " + name
525                                                 + " functions    **********/");
526                                 // Define @Transition for INTERFACE
527                                 code.addLine(ShortComment("Define @" + SpecNaming.Transition
528                                                 + " for " + name));
529                                 code.addLine("void _" + name + "_" + SpecNaming.Transition
530                                                 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
531                                                 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
532                                                 + ") {");
533
534                                 // Initialize value struct fields
535                                 fieldsInit = GenerateInterfaceFieldsInitialization(
536                                                 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
537                                                 construct);
538                                 fieldsInit.align(1);
539                                 code.addLines(fieldsInit);
540
541                                 construct.transition.align(1);
542                                 code.addLine(TabbedLine(ShortComment("Execute Transition")));
543                                 code.addLines(construct.transition);
544
545                                 code.addLine("}");
546                                 code.addLine("");
547
548                                 // Define @PreCondition
549                                 if (!construct.preCondition.isEmpty()) {
550                                         code.addLine(ShortComment("Define @"
551                                                         + SpecNaming.PreCondition + " for " + name));
552                                         code.addLine("bool _" + name + "_"
553                                                         + SpecNaming.PreCondition + "(" + SpecNaming.Method
554                                                         + " " + SpecNaming.Method1 + ") {");
555
556                                         // Initialize value struct fields
557                                         fieldsInit = GenerateInterfaceFieldsInitialization(
558                                                         SpecNaming.Method1, SpecNaming.InterfaceValueInst,
559                                                         construct);
560                                         fieldsInit.align(1);
561                                         code.addLines(fieldsInit);
562
563                                         construct.preCondition.align(1);
564                                         code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
565                                         code.addLines(construct.preCondition);
566
567                                         code.addLine("}");
568                                         code.addLine("");
569
570                                 }
571                                 // Define @PostCondition
572                                 if (!construct.postCondition.isEmpty()) {
573                                         code.addLine(ShortComment("Define @"
574                                                         + SpecNaming.PostCondition + " for " + name));
575                                         code.addLine("bool _" + name + "_"
576                                                         + SpecNaming.PostCondition + "("
577                                                         + SpecNaming.Method + " " + SpecNaming.Method1
578                                                         + ") {");
579
580                                         // Initialize value struct fields
581                                         fieldsInit = GenerateInterfaceFieldsInitialization(
582                                                         SpecNaming.Method1, SpecNaming.InterfaceValueInst,
583                                                         construct);
584                                         fieldsInit.align(1);
585                                         code.addLines(fieldsInit);
586
587                                         construct.postCondition.align(1);
588                                         code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
589                                         code.addLines(construct.postCondition);
590
591                                         code.addLine("}");
592                                         code.addLine("");
593                                 }
594                                 // Define @Print
595                                 if (!construct.print.isEmpty()) {
596                                         code.addLine(ShortComment("Define @"
597                                                         + SpecNaming.PrintValue + " for " + name));
598                                         code.addLine("void _" + name + "_" + SpecNaming.PrintValue
599                                                         + "(" + SpecNaming.Method + " "
600                                                         + SpecNaming.Method1 + ") {");
601                                         // Initialize value struct fields
602                                         fieldsInit = GenerateInterfaceFieldsInitialization(
603                                                         SpecNaming.Method1, SpecNaming.InterfaceValueInst,
604                                                         construct);
605                                         fieldsInit.align(1);
606                                         code.addLines(fieldsInit);
607
608                                         construct.print.align(1);
609                                         if (!construct.autoGenPrint)
610                                                 code.addLine(TabbedLine(ShortComment("Execute user-defined value printing code")));
611                                         else
612                                                 // Auto-generated the value printing function
613                                                 code.addLine(TabbedLine(ShortComment("Execute auto-generated value printing code")));
614                                         code.addLines(construct.print);
615
616                                         code.addLine("}");
617                                         code.addLine("");
618                                 }
619                         }
620                 }
621
622                 // Define INIT annotation instrumentation function
623                 code.addLine(ShortComment("Define INIT annotation instrumentation function"));
624                 code.addLine("void _createInitAnnotation() {");
625
626                 // Init commutativity rules
627                 code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
628                 code.addLine(TabbedLine(DeclareDefine("int",
629                                 SpecNaming.CommutativityRuleSizeInst,
630                                 Integer.toString(globalConstruct.commutativityRules.size()))));
631                 String tmp = SpecNaming.NewSize
632                                 + Brace(SpecNaming.CommutativityRule + ", sizeof"
633                                                 + Brace(SpecNaming.CommutativityRule) + " * "
634                                                 + SpecNaming.CommutativityRuleSizeInst);
635                 code.addLine(TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*"
636                                 + SpecNaming.CommutativityRuleInst, tmp)));
637                 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
638                         CommutativityRule rule = globalConstruct.commutativityRules
639                                         .get(i - 1);
640                         code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ")
641                                         + i));
642                         // new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
643                         // _Commutativity1_str, _checkCommutativity1)
644                         line = "new"
645                                         + Brace(" &" + SpecNaming.CommutativityRuleInst + "["
646                                                         + (i - 1) + "] ") + SpecNaming.CommutativityRule
647                                         + "(" + SpecNaming.AppendStr(rule.method1) + ", "
648                                         + SpecNaming.AppendStr(rule.method2) + ", "
649                                         + SpecNaming.AppendStr(SpecNaming.Commutativity + i) + ", "
650                                         + "_check" + SpecNaming.Commutativity + i + ");";
651                         code.addLine(TabbedLine(line));
652                 }
653
654                 // Initialize AnnoInit
655                 code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
656                 // AnnoInit *init = new AnnoInit(
657                 code.addLine(TabbedLine(SpecNaming.AnnoInit + " *"
658                                 + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit
659                                 + "("));
660                 // new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
661                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
662                                 + SpecNaming.AppendStr(SpecNaming.InitalState) + ", "
663                                 + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
664                                 + SpecNaming.InitalState.toLowerCase() + "),", 2));
665                 // new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
666                 line = "new " + SpecNaming.NamedFunction + "("
667                                 + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
668                                 + SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
669                 if (globalConstruct.finalState.isEmpty()) {
670                         line = line + SpecNaming.NullFunc + "),";
671                 } else {
672                         line = line + "_" + SpecNaming.FinalState.toUpperCase();
673                 }
674                 code.addLine(TabbedLine(line, 2));
675                 // new NamedFunction(_Copy_str, COPY, (void*) _copy),
676                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
677                                 + SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
678                                 + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
679                                 + SpecNaming.CopyState.toLowerCase() + "),", 2));
680                 // new NamedFunction(_Clear_str, CLEAR, (void*) _clear),
681                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
682                                 + SpecNaming.AppendStr(SpecNaming.ClearState) + ", "
683                                 + SpecNaming.ClearState.toUpperCase() + ", " + "(void*) _"
684                                 + SpecNaming.ClearState.toLowerCase() + "),", 2));
685                 // new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
686                 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
687                                 + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
688                                 + SpecNaming.PrintStateType + ", " + "(void*) _"
689                                 + SpecNaming.PrintState.toLowerCase() + "),", 2));
690                 // commuteRules, CommuteRuleSize);
691                 code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
692                                 + SpecNaming.CommutativityRuleSizeInst + ");", 2));
693                 code.addLine("");
694
695                 // Declare StateFunctions map
696                 code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
697                 code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*"
698                                 + SpecNaming.StateFunctionsInst)));
699                 code.addLine("");
700
701                 // StateFunction for interface
702                 for (File file : interfaceListMap.keySet()) {
703                         ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
704                         for (InterfaceConstruct construct : list) {
705                                 String name = construct.getName();
706                                 code.addLine(TabbedLine(ShortComment("StateFunction for "
707                                                 + name)));
708                                 // stateFuncs = new StateFunctions(
709                                 code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
710                                                 + " = new " + SpecNaming.StateFunctions + "("));
711                                 // new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
712                                 // _ENQ_Transition),
713                                 // Transition
714                                 code.addLine(TabbedLine(
715                                                 "new "
716                                                                 + SpecNaming.NamedFunction
717                                                                 + "("
718                                                                 + SpecNaming.AppendStr(name + "_"
719                                                                                 + SpecNaming.Transition) + ", "
720                                                                 + SpecNaming.TransitionType + ", (void*) _"
721                                                                 + name + "_" + SpecNaming.Transition + "),", 2));
722                                 // PreCondition
723                                 line = "new "
724                                                 + SpecNaming.NamedFunction
725                                                 + "("
726                                                 + SpecNaming.AppendStr(name + "_"
727                                                                 + SpecNaming.PreCondition) + ", "
728                                                 + SpecNaming.PreConditionType + ", (void*) ";
729                                 if (construct.preCondition.isEmpty()) {
730                                         line = line + SpecNaming.NullFunc + "),";
731                                 } else {
732                                         line = line + "_" + name + "_" + SpecNaming.PreCondition
733                                                         + "),";
734                                 }
735                                 code.addLine(TabbedLine(line, 2));
736                                 // PostCondition
737                                 line = "new "
738                                                 + SpecNaming.NamedFunction
739                                                 + "("
740                                                 + SpecNaming.AppendStr(name + "_"
741                                                                 + SpecNaming.PostCondition) + ", "
742                                                 + SpecNaming.PostConditionType + ", (void*) ";
743                                 if (construct.postCondition.isEmpty()) {
744                                         line = line + SpecNaming.NullFunc + "),";
745                                 } else {
746                                         line = line + "_" + name + "_" + SpecNaming.PostCondition
747                                                         + "),";
748                                 }
749                                 code.addLine(TabbedLine(line, 2));
750                                 // Print (PrintValue
751                                 line = "new "
752                                                 + SpecNaming.NamedFunction
753                                                 + "("
754                                                 + SpecNaming.AppendStr(name + "_"
755                                                                 + SpecNaming.PrintValue) + ", "
756                                                 + SpecNaming.PrintValueType + ", (void*) ";
757                                 if (construct.print.isEmpty()) {
758                                         line = line + SpecNaming.NullFunc + ")";
759                                 } else {
760                                         line = line + "_" + name + "_" + SpecNaming.PrintValue
761                                                         + ")";
762                                 }
763                                 code.addLine(TabbedLine(line, 2));
764                                 code.addLine(TabbedLine(");"));
765
766                                 // init->addInterfaceFunctions(_ENQ_str, stateFuncs);
767                                 code.addLine(TabbedLine(SpecNaming.AnnoInitInst
768                                                 + "->"
769                                                 + SpecNaming.AddInterfaceFunctions
770                                                 + Brace(SpecNaming.AppendStr(name) + ", "
771                                                                 + SpecNaming.StateFunctionsInst) + ";"));
772                                 code.addLine("");
773                         }
774                 }
775
776                 // Create and instrument with the INIT annotation
777                 code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
778                 // cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
779                 code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc
780                                 + Brace(SpecNaming.SPEC_ANALYSIS
781                                                 + ", new "
782                                                 + SpecNaming.SpecAnnotation
783                                                 + Brace(SpecNaming.AnnoTypeInit + ", "
784                                                                 + SpecNaming.AnnoInitInst)) + ";"));
785
786                 code.addLine("}");
787                 code.addLine("");
788
789                 return code;
790         }
791
792         /**
793          * <p>
794          * This function generates a list of lines that initialize the fields of the
795          * global state struct. See below.
796          * </p>
797          * 
798          * <p>
799          * <code>
800          * StateStruct *state = (StateStruct*) _M->state;
801          * <br>
802          * IntList * q = state->q;
803          * </code>
804          * </p>
805          * 
806          * <p>
807          * In this example, _M --> methodInst, state --> inst.
808          * </p>
809          * 
810          * @param methodInst
811          *            See description
812          * @param inst
813          *            See description
814          * @param construct
815          *            The global state construct
816          * @return The generated code
817          */
818         public static Code GenerateStateFieldsInitialization(String methodInst,
819                         String inst, GlobalConstruct construct) {
820                 Code res = new Code();
821                 res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct
822                                 + " fields"));
823                 res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst, "("
824                                 + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
825                 for (VariableDeclaration decl : construct.declState) {
826                         res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
827                                         + decl.name));
828                 }
829                 return res;
830         }
831
832         /**
833          * <p>
834          * This function generates a list of lines that initialize the fields of a
835          * specific interface struct. See below.
836          * </p>
837          * 
838          * <p>
839          * <code>
840          * ENQ *info = (ENQ*) _M->value;
841          * <br>
842          * IntList * q = info->q;
843          * </code>
844          * </p>
845          * 
846          * <p>
847          * In this example, ENQ --> structType, _M --> methodInst, info --> inst
848          * </p>
849          * 
850          * @param methodInst
851          *            See description
852          * @param inst
853          *            See description
854          * @param construct
855          *            The corresponding interface construct
856          * @return The generated code
857          */
858         public static Code GenerateInterfaceFieldsInitialization(String methodInst,
859                         String inst, InterfaceConstruct construct) {
860                 Code res = new Code();
861                 String name = construct.getName();
862                 res.addLine(ShortComment("Initialize fields for " + name));
863                 // The very first assignment "
864                 res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) "
865                                 + methodInst + "->" + SpecNaming.MethodValueField));
866                 // Don't leave out the RET field
867                 if (!construct.getFunctionHeader().isReturnVoid()) {
868                         res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
869                                         SpecNaming.RET, inst + "->" + SpecNaming.RET));
870                 }
871                 // For arguments
872                 for (VariableDeclaration decl : construct.getFunctionHeader().args) {
873                         res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
874                                         + decl.name));
875                 }
876                 return res;
877         }
878
879         /**
880          * <p>
881          * This function generates the code to be inserted right after the ordering
882          * point construct (instrumentation code)
883          * </p>
884          * 
885          * @param construct
886          *            The corresponding ordering point construct
887          * @return The generated code
888          */
889         public static Code Generate4OPConstruct(OPConstruct construct) {
890                 Code code = new Code();
891                 String curLine = construct.annotation;
892                 String label = construct.label;
893                 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
894                 if (!construct.condition.equals("true")) {
895                         code.addLine(prefixTabs + "if (" + construct.condition + ")");
896                         prefixTabs = prefixTabs + "\t";
897                 }
898
899                 switch (construct.type) {
900                 case OPDefine:
901                         code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
902                         break;
903                 case PotentialOP:
904                         code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
905                                         + "(" + SpecNaming.AppendStr(label) + ");");
906                         break;
907                 case OPCheck:
908                         code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "("
909                                         + SpecNaming.AppendStr(label) + ");");
910                         break;
911                 case OPClear:
912                         code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();");
913                         break;
914                 case OPClearDefine:
915                         code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
916                                         + "();");
917                         break;
918                 default:
919                         break;
920                 }
921                 return code;
922         }
923
924         /**
925          * <p>
926          * This function generates the code to be inserted right after the entry
927          * construct (instrumentation code)
928          * </p>
929          * 
930          * @param construct
931          *            The corresponding entry construct
932          * @return
933          */
934         public static Code Generate4Entry(EntryConstruct construct) {
935                 Code res = new Code();
936                 String curLine = construct.annotation;
937                 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
938                 // _createInitAnnotation();
939                 res.addLine(prefixTabs + SpecNaming.CreateInitAnnoFunc + "();");
940                 return res;
941         }
942
943         /**
944          * <p>
945          * This function generates the code to be inserted right after the "@Define"
946          * construct (instrumentation code)
947          * </p>
948          * 
949          * @param construct
950          *            The corresponding entry construct
951          * @return
952          */
953         public static Code Generate4Define(DefineConstruct construct) {
954                 Code code = new Code();
955                 code.addLine("");
956                 code.addLine("/**********    User-defined code in annotation (BEGIN)    **********/");
957                 code.addLines(construct.code);
958                 code.addLine("/**********    User-defined code in annotation (END)    **********/");
959                 return code;
960         }
961
962         /**
963          * <p>
964          * This function generates the new interface wrapper code to be inserted
965          * right after the end of the interface definition
966          * </p>
967          * 
968          * @param construct
969          *            The corresponding interface construct
970          * @return The generated code
971          */
972         public static Code GenerateInterfaceWrapper(InterfaceConstruct construct) {
973                 Code code = new Code();
974
975                 String name = construct.getName();
976                 String beginLine = construct.getFunctionHeader().getHeaderLine();
977                 Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
978                 Matcher matcherSpace = regexpSpace.matcher(beginLine);
979                 String prefixTabs = "";
980                 if (matcherSpace.find())
981                         prefixTabs = matcherSpace.group(1);
982
983                 // Add one line to separate
984                 code.addLine("");
985                 code.addLine(prefixTabs
986                                 + ShortComment("Generated wrapper interface for " + name));
987                 if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
988                                                                                         // of the line
989                         code.addLine(beginLine + " {");
990                 } else {
991                         code.addLine(beginLine);
992                 }
993                 // Instrument with the INTERFACE_BEGIN annotations
994                 code.addLine(prefixTabs
995                                 + "\t"
996                                 + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
997                 // CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
998                 code.addLine(prefixTabs
999                                 + "\t"
1000                                 + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
1001                                                 + SpecNaming.AnnoInterfaceInfoInst,
1002                                                 SpecNaming.CreateInterfaceBeginAnnoFunc
1003                                                                 + Brace(SpecNaming.AppendStr(name))));
1004                 // Call the actual function
1005                 code.addLine(prefixTabs + "\t"
1006                                 + ShortComment("Call the actual function"));
1007                 // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
1008                 code.addLine(prefixTabs + "\t"
1009                                 + construct.getFunctionHeader().getRenamedCall() + ";");
1010                 code.addLine("");
1011
1012                 // Initialize the value struct
1013                 code.addLine(prefixTabs + "\t"
1014                                 + ShortComment("Initialize the value struct"));
1015                 // The very first assignment "
1016                 code.addLine(prefixTabs
1017                                 + "\t"
1018                                 + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst,
1019                                                 SpecNaming.New + Brace(name)));
1020                 // Don't leave out the RET field
1021                 if (!construct.getFunctionHeader().isReturnVoid())
1022                         code.addLine(prefixTabs
1023                                         + "\t"
1024                                         + AssignToPtr(SpecNaming.InterfaceValueInst,
1025                                                         SpecNaming.RET, SpecNaming.RET));
1026                 // For arguments
1027                 for (VariableDeclaration decl : construct.getFunctionHeader().args)
1028                         code.addLine(prefixTabs
1029                                         + "\t"
1030                                         + AssignToPtr(SpecNaming.InterfaceValueInst, decl.name,
1031                                                         decl.name));
1032                 code.addLine("");
1033
1034                 // Store the value info into the current MethodCall
1035                 // _setInterfaceBeginAnnotationValue(info, value);
1036                 code.addLine(prefixTabs
1037                                 + "\t"
1038                                 + ShortComment("Store the value info into the current MethodCall"));
1039                 code.addLine(prefixTabs
1040                                 + "\t"
1041                                 + SpecNaming.SetInterfaceBeginAnnoValueFunc
1042                                 + Brace(SpecNaming.AnnoInterfaceInfoInst + ", "
1043                                                 + SpecNaming.InterfaceValueInst) + ";");
1044                 code.addLine("");
1045
1046                 // Return if necessary
1047                 if (!construct.getFunctionHeader().isReturnVoid())
1048                         code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");
1049                 code.addLine(prefixTabs + "}");
1050
1051                 return code;
1052         }
1053
1054         /**
1055          * <p>
1056          * Write a list of lines (as the whole of the file) to a file ---
1057          * newFileName. If that file does not exist, we create that file and then
1058          * write the lines.
1059          * </p>
1060          * 
1061          * @param newFileName
1062          *            The name of the file to be written
1063          * @param content
1064          *            The list of lines that as a whole become the content of the
1065          *            file
1066          */
1067         public static void write2File(String newFileName, ArrayList<String> content) {
1068                 File newFile = new File(newFileName);
1069                 newFile.getParentFile().mkdirs();
1070                 if (!newFile.exists()) {
1071                         try {
1072                                 newFile.createNewFile();
1073                         } catch (IOException e) {
1074                                 e.printStackTrace();
1075                         }
1076                 }
1077                 BufferedWriter bw = null;
1078                 try {
1079                         bw = new BufferedWriter(new FileWriter(newFile));
1080                         for (int i = 0; i < content.size(); i++) {
1081                                 bw.write(content.get(i) + "\n");
1082                         }
1083                         bw.flush();
1084                 } catch (IOException e) {
1085                         e.printStackTrace();
1086                 } finally {
1087                         if (bw != null)
1088                                 try {
1089                                         bw.close();
1090                                 } catch (IOException e) {
1091                                         e.printStackTrace();
1092                                 }
1093                 }
1094         }
1095 }