1 package edu.uci.eecs.codeGenerator;
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;
10 import java.io.FileWriter;
11 import java.io.IOException;
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;
27 * Some utility functions for generating specification checking code.
33 public class CodeGeneratorUtils {
35 public static void PrintCode(ArrayList<String> code) {
36 for (int i = 0; i < code.size(); i++) {
37 System.out.println(code.get(i));
41 public static String Comment(String comment) {
42 return "/** " + comment + " */";
45 public static String ShortComment(String comment) {
46 return "// " + comment;
49 public static String IncludeHeader(String header) {
50 return "#include " + header;
53 public static String Brace(String val) {
54 return "(" + val + ")";
57 public static String Quote(String val) {
58 return "\"" + val + "\"";
61 public static String Assign(String varName, String val) {
62 return varName + " = " + val + ";";
65 public static String AssignToPtr(String structName, String field, String val) {
66 return structName + "->" + field + " = " + val + ";";
69 public static String Declare(String type, String name) {
70 return type + " " + name + ";";
73 public static String Declare(VariableDeclaration varDecl) {
74 return Declare(varDecl.type, varDecl.name);
77 public static String DeclareDefine(String type, String var, String val) {
78 return type + " " + var + " = " + val + ";";
83 * Insert a number of tabs at the beginning of the line.
89 * The number of tabs to be inserted
90 * @return A line that starts with the specific inserted tabs
92 public static String TabbedLine(String line, int tabCnt) {
94 for (int i = 0; i < tabCnt; i++)
102 * Insert a tab at the beginning of the line.
107 * @return A line that starts with one inserted tab
109 public static String TabbedLine(String line) {
115 * This function generates the code for the header file that our
116 * specification generates automatically --- cdsspec-generated.h.
120 * The SpecExtractor that contains the extracted information
121 * @return The generated code
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;
129 Code code = new Code();
131 // Add auto-generated comments
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."));
143 code.addLine("#ifndef _" + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-', '_') + "_H");
144 code.addLine("#define _" + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-', '_') + "_H");
147 // FIXME: We have included ad-hoc header files here
148 // System included headers
149 code.addLine(ShortComment("System included headers go here"));
150 code.addLine(IncludeHeader(SpecNaming.SPECANNOTATION_API));
151 code.addLine(IncludeHeader(SpecNaming.STDLIB));
155 // Users included headers
156 code.addLine(ShortComment("User included headers go here"));
157 for (String header : headerFiles) {
158 code.addLine(IncludeHeader(header));
162 // Decalre extern "C" --- begin
163 code.addLine("#ifdef __cplusplus");
164 code.addLine("extern \"C\" {");
165 code.addLine("#endif");
168 code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
169 code.addLine(ShortComment("A special empty string"));
170 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.EmptyCString));
173 // Interface name strings
174 code.addLine(ShortComment("Interface name strings"));
175 for (File file : interfaceListMap.keySet()) {
176 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
177 for (InterfaceConstruct construct : list) {
178 String name = construct.getName();
179 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(name)));
184 // Commutativity rule strings
185 code.addLine(ShortComment("Commutativity rule strings"));
186 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
187 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.Commutativity + i)));
191 // Ordering points label strings
192 code.addLine(ShortComment("Ordering points label strings"));
193 for (String label : OPLabelSet) {
194 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(label)));
198 // Special function name strings
199 code.addLine(ShortComment("Special function name strings"));
200 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.InitalState)));
201 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.CopyState)));
202 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.FinalState)));
203 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.PrintState)));
206 // Interface name strings
207 for (File file : interfaceListMap.keySet()) {
208 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
209 for (InterfaceConstruct construct : list) {
210 String name = construct.getName();
211 code.addLine(ShortComment(name + " function strings"));
213 String tmpFunc = name + "_" + SpecNaming.Transition;
214 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
216 tmpFunc = name + "_" + SpecNaming.PreCondition;
217 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
219 tmpFunc = name + "_" + SpecNaming.SideEffect;
220 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
222 tmpFunc = name + "_" + SpecNaming.PostCondition;
223 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
225 tmpFunc = name + "_" + SpecNaming.PrintValue;
226 code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
231 // Declare customized value struct
232 for (File file : interfaceListMap.keySet()) {
233 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
234 for (InterfaceConstruct construct : list) {
235 // Declare custom value struct for the interface
236 String name = construct.getName();
237 code.addLine(ShortComment("Declare custom value struct for " + name));
238 code.addLine("typedef struct " + name + " {");
239 FunctionHeader funcHeader = construct.getFunctionHeader();
241 if (!funcHeader.returnType.equals("void"))
242 code.addLine(TabbedLine(Declare(funcHeader.returnType, SpecNaming.RET)));
244 for (VariableDeclaration decl : funcHeader.args) {
245 code.addLine(TabbedLine(Declare(decl)));
247 code.addLine("} " + name + ";");
253 code.addLine(ShortComment("Declare @" + SpecNaming.InitalState));
254 code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "(" + SpecNaming.Method + " "
255 + SpecNaming.Method1 + ");");
258 code.addLine(ShortComment("Declare @" + SpecNaming.CopyState));
259 code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "(" + SpecNaming.Method + " " + "dest, "
260 + SpecNaming.Method + " src);");
263 code.addLine(ShortComment("Declare @" + SpecNaming.PrintState));
264 if (!globalConstruct.printState.isEmpty()) {
265 code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "(" + SpecNaming.Method + " "
266 + SpecNaming.Method1 + ");");
270 // Declare @Commutativity
271 code.addLine(ShortComment("Declare commutativity checking functions"));
272 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
273 code.addLine("bool _check" + SpecNaming.Commutativity + i + "(" + SpecNaming.Method + " m1, "
274 + SpecNaming.Method + " m2);");
278 // Declare customized interface functions
279 for (File file : interfaceListMap.keySet()) {
280 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
281 for (InterfaceConstruct construct : list) {
282 // Declare interface functions
283 String name = construct.getName();
284 code.addLine("/********** " + name + " functions **********/");
285 // Declare @Transition for INTERFACE
286 code.addLine(ShortComment("Declare @" + SpecNaming.Transition + " for " + name));
287 code.addLine("void _" + name + "_" + SpecNaming.Transition + "(" + SpecNaming.Method + " "
288 + SpecNaming.Method1 + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ");");
290 // Declare @PreCondition
291 if (!construct.preCondition.isEmpty()) {
292 code.addLine(ShortComment("Declare @" + SpecNaming.PreCondition + " for " + name));
293 code.addLine("bool _" + name + "_" + SpecNaming.PreCondition + "(" + SpecNaming.Method + " "
294 + SpecNaming.Method1 + ");");
297 // Declare @SideEffect
298 if (!construct.sideEffect.isEmpty()) {
299 code.addLine(ShortComment("Declare @" + SpecNaming.SideEffect + " for " + name));
300 code.addLine("void _" + name + "_" + SpecNaming.SideEffect + "(" + SpecNaming.Method + " "
301 + SpecNaming.Method1 + ");");
304 // Declare @PostCondition
305 if (!construct.postCondition.isEmpty()) {
306 code.addLine(ShortComment("Declare @" + SpecNaming.PostCondition + " for " + name));
307 code.addLine("bool _" + name + "_" + SpecNaming.PostCondition + "(" + SpecNaming.Method + " "
308 + SpecNaming.Method1 + ");");
312 if (!construct.print.isEmpty()) {
313 code.addLine(ShortComment("Declare @" + SpecNaming.PrintValue + " for " + name));
314 code.addLine("void _" + name + "_" + SpecNaming.PrintValue + "(" + SpecNaming.Method + " "
315 + SpecNaming.Method1 + ");");
321 // Declare INIT annotation instrumentation function
322 code.addLine(ShortComment("Declare INIT annotation instrumentation function"));
323 code.addLine("void _createInitAnnotation();");
326 // Decalre extern "C" --- begin
327 code.addLine("#ifdef __cplusplus");
329 code.addLine("#endif");
333 code.addLine("#endif");
340 * This function generates the code for the CPP file that our specification
341 * generates automatically --- cdsspec-generated.cc.
345 * The SpecExtractor that contains the extracted information
346 * @return The generated code
348 public static Code GenerateCDSSpecCPPFile(SpecExtractor extractor) {
349 GlobalConstruct globalConstruct = extractor.getGlobalConstruct();
350 HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap = extractor.interfaceListMap;
351 HashSet<String> OPLabelSet = extractor.OPLabelSet;
353 Code code = new Code();
356 // Add auto-generated comments
358 code.addLine(TabbedLine("This is an implementation file auto-generated by CDSSpec compiler to"));
359 code.addLine(TabbedLine("instrument your benchmark for CDSSpec checker to check. Currently we require"));
360 code.addLine(TabbedLine("a C++ compiler that supports C++11."));
364 code.addLine("#include " + SpecNaming.CDSSpecGeneratedHeader);
365 code.addLine("#include " + SpecNaming.CDSANNOTATE);
366 code.addLine("#include " + SpecNaming.SPEC_COMMON);
367 code.addLine("#include " + SpecNaming.METHODCALL);
368 code.addLine("#include " + SpecNaming.CDSSPEC);
369 code.addLine("#include " + SpecNaming.SPECANNOTATION);
373 // Declare customized StateStruct
374 code.addLine(ShortComment("Declare customized StateStruct"));
375 code.addLine("typedef struct " + SpecNaming.StateStruct + " {");
376 for (VariableDeclaration decl : globalConstruct.declState) {
377 code.addLine(TabbedLine(Declare(decl)));
380 code.addLine(TabbedLine("SNAPSHOTALLOC"));
381 code.addLine("} " + SpecNaming.StateStruct + ";");
385 code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
386 code.addLine(ShortComment("A special empty string"));
387 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString, "\"\""));
390 // Interface name strings
391 code.addLine(ShortComment("Interface name strings"));
392 for (File file : interfaceListMap.keySet()) {
393 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
394 for (InterfaceConstruct construct : list) {
395 String name = construct.getName();
396 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(name), Quote(name)));
401 // Commutativity rule strings
402 code.addLine(ShortComment("Commutativity rule strings"));
403 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
404 CommutativityRule rule = globalConstruct.commutativityRules.get(i - 1);
405 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.Commutativity + i),
406 Quote(rule.toString())));
410 // Ordering points label strings
411 code.addLine(ShortComment("Ordering points label strings"));
412 for (String label : OPLabelSet) {
413 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(label), Quote(label)));
417 // Special function name strings
418 code.addLine(ShortComment("Special function name strings"));
419 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.InitalState),
420 Quote("_" + SpecNaming.InitalState.toLowerCase())));
421 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.CopyState),
422 Quote("_" + SpecNaming.CopyState.toLowerCase())));
423 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.FinalState),
424 Quote("_" + SpecNaming.FinalState.toLowerCase())));
425 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.PrintState),
426 Quote("_" + SpecNaming.PrintState.toLowerCase())));
429 // Interface name strings
430 for (File file : interfaceListMap.keySet()) {
431 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
432 for (InterfaceConstruct construct : list) {
433 String name = construct.getName();
434 code.addLine(ShortComment(name + " function strings"));
436 String tmpFunc = name + "_" + SpecNaming.Transition;
437 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
439 tmpFunc = name + "_" + SpecNaming.PreCondition;
440 if (!construct.preCondition.isEmpty())
442 DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
445 DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
447 tmpFunc = name + "_" + SpecNaming.SideEffect;
448 if (!construct.sideEffect.isEmpty())
450 DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
453 DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
455 tmpFunc = name + "_" + SpecNaming.PostCondition;
456 if (!construct.postCondition.isEmpty())
458 DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
461 DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
463 tmpFunc = name + "_" + SpecNaming.PrintValue;
464 if (!construct.print.isEmpty())
466 DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
469 DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
475 code.addLine(ShortComment("Define @" + SpecNaming.InitalState));
476 code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "(" + SpecNaming.Method + " "
477 + SpecNaming.Method1 + ") {");
478 code.addLine(TabbedLine(
479 DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
481 for (VariableDeclaration decl : globalConstruct.declState) {
482 code.addLine(TabbedLine("#define " + decl.name + " " + SpecNaming.StateInst + "->" + decl.name));
484 if (!globalConstruct.autoGenInitial)
485 code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
487 // Auto-generated the initialization function
488 code.addLine(TabbedLine(ShortComment("Auto-generated state intialization code")));
489 // Align the code with one tab
490 globalConstruct.initState.align(1);
491 code.addLines(globalConstruct.initState);
493 for (VariableDeclaration decl : globalConstruct.declState) {
494 code.addLine(TabbedLine("#undef " + decl.name));
497 code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1, SpecNaming.StateInst, SpecNaming.StateInst)));
502 code.addLine(ShortComment("Define @" + SpecNaming.CopyState));
503 code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "(" + SpecNaming.Method + " " + "dest, "
504 + SpecNaming.Method + " src) {");
505 // StateStruct *OLD = (StateStruct*) src->state;
506 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.OldStateInst,
507 Brace(SpecNaming.StateStruct + "*") + " src->" + SpecNaming.StateInst)));
508 // StateStruct *NEW = new StateStruct;
509 code.addLine(TabbedLine(
510 DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
511 if (!globalConstruct.autoGenCopy)
512 code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
514 // Auto-generated the copy function
515 code.addLine(TabbedLine(ShortComment("Auto-generated state copy statements")));
516 globalConstruct.copyState.align(1);
517 code.addLines(globalConstruct.copyState);
519 code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst, SpecNaming.NewStateInst)));
524 if (!globalConstruct.printState.isEmpty()) {
525 code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
526 code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "(" + SpecNaming.Method + " "
527 + SpecNaming.Method1 + ") {");
529 // Initialize state struct fields
530 Code fieldsInit = GenerateStateFieldsInitialization(SpecNaming.Method1, SpecNaming.StateInst,
533 code.addLines(fieldsInit);
535 if (!globalConstruct.autoGenPrint)
536 code.addLine(TabbedLine(ShortComment("Execute user-defined state printing code")));
538 // Auto-generated the copy function
539 code.addLine(TabbedLine(ShortComment("Execute auto-generated state printing code")));
541 // Align the code with one tab
542 globalConstruct.printState.align(1);
543 code.addLines(globalConstruct.printState);
548 // Define @Commutativity
549 code.addLine(ShortComment("Define commutativity checking functions"));
550 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
551 CommutativityRule rule = globalConstruct.commutativityRules.get(i - 1);
552 code.addLine("bool _check" + SpecNaming.Commutativity + i + "(" + SpecNaming.Method + " m1, "
553 + SpecNaming.Method + " m2) {");
554 // if (m1->name == _ENQ_str && m2->name == _DEQ_str) {
555 code.addLine(TabbedLine("if (m1->name == " + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
556 + SpecNaming.AppendStr(rule.method2) + ") {"));
557 // Initialize M1 & M2 in commutativity rule
558 // e.g. ENQ *M1 = (ENQ*) m1->value;
559 code.addLine(TabbedLine(DeclareDefine(rule.method1, "*M1", "(" + rule.method1 + "*) m1->value"), 2));
560 code.addLine(TabbedLine(DeclareDefine(rule.method2, "*M2", "(" + rule.method2 + "*) m2->value"), 2));
561 code.addLine(TabbedLine("return " + rule.condition + ";", 2));
562 code.addLine(TabbedLine("}"));
563 code.addLine(TabbedLine("return false;"));
569 // Define customized interface functions
570 for (File file : interfaceListMap.keySet()) {
571 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
572 for (InterfaceConstruct construct : list) {
573 Code fieldsInit = null;
575 // Define interface functions
576 String name = construct.getName();
577 code.addLine("/********** " + name + " functions **********/");
578 // Define @Transition for INTERFACE
579 code.addLine(ShortComment("Define @" + SpecNaming.Transition + " for " + name));
580 code.addLine("void _" + name + "_" + SpecNaming.Transition + "(" + SpecNaming.Method + " "
581 + SpecNaming.Method1 + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ") {");
583 // Initialize value struct fields
584 fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method2, "value", construct);
586 code.addLines(fieldsInit);
588 construct.transition.align(1);
589 code.addLine(TabbedLine(ShortComment("Execute Transition")));
590 code.addLines(construct.transition);
595 // Define @PreCondition
596 if (!construct.preCondition.isEmpty()) {
597 code.addLine(ShortComment("Define @" + SpecNaming.PreCondition + " for " + name));
598 code.addLine("bool _" + name + "_" + SpecNaming.PreCondition + "(" + SpecNaming.Method + " "
599 + SpecNaming.Method1 + ") {");
601 // Initialize value struct fields
602 fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
604 code.addLines(fieldsInit);
606 construct.preCondition.align(1);
607 code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
608 code.addLines(construct.preCondition);
614 // Define @SideEffect
615 if (!construct.sideEffect.isEmpty()) {
616 code.addLine(ShortComment("Define @" + SpecNaming.SideEffect + " for " + name));
617 code.addLine("void _" + name + "_" + SpecNaming.SideEffect + "(" + SpecNaming.Method + " "
618 + SpecNaming.Method1 + ") {");
620 // Initialize value struct fields
621 fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
623 code.addLines(fieldsInit);
625 construct.sideEffect.align(1);
626 code.addLine(TabbedLine(ShortComment("Execute SideEffect")));
627 code.addLines(construct.sideEffect);
632 // Define @PostCondition
633 if (!construct.postCondition.isEmpty()) {
634 code.addLine(ShortComment("Define @" + SpecNaming.PostCondition + " for " + name));
635 code.addLine("bool _" + name + "_" + SpecNaming.PostCondition + "(" + SpecNaming.Method + " "
636 + SpecNaming.Method1 + ") {");
638 // Initialize value struct fields
639 fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
641 code.addLines(fieldsInit);
643 construct.postCondition.align(1);
644 code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
645 code.addLines(construct.postCondition);
651 if (!construct.print.isEmpty()) {
652 code.addLine(ShortComment("Define @" + SpecNaming.PrintValue + " for " + name));
653 code.addLine("void _" + name + "_" + SpecNaming.PrintValue + "(" + SpecNaming.Method + " "
654 + SpecNaming.Method1 + ") {");
655 // Initialize value struct fields
656 fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
658 code.addLines(fieldsInit);
660 construct.print.align(1);
661 if (!construct.autoGenPrint)
662 code.addLine(TabbedLine(ShortComment("Execute user-defined value printing code")));
664 // Auto-generated the value printing function
665 code.addLine(TabbedLine(ShortComment("Execute auto-generated value printing code")));
666 code.addLines(construct.print);
674 // Define INIT annotation instrumentation function
675 code.addLine(ShortComment("Define INIT annotation instrumentation function"));
676 code.addLine("void _createInitAnnotation() {");
678 // Init commutativity rules
679 code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
680 code.addLine(TabbedLine(DeclareDefine("int", SpecNaming.CommutativityRuleSizeInst,
681 Integer.toString(globalConstruct.commutativityRules.size()))));
682 String tmp = SpecNaming.NewSize + Brace(SpecNaming.CommutativityRule + ", sizeof"
683 + Brace(SpecNaming.CommutativityRule) + " * " + SpecNaming.CommutativityRuleSizeInst);
685 TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*" + SpecNaming.CommutativityRuleInst, tmp)));
686 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
687 CommutativityRule rule = globalConstruct.commutativityRules.get(i - 1);
688 code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ") + i));
689 // new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
690 // _Commutativity1_str, _checkCommutativity1)
691 line = "new" + Brace(" &" + SpecNaming.CommutativityRuleInst + "[" + (i - 1) + "] ")
692 + SpecNaming.CommutativityRule + "(" + SpecNaming.AppendStr(rule.method1) + ", "
693 + SpecNaming.AppendStr(rule.method2) + ", " + SpecNaming.AppendStr(SpecNaming.Commutativity + i)
694 + ", " + "_check" + SpecNaming.Commutativity + i + ");";
695 code.addLine(TabbedLine(line));
698 // Initialize AnnoInit
699 code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
700 // AnnoInit *init = new AnnoInit(
701 code.addLine(TabbedLine(
702 SpecNaming.AnnoInit + " *" + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit + "("));
703 // new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
704 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.InitalState)
705 + ", " + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
706 + SpecNaming.InitalState.toLowerCase() + "),", 2));
707 // new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
708 line = "new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
709 + SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
710 if (globalConstruct.finalState.isEmpty()) {
711 line = line + SpecNaming.NullFunc + "),";
713 line = line + "_" + SpecNaming.FinalState.toUpperCase();
715 code.addLine(TabbedLine(line, 2));
716 // new NamedFunction(_Copy_str, COPY, (void*) _copy),
717 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.CopyState)
718 + ", " + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _" + SpecNaming.CopyState.toLowerCase()
720 // new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
721 line = "new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
722 + SpecNaming.PrintStateType + ", " + "(void*)";
723 if (globalConstruct.printState.isEmpty()) {
724 line = line + SpecNaming.NullFunc + "),";
726 line = line + "_" + SpecNaming.PrintState.toLowerCase() + "),";
728 code.addLine(TabbedLine(line, 2));
729 // commuteRules, CommuteRuleSize);
731 TabbedLine(SpecNaming.CommutativityRuleInst + ", " + SpecNaming.CommutativityRuleSizeInst + ");", 2));
734 // Declare StateFunctions map
735 code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
736 code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*" + SpecNaming.StateFunctionsInst)));
739 // StateFunction for interface
740 for (File file : interfaceListMap.keySet()) {
741 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
742 for (InterfaceConstruct construct : list) {
743 String name = construct.getName();
744 code.addLine(TabbedLine(ShortComment("StateFunction for " + name)));
745 // stateFuncs = new StateFunctions(
746 code.addLine(TabbedLine(SpecNaming.StateFunctionsInst + " = new " + SpecNaming.StateFunctions + "("));
747 // new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
750 code.addLine(TabbedLine(
751 "new " + SpecNaming.NamedFunction + "("
752 + SpecNaming.AppendStr(name + "_" + SpecNaming.Transition) + ", "
753 + SpecNaming.TransitionType + ", (void*) _" + name + "_" + SpecNaming.Transition + "),",
756 line = "new " + SpecNaming.NamedFunction + "("
757 + SpecNaming.AppendStr(name + "_" + SpecNaming.PreCondition) + ", "
758 + SpecNaming.PreConditionType + ", (void*) ";
759 if (construct.preCondition.isEmpty()) {
760 line = line + SpecNaming.NullFunc + "),";
762 line = line + "_" + name + "_" + SpecNaming.PreCondition + "),";
764 code.addLine(TabbedLine(line, 2));
766 line = "new " + SpecNaming.NamedFunction + "("
767 + SpecNaming.AppendStr(name + "_" + SpecNaming.SideEffect) + ", " + SpecNaming.SideEffectType
769 if (construct.sideEffect.isEmpty()) {
770 line = line + SpecNaming.NullFunc + "),";
772 line = line + "_" + name + "_" + SpecNaming.SideEffect + "),";
774 code.addLine(TabbedLine(line, 2));
776 line = "new " + SpecNaming.NamedFunction + "("
777 + SpecNaming.AppendStr(name + "_" + SpecNaming.PostCondition) + ", "
778 + SpecNaming.PostConditionType + ", (void*) ";
779 if (construct.postCondition.isEmpty()) {
780 line = line + SpecNaming.NullFunc + "),";
782 line = line + "_" + name + "_" + SpecNaming.PostCondition + "),";
784 code.addLine(TabbedLine(line, 2));
786 line = "new " + SpecNaming.NamedFunction + "("
787 + SpecNaming.AppendStr(name + "_" + SpecNaming.PrintValue) + ", " + SpecNaming.PrintValueType
789 if (construct.print.isEmpty()) {
790 line = line + SpecNaming.NullFunc + ")";
792 line = line + "_" + name + "_" + SpecNaming.PrintValue + ")";
794 code.addLine(TabbedLine(line, 2));
795 code.addLine(TabbedLine(");"));
797 // init->addInterfaceFunctions(_ENQ_str, stateFuncs);
798 code.addLine(TabbedLine(SpecNaming.AnnoInitInst + "->" + SpecNaming.AddInterfaceFunctions
799 + Brace(SpecNaming.AppendStr(name) + ", " + SpecNaming.StateFunctionsInst) + ";"));
804 // Create and instrument with the INIT annotation
805 code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
806 // cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
807 code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc + Brace(SpecNaming.SPEC_ANALYSIS + ", new "
808 + SpecNaming.SpecAnnotation + Brace(SpecNaming.AnnoTypeInit + ", " + SpecNaming.AnnoInitInst)) + ";"));
818 * This function generates a list of lines that initialize the fields of the
819 * global state struct. See below.
824 * StateStruct *state = (StateStruct*) _M->state;
826 * IntList * q = state->q;
831 * In this example, _M --> methodInst, state --> inst.
839 * The global state construct
840 * @return The generated code
842 public static Code GenerateStateFieldsInitialization(String methodInst, String inst, GlobalConstruct construct) {
843 Code res = new Code();
844 res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct + " fields"));
845 res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst,
846 "(" + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
847 for (VariableDeclaration decl : construct.declState) {
848 res.addLine(DeclareDefine(decl.type, decl.name, inst + "->" + decl.name));
855 * This function generates a list of lines that initialize the fields of a
856 * specific interface struct. See below.
861 * ENQ *info = (ENQ*) _M->value;
863 * IntList * q = info->q;
868 * In this example, ENQ --> structType, _M --> methodInst, info --> inst
876 * The corresponding interface construct
877 * @return The generated code
879 public static Code GenerateInterfaceFieldsInitialization(String methodInst, String inst,
880 InterfaceConstruct construct) {
881 Code res = new Code();
882 String name = construct.getName();
883 res.addLine(ShortComment("Initialize fields for " + name));
884 // The very first assignment "
885 res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) " + methodInst + "->value"));
886 // Don't leave out the RET field
887 if (!construct.getFunctionHeader().isReturnVoid()) {
888 res.addLine(DeclareDefine(construct.getFunctionHeader().returnType, SpecNaming.RET,
889 "value->" + SpecNaming.RET));
892 for (VariableDeclaration decl : construct.getFunctionHeader().args) {
893 res.addLine(DeclareDefine(decl.type, decl.name, inst + "->" + decl.name));
900 * This function generates the code to be inserted right after the ordering
901 * point construct (instrumentation code)
905 * The corresponding ordering point construct
906 * @return The generated code
908 public static Code Generate4OPConstruct(OPConstruct construct) {
909 Code code = new Code();
910 String curLine = construct.annotation;
911 String label = construct.label;
912 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
913 if (!construct.condition.equals("true")) {
914 code.addLine(prefixTabs + "if (" + construct.condition + ")");
915 prefixTabs = prefixTabs + "\t";
918 switch (construct.type) {
920 code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
923 code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc + "(" + SpecNaming.AppendStr(label) + ");");
926 code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "(" + SpecNaming.AppendStr(label) + ");");
929 code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();");
932 code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc + "();");
942 * This function generates the code to be inserted right after the entry
943 * construct (instrumentation code)
947 * The corresponding entry construct
950 public static Code Generate4Entry(EntryConstruct construct) {
951 Code res = new Code();
952 String curLine = construct.annotation;
953 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
954 // _createInitAnnotation();
955 res.addLine(prefixTabs + SpecNaming.CreateInitAnnoFunc + "();");
961 * This function generates the code to be inserted right after the "@Define"
962 * construct (instrumentation code)
966 * The corresponding entry construct
969 public static Code Generate4Define(DefineConstruct construct) {
970 Code code = new Code();
972 code.addLine("/********** User-defined code in annotation (BEGIN) **********/");
973 code.addLines(construct.code);
974 code.addLine("/********** User-defined code in annotation (END) **********/");
980 * This function generates the new interface wrapper code to be inserted
981 * right after the end of the interface definition
985 * The corresponding interface construct
986 * @return The generated code
988 public static Code GenerateInterfaceWrapper(InterfaceConstruct construct) {
989 Code code = new Code();
991 String name = construct.getName();
992 String beginLine = construct.getFunctionHeader().getHeaderLine();
993 Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
994 Matcher matcherSpace = regexpSpace.matcher(beginLine);
995 String prefixTabs = "";
996 if (matcherSpace.find())
997 prefixTabs = matcherSpace.group(1);
999 // Add one line to separate
1001 code.addLine(prefixTabs + ShortComment("Generated wrapper interface for " + name));
1002 if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
1004 code.addLine(beginLine + " {");
1006 code.addLine(beginLine);
1008 // Instrument with the INTERFACE_BEGIN annotations
1009 code.addLine(prefixTabs + "\t" + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
1010 // CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
1012 prefixTabs + "\t" + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*" + SpecNaming.AnnoInterfaceInfoInst,
1013 SpecNaming.CreateInterfaceBeginAnnoFunc + Brace(SpecNaming.AppendStr(name))));
1014 // Call the actual function
1015 code.addLine(prefixTabs + "\t" + ShortComment("Call the actual function"));
1016 // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
1017 code.addLine(prefixTabs + "\t" + construct.getFunctionHeader().getRenamedCall() + ";");
1020 // Initialize the value struct
1021 code.addLine(prefixTabs + "\t" + ShortComment("Initialize the value struct"));
1022 // The very first assignment "
1023 code.addLine(prefixTabs + "\t" + DeclareDefine(name, "*value", SpecNaming.New + Brace(name)));
1024 // Don't leave out the RET field
1025 if (!construct.getFunctionHeader().isReturnVoid())
1026 code.addLine(prefixTabs + "\t" + AssignToPtr("value", SpecNaming.RET, SpecNaming.RET));
1028 for (VariableDeclaration decl : construct.getFunctionHeader().args)
1029 code.addLine(prefixTabs + "\t" + AssignToPtr("value", decl.name, decl.name));
1032 // Store the value info into the current MethodCall
1033 // _setInterfaceBeginAnnotationValue(info, value);
1034 code.addLine(prefixTabs + "\t" + ShortComment("Store the value info into the current MethodCall"));
1035 code.addLine(prefixTabs + "\t" + SpecNaming.SetInterfaceBeginAnnoValueFunc
1036 + Brace(SpecNaming.AnnoInterfaceInfoInst + ", value") + ";");
1039 // Return if necessary
1040 if (!construct.getFunctionHeader().isReturnVoid())
1041 code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");
1042 code.addLine(prefixTabs + "}");
1049 * Write a list of lines (as the whole of the file) to a file ---
1050 * newFileName. If that file does not exist, we create that file and then
1054 * @param newFileName
1055 * The name of the file to be written
1057 * The list of lines that as a whole become the content of the
1060 public static void write2File(String newFileName, ArrayList<String> content) {
1061 File newFile = new File(newFileName);
1062 newFile.getParentFile().mkdirs();
1063 if (!newFile.exists()) {
1065 newFile.createNewFile();
1066 } catch (IOException e) {
1067 e.printStackTrace();
1070 BufferedWriter bw = null;
1072 bw = new BufferedWriter(new FileWriter(newFile));
1073 for (int i = 0; i < content.size(); i++) {
1074 bw.write(content.get(i) + "\n");
1077 } catch (IOException e) {
1078 e.printStackTrace();
1083 } catch (IOException e) {
1084 e.printStackTrace();