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 code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
173 code.addLine(ShortComment("A special empty string"));
174 code.addLine(Declare("extern " + SpecNaming.CString,
175 SpecNaming.EmptyCString));
178 // Interface name strings
179 code.addLine(ShortComment("Interface name strings"));
180 for (File file : interfaceListMap.keySet()) {
181 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
182 for (InterfaceConstruct construct : list) {
183 String name = construct.getName();
184 code.addLine(Declare("extern " + SpecNaming.CString,
185 SpecNaming.AppendStr(name)));
190 // Commutativity rule strings
191 code.addLine(ShortComment("Commutativity rule strings"));
192 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
193 code.addLine(Declare("extern " + SpecNaming.CString,
194 SpecNaming.AppendStr(SpecNaming.Commutativity + i)));
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 // Special function name strings
207 code.addLine(ShortComment("Special function name strings"));
208 code.addLine(Declare("extern " + SpecNaming.CString,
209 SpecNaming.AppendStr(SpecNaming.InitalState)));
210 code.addLine(Declare("extern " + SpecNaming.CString,
211 SpecNaming.AppendStr(SpecNaming.CopyState)));
212 code.addLine(Declare("extern " + SpecNaming.CString,
213 SpecNaming.AppendStr(SpecNaming.FinalState)));
214 code.addLine(Declare("extern " + SpecNaming.CString,
215 SpecNaming.AppendStr(SpecNaming.PrintState)));
218 // Interface name strings
219 for (File file : interfaceListMap.keySet()) {
220 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
221 for (InterfaceConstruct construct : list) {
222 String name = construct.getName();
223 code.addLine(ShortComment(name + " function strings"));
225 String tmpFunc = name + "_" + SpecNaming.Transition;
226 code.addLine(Declare("extern " + SpecNaming.CString,
227 SpecNaming.AppendStr(tmpFunc)));
229 tmpFunc = name + "_" + SpecNaming.PreCondition;
230 code.addLine(Declare("extern " + SpecNaming.CString,
231 SpecNaming.AppendStr(tmpFunc)));
233 tmpFunc = name + "_" + SpecNaming.SideEffect;
234 code.addLine(Declare("extern " + SpecNaming.CString,
235 SpecNaming.AppendStr(tmpFunc)));
237 tmpFunc = name + "_" + SpecNaming.PostCondition;
238 code.addLine(Declare("extern " + SpecNaming.CString,
239 SpecNaming.AppendStr(tmpFunc)));
241 tmpFunc = name + "_" + SpecNaming.PrintValue;
242 code.addLine(Declare("extern " + SpecNaming.CString,
243 SpecNaming.AppendStr(tmpFunc)));
248 // Declare customized value struct
249 for (File file : interfaceListMap.keySet()) {
250 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
251 for (InterfaceConstruct construct : list) {
252 // Declare custom value struct for the interface
253 String name = construct.getName();
254 code.addLine(ShortComment("Declare custom value struct for "
256 code.addLine("typedef struct " + name + " {");
257 FunctionHeader funcHeader = construct.getFunctionHeader();
259 if (!funcHeader.returnType.equals("void"))
260 code.addLine(TabbedLine(Declare(funcHeader.returnType,
263 for (VariableDeclaration decl : funcHeader.args) {
264 code.addLine(TabbedLine(Declare(decl)));
266 code.addLine("} " + name + ";");
272 code.addLine(ShortComment("Declare @" + SpecNaming.InitalState));
273 code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
274 + SpecNaming.Method + " " + SpecNaming.Method1 + ");");
277 code.addLine(ShortComment("Declare @" + SpecNaming.CopyState));
278 code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
279 + SpecNaming.Method + " " + "dest, " + SpecNaming.Method
283 code.addLine(ShortComment("Declare @" + SpecNaming.PrintState));
284 if (!globalConstruct.printState.isEmpty()) {
285 code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
286 + SpecNaming.Method + " " + SpecNaming.Method1 + ");");
290 // Declare @Commutativity
291 code.addLine(ShortComment("Declare commutativity checking functions"));
292 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
293 code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
294 + SpecNaming.Method + " m1, " + SpecNaming.Method + " m2);");
298 // Declare customized interface functions
299 for (File file : interfaceListMap.keySet()) {
300 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
301 for (InterfaceConstruct construct : list) {
302 // Declare interface functions
303 String name = construct.getName();
304 code.addLine("/********** " + name
305 + " functions **********/");
306 // Declare @Transition for INTERFACE
307 code.addLine(ShortComment("Declare @" + SpecNaming.Transition
309 code.addLine("void _" + name + "_" + SpecNaming.Transition
310 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
311 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
314 // Declare @PreCondition
315 if (!construct.preCondition.isEmpty()) {
316 code.addLine(ShortComment("Declare @"
317 + SpecNaming.PreCondition + " for " + name));
318 code.addLine("bool _" + name + "_"
319 + SpecNaming.PreCondition + "(" + SpecNaming.Method
320 + " " + SpecNaming.Method1 + ");");
323 // Declare @SideEffect
324 if (!construct.sideEffect.isEmpty()) {
325 code.addLine(ShortComment("Declare @"
326 + SpecNaming.SideEffect + " for " + name));
327 code.addLine("void _" + name + "_" + SpecNaming.SideEffect
328 + "(" + SpecNaming.Method + " "
329 + SpecNaming.Method1 + ");");
332 // Declare @PostCondition
333 if (!construct.postCondition.isEmpty()) {
334 code.addLine(ShortComment("Declare @"
335 + SpecNaming.PostCondition + " for " + name));
336 code.addLine("bool _" + name + "_"
337 + SpecNaming.PostCondition + "("
338 + SpecNaming.Method + " " + SpecNaming.Method1
343 if (!construct.print.isEmpty()) {
344 code.addLine(ShortComment("Declare @"
345 + SpecNaming.PrintValue + " for " + name));
346 code.addLine("void _" + name + "_" + SpecNaming.PrintValue
347 + "(" + SpecNaming.Method + " "
348 + SpecNaming.Method1 + ");");
354 // Declare INIT annotation instrumentation function
355 code.addLine(ShortComment("Declare INIT annotation instrumentation function"));
356 code.addLine("void _createInitAnnotation();");
359 // Decalre extern "C" --- begin
360 code.addLine("#ifdef __cplusplus");
362 code.addLine("#endif");
366 code.addLine("#endif");
373 * This function generates the code for the CPP file that our specification
374 * generates automatically --- cdsspec-generated.cc.
378 * The SpecExtractor that contains the extracted information
379 * @return The generated code
381 public static Code GenerateCDSSpecCPPFile(SpecExtractor extractor) {
382 GlobalConstruct globalConstruct = extractor.getGlobalConstruct();
383 HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap = extractor.interfaceListMap;
384 HashSet<String> OPLabelSet = extractor.OPLabelSet;
386 Code code = new Code();
389 // Add auto-generated comments
391 code.addLine(TabbedLine("This is an implementation file auto-generated by CDSSpec compiler to"));
392 code.addLine(TabbedLine("instrument your benchmark for CDSSpec checker to check. Currently we require"));
393 code.addLine(TabbedLine("a C++ compiler that supports C++11."));
397 code.addLine("#include " + SpecNaming.CDSSpecGeneratedHeader);
398 code.addLine("#include " + SpecNaming.CDSANNOTATE);
399 code.addLine("#include " + SpecNaming.SPEC_COMMON);
400 code.addLine("#include " + SpecNaming.METHODCALL);
401 code.addLine("#include " + SpecNaming.CDSSPEC);
402 code.addLine("#include " + SpecNaming.SPECANNOTATION);
406 // Declare customized StateStruct
407 code.addLine(ShortComment("Declare customized StateStruct"));
408 code.addLine("typedef struct " + SpecNaming.StateStruct + " {");
409 for (VariableDeclaration decl : globalConstruct.declState) {
410 code.addLine(TabbedLine(Declare(decl)));
413 code.addLine(TabbedLine("SNAPSHOTALLOC"));
414 code.addLine("} " + SpecNaming.StateStruct + ";");
418 code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
419 code.addLine(ShortComment("A special empty string"));
420 code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,
424 // Interface name strings
425 code.addLine(ShortComment("Interface name strings"));
426 for (File file : interfaceListMap.keySet()) {
427 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
428 for (InterfaceConstruct construct : list) {
429 String name = construct.getName();
430 code.addLine(DeclareDefine(SpecNaming.CString,
431 SpecNaming.AppendStr(name), Quote(name)));
436 // Commutativity rule strings
437 code.addLine(ShortComment("Commutativity rule strings"));
438 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
439 CommutativityRule rule = globalConstruct.commutativityRules
441 code.addLine(DeclareDefine(SpecNaming.CString,
442 SpecNaming.AppendStr(SpecNaming.Commutativity + i),
443 Quote(rule.toString())));
447 // Ordering points label strings
448 code.addLine(ShortComment("Ordering points label strings"));
449 for (String label : OPLabelSet) {
450 code.addLine(DeclareDefine(SpecNaming.CString,
451 SpecNaming.AppendStr(label), Quote(label)));
455 // Special function name strings
456 code.addLine(ShortComment("Special function name strings"));
457 code.addLine(DeclareDefine(SpecNaming.CString,
458 SpecNaming.AppendStr(SpecNaming.InitalState), Quote("_"
459 + SpecNaming.InitalState.toLowerCase())));
460 code.addLine(DeclareDefine(SpecNaming.CString,
461 SpecNaming.AppendStr(SpecNaming.CopyState), Quote("_"
462 + SpecNaming.CopyState.toLowerCase())));
463 code.addLine(DeclareDefine(SpecNaming.CString,
464 SpecNaming.AppendStr(SpecNaming.FinalState), Quote("_"
465 + SpecNaming.FinalState.toLowerCase())));
466 code.addLine(DeclareDefine(SpecNaming.CString,
467 SpecNaming.AppendStr(SpecNaming.PrintState), Quote("_"
468 + SpecNaming.PrintState.toLowerCase())));
471 // Interface name strings
472 for (File file : interfaceListMap.keySet()) {
473 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
474 for (InterfaceConstruct construct : list) {
475 String name = construct.getName();
476 code.addLine(ShortComment(name + " function strings"));
478 String tmpFunc = name + "_" + SpecNaming.Transition;
479 code.addLine(DeclareDefine(SpecNaming.CString,
480 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
482 tmpFunc = name + "_" + SpecNaming.PreCondition;
483 if (!construct.preCondition.isEmpty())
484 code.addLine(DeclareDefine(SpecNaming.CString,
485 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
487 code.addLine(DeclareDefine(SpecNaming.CString,
488 SpecNaming.AppendStr(tmpFunc),
489 SpecNaming.EmptyCString));
491 tmpFunc = name + "_" + SpecNaming.SideEffect;
492 if (!construct.sideEffect.isEmpty())
493 code.addLine(DeclareDefine(SpecNaming.CString,
494 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
496 code.addLine(DeclareDefine(SpecNaming.CString,
497 SpecNaming.AppendStr(tmpFunc),
498 SpecNaming.EmptyCString));
500 tmpFunc = name + "_" + SpecNaming.PostCondition;
501 if (!construct.postCondition.isEmpty())
502 code.addLine(DeclareDefine(SpecNaming.CString,
503 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
505 code.addLine(DeclareDefine(SpecNaming.CString,
506 SpecNaming.AppendStr(tmpFunc),
507 SpecNaming.EmptyCString));
509 tmpFunc = name + "_" + SpecNaming.PrintValue;
510 if (!construct.print.isEmpty())
511 code.addLine(DeclareDefine(SpecNaming.CString,
512 SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
514 code.addLine(DeclareDefine(SpecNaming.CString,
515 SpecNaming.AppendStr(tmpFunc),
516 SpecNaming.EmptyCString));
522 code.addLine(ShortComment("Define @" + SpecNaming.InitalState));
523 code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
524 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
525 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
526 + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
528 for (VariableDeclaration decl : globalConstruct.declState) {
529 code.addLine(TabbedLine("#define " + decl.name + " "
530 + SpecNaming.StateInst + "->" + decl.name));
532 code.addLine(TabbedLine(ShortComment("User-defined intial state code")));
533 // Align the code with one tab
534 globalConstruct.initState.align(1);
535 code.addLines(globalConstruct.initState);
537 for (VariableDeclaration decl : globalConstruct.declState) {
538 code.addLine(TabbedLine("#undef " + decl.name));
541 code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1,
542 SpecNaming.StateInst, SpecNaming.StateInst)));
547 code.addLine(ShortComment("Define @" + SpecNaming.CopyState));
548 code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
549 + SpecNaming.Method + " " + "dest, " + SpecNaming.Method
551 // StateStruct *OLD = (StateStruct*) src->state;
552 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
553 + SpecNaming.OldStateInst, Brace(SpecNaming.StateStruct + "*")
554 + " src->" + SpecNaming.StateInst)));
555 // StateStruct *NEW = new StateStruct;
556 code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
557 + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
558 if (!globalConstruct.autoGenCopy)
559 code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
561 // Auto-generated the copy function
562 code.addLine(TabbedLine(ShortComment("Auto-generated state copy statements")));
563 globalConstruct.copyState.align(1);
564 code.addLines(globalConstruct.copyState);
566 code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst,
567 SpecNaming.NewStateInst)));
572 if (!globalConstruct.printState.isEmpty()) {
573 code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
574 code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
575 + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
577 // Initialize state struct fields
578 Code fieldsInit = GenerateStateFieldsInitialization(
579 SpecNaming.Method1, SpecNaming.StateInst, globalConstruct);
581 code.addLines(fieldsInit);
583 code.addLine(TabbedLine(ShortComment("Execute the print-out")));
584 // Align the code with one tab
585 globalConstruct.printState.align(1);
586 code.addLines(globalConstruct.printState);
591 // Define @Commutativity
592 code.addLine(ShortComment("Define commutativity checking functions"));
593 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
594 CommutativityRule rule = globalConstruct.commutativityRules
596 code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
597 + SpecNaming.Method + " m1, " + SpecNaming.Method
599 // if (m1->name == _ENQ_str && m2->name == _DEQ_str) {
600 code.addLine(TabbedLine("if (m1->name == "
601 + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
602 + SpecNaming.AppendStr(rule.method2) + ") {"));
603 // Initialize M1 & M2 in commutativity rule
604 // e.g. ENQ *M1 = (ENQ*) m1->value;
605 code.addLine(TabbedLine(
606 DeclareDefine(rule.method1, "*M1", "(" + rule.method1
607 + "*) m1->value"), 2));
608 code.addLine(TabbedLine(
609 DeclareDefine(rule.method2, "*M2", "(" + rule.method2
610 + "*) m2->value"), 2));
611 code.addLine(TabbedLine("return " + rule.condition + ";", 2));
612 code.addLine(TabbedLine("}"));
613 code.addLine(TabbedLine("return false;"));
619 // Define customized interface functions
620 for (File file : interfaceListMap.keySet()) {
621 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
622 for (InterfaceConstruct construct : list) {
623 Code fieldsInit = null;
625 // Define interface functions
626 String name = construct.getName();
627 code.addLine("/********** " + name
628 + " functions **********/");
629 // Define @Transition for INTERFACE
630 code.addLine(ShortComment("Define @" + SpecNaming.Transition
632 code.addLine("void _" + name + "_" + SpecNaming.Transition
633 + "(" + SpecNaming.Method + " " + SpecNaming.Method1
634 + ", " + SpecNaming.Method + " " + SpecNaming.Method2
637 // Initialize value struct fields
638 fieldsInit = GenerateInterfaceFieldsInitialization(
639 SpecNaming.Method2, "value", construct);
641 code.addLines(fieldsInit);
643 construct.transition.align(1);
644 code.addLine(TabbedLine(ShortComment("Execute Transition")));
645 code.addLines(construct.transition);
650 // Define @PreCondition
651 if (!construct.preCondition.isEmpty()) {
652 code.addLine(ShortComment("Define @"
653 + SpecNaming.PreCondition + " for " + name));
654 code.addLine("bool _" + name + "_"
655 + SpecNaming.PreCondition + "(" + SpecNaming.Method
656 + " " + SpecNaming.Method1 + ") {");
658 // Initialize value struct fields
659 fieldsInit = GenerateInterfaceFieldsInitialization(
660 SpecNaming.Method1, "value", construct);
662 code.addLines(fieldsInit);
664 construct.preCondition.align(1);
665 code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
666 code.addLines(construct.preCondition);
672 // Define @SideEffect
673 if (!construct.sideEffect.isEmpty()) {
674 code.addLine(ShortComment("Define @"
675 + SpecNaming.SideEffect + " for " + name));
676 code.addLine("void _" + name + "_" + SpecNaming.SideEffect
677 + "(" + SpecNaming.Method + " "
678 + SpecNaming.Method1 + ") {");
680 // Initialize value struct fields
681 fieldsInit = GenerateInterfaceFieldsInitialization(
682 SpecNaming.Method1, "value", construct);
684 code.addLines(fieldsInit);
686 construct.sideEffect.align(1);
687 code.addLine(TabbedLine(ShortComment("Execute SideEffect")));
688 code.addLines(construct.sideEffect);
693 // Define @PostCondition
694 if (!construct.postCondition.isEmpty()) {
695 code.addLine(ShortComment("Define @"
696 + SpecNaming.PostCondition + " for " + name));
697 code.addLine("bool _" + name + "_"
698 + SpecNaming.PostCondition + "("
699 + SpecNaming.Method + " " + SpecNaming.Method1
702 // Initialize value struct fields
703 fieldsInit = GenerateInterfaceFieldsInitialization(
704 SpecNaming.Method1, "value", construct);
706 code.addLines(fieldsInit);
708 construct.postCondition.align(1);
709 code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
710 code.addLines(construct.postCondition);
716 if (!construct.print.isEmpty()) {
717 code.addLine(ShortComment("Define @"
718 + SpecNaming.PrintValue + " for " + name));
719 code.addLine("void _" + name + "_" + SpecNaming.PrintValue
720 + "(" + SpecNaming.Method + " "
721 + SpecNaming.Method1 + ") {");
722 // Initialize value struct fields
723 fieldsInit = GenerateInterfaceFieldsInitialization(
724 SpecNaming.Method1, "value", construct);
726 code.addLines(fieldsInit);
728 construct.print.align(1);
729 code.addLine(TabbedLine(ShortComment("Execute Print")));
730 code.addLines(construct.print);
738 // Define INIT annotation instrumentation function
739 code.addLine(ShortComment("Define INIT annotation instrumentation function"));
740 code.addLine("void _createInitAnnotation() {");
742 // Init commutativity rules
743 code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
744 code.addLine(TabbedLine(DeclareDefine("int",
745 SpecNaming.CommutativityRuleSizeInst,
746 Integer.toString(globalConstruct.commutativityRules.size()))));
747 String tmp = SpecNaming.NewSize
748 + Brace(SpecNaming.CommutativityRule + ", sizeof"
749 + Brace(SpecNaming.CommutativityRule) + " * "
750 + SpecNaming.CommutativityRuleSizeInst);
751 code.addLine(TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*"
752 + SpecNaming.CommutativityRuleInst, tmp)));
753 for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
754 CommutativityRule rule = globalConstruct.commutativityRules
756 code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ")
758 // new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
759 // _Commutativity1_str, _checkCommutativity1)
761 + Brace(" &" + SpecNaming.CommutativityRuleInst + "["
762 + (i - 1) + "] ") + SpecNaming.CommutativityRule
763 + "(" + SpecNaming.AppendStr(rule.method1) + ", "
764 + SpecNaming.AppendStr(rule.method2) + ", "
765 + SpecNaming.AppendStr(SpecNaming.Commutativity + i) + ", "
766 + "_check" + SpecNaming.Commutativity + i + ");";
767 code.addLine(TabbedLine(line));
770 // Initialize AnnoInit
771 code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
772 // AnnoInit *init = new AnnoInit(
773 code.addLine(TabbedLine(SpecNaming.AnnoInit + " *"
774 + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit
776 // new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
777 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
778 + SpecNaming.AppendStr(SpecNaming.InitalState) + ", "
779 + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
780 + SpecNaming.InitalState.toLowerCase() + "),", 2));
781 // new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
782 line = "new " + SpecNaming.NamedFunction + "("
783 + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
784 + SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
785 if (globalConstruct.finalState.isEmpty()) {
786 line = line + SpecNaming.NullFunc + "),";
788 line = line + "_" + SpecNaming.FinalState.toUpperCase();
790 code.addLine(TabbedLine(line, 2));
791 // new NamedFunction(_Copy_str, COPY, (void*) _copy),
792 code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
793 + SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
794 + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
795 + SpecNaming.CopyState.toLowerCase() + "),", 2));
796 // new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
797 line = "new " + SpecNaming.NamedFunction + "("
798 + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
799 + SpecNaming.PrintStateType + ", " + "(void*)";
800 if (globalConstruct.printState.isEmpty()) {
801 line = line + SpecNaming.NullFunc + "),";
803 line = line + "_" + SpecNaming.PrintState.toLowerCase() + "),";
805 code.addLine(TabbedLine(line, 2));
806 // commuteRules, CommuteRuleSize);
807 code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
808 + SpecNaming.CommutativityRuleSizeInst + ");", 2));
811 // Declare StateFunctions map
812 code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
813 code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*"
814 + SpecNaming.StateFunctionsInst)));
817 // StateFunction for interface
818 for (File file : interfaceListMap.keySet()) {
819 ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
820 for (InterfaceConstruct construct : list) {
821 String name = construct.getName();
822 code.addLine(TabbedLine(ShortComment("StateFunction for "
824 // stateFuncs = new StateFunctions(
825 code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
826 + " = new " + SpecNaming.StateFunctions + "("));
827 // new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
830 code.addLine(TabbedLine(
832 + SpecNaming.NamedFunction
834 + SpecNaming.AppendStr(name + "_"
835 + SpecNaming.Transition) + ", "
836 + SpecNaming.TransitionType + ", (void*) _"
837 + name + "_" + SpecNaming.Transition + "),", 2));
840 + SpecNaming.NamedFunction
842 + SpecNaming.AppendStr(name + "_"
843 + SpecNaming.PreCondition) + ", "
844 + SpecNaming.PreConditionType + ", (void*) ";
845 if (construct.preCondition.isEmpty()) {
846 line = line + SpecNaming.NullFunc + "),";
848 line = line + "_" + name + "_" + SpecNaming.PreCondition
851 code.addLine(TabbedLine(line, 2));
854 + SpecNaming.NamedFunction
856 + SpecNaming.AppendStr(name + "_"
857 + SpecNaming.SideEffect) + ", "
858 + SpecNaming.SideEffectType + ", (void*) ";
859 if (construct.sideEffect.isEmpty()) {
860 line = line + SpecNaming.NullFunc + "),";
862 line = line + "_" + name + "_" + SpecNaming.SideEffect
865 code.addLine(TabbedLine(line, 2));
868 + SpecNaming.NamedFunction
870 + SpecNaming.AppendStr(name + "_"
871 + SpecNaming.PostCondition) + ", "
872 + SpecNaming.PostConditionType + ", (void*) ";
873 if (construct.postCondition.isEmpty()) {
874 line = line + SpecNaming.NullFunc + "),";
876 line = line + "_" + name + "_" + SpecNaming.PostCondition
879 code.addLine(TabbedLine(line, 2));
882 + SpecNaming.NamedFunction
884 + SpecNaming.AppendStr(name + "_"
885 + SpecNaming.PrintValue) + ", "
886 + SpecNaming.PrintValueType + ", (void*) ";
887 if (construct.print.isEmpty()) {
888 line = line + SpecNaming.NullFunc + ")";
890 line = line + "_" + name + "_" + SpecNaming.PrintValue
893 code.addLine(TabbedLine(line, 2));
894 code.addLine(TabbedLine(");"));
896 // init->addInterfaceFunctions(_ENQ_str, stateFuncs);
897 code.addLine(TabbedLine(SpecNaming.AnnoInitInst
899 + SpecNaming.AddInterfaceFunctions
900 + Brace(SpecNaming.AppendStr(name) + ", "
901 + SpecNaming.StateFunctionsInst) + ";"));
906 // Create and instrument with the INIT annotation
907 code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
908 // cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
909 code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc
910 + Brace(SpecNaming.SPEC_ANALYSIS
912 + SpecNaming.SpecAnnotation
913 + Brace(SpecNaming.AnnoTypeInit + ", "
914 + SpecNaming.AnnoInitInst)) + ";"));
924 * This function generates a list of lines that initialize the fields of the
925 * global state struct. See below.
930 * StateStruct *state = (StateStruct*) _M->state;
932 * IntList * q = state->q;
937 * In this example, _M --> methodInst, state --> inst.
945 * The global state construct
946 * @return The generated code
948 public static Code GenerateStateFieldsInitialization(String methodInst,
949 String inst, GlobalConstruct construct) {
950 Code res = new Code();
951 res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct
953 res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst, "("
954 + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
955 for (VariableDeclaration decl : construct.declState) {
956 res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
964 * This function generates a list of lines that initialize the fields of a
965 * specific interface struct. See below.
970 * ENQ *info = (ENQ*) _M->value;
972 * IntList * q = info->q;
977 * In this example, ENQ --> structType, _M --> methodInst, info --> inst
985 * The corresponding interface construct
986 * @return The generated code
988 public static Code GenerateInterfaceFieldsInitialization(String methodInst,
989 String inst, InterfaceConstruct construct) {
990 Code res = new Code();
991 String name = construct.getName();
992 res.addLine(ShortComment("Initialize fields for " + name));
993 // The very first assignment "
994 res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) "
995 + methodInst + "->value"));
996 // Don't leave out the RET field
997 if (!construct.getFunctionHeader().isReturnVoid()) {
998 res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
999 SpecNaming.RET, "value->" + SpecNaming.RET));
1002 for (VariableDeclaration decl : construct.getFunctionHeader().args) {
1003 res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
1011 * This function generates the code to be inserted right after the ordering
1012 * point construct (instrumentation code)
1016 * The corresponding ordering point construct
1017 * @return The generated code
1019 public static Code Generate4OPConstruct(OPConstruct construct) {
1020 Code code = new Code();
1021 String curLine = construct.annotation;
1022 String label = construct.label;
1023 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
1024 code.addLine(prefixTabs + "if (" + construct.condition + ")");
1025 switch (construct.type) {
1027 code.addLine(prefixTabs + "\t" + SpecNaming.CreateOPDefineAnnoFunc
1031 code.addLine(prefixTabs + "\t"
1032 + SpecNaming.CreatePotentialOPAnnoFunc + "("
1033 + SpecNaming.AppendStr(label) + ");");
1036 code.addLine(prefixTabs + "\t" + SpecNaming.CreateOPCheckAnnoFunc
1037 + "(" + SpecNaming.AppendStr(label) + ");");
1040 code.addLine(prefixTabs + "\t" + SpecNaming.CreateOPClearAnnoFunc
1044 code.addLine(prefixTabs + "\t"
1045 + SpecNaming.CreateOPClearDefineAnnoFunc + "();");
1055 * This function generates the code to be inserted right after the entry
1056 * construct (instrumentation code)
1060 * The corresponding entry construct
1063 public static Code Generate4Entry(EntryConstruct construct) {
1064 Code res = new Code();
1065 String curLine = construct.annotation;
1066 String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
1067 // _createInitAnnotation();
1068 res.addLine(prefixTabs + SpecNaming.CreateInitAnnoFunc + "();");
1074 * This function generates the code to be inserted right after the "@Define"
1075 * construct (instrumentation code)
1079 * The corresponding entry construct
1082 public static Code Generate4Define(DefineConstruct construct) {
1083 Code code = new Code();
1085 code.addLine("/********** User-defined code in annotation (BEGIN) **********/");
1086 code.addLines(construct.code);
1087 code.addLine("/********** User-defined code in annotation (END) **********/");
1093 * This function generates the new interface wrapper code to be inserted
1094 * right after the end of the interface definition
1098 * The corresponding interface construct
1099 * @return The generated code
1101 public static Code GenerateInterfaceWrapper(InterfaceConstruct construct) {
1102 Code code = new Code();
1104 String name = construct.getName();
1105 String beginLine = construct.getFunctionHeader().getHeaderLine();
1106 Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
1107 Matcher matcherSpace = regexpSpace.matcher(beginLine);
1108 String prefixTabs = "";
1109 if (matcherSpace.find())
1110 prefixTabs = matcherSpace.group(1);
1112 // Add one line to separate
1114 code.addLine(prefixTabs
1115 + ShortComment("Generated wrapper interface for " + name));
1116 if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
1118 code.addLine(beginLine + " {");
1120 code.addLine(beginLine);
1122 // Instrument with the INTERFACE_BEGIN annotations
1123 code.addLine(prefixTabs
1125 + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
1126 // CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
1127 code.addLine(prefixTabs
1129 + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
1130 + SpecNaming.AnnoInterfaceInfoInst,
1131 SpecNaming.CreateInterfaceBeginAnnoFunc
1132 + Brace(SpecNaming.AppendStr(name))));
1133 // Call the actual function
1134 code.addLine(prefixTabs + "\t"
1135 + ShortComment("Call the actual function"));
1136 // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
1137 code.addLine(prefixTabs + "\t"
1138 + construct.getFunctionHeader().getRenamedCall() + ";");
1141 // Initialize the value struct
1142 code.addLine(prefixTabs + "\t"
1143 + ShortComment("Initialize the value struct"));
1144 // The very first assignment "
1145 code.addLine(prefixTabs + "\t"
1146 + DeclareDefine(name, "*value", SpecNaming.New + Brace(name)));
1147 // Don't leave out the RET field
1148 if (!construct.getFunctionHeader().isReturnVoid())
1149 code.addLine(prefixTabs + "\t"
1150 + AssignToPtr("value", SpecNaming.RET, SpecNaming.RET));
1152 for (VariableDeclaration decl : construct.getFunctionHeader().args)
1153 code.addLine(prefixTabs + "\t"
1154 + AssignToPtr("value", decl.name, decl.name));
1157 // Store the value info into the current MethodCall
1158 // _setInterfaceBeginAnnotationValue(info, value);
1159 code.addLine(prefixTabs
1161 + ShortComment("Store the value info into the current MethodCall"));
1162 code.addLine(prefixTabs + "\t"
1163 + SpecNaming.SetInterfaceBeginAnnoValueFunc
1164 + Brace(SpecNaming.AnnoInterfaceInfoInst + ", value") + ";");
1167 // Return if necessary
1168 if (!construct.getFunctionHeader().isReturnVoid())
1169 code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");
1170 code.addLine(prefixTabs + "}");
1177 * Write a list of lines (as the whole of the file) to a file ---
1178 * newFileName. If that file does not exist, we create that file and then
1182 * @param newFileName
1183 * The name of the file to be written
1185 * The list of lines that as a whole become the content of the
1188 public static void write2File(String newFileName, ArrayList<String> content) {
1189 File newFile = new File(newFileName);
1190 newFile.getParentFile().mkdirs();
1191 if (!newFile.exists()) {
1193 newFile.createNewFile();
1194 } catch (IOException e) {
1195 e.printStackTrace();
1198 BufferedWriter bw = null;
1200 bw = new BufferedWriter(new FileWriter(newFile));
1201 for (int i = 0; i < content.size(); i++) {
1202 bw.write(content.get(i) + "\n");
1205 } catch (IOException e) {
1206 e.printStackTrace();
1211 } catch (IOException e) {
1212 e.printStackTrace();