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();
217 // C_RET & also the S_RET
218 // The idea is that we store the S_RET in the __value struct, and every time we access/update
219 // S_RET, we actually access "__value->S_RET" (good for read and write)...
220 if (!funcHeader.returnType.equals("void")) {
221 code.addLine(TabbedLine(Declare(funcHeader.returnType,
223 code.addLine(TabbedLine(Declare(funcHeader.returnType,
227 for (VariableDeclaration decl : funcHeader.args) {
228 code.addLine(TabbedLine(Declare(decl)));
230 code.addLine("} " + structName + ";");
235 // Declare INIT annotation instrumentation function
236 code.addLine(ShortComment("Declare INIT annotation instrumentation function"));
237 code.addLine("void _createInitAnnotation();");
240 // Decalre extern "C" --- begin
241 code.addLine("#ifdef __cplusplus");
243 code.addLine("#endif");
247 code.addLine("#endif");
254 * This function generates the code for the CPP file that our specification
255 * generates automatically --- cdsspec-generated.cc.
259 * The SpecExtractor that contains the extracted information
260 * @return The generated code
262 public static Code GenerateCDSSpecCPPFile(SpecExtractor extractor) {
263 GlobalConstruct globalConstruct = extractor.getGlobalConstruct();
264 HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap = extractor.interfaceListMap;
265 HashSet<String> OPLabelSet = extractor.OPLabelSet;
267 Code code = new Code();
269 Code fieldsInit = null;
271 // Add auto-generated comments
273 code.addLine(TabbedLine("This is an implementation file auto-generated by CDSSpec compiler to"));
274 code.addLine(TabbedLine("instrument your benchmark for CDSSpec checker to check. Currently we require"));
275 code.addLine(TabbedLine("a C++ compiler that supports C++11."));
279 code.addLine("#include " + SpecNaming.CDSSpecGeneratedHeader);
280 code.addLine("#include " + SpecNaming.CDSANNOTATE);
281 code.addLine("#include " + SpecNaming.SPEC_COMMON);
282 code.addLine("#include " + SpecNaming.METHODCALL);
283 code.addLine("#include " + SpecNaming.CDSSPEC);
284 code.addLine("#include " + SpecNaming.SPECANNOTATION);
288 // Declare customized StateStruct
289 code.addLine(ShortComment("Declare customized StateStruct"));
290 code.addLine("typedef struct " + SpecNaming.StateStruct + " {");
291 for (VariableDeclaration decl : globalConstruct.declState) {
292 code.addLine(TabbedLine(Declare(decl)));
295 // Define state destructor
296 code.addLine(TabbedLine(ShortComment("Define state destructor")));
297 code.addLine(TabbedLine("~" + SpecNaming.StateStruct + "() {"));
298 if (!globalConstruct.autoGenClear) {
299 code.addLine(TabbedLine(
300 ShortComment("Execute user-defined state clear code"), 2));
302 code.addLine(TabbedLine(
303 ShortComment("Execute auto-generated state clear code"), 2));
305 globalConstruct.clearState.align(2);
306 code.addLines(globalConstruct.clearState);
307 code.addLine(TabbedLine("}"));
310 code.addLine(TabbedLine("SNAPSHOTALLOC"));
312 code.addLine("} " + SpecNaming.StateStruct + ";");
316 // Define the fake ordering point operation
317 code.addLine(ShortComment("Define the fake ordering point operation"));
318 // atomic_int _FAKE_OP_;
319 code.addLine("atomic_int " + SpecNaming.FakeOP + ";");
322 // Define _createOPDefineUnattached
323 code.addLine(ShortComment("Define _createOPDefineUnattached"));
324 code.addLine("void " + SpecNaming.CreateOPDefineUnattachedFunc + "() {");
325 code.addLine(TabbedLine(ShortComment("A load acting as the fake OP")));
326 code.addLine(TabbedLine(SpecNaming.FakeOP
327 + ".load(memory_order_relaxed);"));
328 code.addLine(TabbedLine(SpecNaming.CreateOPDefineAnnoFunc + "();"));
331 // Define _createOPClearDefineUnattached
332 code.addLine(ShortComment("Define _createOPClearDefineUnattached"));
333 code.addLine("void " + SpecNaming.CreateOPClearDefineUnattachedFunc
335 code.addLine(TabbedLine(ShortComment("A load acting as the fake OP")));
336 code.addLine(TabbedLine(SpecNaming.FakeOP
337 + ".load(memory_order_relaxed);"));
338 code.addLine(TabbedLine(SpecNaming.CreateOPClearDefineAnnoFunc + "();"));
341 code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
342 code.addLine(ShortComment("A special empty string"));
343 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,
347 // Interface name strings
348 code.addLine(ShortComment("Interface name strings"));
349 for (File file : interfaceListMap.keySet()) {
350 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
351 for (InterfaceConstruct construct : list) {
352 String name = construct.getName();
353 code.addLine(DeclareDefine(SpecNaming.CString,
354 SpecNaming.AppendStr(name), Quote(name)));
359 // Commutativity rule strings
360 code.addLine(ShortComment("Commutativity rule strings"));
361 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
362 CommutativityRule rule = globalConstruct.commutativityRules
364 code.addLine(DeclareDefine(SpecNaming.CString,
365 SpecNaming.AppendStr(SpecNaming.Commutativity + i),
366 Quote(rule.toString())));
370 // Ordering points label strings
371 code.addLine(ShortComment("Ordering points label strings"));
372 for (String label : OPLabelSet) {
373 code.addLine(DeclareDefine(SpecNaming.CString,
374 SpecNaming.AppendStr(label), Quote(label)));
378 // Special function name strings
379 code.addLine(ShortComment("Special function name strings"));
380 code.addLine(DeclareDefine(SpecNaming.CString,
381 SpecNaming.AppendStr(SpecNaming.InitalState), Quote("_"
382 + SpecNaming.InitalState.toLowerCase())));
383 code.addLine(DeclareDefine(SpecNaming.CString,
384 SpecNaming.AppendStr(SpecNaming.CopyState), Quote("_"
385 + SpecNaming.CopyState.toLowerCase())));
386 code.addLine(DeclareDefine(SpecNaming.CString,
387 SpecNaming.AppendStr(SpecNaming.ClearState), Quote("_"
388 + SpecNaming.ClearState.toLowerCase())));
389 code.addLine(DeclareDefine(SpecNaming.CString,
390 SpecNaming.AppendStr(SpecNaming.FinalState), Quote("_"
391 + SpecNaming.FinalState.toLowerCase())));
392 code.addLine(DeclareDefine(SpecNaming.CString,
393 SpecNaming.AppendStr(SpecNaming.PrintState), Quote("_"
394 + SpecNaming.PrintState.toLowerCase())));
397 // Interface name strings
398 for (File file : interfaceListMap.keySet()) {
399 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
400 for (InterfaceConstruct construct : list) {
401 String name = construct.getName();
402 code.addLine(ShortComment(name + " function strings"));
404 String tmpFunc = name + "_" + SpecNaming.Transition;
405 code.addLine(DeclareDefine(SpecNaming.CString,
406 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
408 tmpFunc = name + "_" + SpecNaming.PreCondition;
409 if (!construct.preCondition.isEmpty())
410 code.addLine(DeclareDefine(SpecNaming.CString,
411 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
413 code.addLine(DeclareDefine(SpecNaming.CString,
414 SpecNaming.AppendStr(tmpFunc),
415 SpecNaming.EmptyCString));
416 // JustifyingPrecondition
417 tmpFunc = name + "_" + SpecNaming.JustifyingPrecondition;
418 if (!construct.justifyingPrecondition.isEmpty())
419 code.addLine(DeclareDefine(SpecNaming.CString,
420 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
422 code.addLine(DeclareDefine(SpecNaming.CString,
423 SpecNaming.AppendStr(tmpFunc),
424 SpecNaming.EmptyCString));
425 // JustifyingPostcondition
426 tmpFunc = name + "_" + SpecNaming.JustifyingPostcondition;
427 if (!construct.justifyingPostcondition.isEmpty())
428 code.addLine(DeclareDefine(SpecNaming.CString,
429 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
431 code.addLine(DeclareDefine(SpecNaming.CString,
432 SpecNaming.AppendStr(tmpFunc),
433 SpecNaming.EmptyCString));
435 tmpFunc = name + "_" + SpecNaming.PostCondition;
436 if (!construct.postCondition.isEmpty())
437 code.addLine(DeclareDefine(SpecNaming.CString,
438 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
440 code.addLine(DeclareDefine(SpecNaming.CString,
441 SpecNaming.AppendStr(tmpFunc),
442 SpecNaming.EmptyCString));
444 tmpFunc = name + "_" + SpecNaming.PrintValue;
445 if (!construct.print.isEmpty())
446 code.addLine(DeclareDefine(SpecNaming.CString,
447 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
449 code.addLine(DeclareDefine(SpecNaming.CString,
450 SpecNaming.AppendStr(tmpFunc),
451 SpecNaming.EmptyCString));
457 code.addLine(ShortComment("Define @" + SpecNaming.InitalState));
458 code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
459 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
460 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
461 + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
463 for (VariableDeclaration decl : globalConstruct.declState) {
464 code.addLine(TabbedLine("#define " + decl.name + " "
465 + SpecNaming.StateInst + "->" + decl.name));
467 if (!globalConstruct.autoGenInitial)
468 code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
470 // Auto-generated the initialization function
471 code.addLine(TabbedLine(ShortComment("Auto-generated state intialization code")));
472 // Align the code with one tab
473 globalConstruct.initState.align(1);
474 code.addLines(globalConstruct.initState);
476 for (VariableDeclaration decl : globalConstruct.declState) {
477 code.addLine(TabbedLine("#undef " + decl.name));
480 code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1,
481 SpecNaming.StateInst, SpecNaming.StateInst)));
486 code.addLine(ShortComment("Define @" + SpecNaming.CopyState));
487 code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
488 + SpecNaming.Method + " " + "dest, " + SpecNaming.Method
490 // StateStruct *OLD = (StateStruct*) src->state;
491 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
492 + SpecNaming.OldStateInst, Brace(SpecNaming.StateStruct + "*")
493 + " src->" + SpecNaming.StateInst)));
494 // StateStruct *NEW = new StateStruct;
495 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
496 + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
497 if (!globalConstruct.autoGenCopy)
498 code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
500 // Auto-generated the copy function
501 code.addLine(TabbedLine(ShortComment("Auto-generated state copy statements")));
502 globalConstruct.copyState.align(1);
503 code.addLines(globalConstruct.copyState);
505 code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst,
506 SpecNaming.NewStateInst)));
511 code.addLine(ShortComment("Define @" + SpecNaming.ClearState));
512 code.addLine("void _" + SpecNaming.ClearState.toLowerCase() + "("
513 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
514 // Retrieve the state
515 code.addLine(TabbedLine(ShortComment("Retrieve the state")));
516 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
517 + SpecNaming.StateInst, "(" + SpecNaming.StateStruct + "*) "
518 + SpecNaming.Method1 + "->state")));
519 // Explicitly call the state destructor
520 code.addLine(TabbedLine(ShortComment("Explicitly call the state destructor")));
521 code.addLine(TabbedLine("delete " + SpecNaming.StateInst + ";"));
526 code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
527 code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
528 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
530 // Initialize state struct fields
531 fieldsInit = GenerateStateFieldsInitialization(SpecNaming.Method1,
532 SpecNaming.StateInst, globalConstruct);
534 code.addLines(fieldsInit);
536 if (!globalConstruct.autoGenPrint)
537 code.addLine(TabbedLine(ShortComment("Execute user-defined state printing code")));
539 // Auto-generated the copy function
540 code.addLine(TabbedLine(ShortComment("Execute auto-generated state printing code")));
542 // Align the code with one tab
543 globalConstruct.printState.align(1);
544 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
553 code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
554 + SpecNaming.Method + " m1, " + SpecNaming.Method
556 // if (m1->name == _ENQ_str && m2->name == _DEQ_str) {
557 code.addLine(TabbedLine("if (m1->name == "
558 + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
559 + SpecNaming.AppendStr(rule.method2) + ") {"));
560 // Initialize M1 & M2 in commutativity rule
561 // e.g. ENQ *M1 = (ENQ*) m1->value;
562 String structName1 = InterfaceConstruct
563 .createStructName(rule.method1);
564 String structName2 = InterfaceConstruct
565 .createStructName(rule.method2);
566 code.addLine(TabbedLine(
567 DeclareDefine(structName1, "*M1", "(" + structName1
568 + "*) m1->value"), 2));
569 code.addLine(TabbedLine(
570 DeclareDefine(structName2, "*M2", "(" + structName2
571 + "*) m2->value"), 2));
572 code.addLine(TabbedLine("return " + rule.condition + ";", 2));
573 code.addLine(TabbedLine("}"));
574 code.addLine(TabbedLine("return false;"));
580 // Define customized interface functions
581 for (File file : interfaceListMap.keySet()) {
582 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
583 for (InterfaceConstruct construct : list) {
586 // Define interface functions
587 String name = construct.getName();
588 String structName = construct.getStructName();
589 code.addLine("/********** " + name
590 + " functions **********/");
591 // Define @Transition for INTERFACE
592 code.addLine(ShortComment("Define @" + SpecNaming.Transition
594 code.addLine("bool _" + name + "_" + SpecNaming.Transition
595 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
596 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
599 // Initialize value struct fields
600 fieldsInit = GenerateInterfaceFieldsInitialization(
601 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
604 code.addLines(fieldsInit);
606 construct.transition.align(1);
607 code.addLine(TabbedLine(ShortComment("Execute Transition")));
608 code.addLines(construct.transition);
610 // By default, we will return true for state transition
611 code.addLine(TabbedLine(ShortComment("By default @Transition returns true")));
612 code.addLine(TabbedLine("return true;"));
616 // Define @PreCondition
617 if (!construct.preCondition.isEmpty()) {
618 code.addLine(ShortComment("Define @"
619 + SpecNaming.PreCondition + " for " + name));
620 code.addLine("bool _" + name + "_" + SpecNaming.PreCondition
621 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
622 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
625 // Initialize value struct fields
626 fieldsInit = GenerateInterfaceFieldsInitialization(
627 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
630 code.addLines(fieldsInit);
632 construct.preCondition.align(1);
633 code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
634 code.addLines(construct.preCondition);
636 // By default, we will return true for @PreCondition
637 code.addLine(TabbedLine(ShortComment("By default @PreCondition returns true")));
638 code.addLine(TabbedLine("return true;"));
644 // Define @JustifyingPrecondition
645 if (!construct.justifyingPrecondition.isEmpty()) {
646 code.addLine(ShortComment("Define @"
647 + SpecNaming.JustifyingPrecondition + " for " + name));
648 code.addLine("bool _" + name + "_" + SpecNaming.JustifyingPrecondition
649 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
650 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
653 // Initialize value struct fields
654 fieldsInit = GenerateInterfaceFieldsInitialization(
655 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
658 code.addLines(fieldsInit);
660 construct.justifyingPrecondition.align(1);
661 code.addLine(TabbedLine(ShortComment("Execute JustifyingPrecondition")));
662 code.addLines(construct.justifyingPrecondition);
664 // By default, we will return true for @JustifyingPrecondition
665 code.addLine(TabbedLine(ShortComment("By default @JustifyingPrecondition returns true")));
666 code.addLine(TabbedLine("return true;"));
672 // Define @JustifyingPostcondition
673 if (!construct.justifyingPostcondition.isEmpty()) {
674 code.addLine(ShortComment("Define @"
675 + SpecNaming.JustifyingPostcondition + " for " + name));
676 code.addLine("bool _" + name + "_" + SpecNaming.JustifyingPostcondition
677 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
678 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
681 // Initialize value struct fields
682 fieldsInit = GenerateInterfaceFieldsInitialization(
683 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
686 code.addLines(fieldsInit);
688 construct.justifyingPostcondition.align(1);
689 code.addLine(TabbedLine(ShortComment("Execute JustifyingPostcondition")));
690 code.addLines(construct.justifyingPostcondition);
692 // By default, we will return true for @JustifyingPostcondition
693 code.addLine(TabbedLine(ShortComment("By default @JustifyingPostcondition returns true")));
694 code.addLine(TabbedLine("return true;"));
700 // Define @PostCondition
701 if (!construct.postCondition.isEmpty()) {
702 code.addLine(ShortComment("Define @"
703 + SpecNaming.PostCondition + " for " + name));
704 code.addLine("bool _" + name + "_" + SpecNaming.PostCondition
705 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
706 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
709 // Initialize value struct fields
710 fieldsInit = GenerateInterfaceFieldsInitialization(
711 SpecNaming.Method2, SpecNaming.InterfaceValueInst,
714 code.addLines(fieldsInit);
716 construct.postCondition.align(1);
717 code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
718 code.addLines(construct.postCondition);
720 // By default, we will return true for @PostCondition
721 code.addLine(TabbedLine(ShortComment("By default @PostCondition returns true")));
722 code.addLine(TabbedLine("return true;"));
728 if (!construct.print.isEmpty()) {
729 code.addLine(ShortComment("Define @"
730 + SpecNaming.PrintValue + " for " + name));
731 code.addLine("void _" + name + "_" + SpecNaming.PrintValue
732 + "(" + SpecNaming.Method + " "
733 + SpecNaming.Method1 + ") {");
734 // Initialize value struct fields
735 fieldsInit = GenerateInterfaceFieldsInitialization(
736 SpecNaming.Method1, SpecNaming.InterfaceValueInst,
739 code.addLines(fieldsInit);
741 construct.print.align(1);
742 if (!construct.autoGenPrint)
743 code.addLine(TabbedLine(ShortComment("Execute user-defined value printing code")));
745 // Auto-generated the value printing function
746 code.addLine(TabbedLine(ShortComment("Execute auto-generated value printing code")));
747 code.addLines(construct.print);
755 // Define INIT annotation instrumentation function
756 code.addLine(ShortComment("Define INIT annotation instrumentation function"));
757 code.addLine("void _createInitAnnotation() {");
759 // Init the fake ordering point place holder
760 code.addLine(TabbedLine(ShortComment("Init the fake ordering point place holder")));
761 code.addLine(TabbedLine(SpecNaming.FakeOP
762 + ".store(1, memory_order_relaxed);"));
764 // Init commutativity rules
765 code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
766 code.addLine(TabbedLine(DeclareDefine("int",
767 SpecNaming.CommutativityRuleSizeInst,
768 Integer.toString(globalConstruct.commutativityRules.size()))));
769 String tmp = SpecNaming.NewSize
770 + Brace(SpecNaming.CommutativityRule + ", sizeof"
771 + Brace(SpecNaming.CommutativityRule) + " * "
772 + SpecNaming.CommutativityRuleSizeInst);
773 code.addLine(TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*"
774 + SpecNaming.CommutativityRuleInst, tmp)));
775 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
776 CommutativityRule rule = globalConstruct.commutativityRules
778 code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ")
780 // new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
781 // _Commutativity1_str, _checkCommutativity1)
783 + Brace(" &" + SpecNaming.CommutativityRuleInst + "["
784 + (i - 1) + "] ") + SpecNaming.CommutativityRule
785 + "(" + SpecNaming.AppendStr(rule.method1) + ", "
786 + SpecNaming.AppendStr(rule.method2) + ", "
787 + SpecNaming.AppendStr(SpecNaming.Commutativity + i) + ", "
788 + "_check" + SpecNaming.Commutativity + i + ");";
789 code.addLine(TabbedLine(line));
792 // Initialize AnnoInit
793 code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
794 // AnnoInit *init = new AnnoInit(
795 code.addLine(TabbedLine(SpecNaming.AnnoInit + " *"
796 + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit
798 // new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
799 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
800 + SpecNaming.AppendStr(SpecNaming.InitalState) + ", "
801 + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
802 + SpecNaming.InitalState.toLowerCase() + "),", 2));
803 // new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
804 line = "new " + SpecNaming.NamedFunction + "("
805 + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
806 + SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
807 if (globalConstruct.finalState.isEmpty()) {
808 line = line + SpecNaming.NullFunc + "),";
810 line = line + "_" + SpecNaming.FinalState.toUpperCase();
812 code.addLine(TabbedLine(line, 2));
813 // new NamedFunction(_Copy_str, COPY, (void*) _copy),
814 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
815 + SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
816 + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
817 + SpecNaming.CopyState.toLowerCase() + "),", 2));
818 // new NamedFunction(_Clear_str, CLEAR, (void*) _clear),
819 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
820 + SpecNaming.AppendStr(SpecNaming.ClearState) + ", "
821 + SpecNaming.ClearState.toUpperCase() + ", " + "(void*) _"
822 + SpecNaming.ClearState.toLowerCase() + "),", 2));
823 // new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
824 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
825 + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
826 + SpecNaming.PrintStateType + ", " + "(void*) _"
827 + SpecNaming.PrintState.toLowerCase() + "),", 2));
828 // commuteRules, CommuteRuleSize);
829 code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
830 + SpecNaming.CommutativityRuleSizeInst + ");", 2));
833 // Declare StateFunctions map
834 code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
835 code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*"
836 + SpecNaming.StateFunctionsInst)));
839 // StateFunction for interface
840 for (File file : interfaceListMap.keySet()) {
841 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
842 for (InterfaceConstruct construct : list) {
843 String name = construct.getName();
844 code.addLine(TabbedLine(ShortComment("StateFunction for "
846 // stateFuncs = new StateFunctions(
847 code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
848 + " = new " + SpecNaming.StateFunctions + "("));
849 // new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
852 code.addLine(TabbedLine(
854 + SpecNaming.NamedFunction
856 + SpecNaming.AppendStr(name + "_"
857 + SpecNaming.Transition) + ", "
858 + SpecNaming.TransitionType + ", (void*) _"
859 + name + "_" + SpecNaming.Transition + "),", 2));
862 + SpecNaming.NamedFunction
864 + SpecNaming.AppendStr(name + "_"
865 + SpecNaming.PreCondition) + ", "
866 + SpecNaming.PreConditionType + ", (void*) ";
867 if (construct.preCondition.isEmpty()) {
868 line = line + SpecNaming.NullFunc + "),";
870 line = line + "_" + name + "_" + SpecNaming.PreCondition
873 code.addLine(TabbedLine(line, 2));
874 // JustifyingPrecondition
876 + SpecNaming.NamedFunction
878 + SpecNaming.AppendStr(name + "_"
879 + SpecNaming.JustifyingPrecondition) + ", "
880 + SpecNaming.JustifyingPreconditionType + ", (void*) ";
881 if (construct.justifyingPrecondition.isEmpty()) {
882 line = line + SpecNaming.NullFunc + "),";
884 line = line + "_" + name + "_" + SpecNaming.JustifyingPrecondition
887 code.addLine(TabbedLine(line, 2));
888 // JustifyingPostcondition
890 + SpecNaming.NamedFunction
892 + SpecNaming.AppendStr(name + "_"
893 + SpecNaming.JustifyingPostcondition) + ", "
894 + SpecNaming.JustifyingPostconditionType + ", (void*) ";
895 if (construct.justifyingPostcondition.isEmpty()) {
896 line = line + SpecNaming.NullFunc + "),";
898 line = line + "_" + name + "_" + SpecNaming.JustifyingPostcondition
901 code.addLine(TabbedLine(line, 2));
904 + SpecNaming.NamedFunction
906 + SpecNaming.AppendStr(name + "_"
907 + SpecNaming.PostCondition) + ", "
908 + SpecNaming.PostConditionType + ", (void*) ";
909 if (construct.postCondition.isEmpty()) {
910 line = line + SpecNaming.NullFunc + "),";
912 line = line + "_" + name + "_" + SpecNaming.PostCondition
915 code.addLine(TabbedLine(line, 2));
918 + SpecNaming.NamedFunction
920 + SpecNaming.AppendStr(name + "_"
921 + SpecNaming.PrintValue) + ", "
922 + SpecNaming.PrintValueType + ", (void*) ";
923 if (construct.print.isEmpty()) {
924 line = line + SpecNaming.NullFunc + ")";
926 line = line + "_" + name + "_" + SpecNaming.PrintValue
929 code.addLine(TabbedLine(line, 2));
930 code.addLine(TabbedLine(");"));
932 // init->addInterfaceFunctions(_ENQ_str, stateFuncs);
933 code.addLine(TabbedLine(SpecNaming.AnnoInitInst
935 + SpecNaming.AddInterfaceFunctions
936 + Brace(SpecNaming.AppendStr(name) + ", "
937 + SpecNaming.StateFunctionsInst) + ";"));
942 // Create and instrument with the INIT annotation
943 code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
944 // cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
945 code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc
946 + Brace(SpecNaming.SPEC_ANALYSIS
948 + SpecNaming.SpecAnnotation
949 + Brace(SpecNaming.AnnoTypeInit + ", "
950 + SpecNaming.AnnoInitInst)) + ";"));
960 * This function generates a list of lines that initialize the fields of the
961 * global state struct. See below.
966 * StateStruct *state = (StateStruct*) _M->state;
968 * IntList * q = state->q;
973 * In this example, _M --> methodInst, state --> inst.
981 * The global state construct
982 * @return The generated code
984 public static Code GenerateStateFieldsInitialization(String methodInst,
985 String inst, GlobalConstruct construct) {
986 Code res = new Code();
987 res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct
989 res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst, "("
990 + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
991 for (VariableDeclaration decl : construct.declState) {
992 res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
1000 * This function generates a list of lines that initialize the fields of a
1001 * specific interface struct. See below.
1006 * ENQ *info = (ENQ*) _M->value;
1008 * IntList * q = info->q;
1013 * In this example, ENQ --> structType, _M --> methodInst, info --> inst
1021 * The corresponding interface construct
1022 * @return The generated code
1024 public static Code GenerateInterfaceFieldsInitialization(String methodInst,
1025 String inst, InterfaceConstruct construct) {
1026 Code res = new Code();
1027 String name = construct.getName();
1028 String structName = construct.getStructName();
1029 res.addLine(ShortComment("Initialize fields for " + name));
1030 // The very first assignment "
1031 res.addLine(DeclareDefine(structName, "*" + inst, "(" + structName
1032 + "*) " + methodInst + "->" + SpecNaming.MethodValueField));
1033 // Don't leave out the C_RET field
1034 if (!construct.getFunctionHeader().isReturnVoid()) {
1035 res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
1036 SpecNaming.C_RET, inst + "->" + SpecNaming.C_RET));
1039 for (VariableDeclaration decl : construct.getFunctionHeader().args) {
1040 res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
1048 * This function generates the code to be inserted right after the ordering
1049 * point construct (instrumentation code)
1053 * The corresponding ordering point construct
1054 * @return The generated code
1056 public static Code Generate4OPConstruct(OPConstruct construct) {
1057 Code code = new Code();
1058 String curLine = construct.annotation;
1059 String label = construct.label;
1060 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
1061 if (!construct.condition.equals("true")) {
1062 code.addLine(prefixTabs + "if (" + construct.condition + ")");
1063 prefixTabs = prefixTabs + "\t";
1066 switch (construct.type) {
1068 code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
1070 case OPDefineUnattached:
1071 code.addLine(prefixTabs + SpecNaming.CreateOPDefineUnattachedFunc
1075 code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
1076 + "(" + SpecNaming.AppendStr(label) + ");");
1079 code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "("
1080 + SpecNaming.AppendStr(label) + ");");
1083 code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();");
1086 code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
1089 case OPClearDefineUnattached:
1090 code.addLine(prefixTabs
1091 + SpecNaming.CreateOPClearDefineUnattachedFunc + "();");
1101 * This function generates the code to be inserted right after the entry
1102 * construct (instrumentation code)
1106 * The corresponding entry construct
1109 public static Code Generate4Entry(EntryConstruct construct) {
1110 Code res = new Code();
1111 String curLine = construct.annotation;
1112 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
1113 // _createInitAnnotation();
1114 res.addLine(prefixTabs + SpecNaming.CreateInitAnnoFunc + "();");
1120 * This function generates the code to be inserted right after the "@Define"
1121 * construct (instrumentation code)
1125 * The corresponding entry construct
1128 public static Code Generate4Define(DefineConstruct construct) {
1129 Code code = new Code();
1131 code.addLine("/********** User-defined code in annotation (BEGIN) **********/");
1132 code.addLines(construct.code);
1133 code.addLine("/********** User-defined code in annotation (END) **********/");
1139 * This function generates the new interface wrapper code to be inserted
1140 * right after the end of the interface definition
1144 * The corresponding interface construct
1145 * @return The generated code
1147 public static Code GenerateInterfaceWrapper(InterfaceConstruct construct) {
1148 Code code = new Code();
1150 String name = construct.getName();
1151 String structName = construct.getStructName();
1152 String beginLine = construct.getFunctionHeader().getHeaderLine();
1153 Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
1154 Matcher matcherSpace = regexpSpace.matcher(beginLine);
1155 String prefixTabs = "";
1156 if (matcherSpace.find())
1157 prefixTabs = matcherSpace.group(1);
1159 // Add one line to separate
1161 code.addLine(prefixTabs
1162 + ShortComment("Generated wrapper interface for " + name));
1163 if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
1165 code.addLine(beginLine + " {");
1167 code.addLine(beginLine);
1169 // Instrument with the INTERFACE_BEGIN annotations
1170 code.addLine(prefixTabs
1172 + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
1173 // CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
1174 code.addLine(prefixTabs
1176 + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
1177 + SpecNaming.AnnoInterfaceInfoInst,
1178 SpecNaming.CreateInterfaceBeginAnnoFunc
1179 + Brace(SpecNaming.AppendStr(name))));
1180 // Call the actual function
1181 code.addLine(prefixTabs + "\t"
1182 + ShortComment("Call the actual function"));
1183 // bool C_RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
1184 code.addLine(prefixTabs + "\t"
1185 + construct.getFunctionHeader().getRenamedCall() + ";");
1188 // Initialize the value struct
1189 code.addLine(prefixTabs + "\t"
1190 + ShortComment("Initialize the value struct"));
1191 // The very first assignment "
1192 code.addLine(prefixTabs
1194 + DeclareDefine(structName,
1195 "*" + SpecNaming.InterfaceValueInst, SpecNaming.New
1196 + Brace(structName)));
1197 // Don't leave out the C_RET field
1198 if (!construct.getFunctionHeader().isReturnVoid())
1199 code.addLine(prefixTabs
1201 + AssignToPtr(SpecNaming.InterfaceValueInst,
1202 SpecNaming.C_RET, SpecNaming.C_RET));
1204 for (VariableDeclaration decl : construct.getFunctionHeader().args)
1205 code.addLine(prefixTabs
1207 + AssignToPtr(SpecNaming.InterfaceValueInst, decl.name,
1211 // Store the value info into the current MethodCall
1212 // _setInterfaceBeginAnnotationValue(info, value);
1213 code.addLine(prefixTabs
1215 + ShortComment("Store the value info into the current MethodCall"));
1216 code.addLine(prefixTabs
1218 + SpecNaming.SetInterfaceBeginAnnoValueFunc
1219 + Brace(SpecNaming.AnnoInterfaceInfoInst + ", "
1220 + SpecNaming.InterfaceValueInst) + ";");
1223 // Instrument with the INTERFACE_END annotations
1224 code.addLine(prefixTabs + "\t"
1225 + ShortComment("Instrument with the INTERFACE_END annotation"));
1226 // _createInterfaceEndAnnotation(_DEQ_str);
1227 code.addLine(prefixTabs + "\t"
1228 + SpecNaming.CreateInterfaceEndAnnoFunc
1229 + Brace(SpecNaming.AppendStr(name)) + ";");
1231 // Return if necessary
1232 if (!construct.getFunctionHeader().isReturnVoid())
1233 code.addLine(prefixTabs + "\treturn " + SpecNaming.C_RET + ";");
1234 code.addLine(prefixTabs + "}");
1241 * Write a list of lines (as the whole of the file) to a file ---
1242 * newFileName. If that file does not exist, we create that file and then
1246 * @param newFileName
1247 * The name of the file to be written
1249 * The list of lines that as a whole become the content of the
1252 public static void write2File(String newFileName, ArrayList<String> content) {
1253 File newFile = new File(newFileName);
1254 newFile.getParentFile().mkdirs();
1255 if (!newFile.exists()) {
1257 newFile.createNewFile();
1258 } catch (IOException e) {
1259 e.printStackTrace();
1262 BufferedWriter bw = null;
1264 bw = new BufferedWriter(new FileWriter(newFile));
1265 for (int i = 0; i < content.size(); i++) {
1266 bw.write(content.get(i) + "\n");
1269 } catch (IOException e) {
1270 e.printStackTrace();
1275 } catch (IOException e) {
1276 e.printStackTrace();