--- /dev/null
+package edu.uci.eecs.codeGenerator;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.FileWriter;
+import java.io.IOException;
+
+import edu.uci.eecs.specExtraction.Code;
+import edu.uci.eecs.specExtraction.CommutativityRule;
+import edu.uci.eecs.specExtraction.EntryConstruct;
+import edu.uci.eecs.specExtraction.FunctionHeader;
+import edu.uci.eecs.specExtraction.GlobalConstruct;
+import edu.uci.eecs.specExtraction.InterfaceConstruct;
+import edu.uci.eecs.specExtraction.OPConstruct;
+import edu.uci.eecs.specExtraction.SpecExtractor;
+import edu.uci.eecs.specExtraction.SpecNaming;
+import edu.uci.eecs.specExtraction.VariableDeclaration;
+
+/**
+ * <p>
+ * Some utility functions for generating specification checking code.
+ * </p>
+ *
+ * @author Peizhao Ou
+ *
+ */
+public class CodeGeneratorUtils {
+
+ public static void PrintCode(ArrayList<String> code) {
+ for (int i = 0; i < code.size(); i++) {
+ System.out.println(code.get(i));
+ }
+ }
+
+ public static String Comment(String comment) {
+ return "/** " + comment + " */";
+ }
+
+ public static String ShortComment(String comment) {
+ return "// " + comment;
+ }
+
+ public static String IncludeHeader(String header) {
+ return "#include " + header;
+ }
+
+ public static String Brace(String val) {
+ return "(" + val + ")";
+ }
+
+ public static String Quote(String val) {
+ return "\"" + val + "\"";
+ }
+
+ public static String Assign(String varName, String val) {
+ return varName + " = " + val + ";";
+ }
+
+ public static String AssignToPtr(String structName, String field, String val) {
+ return structName + "->" + field + " = " + val + ";";
+ }
+
+ public static String Declare(String type, String name) {
+ return type + " " + name + ";";
+ }
+
+ public static String Declare(VariableDeclaration varDecl) {
+ return Declare(varDecl.type, varDecl.name);
+ }
+
+ public static String DeclareDefine(String type, String var, String val) {
+ return type + " " + var + " = " + val + ";";
+ }
+
+ /**
+ * <p>
+ * Insert a number of tabs at the beginning of the line.
+ * </p>
+ *
+ * @param line
+ * Input line
+ * @param tabCnt
+ * The number of tabs to be inserted
+ * @return A line that starts with the specific inserted tabs
+ */
+ public static String TabbedLine(String line, int tabCnt) {
+ String res = "";
+ for (int i = 0; i < tabCnt; i++)
+ res = "\t" + res;
+ res = res + line;
+ return res;
+ }
+
+ /**
+ * <p>
+ * Insert a tab at the beginning of the line.
+ * </p>
+ *
+ * @param line
+ * Input line
+ * @return A line that starts with one inserted tab
+ */
+ public static String TabbedLine(String line) {
+ return "\t" + line;
+ }
+
+ /**
+ * <p>
+ * This function generates the code for the header file that our
+ * specification generates automatically --- cdsspec-generated.h.
+ * </p>
+ *
+ * @param extractor
+ * The SpecExtractor that contains the extracted information
+ * @return The generated code
+ */
+ public static Code GenerateCDSSpecHeaderFile(SpecExtractor extractor) {
+ HashSet<String> headerFiles = extractor.headerFiles;
+ GlobalConstruct globalConstruct = extractor.getGlobalConstruct();
+ HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap = extractor.interfaceListMap;
+ HashSet<String> OPLabelSet = extractor.OPLabelSet;
+
+ Code code = new Code();
+
+ // Add auto-generated comments
+ code.addLine("/**");
+ code.addLine(TabbedLine("This is a header file auto-generated by CDSSpec compiler; together, CDSSpec"));
+ code.addLine(TabbedLine("compiler should have generated the accompanying implementation file that"));
+ code.addLine(TabbedLine("implements the some functions declared in this file. In order to instrument"));
+ code.addLine(TabbedLine("your benchmark for CDSSpec checker to check, you should include this header"));
+ code.addLine(TabbedLine("file in every file you use an CDSSpec annotation. Note that it should be"));
+ code.addLine(TabbedLine("placed in the end of all other header files. Currently we require a C++"));
+ code.addLine(TabbedLine("compiler that supports C++11."));
+ code.addLine("*/");
+ code.addLine("");
+
+ code.addLine("#ifndef _"
+ + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
+ '_') + "_H");
+ code.addLine("#define _"
+ + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
+ '_') + "_H");
+ code.addLine("");
+
+ // System included headers
+ code.addLine(ShortComment("System included headers go here"));
+ for (String header : SpecNaming.includedHeadersList) {
+ code.addLine(IncludeHeader(header));
+ }
+ code.addLine("");
+
+ // Users included headers
+ code.addLine(ShortComment("User included headers go here"));
+ for (String header : headerFiles) {
+ code.addLine(IncludeHeader(header));
+ }
+ code.addLine("");
+
+ code.addLine("using namespace std;");
+ code.addLine("");
+ code.addLine("");
+
+ code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
+ code.addLine(ShortComment("A special empty string"));
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.EmptyCString));
+ code.addLine("");
+
+ // Interface name strings
+ code.addLine(ShortComment("Interface name strings"));
+ for (File file : interfaceListMap.keySet()) {
+ ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
+ for (InterfaceConstruct construct : list) {
+ String name = construct.getName();
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(name)));
+ }
+ }
+ code.addLine("");
+
+ // Commutativity rule strings
+ code.addLine(ShortComment("Commutativity rule strings"));
+ for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.Commutativity + i)));
+ }
+ code.addLine("");
+
+ // Ordering points label strings
+ code.addLine(ShortComment("Ordering points label strings"));
+ for (String label : OPLabelSet) {
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(label)));
+ }
+ code.addLine("");
+
+ // Special function name strings
+ code.addLine(ShortComment("Special function name strings"));
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.InitalState)));
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.CopyState)));
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.FinalState)));
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.PrintState)));
+ code.addLine("");
+
+ // Interface name strings
+ for (File file : interfaceListMap.keySet()) {
+ ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
+ for (InterfaceConstruct construct : list) {
+ String name = construct.getName();
+ code.addLine(ShortComment(name + " function strings"));
+ // Transition
+ String tmpFunc = name + "_" + SpecNaming.Transition;
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc)));
+ // PreCondition
+ tmpFunc = name + "_" + SpecNaming.PreCondition;
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc)));
+ // SideEffect
+ tmpFunc = name + "_" + SpecNaming.SideEffect;
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc)));
+ // PostCondition
+ tmpFunc = name + "_" + SpecNaming.PostCondition;
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc)));
+ // Print
+ tmpFunc = name + "_" + SpecNaming.PrintValue;
+ code.addLine(Declare("extern " + SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc)));
+ code.addLine("");
+ }
+ }
+
+ // Declare customized StateStruct
+ code.addLine(ShortComment("Declare customized StateStruct"));
+ code.addLine("typedef struct " + SpecNaming.StateStruct + " {");
+ for (VariableDeclaration decl : globalConstruct.declState) {
+ code.addLine(TabbedLine(Declare(decl)));
+ }
+ code.addLine("");
+ code.addLine(TabbedLine("SNAPSHOTALLOC"));
+ code.addLine("} " + SpecNaming.StateStruct + ";");
+ code.addLine("");
+
+ // Declare customized value struct
+ for (File file : interfaceListMap.keySet()) {
+ ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
+ for (InterfaceConstruct construct : list) {
+ // Declare custom value struct for the interface
+ String name = construct.getName();
+ code.addLine(ShortComment("Declare custom value struct for "
+ + name));
+ code.addLine("typedef struct " + name + " {");
+ FunctionHeader funcHeader = construct.getFunctionHeader();
+ // RET
+ if (!funcHeader.returnType.equals("void"))
+ code.addLine(TabbedLine(Declare(funcHeader.returnType,
+ SpecNaming.RET)));
+ // Arguments
+ for (VariableDeclaration decl : funcHeader.args) {
+ code.addLine(TabbedLine(Declare(decl)));
+ }
+ code.addLine("} " + name + ";");
+ code.addLine("");
+ }
+ }
+
+ // Declare @Initial
+ code.addLine(ShortComment("Declare @" + SpecNaming.InitalState));
+ code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
+ + SpecNaming.Method + " " + SpecNaming.Method1 + ");");
+ code.addLine("");
+ // Declare @Copy
+ code.addLine(ShortComment("Declare @" + SpecNaming.CopyState));
+ code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
+ + SpecNaming.Method + " " + "dest, " + SpecNaming.Method
+ + " src);");
+ code.addLine("");
+ // Declare @Print
+ code.addLine(ShortComment("Declare @" + SpecNaming.PrintState));
+ if (!globalConstruct.printState.isEmpty()) {
+ code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
+ + SpecNaming.Method + " " + SpecNaming.Method1 + ");");
+ code.addLine("");
+ }
+
+ // Declare @Commutativity
+ code.addLine(ShortComment("Declare commutativity checking functions"));
+ for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
+ code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
+ + SpecNaming.Method + " m1, " + SpecNaming.Method + " m2);");
+ }
+ code.addLine("");
+
+ // Declare customized interface functions
+ for (File file : interfaceListMap.keySet()) {
+ ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
+ for (InterfaceConstruct construct : list) {
+ // Declare interface functions
+ String name = construct.getName();
+ code.addLine("/********** " + name
+ + " functions **********/");
+ // Declare @Transition for INTERFACE
+ code.addLine(ShortComment("Declare @" + SpecNaming.Transition
+ + " for " + name));
+ code.addLine("void _" + name + "_" + SpecNaming.Transition
+ + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+ + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+ + ");");
+ code.addLine("");
+ // Declare @PreCondition
+ if (!construct.preCondition.isEmpty()) {
+ code.addLine(ShortComment("Declare @"
+ + SpecNaming.PreCondition + " for " + name));
+ code.addLine("bool _" + name + "_"
+ + SpecNaming.PreCondition + "(" + SpecNaming.Method
+ + " " + SpecNaming.Method1 + ");");
+ code.addLine("");
+ }
+ // Declare @SideEffect
+ if (!construct.sideEffect.isEmpty()) {
+ code.addLine(ShortComment("Declare @"
+ + SpecNaming.SideEffect + " for " + name));
+ code.addLine("void _" + name + "_" + SpecNaming.SideEffect
+ + "(" + SpecNaming.Method + " "
+ + SpecNaming.Method1 + ");");
+ code.addLine("");
+ }
+ // Declare @PostCondition
+ if (!construct.postCondition.isEmpty()) {
+ code.addLine(ShortComment("Declare @"
+ + SpecNaming.PostCondition + " for " + name));
+ code.addLine("bool _" + name + "_"
+ + SpecNaming.PostCondition + "("
+ + SpecNaming.Method + " " + SpecNaming.Method1
+ + ");");
+ code.addLine("");
+ }
+ // Declare @Print
+ if (!construct.print.isEmpty()) {
+ code.addLine(ShortComment("Declare @"
+ + SpecNaming.PrintValue + " for " + name));
+ code.addLine("void _" + name + "_" + SpecNaming.PrintValue
+ + "(" + SpecNaming.Method + " "
+ + SpecNaming.Method1 + ");");
+ code.addLine("");
+ }
+ }
+ }
+
+ // Declare INIT annotation instrumentation function
+ code.addLine(ShortComment("Declare INIT annotation instrumentation function"));
+ code.addLine("void _createInitAnnotation();");
+ code.addLine("");
+ code.addLine("#endif");
+
+ return code;
+ }
+
+ /**
+ * <p>
+ * This function generates the code for the CPP file that our specification
+ * generates automatically --- cdsspec-generated.cc.
+ * </p>
+ *
+ * @param extractor
+ * The SpecExtractor that contains the extracted information
+ * @return The generated code
+ */
+ public static Code GenerateCDSSpecCPPFile(SpecExtractor extractor) {
+ GlobalConstruct globalConstruct = extractor.getGlobalConstruct();
+ HashMap<File, ArrayList<InterfaceConstruct>> interfaceListMap = extractor.interfaceListMap;
+ HashSet<String> OPLabelSet = extractor.OPLabelSet;
+
+ Code code = new Code();
+ String line = null;
+
+ // Add auto-generated comments
+ code.addLine("/**");
+ code.addLine(TabbedLine("This is an implementation file auto-generated by CDSSpec compiler to"));
+ code.addLine(TabbedLine("instrument your benchmark for CDSSpec checker to check. Currently we require"));
+ code.addLine(TabbedLine("a C++ compiler that supports C++11."));
+ code.addLine("*/");
+ code.addLine("");
+
+ code.addLine("#include " + SpecNaming.CDSSpecGeneratedHeader);
+ code.addLine("");
+ code.addLine("");
+
+ code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
+ code.addLine(ShortComment("A special empty string"));
+ code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,
+ "\"\""));
+ code.addLine("");
+
+ // Interface name strings
+ code.addLine(ShortComment("Interface name strings"));
+ for (File file : interfaceListMap.keySet()) {
+ ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
+ for (InterfaceConstruct construct : list) {
+ String name = construct.getName();
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(name), Quote(name)));
+ }
+ }
+ code.addLine("");
+
+ // Commutativity rule strings
+ code.addLine(ShortComment("Commutativity rule strings"));
+ for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
+ CommutativityRule rule = globalConstruct.commutativityRules
+ .get(i - 1);
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.Commutativity + i),
+ Quote(rule.toString())));
+ }
+ code.addLine("");
+
+ // Ordering points label strings
+ code.addLine(ShortComment("Ordering points label strings"));
+ for (String label : OPLabelSet) {
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(label), Quote(label)));
+ }
+ code.addLine("");
+
+ // Special function name strings
+ code.addLine(ShortComment("Special function name strings"));
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.InitalState), Quote("_"
+ + SpecNaming.InitalState.toLowerCase())));
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.CopyState), Quote("_"
+ + SpecNaming.CopyState.toLowerCase())));
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.FinalState), Quote("_"
+ + SpecNaming.FinalState.toLowerCase())));
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.PrintState), Quote("_"
+ + SpecNaming.PrintState.toLowerCase())));
+ code.addLine("");
+
+ // Interface name strings
+ for (File file : interfaceListMap.keySet()) {
+ ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
+ for (InterfaceConstruct construct : list) {
+ String name = construct.getName();
+ code.addLine(ShortComment(name + " function strings"));
+ // Transition
+ String tmpFunc = name + "_" + SpecNaming.Transition;
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+ // PreCondition
+ tmpFunc = name + "_" + SpecNaming.PreCondition;
+ if (!construct.preCondition.isEmpty())
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+ else
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc),
+ SpecNaming.EmptyCString));
+ // SideEffect
+ tmpFunc = name + "_" + SpecNaming.SideEffect;
+ if (!construct.sideEffect.isEmpty())
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+ else
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc),
+ SpecNaming.EmptyCString));
+ // PostCondition
+ tmpFunc = name + "_" + SpecNaming.PostCondition;
+ if (!construct.postCondition.isEmpty())
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+ else
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc),
+ SpecNaming.EmptyCString));
+ // Print
+ tmpFunc = name + "_" + SpecNaming.PrintValue;
+ if (!construct.print.isEmpty())
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+ else
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc),
+ SpecNaming.EmptyCString));
+ code.addLine("");
+ }
+ }
+
+ // Define @Initial
+ code.addLine(ShortComment("Define @" + SpecNaming.InitalState));
+ code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
+ + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
+ code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+ + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
+ // Define macros
+ for (VariableDeclaration decl : globalConstruct.declState) {
+ code.addLine(TabbedLine("#define " + decl.name + " "
+ + SpecNaming.StateInst + "->" + decl.name));
+ }
+ code.addLine(TabbedLine(ShortComment("User-defined intial state code")));
+ // Align the code with one tab
+ globalConstruct.initState.align(1);
+ code.addLines(globalConstruct.initState);
+ // Undefine macros
+ for (VariableDeclaration decl : globalConstruct.declState) {
+ code.addLine(TabbedLine("#undef " + decl.name));
+ }
+ code.addLine("");
+ code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1,
+ SpecNaming.StateInst, SpecNaming.StateInst)));
+ code.addLine("}");
+ code.addLine("");
+
+ // Define @Copy
+ code.addLine(ShortComment("Define @" + SpecNaming.CopyState));
+ code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
+ + SpecNaming.Method + " " + "dest, " + SpecNaming.Method
+ + " src) {");
+ // StateStruct *OLD = (StateStruct*) src->state;
+ code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+ + SpecNaming.OldStateInst, Brace(SpecNaming.StateStruct + "*")
+ + " src->" + SpecNaming.StateInst)));
+ // StateStruct *NEW = new StateStruct;
+ code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+ + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
+ if (!globalConstruct.autoGenCopy)
+ code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
+ else
+ // Auto-generated the copy function
+ code.addLine(TabbedLine(ShortComment("Auto-generated state copy statements")));
+ globalConstruct.copyState.align(1);
+ code.addLines(globalConstruct.copyState);
+ code.addLine("");
+ code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst,
+ SpecNaming.NewStateInst)));
+ code.addLine("}");
+ code.addLine("");
+
+ // Define @Print
+ if (!globalConstruct.printState.isEmpty()) {
+ code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
+ code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
+ + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
+
+ // Initialize state struct fields
+ Code fieldsInit = GenerateStateFieldsInitialization(
+ SpecNaming.Method1, SpecNaming.StateInst, globalConstruct);
+ fieldsInit.align(1);
+ code.addLines(fieldsInit);
+ code.addLine("");
+ code.addLine(TabbedLine(ShortComment("Execute the print-out")));
+ // Align the code with one tab
+ globalConstruct.printState.align(1);
+ code.addLines(globalConstruct.printState);
+ code.addLine("}");
+ code.addLine("");
+ }
+
+ // Define @Commutativity
+ code.addLine(ShortComment("Define commutativity checking functions"));
+ for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
+ CommutativityRule rule = globalConstruct.commutativityRules
+ .get(i - 1);
+ code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
+ + SpecNaming.Method + " m1, " + SpecNaming.Method
+ + " m2) {");
+ // if (m1->name == _ENQ_str && m2->name == _DEQ_str) {
+ code.addLine(TabbedLine("if (m1->name == "
+ + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
+ + SpecNaming.AppendStr(rule.method2) + ") {"));
+ // Initialize M1 & M2 in commutativity rule
+ // e.g. ENQ *M1 = (ENQ*) m1->value;
+ code.addLine(TabbedLine(
+ DeclareDefine(rule.method1, "*M1", "(" + rule.method1
+ + "*) m1->value"), 2));
+ code.addLine(TabbedLine(
+ DeclareDefine(rule.method2, "*M2", "(" + rule.method2
+ + "*) m2->value"), 2));
+ code.addLine(TabbedLine("return " + rule.condition + ";", 2));
+ code.addLine(TabbedLine("}"));
+ code.addLine(TabbedLine("return false;"));
+
+ code.addLine("}");
+ code.addLine("");
+ }
+
+ // Define customized interface functions
+ for (File file : interfaceListMap.keySet()) {
+ ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
+ for (InterfaceConstruct construct : list) {
+ Code fieldsInit = null;
+
+ // Define interface functions
+ String name = construct.getName();
+ code.addLine("/********** " + name
+ + " functions **********/");
+ // Define @Transition for INTERFACE
+ code.addLine(ShortComment("Define @" + SpecNaming.Transition
+ + " for " + name));
+ code.addLine("void _" + name + "_" + SpecNaming.Transition
+ + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+ + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+ + ") {");
+
+ // Initialize value struct fields
+ fieldsInit = GenerateInterfaceFieldsInitialization(
+ SpecNaming.Method2, "value", construct);
+ fieldsInit.align(1);
+ code.addLines(fieldsInit);
+
+ construct.transition.align(1);
+ code.addLine(TabbedLine(ShortComment("Execute Transition")));
+ code.addLines(construct.transition);
+
+ code.addLine("}");
+ code.addLine("");
+
+ // Define @PreCondition
+ if (!construct.preCondition.isEmpty()) {
+ code.addLine(ShortComment("Define @"
+ + SpecNaming.PreCondition + " for " + name));
+ code.addLine("bool _" + name + "_"
+ + SpecNaming.PreCondition + "(" + SpecNaming.Method
+ + " " + SpecNaming.Method1 + ") {");
+
+ // Initialize value struct fields
+ fieldsInit = GenerateInterfaceFieldsInitialization(
+ SpecNaming.Method1, "value", construct);
+ fieldsInit.align(1);
+ code.addLines(fieldsInit);
+
+ construct.preCondition.align(1);
+ code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
+ code.addLines(construct.preCondition);
+
+ code.addLine("}");
+ code.addLine("");
+
+ }
+ // Define @SideEffect
+ if (!construct.sideEffect.isEmpty()) {
+ code.addLine(ShortComment("Define @"
+ + SpecNaming.SideEffect + " for " + name));
+ code.addLine("void _" + name + "_" + SpecNaming.SideEffect
+ + "(" + SpecNaming.Method + " "
+ + SpecNaming.Method1 + ") {");
+
+ // Initialize value struct fields
+ fieldsInit = GenerateInterfaceFieldsInitialization(
+ SpecNaming.Method1, "value", construct);
+ fieldsInit.align(1);
+ code.addLines(fieldsInit);
+
+ construct.sideEffect.align(1);
+ code.addLine(TabbedLine(ShortComment("Execute SideEffect")));
+ code.addLines(construct.sideEffect);
+
+ code.addLine("}");
+ code.addLine("");
+ }
+ // Define @PostCondition
+ if (!construct.postCondition.isEmpty()) {
+ code.addLine(ShortComment("Define @"
+ + SpecNaming.PostCondition + " for " + name));
+ code.addLine("bool _" + name + "_"
+ + SpecNaming.PostCondition + "("
+ + SpecNaming.Method + " " + SpecNaming.Method1
+ + ") {");
+
+ // Initialize value struct fields
+ fieldsInit = GenerateInterfaceFieldsInitialization(
+ SpecNaming.Method1, "value", construct);
+ fieldsInit.align(1);
+ code.addLines(fieldsInit);
+
+ construct.postCondition.align(1);
+ code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
+ code.addLines(construct.postCondition);
+
+ code.addLine("}");
+ code.addLine("");
+ }
+ // Define @Print
+ if (!construct.print.isEmpty()) {
+ code.addLine(ShortComment("Define @"
+ + SpecNaming.PrintValue + " for " + name));
+ code.addLine("void _" + name + "_" + SpecNaming.PrintValue
+ + "(" + SpecNaming.Method + " "
+ + SpecNaming.Method1 + ") {");
+ // Initialize value struct fields
+ fieldsInit = GenerateInterfaceFieldsInitialization(
+ SpecNaming.Method1, "value", construct);
+ fieldsInit.align(1);
+ code.addLines(fieldsInit);
+
+ construct.print.align(1);
+ code.addLine(TabbedLine(ShortComment("Execute Print")));
+ code.addLines(construct.print);
+
+ code.addLine("}");
+ code.addLine("");
+ }
+ }
+ }
+
+ // Define INIT annotation instrumentation function
+ code.addLine(ShortComment("Define INIT annotation instrumentation function"));
+ code.addLine("void _createInitAnnotation() {");
+
+ // Init commutativity rules
+ code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
+ code.addLine(TabbedLine(DeclareDefine("int",
+ SpecNaming.CommutativityRuleSizeInst,
+ Integer.toString(globalConstruct.commutativityRules.size()))));
+ String tmp = SpecNaming.NewSize
+ + Brace(SpecNaming.CommutativityRule + ", sizeof"
+ + Brace(SpecNaming.CommutativityRule) + " * "
+ + SpecNaming.CommutativityRuleSizeInst);
+ code.addLine(TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*"
+ + SpecNaming.CommutativityRuleInst, tmp)));
+ for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
+ CommutativityRule rule = globalConstruct.commutativityRules
+ .get(i - 1);
+ code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ")
+ + i));
+ // new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
+ // _Commutativity1_str, _checkCommutativity1)
+ line = "new"
+ + Brace(" &" + SpecNaming.CommutativityRuleInst + "["
+ + (i - 1) + "] ") + SpecNaming.CommutativityRule
+ + "(" + SpecNaming.AppendStr(rule.method1) + ", "
+ + SpecNaming.AppendStr(rule.method2) + ", "
+ + SpecNaming.AppendStr(SpecNaming.Commutativity + i) + ", "
+ + "_check" + SpecNaming.Commutativity + i + ");";
+ code.addLine(TabbedLine(line));
+ }
+
+ // Initialize AnnoInit
+ code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
+ // AnnoInit *init = new AnnoInit(
+ code.addLine(TabbedLine(SpecNaming.AnnoInit + " *"
+ + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit
+ + "("));
+ // new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
+ code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+ + SpecNaming.AppendStr(SpecNaming.InitalState) + ", "
+ + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
+ + SpecNaming.InitalState.toLowerCase() + "),", 2));
+ // new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
+ line = "new " + SpecNaming.NamedFunction + "("
+ + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
+ + SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
+ if (globalConstruct.finalState.isEmpty()) {
+ line = line + SpecNaming.NullFunc + "),";
+ } else {
+ line = line + "_" + SpecNaming.FinalState.toUpperCase();
+ }
+ code.addLine(TabbedLine(line, 2));
+ // new NamedFunction(_Copy_str, COPY, (void*) _copy),
+ code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+ + SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
+ + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
+ + SpecNaming.CopyState.toLowerCase() + "),", 2));
+ // new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
+ code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+ + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
+ + SpecNaming.PrintStateType + ", " + "(void*) _"
+ + SpecNaming.PrintState.toLowerCase() + "),", 2));
+ // commuteRules, CommuteRuleSize);
+ code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
+ + SpecNaming.CommutativityRuleSizeInst + ");", 2));
+ code.addLine("");
+
+ // Declare StateFunctions map
+ code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
+ code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*"
+ + SpecNaming.StateFunctionsInst)));
+ code.addLine("");
+
+ // StateFunction for interface
+ for (File file : interfaceListMap.keySet()) {
+ ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
+ for (InterfaceConstruct construct : list) {
+ String name = construct.getName();
+ code.addLine(TabbedLine(ShortComment("StateFunction for "
+ + name)));
+ // stateFuncs = new StateFunctions(
+ code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
+ + " = new " + SpecNaming.StateFunctions + "("));
+ // new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
+ // _ENQ_Transition),
+ // Transition
+ code.addLine(TabbedLine(
+ "new "
+ + SpecNaming.NamedFunction
+ + "("
+ + SpecNaming.AppendStr(name + "_"
+ + SpecNaming.Transition) + ", "
+ + SpecNaming.TransitionType + ", (void*) _"
+ + name + "_" + SpecNaming.Transition + "),", 2));
+ // PreCondition
+ line = "new "
+ + SpecNaming.NamedFunction
+ + "("
+ + SpecNaming.AppendStr(name + "_"
+ + SpecNaming.PreCondition) + ", "
+ + SpecNaming.PreConditionType + ", (void*) ";
+ if (construct.preCondition.isEmpty()) {
+ line = line + SpecNaming.NullFunc + "),";
+ } else {
+ line = line + "_" + name + "_" + SpecNaming.PreCondition
+ + "),";
+ }
+ code.addLine(TabbedLine(line, 2));
+ // SideEffect
+ line = "new "
+ + SpecNaming.NamedFunction
+ + "("
+ + SpecNaming.AppendStr(name + "_"
+ + SpecNaming.SideEffect) + ", "
+ + SpecNaming.SideEffectType + ", (void*) ";
+ if (construct.sideEffect.isEmpty()) {
+ line = line + SpecNaming.NullFunc + "),";
+ } else {
+ line = line + "_" + name + "_" + SpecNaming.SideEffect
+ + "),";
+ }
+ code.addLine(TabbedLine(line, 2));
+ // PostCondition
+ line = "new "
+ + SpecNaming.NamedFunction
+ + "("
+ + SpecNaming.AppendStr(name + "_"
+ + SpecNaming.PostCondition) + ", "
+ + SpecNaming.PostConditionType + ", (void*) ";
+ if (construct.postCondition.isEmpty()) {
+ line = line + SpecNaming.NullFunc + "),";
+ } else {
+ line = line + "_" + name + "_" + SpecNaming.PostCondition
+ + "),";
+ }
+ code.addLine(TabbedLine(line, 2));
+ // Print (PrintValue
+ line = "new "
+ + SpecNaming.NamedFunction
+ + "("
+ + SpecNaming.AppendStr(name + "_"
+ + SpecNaming.PrintValue) + ", "
+ + SpecNaming.PrintValueType + ", (void*) ";
+ if (construct.print.isEmpty()) {
+ line = line + SpecNaming.NullFunc + "),";
+ } else {
+ line = line + "_" + name + "_" + SpecNaming.PrintValue
+ + ")";
+ }
+ code.addLine(TabbedLine(line, 2));
+ code.addLine(TabbedLine(");"));
+
+ // init->addInterfaceFunctions(_ENQ_str, stateFuncs);
+ code.addLine(TabbedLine(SpecNaming.AnnoInitInst
+ + "->"
+ + SpecNaming.AddInterfaceFunctions
+ + Brace(SpecNaming.AppendStr(name) + ", "
+ + SpecNaming.StateFunctionsInst) + ";"));
+ code.addLine("");
+ }
+ }
+
+ // Create and instrument with the INIT annotation
+ code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
+ // cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
+ code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc
+ + Brace(SpecNaming.SPEC_ANALYSIS
+ + ", new "
+ + SpecNaming.SpecAnnotation
+ + Brace(SpecNaming.AnnoTypeInit + ", "
+ + SpecNaming.AnnoInitInst)) + ";"));
+
+ code.addLine("}");
+ code.addLine("");
+
+ return code;
+ }
+
+ /**
+ * <p>
+ * This function generates a list of lines that initialize the fields of the
+ * global state struct. See below.
+ * </p>
+ *
+ * <p>
+ * <code>
+ * StateStruct *state = (StateStruct*) _M->state;
+ * <br>
+ * IntList * q = state->q;
+ * </code>
+ * </p>
+ *
+ * <p>
+ * In this example, _M --> methodInst, state --> inst.
+ * </p>
+ *
+ * @param methodInst
+ * See description
+ * @param inst
+ * See description
+ * @param construct
+ * The global state construct
+ * @return The generated code
+ */
+ public static Code GenerateStateFieldsInitialization(String methodInst,
+ String inst, GlobalConstruct construct) {
+ Code res = new Code();
+ res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct
+ + " fields"));
+ res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst, "("
+ + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
+ for (VariableDeclaration decl : construct.declState) {
+ res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
+ + decl.name));
+ }
+ return res;
+ }
+
+ /**
+ * <p>
+ * This function generates a list of lines that initialize the fields of a
+ * specific interface struct. See below.
+ * </p>
+ *
+ * <p>
+ * <code>
+ * ENQ *info = (ENQ*) _M->value;
+ * <br>
+ * IntList * q = info->q;
+ * </code>
+ * </p>
+ *
+ * <p>
+ * In this example, ENQ --> structType, _M --> methodInst, info --> inst
+ * </p>
+ *
+ * @param methodInst
+ * See description
+ * @param inst
+ * See description
+ * @param construct
+ * The corresponding interface construct
+ * @return The generated code
+ */
+ public static Code GenerateInterfaceFieldsInitialization(String methodInst,
+ String inst, InterfaceConstruct construct) {
+ Code res = new Code();
+ String name = construct.getName();
+ res.addLine(ShortComment("Initialize fields for " + name));
+ // The very first assignment "
+ res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) "
+ + methodInst + "->value"));
+ // Don't leave out the RET field
+ if (!construct.getFunctionHeader().isReturnVoid()) {
+ res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
+ SpecNaming.RET, "value->" + SpecNaming.RET));
+ }
+ // For arguments
+ for (VariableDeclaration decl : construct.getFunctionHeader().args) {
+ res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
+ + decl.name));
+ }
+ return res;
+ }
+
+ /**
+ * <p>
+ * This function generates the code to be inserted right after the ordering
+ * point construct (instrumentation code)
+ * </p>
+ *
+ * @param construct
+ * The corresponding ordering point construct
+ * @return The generated code
+ */
+ public static Code Generate4OPConstruct(OPConstruct construct) {
+ Code code = new Code();
+ String curLine = construct.annotation;
+ String label = construct.label;
+ String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
+ code.addLine(prefixTabs + "if (" + construct.condition + ")");
+ switch (construct.type) {
+ case OPDefine:
+ code.addLine(prefixTabs + "\t" + SpecNaming.CreateOPDefineAnnoFunc
+ + "();");
+ break;
+ case PotentialOP:
+ code.addLine(prefixTabs + "\t"
+ + SpecNaming.CreatePotentialOPAnnoFunc + "("
+ + SpecNaming.AppendStr(label) + ");");
+ break;
+ case OPCheck:
+ code.addLine(prefixTabs + "\t" + SpecNaming.CreateOPCheckAnnoFunc
+ + "(" + SpecNaming.AppendStr(label) + ");");
+ break;
+ case OPClear:
+ code.addLine(prefixTabs + "\t" + SpecNaming.CreateOPClearAnnoFunc
+ + "();");
+ break;
+ case OPClearDefine:
+ code.addLine(prefixTabs + "\t"
+ + SpecNaming.CreateOPClearDefineAnnoFunc + "();");
+ break;
+ default:
+ break;
+ }
+ return code;
+ }
+
+ /**
+ * <p>
+ * This function generates the code to be inserted right after the entry
+ * construct (instrumentation code)
+ * </p>
+ *
+ * @param construct
+ * The corresponding entry construct
+ * @return
+ */
+ public static Code Generate4Entry(EntryConstruct construct) {
+ Code res = new Code();
+ String curLine = construct.annotation;
+ String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
+ // _createInitAnnotation();
+ res.addLine(prefixTabs + SpecNaming.CreateInitAnnoFunc + "();");
+ return res;
+ }
+
+ /**
+ * <p>
+ * This function generates the new interface wrapper code to be inserted
+ * right after the end of the interface definition
+ * </p>
+ *
+ * @param construct
+ * The corresponding interface construct
+ * @return The generated code
+ */
+ public static Code GenerateInterfaceWrapper(InterfaceConstruct construct) {
+ Code code = new Code();
+
+ String name = construct.getName();
+ String beginLine = construct.getFunctionHeader().getHeaderLine();
+ Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
+ Matcher matcherSpace = regexpSpace.matcher(beginLine);
+ String prefixTabs = "";
+ if (matcherSpace.find())
+ prefixTabs = matcherSpace.group(1);
+
+ // Add one line to separate
+ code.addLine("");
+ code.addLine(prefixTabs
+ + ShortComment("Generated wrapper interface for " + name));
+ if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
+ // of the line
+ code.addLine(beginLine + " {");
+ } else {
+ code.addLine(beginLine);
+ }
+ // Instrument with the INTERFACE_BEGIN annotation
+ code.addLine(prefixTabs
+ + "\t"
+ + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
+ // AnnoInterfaceInfo *info = _createInterfaceBeginAnnotation(_DEQ_str);
+ code.addLine(prefixTabs
+ + "\t"
+ + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
+ + SpecNaming.AnnoInterfaceInfoInst,
+ SpecNaming.CreateInterfaceBeginAnnoFunc
+ + Brace(SpecNaming.AppendStr(name))));
+ // Call the actual function
+ code.addLine(prefixTabs + "\t"
+ + ShortComment("Call the actual function"));
+ // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
+ code.addLine(prefixTabs + "\t"
+ + construct.getFunctionHeader().getRenamedCall() + ";");
+ code.addLine("");
+
+ // Initialize the value struct
+ code.addLine(prefixTabs + "\t"
+ + ShortComment("Initialize the value struct"));
+ // The very first assignment "
+ code.addLine(prefixTabs + "\t"
+ + DeclareDefine(name, "*value", "new " + name));
+ // Don't leave out the RET field
+ if (!construct.getFunctionHeader().isReturnVoid())
+ code.addLine(prefixTabs + "\t"
+ + AssignToPtr("value", SpecNaming.RET, SpecNaming.RET));
+ // For arguments
+ for (VariableDeclaration decl : construct.getFunctionHeader().args)
+ code.addLine(prefixTabs + "\t"
+ + AssignToPtr("value", decl.name, decl.name));
+ code.addLine("");
+
+ // Store the value info into the current MethodCall
+ code.addLine(prefixTabs
+ + "\t"
+ + ShortComment("Store the value info into the current MethodCall"));
+ code.addLine(prefixTabs
+ + "\t"
+ + AssignToPtr(SpecNaming.AnnoInterfaceInfoInst, "value",
+ "value"));
+ code.addLine("");
+
+ // Return if necessary
+ if (!construct.getFunctionHeader().isReturnVoid())
+ code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");
+ code.addLine(prefixTabs + "}");
+
+ return code;
+ }
+
+ /**
+ * <p>
+ * Write a list of lines (as the whole of the file) to a file ---
+ * newFileName. If that file does not exist, we create that file and then
+ * write the lines.
+ * </p>
+ *
+ * @param newFileName
+ * The name of the file to be written
+ * @param content
+ * The list of lines that as a whole become the content of the
+ * file
+ */
+ public static void write2File(String newFileName, ArrayList<String> content) {
+ File newFile = new File(newFileName);
+ newFile.getParentFile().mkdirs();
+ if (!newFile.exists()) {
+ try {
+ newFile.createNewFile();
+ } catch (IOException e) {
+ e.printStackTrace();
+ }
+ }
+ BufferedWriter bw = null;
+ try {
+ bw = new BufferedWriter(new FileWriter(newFile));
+ for (int i = 0; i < content.size(); i++) {
+ bw.write(content.get(i) + "\n");
+ }
+ bw.flush();
+ } catch (IOException e) {
+ e.printStackTrace();
+ } finally {
+ if (bw != null)
+ try {
+ bw.close();
+ } catch (IOException e) {
+ e.printStackTrace();
+ }
+ }
+ }
+}
projects / cdsspec-compiler.git / blobdiff