code.addLine("#endif");
code.addLine("");
+ // 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
+ 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("");
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(tmpFunc),
SpecNaming.EmptyCString));
+ // 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(DeclareDefine(SpecNaming.CString,
+ SpecNaming.AppendStr(tmpFunc),
+ SpecNaming.EmptyCString));
// PostCondition
tmpFunc = name + "_" + SpecNaming.PostCondition;
if (!construct.postCondition.isEmpty())
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, SpecNaming.InterfaceValueInst,
+ 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 @JustifyingPrecondition
+ if (!construct.justifyingPrecondition.isEmpty()) {
+ code.addLine(ShortComment("Define @"
+ + 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.Method2, SpecNaming.InterfaceValueInst,
+ construct);
+ fieldsInit.align(1);
+ code.addLines(fieldsInit);
+
+ 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("");
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, SpecNaming.InterfaceValueInst,
+ 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("");
}
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",
+ "),";
}
code.addLine(TabbedLine(line, 2));
+ // JustifyingPrecondition
+ line = "new "
+ + SpecNaming.NamedFunction
+ + "("
+ + SpecNaming.AppendStr(name + "_"
+ + SpecNaming.JustifyingPrecondition) + ", "
+ + SpecNaming.JustifyingPreconditionType + ", (void*) ";
+ if (construct.justifyingPrecondition.isEmpty()) {
+ line = line + SpecNaming.NullFunc + "),";
+ } else {
+ 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));
// PostCondition
line = "new "
+ SpecNaming.NamedFunction
// The very first assignment "
res.addLine(DeclareDefine(structName, "*" + inst, "(" + structName
+ "*) " + methodInst + "->" + SpecNaming.MethodValueField));
- // Don't leave out the RET field
+ // Don't leave out the C_RET field
if (!construct.getFunctionHeader().isReturnVoid()) {
res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
- SpecNaming.RET, inst + "->" + SpecNaming.RET));
+ SpecNaming.C_RET, inst + "->" + SpecNaming.C_RET));
}
// For arguments
for (VariableDeclaration decl : construct.getFunctionHeader().args) {
case OPDefine:
code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
break;
+ case OPDefineUnattached:
+ code.addLine(prefixTabs + SpecNaming.CreateOPDefineUnattachedFunc
+ + "();");
+ break;
case PotentialOP:
code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
+ "(" + SpecNaming.AppendStr(label) + ");");
code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
+ "();");
break;
+ case OPClearDefineUnattached:
+ code.addLine(prefixTabs
+ + SpecNaming.CreateOPClearDefineUnattachedFunc + "();");
+ break;
default:
break;
}
// 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("");
+ DeclareDefine(structName,
"*" + SpecNaming.InterfaceValueInst, SpecNaming.New
+ Brace(structName)));
- // Don't leave out the RET field
+ // Don't leave out the C_RET field
if (!construct.getFunctionHeader().isReturnVoid())
code.addLine(prefixTabs
+ "\t"
+ AssignToPtr(SpecNaming.InterfaceValueInst,
- SpecNaming.RET, SpecNaming.RET));
+ SpecNaming.C_RET, SpecNaming.C_RET));
// For arguments
for (VariableDeclaration decl : construct.getFunctionHeader().args)
code.addLine(prefixTabs
+ 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