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 _"
144 + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
146 code.addLine("#define _"
147 + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
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));
159 // Users included headers
160 code.addLine(ShortComment("User included headers go here"));
161 for (String header : headerFiles) {
162 code.addLine(IncludeHeader(header));
166 // Decalre extern "C" --- begin
167 code.addLine("#ifdef __cplusplus");
168 code.addLine("extern \"C\" {");
169 code.addLine("#endif");
172 // Declare _createOPDefineUnattached
173 code.addLine(ShortComment("Declare _createOPDefineUnattached"));
174 // void _createOPDefineUnattached();
175 code.addLine("void _createOPDefineUnattached();");
178 // Declare _createOPClearDefineUnattached
179 code.addLine(ShortComment("Declare _createOPClearDefineUnattached"));
180 // void _createOPClearDefineUnattached();
181 code.addLine("void _createOPClearDefineUnattached();");
184 code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
186 // Interface name strings
187 code.addLine(ShortComment("Interface name strings"));
188 for (File file : interfaceListMap.keySet()) {
189 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
190 for (InterfaceConstruct construct : list) {
191 String name = construct.getName();
192 code.addLine(Declare("extern " + SpecNaming.CString,
193 SpecNaming.AppendStr(name)));
198 // Ordering points label strings
199 code.addLine(ShortComment("Ordering points label strings"));
200 for (String label : OPLabelSet) {
201 code.addLine(Declare("extern " + SpecNaming.CString,
202 SpecNaming.AppendStr(label)));
206 // Declare customized value struct
207 for (File file : interfaceListMap.keySet()) {
208 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
209 for (InterfaceConstruct construct : list) {
210 // Declare custom value struct for the interface
211 String name = construct.getName();
212 String structName = construct.getStructName();
213 code.addLine(ShortComment("Declare custom value struct for "
215 code.addLine("typedef struct " + structName + " {");
216 FunctionHeader funcHeader = construct.getFunctionHeader();
218 if (!funcHeader.returnType.equals("void"))
219 code.addLine(TabbedLine(Declare(funcHeader.returnType,
222 for (VariableDeclaration decl : funcHeader.args) {
223 code.addLine(TabbedLine(Declare(decl)));
225 code.addLine("} " + structName + ";");
230 // Declare INIT annotation instrumentation function
231 code.addLine(ShortComment("Declare INIT annotation instrumentation function"));
232 code.addLine("void _createInitAnnotation();");
235 // Decalre extern "C" --- begin
236 code.addLine("#ifdef __cplusplus");
238 code.addLine("#endif");
242 code.addLine("#endif");
249 * This function generates the code for the CPP file that our specification
250 * generates automatically --- cdsspec-generated.cc.
254 * The SpecExtractor that contains the extracted information
255 * @return The generated code
257 public static Code GenerateCDSSpecCPPFile(SpecExtractor extractor) {
258 GlobalConstruct globalConstruct = extractor.getGlobalConstruct();
259 HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap = extractor.interfaceListMap;
260 HashSet<String> OPLabelSet = extractor.OPLabelSet;
262 Code code = new Code();
264 Code fieldsInit = null;
266 // Add auto-generated comments
268 code.addLine(TabbedLine("This is an implementation file auto-generated by CDSSpec compiler to"));
269 code.addLine(TabbedLine("instrument your benchmark for CDSSpec checker to check. Currently we require"));
270 code.addLine(TabbedLine("a C++ compiler that supports C++11."));
274 code.addLine("#include " + SpecNaming.CDSSpecGeneratedHeader);
275 code.addLine("#include " + SpecNaming.CDSANNOTATE);
276 code.addLine("#include " + SpecNaming.SPEC_COMMON);
277 code.addLine("#include " + SpecNaming.METHODCALL);
278 code.addLine("#include " + SpecNaming.CDSSPEC);
279 code.addLine("#include " + SpecNaming.SPECANNOTATION);
283 // Declare customized StateStruct
284 code.addLine(ShortComment("Declare customized StateStruct"));
285 code.addLine("typedef struct " + SpecNaming.StateStruct + " {");
286 for (VariableDeclaration decl : globalConstruct.declState) {
287 code.addLine(TabbedLine(Declare(decl)));
290 // Define state destructor
291 code.addLine(TabbedLine(ShortComment("Define state destructor")));
292 code.addLine(TabbedLine("~" + SpecNaming.StateStruct + "() {"));
293 if (!globalConstruct.autoGenClear) {
294 code.addLine(TabbedLine(
295 ShortComment("Execute user-defined state clear code"), 2));
297 code.addLine(TabbedLine(
298 ShortComment("Execute auto-generated state clear code"), 2));
300 globalConstruct.clearState.align(2);
301 code.addLines(globalConstruct.clearState);
302 code.addLine(TabbedLine("}"));
305 code.addLine(TabbedLine("SNAPSHOTALLOC"));
307 code.addLine("} " + SpecNaming.StateStruct + ";");
311 // Define the fake ordering point operation
312 code.addLine(ShortComment("Define the fake ordering point operation"));
313 // atomic_int _FAKE_OP_;
314 code.addLine("atomic_int " + SpecNaming.FakeOP + ";");
317 // Define _createOPDefineUnattached
318 code.addLine(ShortComment("Define _createOPDefineUnattached"));
319 code.addLine("void " + SpecNaming.CreateOPDefineUnattachedFunc + "() {");
320 code.addLine(TabbedLine(ShortComment("A load acting as the fake OP")));
321 code.addLine(TabbedLine(SpecNaming.FakeOP
322 + ".load(memory_order_relaxed);"));
323 code.addLine(TabbedLine(SpecNaming.CreateOPDefineAnnoFunc + "();"));
326 // Define _createOPClearDefineUnattached
327 code.addLine(ShortComment("Define _createOPClearDefineUnattached"));
328 code.addLine("void " + SpecNaming.CreateOPClearDefineUnattachedFunc
330 code.addLine(TabbedLine(ShortComment("A load acting as the fake OP")));
331 code.addLine(TabbedLine(SpecNaming.FakeOP
332 + ".load(memory_order_relaxed);"));
333 code.addLine(TabbedLine(SpecNaming.CreateOPClearDefineAnnoFunc + "();"));
336 code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
337 code.addLine(ShortComment("A special empty string"));
338 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,
342 // Interface name strings
343 code.addLine(ShortComment("Interface name strings"));
344 for (File file : interfaceListMap.keySet()) {
345 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
346 for (InterfaceConstruct construct : list) {
347 String name = construct.getName();
348 code.addLine(DeclareDefine(SpecNaming.CString,
349 SpecNaming.AppendStr(name), Quote(name)));
354 // Commutativity rule strings
355 code.addLine(ShortComment("Commutativity rule strings"));
356 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
357 CommutativityRule rule = globalConstruct.commutativityRules
359 code.addLine(DeclareDefine(SpecNaming.CString,
360 SpecNaming.AppendStr(SpecNaming.Commutativity + i),
361 Quote(rule.toString())));
365 // Ordering points label strings
366 code.addLine(ShortComment("Ordering points label strings"));
367 for (String label : OPLabelSet) {
368 code.addLine(DeclareDefine(SpecNaming.CString,
369 SpecNaming.AppendStr(label), Quote(label)));
373 // Special function name strings
374 code.addLine(ShortComment("Special function name strings"));
375 code.addLine(DeclareDefine(SpecNaming.CString,
376 SpecNaming.AppendStr(SpecNaming.InitalState), Quote("_"
377 + SpecNaming.InitalState.toLowerCase())));
378 code.addLine(DeclareDefine(SpecNaming.CString,
379 SpecNaming.AppendStr(SpecNaming.CopyState), Quote("_"
380 + SpecNaming.CopyState.toLowerCase())));
381 code.addLine(DeclareDefine(SpecNaming.CString,
382 SpecNaming.AppendStr(SpecNaming.ClearState), Quote("_"
383 + SpecNaming.ClearState.toLowerCase())));
384 code.addLine(DeclareDefine(SpecNaming.CString,
385 SpecNaming.AppendStr(SpecNaming.FinalState), Quote("_"
386 + SpecNaming.FinalState.toLowerCase())));
387 code.addLine(DeclareDefine(SpecNaming.CString,
388 SpecNaming.AppendStr(SpecNaming.PrintState), Quote("_"
389 + SpecNaming.PrintState.toLowerCase())));
392 // Interface name strings
393 for (File file : interfaceListMap.keySet()) {
394 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
395 for (InterfaceConstruct construct : list) {
396 String name = construct.getName();
397 code.addLine(ShortComment(name + " function strings"));
399 String tmpFunc = name + "_" + SpecNaming.Transition;
400 code.addLine(DeclareDefine(SpecNaming.CString,
401 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
403 tmpFunc = name + "_" + SpecNaming.PreCondition;
404 if (!construct.preCondition.isEmpty())
405 code.addLine(DeclareDefine(SpecNaming.CString,
406 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
408 code.addLine(DeclareDefine(SpecNaming.CString,
409 SpecNaming.AppendStr(tmpFunc),
410 SpecNaming.EmptyCString));
411 // JustifyingCondition
412 tmpFunc = name + "_" + SpecNaming.JustifyingCondition;
413 if (!construct.justifyingCondition.isEmpty())
414 code.addLine(DeclareDefine(SpecNaming.CString,
415 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
417 code.addLine(DeclareDefine(SpecNaming.CString,
418 SpecNaming.AppendStr(tmpFunc),
419 SpecNaming.EmptyCString));
421 tmpFunc = name + "_" + SpecNaming.PostCondition;
422 if (!construct.postCondition.isEmpty())
423 code.addLine(DeclareDefine(SpecNaming.CString,
424 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
426 code.addLine(DeclareDefine(SpecNaming.CString,
427 SpecNaming.AppendStr(tmpFunc),
428 SpecNaming.EmptyCString));
430 tmpFunc = name + "_" + SpecNaming.PrintValue;
431 if (!construct.print.isEmpty())
432 code.addLine(DeclareDefine(SpecNaming.CString,
433 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
435 code.addLine(DeclareDefine(SpecNaming.CString,
436 SpecNaming.AppendStr(tmpFunc),
437 SpecNaming.EmptyCString));
443 code.addLine(ShortComment("Define @" + SpecNaming.InitalState));
444 code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
445 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
446 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
447 + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
449 for (VariableDeclaration decl : globalConstruct.declState) {
450 code.addLine(TabbedLine("#define " + decl.name + " "
451 + SpecNaming.StateInst + "->" + decl.name));
453 if (!globalConstruct.autoGenInitial)
454 code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
456 // Auto-generated the initialization function
457 code.addLine(TabbedLine(ShortComment("Auto-generated state intialization code")));
458 // Align the code with one tab
459 globalConstruct.initState.align(1);
460 code.addLines(globalConstruct.initState);
462 for (VariableDeclaration decl : globalConstruct.declState) {
463 code.addLine(TabbedLine("#undef " + decl.name));
466 code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1,
467 SpecNaming.StateInst, SpecNaming.StateInst)));
472 code.addLine(ShortComment("Define @" + SpecNaming.CopyState));
473 code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
474 + SpecNaming.Method + " " + "dest, " + SpecNaming.Method
476 // StateStruct *OLD = (StateStruct*) src->state;
477 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
478 + SpecNaming.OldStateInst, Brace(SpecNaming.StateStruct + "*")
479 + " src->" + SpecNaming.StateInst)));
480 // StateStruct *NEW = new StateStruct;
481 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
482 + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
483 if (!globalConstruct.autoGenCopy)
484 code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
486 // Auto-generated the copy function
487 code.addLine(TabbedLine(ShortComment("Auto-generated state copy statements")));
488 globalConstruct.copyState.align(1);
489 code.addLines(globalConstruct.copyState);
491 code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst,
492 SpecNaming.NewStateInst)));
497 code.addLine(ShortComment("Define @" + SpecNaming.ClearState));
498 code.addLine("void _" + SpecNaming.ClearState.toLowerCase() + "("
499 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
500 // Retrieve the state
501 code.addLine(TabbedLine(ShortComment("Retrieve the state")));
502 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
503 + SpecNaming.StateInst, "(" + SpecNaming.StateStruct + "*) "
504 + SpecNaming.Method1 + "->state")));
505 // Explicitly call the state destructor
506 code.addLine(TabbedLine(ShortComment("Explicitly call the state destructor")));
507 code.addLine(TabbedLine("delete " + SpecNaming.StateInst + ";"));
512 code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
513 code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
514 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
516 // Initialize state struct fields
517 fieldsInit = GenerateStateFieldsInitialization(SpecNaming.Method1,
518 SpecNaming.StateInst, globalConstruct);
520 code.addLines(fieldsInit);
522 if (!globalConstruct.autoGenPrint)
523 code.addLine(TabbedLine(ShortComment("Execute user-defined state printing code")));
525 // Auto-generated the copy function
526 code.addLine(TabbedLine(ShortComment("Execute auto-generated state printing code")));
528 // Align the code with one tab
529 globalConstruct.printState.align(1);
530 code.addLines(globalConstruct.printState);
534 // Define @Commutativity
535 code.addLine(ShortComment("Define commutativity checking functions"));
536 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
537 CommutativityRule rule = globalConstruct.commutativityRules
539 code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
540 + SpecNaming.Method + " m1, " + SpecNaming.Method
542 // if (m1->name == _ENQ_str && m2->name == _DEQ_str) {
543 code.addLine(TabbedLine("if (m1->name == "
544 + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
545 + SpecNaming.AppendStr(rule.method2) + ") {"));
546 // Initialize M1 & M2 in commutativity rule
547 // e.g. ENQ *M1 = (ENQ*) m1->value;
548 String structName1 = InterfaceConstruct
549 .createStructName(rule.method1);
550 String structName2 = InterfaceConstruct
551 .createStructName(rule.method2);
552 code.addLine(TabbedLine(
553 DeclareDefine(structName1, "*M1", "(" + structName1
554 + "*) m1->value"), 2));
555 code.addLine(TabbedLine(
556 DeclareDefine(structName2, "*M2", "(" + structName2
557 + "*) m2->value"), 2));
558 code.addLine(TabbedLine("return " + rule.condition + ";", 2));
559 code.addLine(TabbedLine("}"));
560 code.addLine(TabbedLine("return false;"));
566 // Define customized interface functions
567 for (File file : interfaceListMap.keySet()) {
568 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
569 for (InterfaceConstruct construct : list) {
572 // Define interface functions
573 String name = construct.getName();
574 String structName = construct.getStructName();
575 code.addLine("/********** " + name
576 + " functions **********/");
577 // Define @Transition for INTERFACE
578 code.addLine(ShortComment("Define @" + SpecNaming.Transition
580 code.addLine("bool _" + name + "_" + SpecNaming.Transition
581 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
582 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
585 // Initialize value struct fields
586 fieldsInit = GenerateInterfaceFieldsInitialization(
587 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
590 code.addLines(fieldsInit);
592 construct.transition.align(1);
593 code.addLine(TabbedLine(ShortComment("Execute Transition")));
594 code.addLines(construct.transition);
596 // By default, we will return true for state transition
597 code.addLine(TabbedLine(ShortComment("By default @Transition returns true")));
598 code.addLine(TabbedLine("return true;"));
602 // Define @PreCondition
603 if (!construct.preCondition.isEmpty()) {
604 code.addLine(ShortComment("Define @"
605 + SpecNaming.PreCondition + " for " + name));
606 code.addLine("bool _" + name + "_" + SpecNaming.PreCondition
607 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
608 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
611 // Initialize value struct fields
612 fieldsInit = GenerateInterfaceFieldsInitialization(
613 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
616 code.addLines(fieldsInit);
618 construct.preCondition.align(1);
619 code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
620 code.addLines(construct.preCondition);
622 // By default, we will return true for @PreCondition
623 code.addLine(TabbedLine(ShortComment("By default @PreCondition returns true")));
624 code.addLine(TabbedLine("return true;"));
630 // Define @JustifyingCondition
631 if (!construct.justifyingCondition.isEmpty()) {
632 code.addLine(ShortComment("Define @"
633 + SpecNaming.JustifyingCondition + " for " + name));
634 code.addLine("bool _" + name + "_" + SpecNaming.JustifyingCondition
635 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
636 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
639 // Initialize value struct fields
640 fieldsInit = GenerateInterfaceFieldsInitialization(
641 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
644 code.addLines(fieldsInit);
646 construct.justifyingCondition.align(1);
647 code.addLine(TabbedLine(ShortComment("Execute JustifyingCondition")));
648 code.addLines(construct.justifyingCondition);
650 // By default, we will return true for @PreCondition
651 code.addLine(TabbedLine(ShortComment("By default @JustifyingCondition returns true")));
652 code.addLine(TabbedLine("return true;"));
658 // Define @PostCondition
659 if (!construct.postCondition.isEmpty()) {
660 code.addLine(ShortComment("Define @"
661 + SpecNaming.PostCondition + " for " + name));
662 code.addLine("bool _" + name + "_" + SpecNaming.PostCondition
663 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
664 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
667 // Initialize value struct fields
668 fieldsInit = GenerateInterfaceFieldsInitialization(
669 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
672 code.addLines(fieldsInit);
674 construct.postCondition.align(1);
675 code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
676 code.addLines(construct.postCondition);
678 // By default, we will return true for @PostCondition
679 code.addLine(TabbedLine(ShortComment("By default @PostCondition returns true")));
680 code.addLine(TabbedLine("return true;"));
686 if (!construct.print.isEmpty()) {
687 code.addLine(ShortComment("Define @"
688 + SpecNaming.PrintValue + " for " + name));
689 code.addLine("void _" + name + "_" + SpecNaming.PrintValue
690 + "(" + SpecNaming.Method + " "
691 + SpecNaming.Method1 + ") {");
692 // Initialize value struct fields
693 fieldsInit = GenerateInterfaceFieldsInitialization(
694 SpecNaming.Method1, SpecNaming.InterfaceValueInst,
697 code.addLines(fieldsInit);
699 construct.print.align(1);
700 if (!construct.autoGenPrint)
701 code.addLine(TabbedLine(ShortComment("Execute user-defined value printing code")));
703 // Auto-generated the value printing function
704 code.addLine(TabbedLine(ShortComment("Execute auto-generated value printing code")));
705 code.addLines(construct.print);
713 // Define INIT annotation instrumentation function
714 code.addLine(ShortComment("Define INIT annotation instrumentation function"));
715 code.addLine("void _createInitAnnotation() {");
717 // Init the fake ordering point place holder
718 code.addLine(TabbedLine(ShortComment("Init the fake ordering point place holder")));
719 code.addLine(TabbedLine(SpecNaming.FakeOP
720 + ".store(1, memory_order_relaxed);"));
722 // Init commutativity rules
723 code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
724 code.addLine(TabbedLine(DeclareDefine("int",
725 SpecNaming.CommutativityRuleSizeInst,
726 Integer.toString(globalConstruct.commutativityRules.size()))));
727 String tmp = SpecNaming.NewSize
728 + Brace(SpecNaming.CommutativityRule + ", sizeof"
729 + Brace(SpecNaming.CommutativityRule) + " * "
730 + SpecNaming.CommutativityRuleSizeInst);
731 code.addLine(TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*"
732 + SpecNaming.CommutativityRuleInst, tmp)));
733 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
734 CommutativityRule rule = globalConstruct.commutativityRules
736 code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ")
738 // new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
739 // _Commutativity1_str, _checkCommutativity1)
741 + Brace(" &" + SpecNaming.CommutativityRuleInst + "["
742 + (i - 1) + "] ") + SpecNaming.CommutativityRule
743 + "(" + SpecNaming.AppendStr(rule.method1) + ", "
744 + SpecNaming.AppendStr(rule.method2) + ", "
745 + SpecNaming.AppendStr(SpecNaming.Commutativity + i) + ", "
746 + "_check" + SpecNaming.Commutativity + i + ");";
747 code.addLine(TabbedLine(line));
750 // Initialize AnnoInit
751 code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
752 // AnnoInit *init = new AnnoInit(
753 code.addLine(TabbedLine(SpecNaming.AnnoInit + " *"
754 + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit
756 // new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
757 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
758 + SpecNaming.AppendStr(SpecNaming.InitalState) + ", "
759 + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
760 + SpecNaming.InitalState.toLowerCase() + "),", 2));
761 // new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
762 line = "new " + SpecNaming.NamedFunction + "("
763 + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
764 + SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
765 if (globalConstruct.finalState.isEmpty()) {
766 line = line + SpecNaming.NullFunc + "),";
768 line = line + "_" + SpecNaming.FinalState.toUpperCase();
770 code.addLine(TabbedLine(line, 2));
771 // new NamedFunction(_Copy_str, COPY, (void*) _copy),
772 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
773 + SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
774 + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
775 + SpecNaming.CopyState.toLowerCase() + "),", 2));
776 // new NamedFunction(_Clear_str, CLEAR, (void*) _clear),
777 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
778 + SpecNaming.AppendStr(SpecNaming.ClearState) + ", "
779 + SpecNaming.ClearState.toUpperCase() + ", " + "(void*) _"
780 + SpecNaming.ClearState.toLowerCase() + "),", 2));
781 // new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
782 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
783 + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
784 + SpecNaming.PrintStateType + ", " + "(void*) _"
785 + SpecNaming.PrintState.toLowerCase() + "),", 2));
786 // commuteRules, CommuteRuleSize);
787 code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
788 + SpecNaming.CommutativityRuleSizeInst + ");", 2));
791 // Declare StateFunctions map
792 code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
793 code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*"
794 + SpecNaming.StateFunctionsInst)));
797 // StateFunction for interface
798 for (File file : interfaceListMap.keySet()) {
799 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
800 for (InterfaceConstruct construct : list) {
801 String name = construct.getName();
802 code.addLine(TabbedLine(ShortComment("StateFunction for "
804 // stateFuncs = new StateFunctions(
805 code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
806 + " = new " + SpecNaming.StateFunctions + "("));
807 // new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
810 code.addLine(TabbedLine(
812 + SpecNaming.NamedFunction
814 + SpecNaming.AppendStr(name + "_"
815 + SpecNaming.Transition) + ", "
816 + SpecNaming.TransitionType + ", (void*) _"
817 + name + "_" + SpecNaming.Transition + "),", 2));
820 + SpecNaming.NamedFunction
822 + SpecNaming.AppendStr(name + "_"
823 + SpecNaming.PreCondition) + ", "
824 + SpecNaming.PreConditionType + ", (void*) ";
825 if (construct.preCondition.isEmpty()) {
826 line = line + SpecNaming.NullFunc + "),";
828 line = line + "_" + name + "_" + SpecNaming.PreCondition
831 code.addLine(TabbedLine(line, 2));
832 // JustifyingCondition
834 + SpecNaming.NamedFunction
836 + SpecNaming.AppendStr(name + "_"
837 + SpecNaming.JustifyingCondition) + ", "
838 + SpecNaming.JustifyingConditionType + ", (void*) ";
839 if (construct.justifyingCondition.isEmpty()) {
840 line = line + SpecNaming.NullFunc + "),";
842 line = line + "_" + name + "_" + SpecNaming.JustifyingCondition
845 code.addLine(TabbedLine(line, 2));
848 + SpecNaming.NamedFunction
850 + SpecNaming.AppendStr(name + "_"
851 + SpecNaming.PostCondition) + ", "
852 + SpecNaming.PostConditionType + ", (void*) ";
853 if (construct.postCondition.isEmpty()) {
854 line = line + SpecNaming.NullFunc + "),";
856 line = line + "_" + name + "_" + SpecNaming.PostCondition
859 code.addLine(TabbedLine(line, 2));
862 + SpecNaming.NamedFunction
864 + SpecNaming.AppendStr(name + "_"
865 + SpecNaming.PrintValue) + ", "
866 + SpecNaming.PrintValueType + ", (void*) ";
867 if (construct.print.isEmpty()) {
868 line = line + SpecNaming.NullFunc + ")";
870 line = line + "_" + name + "_" + SpecNaming.PrintValue
873 code.addLine(TabbedLine(line, 2));
874 code.addLine(TabbedLine(");"));
876 // init->addInterfaceFunctions(_ENQ_str, stateFuncs);
877 code.addLine(TabbedLine(SpecNaming.AnnoInitInst
879 + SpecNaming.AddInterfaceFunctions
880 + Brace(SpecNaming.AppendStr(name) + ", "
881 + SpecNaming.StateFunctionsInst) + ";"));
886 // Create and instrument with the INIT annotation
887 code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
888 // cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
889 code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc
890 + Brace(SpecNaming.SPEC_ANALYSIS
892 + SpecNaming.SpecAnnotation
893 + Brace(SpecNaming.AnnoTypeInit + ", "
894 + SpecNaming.AnnoInitInst)) + ";"));
904 * This function generates a list of lines that initialize the fields of the
905 * global state struct. See below.
910 * StateStruct *state = (StateStruct*) _M->state;
912 * IntList * q = state->q;
917 * In this example, _M --> methodInst, state --> inst.
925 * The global state construct
926 * @return The generated code
928 public static Code GenerateStateFieldsInitialization(String methodInst,
929 String inst, GlobalConstruct construct) {
930 Code res = new Code();
931 res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct
933 res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst, "("
934 + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
935 for (VariableDeclaration decl : construct.declState) {
936 res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
944 * This function generates a list of lines that initialize the fields of a
945 * specific interface struct. See below.
950 * ENQ *info = (ENQ*) _M->value;
952 * IntList * q = info->q;
957 * In this example, ENQ --> structType, _M --> methodInst, info --> inst
965 * The corresponding interface construct
966 * @return The generated code
968 public static Code GenerateInterfaceFieldsInitialization(String methodInst,
969 String inst, InterfaceConstruct construct) {
970 Code res = new Code();
971 String name = construct.getName();
972 String structName = construct.getStructName();
973 res.addLine(ShortComment("Initialize fields for " + name));
974 // The very first assignment "
975 res.addLine(DeclareDefine(structName, "*" + inst, "(" + structName
976 + "*) " + methodInst + "->" + SpecNaming.MethodValueField));
977 // Don't leave out the RET field
978 if (!construct.getFunctionHeader().isReturnVoid()) {
979 res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
980 SpecNaming.RET, inst + "->" + SpecNaming.RET));
983 for (VariableDeclaration decl : construct.getFunctionHeader().args) {
984 res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
992 * This function generates the code to be inserted right after the ordering
993 * point construct (instrumentation code)
997 * The corresponding ordering point construct
998 * @return The generated code
1000 public static Code Generate4OPConstruct(OPConstruct construct) {
1001 Code code = new Code();
1002 String curLine = construct.annotation;
1003 String label = construct.label;
1004 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
1005 if (!construct.condition.equals("true")) {
1006 code.addLine(prefixTabs + "if (" + construct.condition + ")");
1007 prefixTabs = prefixTabs + "\t";
1010 switch (construct.type) {
1012 code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
1014 case OPDefineUnattached:
1015 code.addLine(prefixTabs + SpecNaming.CreateOPDefineUnattachedFunc
1019 code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
1020 + "(" + SpecNaming.AppendStr(label) + ");");
1023 code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "("
1024 + SpecNaming.AppendStr(label) + ");");
1027 code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();");
1030 code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
1033 case OPClearDefineUnattached:
1034 code.addLine(prefixTabs
1035 + SpecNaming.CreateOPClearDefineUnattachedFunc + "();");
1045 * This function generates the code to be inserted right after the entry
1046 * construct (instrumentation code)
1050 * The corresponding entry construct
1053 public static Code Generate4Entry(EntryConstruct construct) {
1054 Code res = new Code();
1055 String curLine = construct.annotation;
1056 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
1057 // _createInitAnnotation();
1058 res.addLine(prefixTabs + SpecNaming.CreateInitAnnoFunc + "();");
1064 * This function generates the code to be inserted right after the "@Define"
1065 * construct (instrumentation code)
1069 * The corresponding entry construct
1072 public static Code Generate4Define(DefineConstruct construct) {
1073 Code code = new Code();
1075 code.addLine("/********** User-defined code in annotation (BEGIN) **********/");
1076 code.addLines(construct.code);
1077 code.addLine("/********** User-defined code in annotation (END) **********/");
1083 * This function generates the new interface wrapper code to be inserted
1084 * right after the end of the interface definition
1088 * The corresponding interface construct
1089 * @return The generated code
1091 public static Code GenerateInterfaceWrapper(InterfaceConstruct construct) {
1092 Code code = new Code();
1094 String name = construct.getName();
1095 String structName = construct.getStructName();
1096 String beginLine = construct.getFunctionHeader().getHeaderLine();
1097 Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
1098 Matcher matcherSpace = regexpSpace.matcher(beginLine);
1099 String prefixTabs = "";
1100 if (matcherSpace.find())
1101 prefixTabs = matcherSpace.group(1);
1103 // Add one line to separate
1105 code.addLine(prefixTabs
1106 + ShortComment("Generated wrapper interface for " + name));
1107 if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
1109 code.addLine(beginLine + " {");
1111 code.addLine(beginLine);
1113 // Instrument with the INTERFACE_BEGIN annotations
1114 code.addLine(prefixTabs
1116 + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
1117 // CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
1118 code.addLine(prefixTabs
1120 + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
1121 + SpecNaming.AnnoInterfaceInfoInst,
1122 SpecNaming.CreateInterfaceBeginAnnoFunc
1123 + Brace(SpecNaming.AppendStr(name))));
1124 // Call the actual function
1125 code.addLine(prefixTabs + "\t"
1126 + ShortComment("Call the actual function"));
1127 // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
1128 code.addLine(prefixTabs + "\t"
1129 + construct.getFunctionHeader().getRenamedCall() + ";");
1132 // Initialize the value struct
1133 code.addLine(prefixTabs + "\t"
1134 + ShortComment("Initialize the value struct"));
1135 // The very first assignment "
1136 code.addLine(prefixTabs
1138 + DeclareDefine(structName,
1139 "*" + SpecNaming.InterfaceValueInst, SpecNaming.New
1140 + Brace(structName)));
1141 // Don't leave out the RET field
1142 if (!construct.getFunctionHeader().isReturnVoid())
1143 code.addLine(prefixTabs
1145 + AssignToPtr(SpecNaming.InterfaceValueInst,
1146 SpecNaming.RET, SpecNaming.RET));
1148 for (VariableDeclaration decl : construct.getFunctionHeader().args)
1149 code.addLine(prefixTabs
1151 + AssignToPtr(SpecNaming.InterfaceValueInst, decl.name,
1155 // Store the value info into the current MethodCall
1156 // _setInterfaceBeginAnnotationValue(info, value);
1157 code.addLine(prefixTabs
1159 + ShortComment("Store the value info into the current MethodCall"));
1160 code.addLine(prefixTabs
1162 + SpecNaming.SetInterfaceBeginAnnoValueFunc
1163 + Brace(SpecNaming.AnnoInterfaceInfoInst + ", "
1164 + SpecNaming.InterfaceValueInst) + ";");
1167 // Instrument with the INTERFACE_END annotations
1168 code.addLine(prefixTabs + "\t"
1169 + ShortComment("Instrument with the INTERFACE_END annotation"));
1170 // _createInterfaceEndAnnotation(_DEQ_str);
1171 code.addLine(prefixTabs + "\t"
1172 + SpecNaming.CreateInterfaceEndAnnoFunc
1173 + Brace(SpecNaming.AppendStr(name)) + ";");
1175 // Return if necessary
1176 if (!construct.getFunctionHeader().isReturnVoid())
1177 code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");
1178 code.addLine(prefixTabs + "}");
1185 * Write a list of lines (as the whole of the file) to a file ---
1186 * newFileName. If that file does not exist, we create that file and then
1190 * @param newFileName
1191 * The name of the file to be written
1193 * The list of lines that as a whole become the content of the
1196 public static void write2File(String newFileName, ArrayList<String> content) {
1197 File newFile = new File(newFileName);
1198 newFile.getParentFile().mkdirs();
1199 if (!newFile.exists()) {
1201 newFile.createNewFile();
1202 } catch (IOException e) {
1203 e.printStackTrace();
1206 BufferedWriter bw = null;
1208 bw = new BufferedWriter(new FileWriter(newFile));
1209 for (int i = 0; i < content.size(); i++) {
1210 bw.write(content.get(i) + "\n");
1213 } catch (IOException e) {
1214 e.printStackTrace();
1219 } catch (IOException e) {
1220 e.printStackTrace();