code.addLine("#endif");
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));
+ // Declare _createOPDefineUnattached
+ code.addLine(ShortComment("Declare _createOPDefineUnattached"));
+ // void _createOPDefineUnattached();
+ code.addLine("void _createOPDefineUnattached();");
+ code.addLine("");
+
+ // Declare _createOPClearDefineUnattached
+ code.addLine(ShortComment("Declare _createOPClearDefineUnattached"));
+ // void _createOPClearDefineUnattached();
+ code.addLine("void _createOPClearDefineUnattached();");
code.addLine("");
+ code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
+
// Interface name strings
code.addLine(ShortComment("Interface name strings"));
for (File file : interfaceListMap.keySet()) {
}
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("");
- // 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 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();
+ String structName = construct.getStructName();
code.addLine(ShortComment("Declare custom value struct for "
+ name));
- code.addLine("typedef struct " + name + " {");
+ code.addLine("typedef struct " + structName + " {");
FunctionHeader funcHeader = construct.getFunctionHeader();
- // RET
- if (!funcHeader.returnType.equals("void"))
+ // C_RET & also the S_RET
+ // The idea is that we store the S_RET in the __value struct, and every time we access/update
+ // S_RET, we actually access "__value->S_RET" (good for read and write)...
+ if (!funcHeader.returnType.equals("void")) {
+ code.addLine(TabbedLine(Declare(funcHeader.returnType,
+ SpecNaming.C_RET)));
code.addLine(TabbedLine(Declare(funcHeader.returnType,
- SpecNaming.RET)));
+ SpecNaming.S_RET)));
+ }
// Arguments
for (VariableDeclaration decl : funcHeader.args) {
code.addLine(TabbedLine(Declare(decl)));
}
- code.addLine("} " + name + ";");
+ code.addLine("} " + structName + ";");
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 code = new Code();
String line = null;
+ Code fieldsInit = null;
// Add auto-generated comments
code.addLine("/**");
code.addLine(TabbedLine(Declare(decl)));
}
code.addLine("");
+ // Define state destructor
+ code.addLine(TabbedLine(ShortComment("Define state destructor")));
+ code.addLine(TabbedLine("~" + SpecNaming.StateStruct + "() {"));
+ if (!globalConstruct.autoGenClear) {
+ code.addLine(TabbedLine(
+ ShortComment("Execute user-defined state clear code"), 2));
+ } else {
+ code.addLine(TabbedLine(
+ ShortComment("Execute auto-generated state clear code"), 2));
+ }
+ globalConstruct.clearState.align(2);
+ code.addLines(globalConstruct.clearState);
+ code.addLine(TabbedLine("}"));
+ code.addLine("");
+
code.addLine(TabbedLine("SNAPSHOTALLOC"));
+ code.addLine("");
code.addLine("} " + SpecNaming.StateStruct + ";");
code.addLine("");
code.addLine("");
+ // Define the fake ordering point operation
+ code.addLine(ShortComment("Define the fake ordering point operation"));
+ // atomic_int _FAKE_OP_;
+ code.addLine("atomic_int " + SpecNaming.FakeOP + ";");
+ code.addLine("");
+
+ // Define _createOPDefineUnattached
+ code.addLine(ShortComment("Define _createOPDefineUnattached"));
+ code.addLine("void " + SpecNaming.CreateOPDefineUnattachedFunc + "() {");
+ code.addLine(TabbedLine(ShortComment("A load acting as the fake OP")));
+ code.addLine(TabbedLine(SpecNaming.FakeOP
+ + ".load(memory_order_relaxed);"));
+ code.addLine(TabbedLine(SpecNaming.CreateOPDefineAnnoFunc + "();"));
+ code.addLine("}");
+
+ // Define _createOPClearDefineUnattached
+ code.addLine(ShortComment("Define _createOPClearDefineUnattached"));
+ code.addLine("void " + SpecNaming.CreateOPClearDefineUnattachedFunc
+ + "() {");
+ code.addLine(TabbedLine(ShortComment("A load acting as the fake OP")));
+ code.addLine(TabbedLine(SpecNaming.FakeOP
+ + ".load(memory_order_relaxed);"));
+ code.addLine(TabbedLine(SpecNaming.CreateOPClearDefineAnnoFunc + "();"));
+ 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(DeclareDefine(SpecNaming.CString,
SpecNaming.AppendStr(SpecNaming.CopyState), Quote("_"
+ SpecNaming.CopyState.toLowerCase())));
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(SpecNaming.ClearState), Quote("_"
+ + SpecNaming.ClearState.toLowerCase())));
code.addLine(DeclareDefine(SpecNaming.CString,
SpecNaming.AppendStr(SpecNaming.FinalState), Quote("_"
+ SpecNaming.FinalState.toLowerCase())));
code.addLine(DeclareDefine(SpecNaming.CString,
SpecNaming.AppendStr(tmpFunc),
SpecNaming.EmptyCString));
- // SideEffect
- tmpFunc = name + "_" + SpecNaming.SideEffect;
- if (!construct.sideEffect.isEmpty())
+ // JustifyingPrecondition
+ tmpFunc = name + "_" + SpecNaming.JustifyingPrecondition;
+ if (!construct.justifyingPrecondition.isEmpty())
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+ else
+ code.addLine(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc),
+ SpecNaming.EmptyCString));
+ // JustifyingPostcondition
+ tmpFunc = name + "_" + SpecNaming.JustifyingPostcondition;
+ if (!construct.justifyingPostcondition.isEmpty())
code.addLine(DeclareDefine(SpecNaming.CString,
SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
else
code.addLine(TabbedLine("#define " + decl.name + " "
+ SpecNaming.StateInst + "->" + decl.name));
}
- code.addLine(TabbedLine(ShortComment("User-defined intial state code")));
+ if (!globalConstruct.autoGenInitial)
+ code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
+ else
+ // Auto-generated the initialization function
+ code.addLine(TabbedLine(ShortComment("Auto-generated state intialization code")));
// Align the code with one tab
globalConstruct.initState.align(1);
code.addLines(globalConstruct.initState);
code.addLine("}");
code.addLine("");
+ // Define @Clear
+ code.addLine(ShortComment("Define @" + SpecNaming.ClearState));
+ code.addLine("void _" + SpecNaming.ClearState.toLowerCase() + "("
+ + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
+ // Retrieve the state
+ code.addLine(TabbedLine(ShortComment("Retrieve the state")));
+ code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+ + SpecNaming.StateInst, "(" + SpecNaming.StateStruct + "*) "
+ + SpecNaming.Method1 + "->state")));
+ // Explicitly call the state destructor
+ code.addLine(TabbedLine(ShortComment("Explicitly call the state destructor")));
+ code.addLine(TabbedLine("delete " + SpecNaming.StateInst + ";"));
+ 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("");
- }
+ code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
+ code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
+ + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
+
+ // Initialize state struct fields
+ fieldsInit = GenerateStateFieldsInitialization(SpecNaming.Method1,
+ SpecNaming.StateInst, globalConstruct);
+ fieldsInit.align(1);
+ code.addLines(fieldsInit);
+ code.addLine("");
+ if (!globalConstruct.autoGenPrint)
+ code.addLine(TabbedLine(ShortComment("Execute user-defined state printing code")));
+ else
+ // Auto-generated the copy function
+ code.addLine(TabbedLine(ShortComment("Execute auto-generated state printing code")));
+
+ // 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"));
+ SpecNaming.AppendStr(rule.method2) + ") {"));
// Initialize M1 & M2 in commutativity rule
// e.g. ENQ *M1 = (ENQ*) m1->value;
+ String structName1 = InterfaceConstruct
+ .createStructName(rule.method1);
+ String structName2 = InterfaceConstruct
+ .createStructName(rule.method2);
code.addLine(TabbedLine(
- DeclareDefine(rule.method1, "*M1", "(" + rule.method1
+ DeclareDefine(structName1, "*M1", "(" + structName1
+ "*) m1->value"), 2));
code.addLine(TabbedLine(
- DeclareDefine(rule.method2, "*M2", "(" + rule.method2
+ DeclareDefine(structName2, "*M2", "(" + structName2
+ "*) m2->value"), 2));
- code.addLine(TabbedLine("return " + rule.condition + ";", 2));
+ code.addLine(TabbedLine("return !(" + rule.condition + ");", 2));
code.addLine(TabbedLine("}"));
- code.addLine(TabbedLine("return false;"));
+ code.addLine(TabbedLine("return true;"));
code.addLine("}");
code.addLine("");
for (File file : interfaceListMap.keySet()) {
ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
for (InterfaceConstruct construct : list) {
- Code fieldsInit = null;
+ fieldsInit = null;
// Define interface functions
String name = construct.getName();
+ String structName = construct.getStructName();
code.addLine("/********** " + name
+ " functions **********/");
// Define @Transition for INTERFACE
code.addLine(ShortComment("Define @" + SpecNaming.Transition
+ " for " + name));
- code.addLine("void _" + name + "_" + SpecNaming.Transition
+ code.addLine("bool _" + name + "_" + SpecNaming.Transition
+ "(" + SpecNaming.Method + " " + SpecNaming.Method1
+ ", " + SpecNaming.Method + " " + SpecNaming.Method2
+ ") {");
// Initialize value struct fields
fieldsInit = GenerateInterfaceFieldsInitialization(
- SpecNaming.Method2, "value", construct);
+ SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+ construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
code.addLine(TabbedLine(ShortComment("Execute Transition")));
code.addLines(construct.transition);
+ // By default, we will return true for state transition
+ code.addLine(TabbedLine(ShortComment("By default @Transition returns true")));
+ code.addLine(TabbedLine("return true;"));
code.addLine("}");
code.addLine("");
if (!construct.preCondition.isEmpty()) {
code.addLine(ShortComment("Define @"
+ SpecNaming.PreCondition + " for " + name));
- code.addLine("bool _" + name + "_"
- + SpecNaming.PreCondition + "(" + SpecNaming.Method
- + " " + SpecNaming.Method1 + ") {");
+ code.addLine("bool _" + name + "_" + SpecNaming.PreCondition
+ + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+ + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+ + ") {");
// Initialize value struct fields
fieldsInit = GenerateInterfaceFieldsInitialization(
- SpecNaming.Method1, "value", construct);
+ SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+ construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
code.addLines(construct.preCondition);
+ // By default, we will return true for @PreCondition
+ code.addLine(TabbedLine(ShortComment("By default @PreCondition returns true")));
+ code.addLine(TabbedLine("return true;"));
+
code.addLine("}");
code.addLine("");
}
- // Define @SideEffect
- if (!construct.sideEffect.isEmpty()) {
+ // Define @JustifyingPrecondition
+ if (!construct.justifyingPrecondition.isEmpty()) {
code.addLine(ShortComment("Define @"
- + SpecNaming.SideEffect + " for " + name));
- code.addLine("void _" + name + "_" + SpecNaming.SideEffect
- + "(" + SpecNaming.Method + " "
- + SpecNaming.Method1 + ") {");
+ + SpecNaming.JustifyingPrecondition + " for " + name));
+ code.addLine("bool _" + name + "_" + SpecNaming.JustifyingPrecondition
+ + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+ + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+ + ") {");
// Initialize value struct fields
fieldsInit = GenerateInterfaceFieldsInitialization(
- SpecNaming.Method1, "value", construct);
+ SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+ construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
- construct.sideEffect.align(1);
- code.addLine(TabbedLine(ShortComment("Execute SideEffect")));
- code.addLines(construct.sideEffect);
+ construct.justifyingPrecondition.align(1);
+ code.addLine(TabbedLine(ShortComment("Execute JustifyingPrecondition")));
+ code.addLines(construct.justifyingPrecondition);
+
+ // By default, we will return true for @JustifyingPrecondition
+ code.addLine(TabbedLine(ShortComment("By default @JustifyingPrecondition returns true")));
+ code.addLine(TabbedLine("return true;"));
code.addLine("}");
code.addLine("");
+
+ }
+ // Define @JustifyingPostcondition
+ if (!construct.justifyingPostcondition.isEmpty()) {
+ code.addLine(ShortComment("Define @"
+ + SpecNaming.JustifyingPostcondition + " for " + name));
+ code.addLine("bool _" + name + "_" + SpecNaming.JustifyingPostcondition
+ + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+ + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+ + ") {");
+
+ // Initialize value struct fields
+ fieldsInit = GenerateInterfaceFieldsInitialization(
+ SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+ construct);
+ fieldsInit.align(1);
+ code.addLines(fieldsInit);
+
+ construct.justifyingPostcondition.align(1);
+ code.addLine(TabbedLine(ShortComment("Execute JustifyingPostcondition")));
+ code.addLines(construct.justifyingPostcondition);
+
+ // By default, we will return true for @JustifyingPostcondition
+ code.addLine(TabbedLine(ShortComment("By default @JustifyingPostcondition returns true")));
+ code.addLine(TabbedLine("return true;"));
+
+ 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
+ code.addLine("bool _" + name + "_" + SpecNaming.PostCondition
+ + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+ + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+ ") {");
// Initialize value struct fields
fieldsInit = GenerateInterfaceFieldsInitialization(
- SpecNaming.Method1, "value", construct);
+ SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+ construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
code.addLine(TabbedLine(ShortComment("Execute PostCondition")));
code.addLines(construct.postCondition);
+ // By default, we will return true for @PostCondition
+ code.addLine(TabbedLine(ShortComment("By default @PostCondition returns true")));
+ code.addLine(TabbedLine("return true;"));
+
code.addLine("}");
code.addLine("");
}
+ SpecNaming.Method1 + ") {");
// Initialize value struct fields
fieldsInit = GenerateInterfaceFieldsInitialization(
- SpecNaming.Method1, "value", construct);
+ SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+ construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
construct.print.align(1);
- code.addLine(TabbedLine(ShortComment("Execute Print")));
+ if (!construct.autoGenPrint)
+ code.addLine(TabbedLine(ShortComment("Execute user-defined value printing code")));
+ else
+ // Auto-generated the value printing function
+ code.addLine(TabbedLine(ShortComment("Execute auto-generated value printing code")));
code.addLines(construct.print);
code.addLine("}");
code.addLine(ShortComment("Define INIT annotation instrumentation function"));
code.addLine("void _createInitAnnotation() {");
+ // Init the fake ordering point place holder
+ code.addLine(TabbedLine(ShortComment("Init the fake ordering point place holder")));
+ code.addLine(TabbedLine(SpecNaming.FakeOP
+ + ".store(1, memory_order_relaxed);"));
+
// Init commutativity rules
code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
code.addLine(TabbedLine(DeclareDefine("int",
+ SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
+ SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
+ SpecNaming.CopyState.toLowerCase() + "),", 2));
+ // new NamedFunction(_Clear_str, CLEAR, (void*) _clear),
+ code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+ + SpecNaming.AppendStr(SpecNaming.ClearState) + ", "
+ + SpecNaming.ClearState.toUpperCase() + ", " + "(void*) _"
+ + SpecNaming.ClearState.toLowerCase() + "),", 2));
// new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
- line = "new " + SpecNaming.NamedFunction + "("
+ code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+ SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
- + SpecNaming.PrintStateType + ", " + "(void*)";
- if (globalConstruct.printState.isEmpty()) {
- line = line + SpecNaming.NullFunc + "),";
- } else {
- line = line + "_" + SpecNaming.PrintState.toLowerCase() + "),";
- }
- code.addLine(TabbedLine(line, 2));
+ + SpecNaming.PrintStateType + ", " + "(void*) _"
+ + SpecNaming.PrintState.toLowerCase() + "),", 2));
// commuteRules, CommuteRuleSize);
code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
+ SpecNaming.CommutativityRuleSizeInst + ");", 2));
+ "),";
}
code.addLine(TabbedLine(line, 2));
- // SideEffect
+ // JustifyingPrecondition
line = "new "
+ SpecNaming.NamedFunction
+ "("
+ SpecNaming.AppendStr(name + "_"
- + SpecNaming.SideEffect) + ", "
- + SpecNaming.SideEffectType + ", (void*) ";
- if (construct.sideEffect.isEmpty()) {
+ + SpecNaming.JustifyingPrecondition) + ", "
+ + SpecNaming.JustifyingPreconditionType + ", (void*) ";
+ if (construct.justifyingPrecondition.isEmpty()) {
line = line + SpecNaming.NullFunc + "),";
} else {
- line = line + "_" + name + "_" + SpecNaming.SideEffect
+ line = line + "_" + name + "_" + SpecNaming.JustifyingPrecondition
+ + "),";
+ }
+ code.addLine(TabbedLine(line, 2));
+ // JustifyingPostcondition
+ line = "new "
+ + SpecNaming.NamedFunction
+ + "("
+ + SpecNaming.AppendStr(name + "_"
+ + SpecNaming.JustifyingPostcondition) + ", "
+ + SpecNaming.JustifyingPostconditionType + ", (void*) ";
+ if (construct.justifyingPostcondition.isEmpty()) {
+ line = line + SpecNaming.NullFunc + "),";
+ } else {
+ line = line + "_" + name + "_" + SpecNaming.JustifyingPostcondition
+ "),";
}
code.addLine(TabbedLine(line, 2));
String inst, InterfaceConstruct construct) {
Code res = new Code();
String name = construct.getName();
+ String structName = construct.getStructName();
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
+ res.addLine(DeclareDefine(structName, "*" + inst, "(" + structName
+ + "*) " + methodInst + "->" + SpecNaming.MethodValueField));
+ // Don't leave out the C_RET field
if (!construct.getFunctionHeader().isReturnVoid()) {
res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
- SpecNaming.RET, "value->" + SpecNaming.RET));
+ SpecNaming.C_RET, inst + "->" + SpecNaming.C_RET));
}
// For arguments
for (VariableDeclaration decl : construct.getFunctionHeader().args) {
String curLine = construct.annotation;
String label = construct.label;
String prefixTabs = curLine.substring(0, curLine.indexOf("/**"));
- code.addLine(prefixTabs + "if (" + construct.condition + ")");
+ if (!construct.condition.equals("true")) {
+ code.addLine(prefixTabs + "if (" + construct.condition + ")");
+ prefixTabs = prefixTabs + "\t";
+ }
+
switch (construct.type) {
case OPDefine:
- code.addLine(prefixTabs + "\t" + SpecNaming.CreateOPDefineAnnoFunc
+ code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
+ break;
+ case OPDefineUnattached:
+ code.addLine(prefixTabs + SpecNaming.CreateOPDefineUnattachedFunc
+ "();");
break;
case PotentialOP:
- code.addLine(prefixTabs + "\t"
- + SpecNaming.CreatePotentialOPAnnoFunc + "("
- + SpecNaming.AppendStr(label) + ");");
+ code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
+ + "(" + SpecNaming.AppendStr(label) + ");");
break;
case OPCheck:
- code.addLine(prefixTabs + "\t" + SpecNaming.CreateOPCheckAnnoFunc
- + "(" + SpecNaming.AppendStr(label) + ");");
+ code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "("
+ + SpecNaming.AppendStr(label) + ");");
break;
case OPClear:
- code.addLine(prefixTabs + "\t" + SpecNaming.CreateOPClearAnnoFunc
- + "();");
+ code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();");
break;
case OPClearDefine:
- code.addLine(prefixTabs + "\t"
- + SpecNaming.CreateOPClearDefineAnnoFunc + "();");
+ code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
+ + "();");
+ break;
+ case OPClearDefineUnattached:
+ code.addLine(prefixTabs
+ + SpecNaming.CreateOPClearDefineUnattachedFunc + "();");
break;
default:
break;
Code code = new Code();
String name = construct.getName();
+ String structName = construct.getStructName();
String beginLine = construct.getFunctionHeader().getHeaderLine();
Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$");
Matcher matcherSpace = regexpSpace.matcher(beginLine);
// Call the actual function
code.addLine(prefixTabs + "\t"
+ ShortComment("Call the actual function"));
- // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
+ // bool C_RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
code.addLine(prefixTabs + "\t"
+ construct.getFunctionHeader().getRenamedCall() + ";");
code.addLine("");
code.addLine(prefixTabs + "\t"
+ ShortComment("Initialize the value struct"));
// The very first assignment "
- code.addLine(prefixTabs + "\t"
- + DeclareDefine(name, "*value", SpecNaming.New + Brace(name)));
- // Don't leave out the RET field
+ code.addLine(prefixTabs
+ + "\t"
+ + DeclareDefine(structName,
+ "*" + SpecNaming.InterfaceValueInst, SpecNaming.New
+ + Brace(structName)));
+ // Don't leave out the C_RET field
if (!construct.getFunctionHeader().isReturnVoid())
- code.addLine(prefixTabs + "\t"
- + AssignToPtr("value", SpecNaming.RET, SpecNaming.RET));
+ code.addLine(prefixTabs
+ + "\t"
+ + AssignToPtr(SpecNaming.InterfaceValueInst,
+ SpecNaming.C_RET, SpecNaming.C_RET));
// For arguments
for (VariableDeclaration decl : construct.getFunctionHeader().args)
- code.addLine(prefixTabs + "\t"
- + AssignToPtr("value", decl.name, decl.name));
+ code.addLine(prefixTabs
+ + "\t"
+ + AssignToPtr(SpecNaming.InterfaceValueInst, 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"
+ code.addLine(prefixTabs
+ + "\t"
+ SpecNaming.SetInterfaceBeginAnnoValueFunc
- + Brace(SpecNaming.AnnoInterfaceInfoInst + ", value") + ";");
+ + Brace(SpecNaming.AnnoInterfaceInfoInst + ", "
+ + SpecNaming.InterfaceValueInst) + ";");
code.addLine("");
+ // Instrument with the INTERFACE_END annotations
+ code.addLine(prefixTabs + "\t"
+ + ShortComment("Instrument with the INTERFACE_END annotation"));
+ // _createInterfaceEndAnnotation(_DEQ_str);
+ code.addLine(prefixTabs + "\t"
+ + SpecNaming.CreateInterfaceEndAnnoFunc
+ + Brace(SpecNaming.AppendStr(name)) + ";");
+
// Return if necessary
if (!construct.getFunctionHeader().isReturnVoid())
- code.addLine(prefixTabs + "\treturn " + SpecNaming.RET + ";");
+ code.addLine(prefixTabs + "\treturn " + SpecNaming.C_RET + ";");
code.addLine(prefixTabs + "}");
return code;
projects / cdsspec-compiler.git / blobdiff