code.addLine("*/");
code.addLine("");
- code.addLine("#ifndef _"
- + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
- '_') + "_H");
- code.addLine("#define _"
- + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
- '_') + "_H");
+ code.addLine("#ifndef _" + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-', '_') + "_H");
+ code.addLine("#define _" + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-', '_') + "_H");
code.addLine("");
// FIXME: We have included ad-hoc header files here
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(Declare("extern " + SpecNaming.CString, SpecNaming.EmptyCString));
code.addLine("");
// Interface name strings
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(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(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(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(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
code.addLine(ShortComment(name + " function strings"));
// Transition
String tmpFunc = name + "_" + SpecNaming.Transition;
- code.addLine(Declare("extern " + SpecNaming.CString,
- SpecNaming.AppendStr(tmpFunc)));
+ code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
// PreCondition
tmpFunc = name + "_" + SpecNaming.PreCondition;
- code.addLine(Declare("extern " + SpecNaming.CString,
- SpecNaming.AppendStr(tmpFunc)));
+ code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
// SideEffect
tmpFunc = name + "_" + SpecNaming.SideEffect;
- code.addLine(Declare("extern " + SpecNaming.CString,
- SpecNaming.AppendStr(tmpFunc)));
+ code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
// PostCondition
tmpFunc = name + "_" + SpecNaming.PostCondition;
- code.addLine(Declare("extern " + SpecNaming.CString,
- SpecNaming.AppendStr(tmpFunc)));
+ 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("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
code.addLine("");
}
}
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(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)));
+ code.addLine(TabbedLine(Declare(funcHeader.returnType, SpecNaming.RET)));
// Arguments
for (VariableDeclaration decl : funcHeader.args) {
code.addLine(TabbedLine(Declare(decl)));
// Declare @Initial
code.addLine(ShortComment("Declare @" + SpecNaming.InitalState));
- code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
- + SpecNaming.Method + " " + SpecNaming.Method1 + ");");
+ 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("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("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("bool _check" + SpecNaming.Commutativity + i + "(" + SpecNaming.Method + " m1, "
+ + SpecNaming.Method + " m2);");
}
code.addLine("");
for (InterfaceConstruct construct : list) {
// Declare interface functions
String name = construct.getName();
- code.addLine("/********** " + name
- + " functions **********/");
+ 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(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(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 + " "
+ 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(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 + " "
+ code.addLine(ShortComment("Declare @" + SpecNaming.PrintValue + " for " + name));
+ code.addLine("void _" + name + "_" + SpecNaming.PrintValue + "(" + SpecNaming.Method + " "
+ SpecNaming.Method1 + ");");
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.EmptyCString, "\"\""));
code.addLine("");
// Interface name strings
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(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),
+ 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(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(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
code.addLine(ShortComment(name + " function strings"));
// Transition
String tmpFunc = name + "_" + SpecNaming.Transition;
- code.addLine(DeclareDefine(SpecNaming.CString,
- SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+ 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)));
+ code.addLine(
+ DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
else
- code.addLine(DeclareDefine(SpecNaming.CString,
- SpecNaming.AppendStr(tmpFunc),
- SpecNaming.EmptyCString));
+ 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)));
+ code.addLine(
+ DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
else
- code.addLine(DeclareDefine(SpecNaming.CString,
- SpecNaming.AppendStr(tmpFunc),
- SpecNaming.EmptyCString));
+ 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)));
+ code.addLine(
+ DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
else
- code.addLine(DeclareDefine(SpecNaming.CString,
- SpecNaming.AppendStr(tmpFunc),
- SpecNaming.EmptyCString));
+ 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)));
+ code.addLine(
+ DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
else
- code.addLine(DeclareDefine(SpecNaming.CString,
- SpecNaming.AppendStr(tmpFunc),
- SpecNaming.EmptyCString));
+ 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)));
+ 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("#define " + decl.name + " " + SpecNaming.StateInst + "->" + decl.name));
}
if (!globalConstruct.autoGenInitial)
code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
code.addLine(TabbedLine("#undef " + decl.name));
}
code.addLine("");
- code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1,
- SpecNaming.StateInst, SpecNaming.StateInst)));
+ 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) {");
+ 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)));
+ 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)));
+ code.addLine(TabbedLine(
+ DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
if (!globalConstruct.autoGenCopy)
code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
else
globalConstruct.copyState.align(1);
code.addLines(globalConstruct.copyState);
code.addLine("");
- code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst,
- SpecNaming.NewStateInst)));
+ 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 + ") {");
+ code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "(" + SpecNaming.Method + " "
+ + SpecNaming.Method1 + ") {");
// Initialize state struct fields
- Code fieldsInit = GenerateStateFieldsInitialization(
- SpecNaming.Method1, SpecNaming.StateInst, globalConstruct);
+ Code fieldsInit = GenerateStateFieldsInitialization(SpecNaming.Method1, SpecNaming.StateInst,
+ globalConstruct);
fieldsInit.align(1);
code.addLines(fieldsInit);
code.addLine("");
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);
// 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) {");
+ 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 == "
+ 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(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;"));
// Define interface functions
String name = construct.getName();
- code.addLine("/********** " + name
- + " functions **********/");
+ 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
- + ") {");
+ 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 = GenerateInterfaceFieldsInitialization(SpecNaming.Method2, "value", construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
// Define @PreCondition
if (!construct.preCondition.isEmpty()) {
- code.addLine(ShortComment("Define @"
- + SpecNaming.PreCondition + " for " + name));
- code.addLine("bool _" + name + "_"
- + SpecNaming.PreCondition + "(" + SpecNaming.Method
- + " " + SpecNaming.Method1 + ") {");
+ 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 = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
}
// Define @SideEffect
if (!construct.sideEffect.isEmpty()) {
- code.addLine(ShortComment("Define @"
- + SpecNaming.SideEffect + " for " + name));
- code.addLine("void _" + name + "_" + SpecNaming.SideEffect
- + "(" + SpecNaming.Method + " "
+ 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 = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
}
// 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(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 = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
}
// Define @Print
if (!construct.print.isEmpty()) {
- code.addLine(ShortComment("Define @"
- + SpecNaming.PrintValue + " for " + name));
- code.addLine("void _" + name + "_" + SpecNaming.PrintValue
- + "(" + SpecNaming.Method + " "
+ 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 = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, "value", construct);
fieldsInit.align(1);
code.addLines(fieldsInit);
// Init commutativity rules
code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
- code.addLine(TabbedLine(DeclareDefine("int",
- SpecNaming.CommutativityRuleSizeInst,
+ 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)));
+ 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));
+ 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 + ");";
+ 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
- + "("));
+ 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*) _"
+ 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) + ", "
+ line = "new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
+ SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
if (globalConstruct.finalState.isEmpty()) {
line = line + SpecNaming.NullFunc + "),";
}
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));
+ 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),
- line = "new " + SpecNaming.NamedFunction + "("
- + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
+ line = "new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
+ SpecNaming.PrintStateType + ", " + "(void*)";
if (globalConstruct.printState.isEmpty()) {
line = line + SpecNaming.NullFunc + "),";
}
code.addLine(TabbedLine(line, 2));
// commuteRules, CommuteRuleSize);
- code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
- + SpecNaming.CommutativityRuleSizeInst + ");", 2));
+ 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(TabbedLine(Declare(SpecNaming.StateFunctions, "*" + SpecNaming.StateFunctionsInst)));
code.addLine("");
// StateFunction for interface
ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
for (InterfaceConstruct construct : list) {
String name = construct.getName();
- code.addLine(TabbedLine(ShortComment("StateFunction for "
- + name)));
+ code.addLine(TabbedLine(ShortComment("StateFunction for " + name)));
// stateFuncs = new StateFunctions(
- code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
- + " = new " + SpecNaming.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));
+ "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) + ", "
+ 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
- + "),";
+ line = line + "_" + name + "_" + SpecNaming.PreCondition + "),";
}
code.addLine(TabbedLine(line, 2));
// SideEffect
- line = "new "
- + SpecNaming.NamedFunction
- + "("
- + SpecNaming.AppendStr(name + "_"
- + SpecNaming.SideEffect) + ", "
- + SpecNaming.SideEffectType + ", (void*) ";
+ 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
- + "),";
+ line = line + "_" + name + "_" + SpecNaming.SideEffect + "),";
}
code.addLine(TabbedLine(line, 2));
// PostCondition
- line = "new "
- + SpecNaming.NamedFunction
- + "("
- + SpecNaming.AppendStr(name + "_"
- + SpecNaming.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
- + "),";
+ line = line + "_" + name + "_" + SpecNaming.PostCondition + "),";
}
code.addLine(TabbedLine(line, 2));
// Print (PrintValue
- line = "new "
- + SpecNaming.NamedFunction
- + "("
- + SpecNaming.AppendStr(name + "_"
- + SpecNaming.PrintValue) + ", "
- + SpecNaming.PrintValueType + ", (void*) ";
+ 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
- + ")";
+ 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(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(TabbedLine(SpecNaming.CDSAnnotateFunc + Brace(SpecNaming.SPEC_ANALYSIS + ", new "
+ + SpecNaming.SpecAnnotation + Brace(SpecNaming.AnnoTypeInit + ", " + SpecNaming.AnnoInitInst)) + ";"));
code.addLine("}");
code.addLine("");
* The global state construct
* @return The generated code
*/
- public static Code GenerateStateFieldsInitialization(String methodInst,
- String inst, GlobalConstruct construct) {
+ 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"));
+ 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));
+ res.addLine(DeclareDefine(decl.type, decl.name, inst + "->" + decl.name));
}
return res;
}
* The corresponding interface construct
* @return The generated code
*/
- public static Code GenerateInterfaceFieldsInitialization(String methodInst,
- String inst, InterfaceConstruct construct) {
+ 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"));
+ 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));
+ 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));
+ res.addLine(DeclareDefine(decl.type, decl.name, inst + "->" + decl.name));
}
return res;
}
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 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;
default:
break;
// Add one line to separate
code.addLine("");
- code.addLine(prefixTabs
- + ShortComment("Generated wrapper interface for " + name));
+ 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 + " {");
code.addLine(beginLine);
}
// Instrument with the INTERFACE_BEGIN annotations
- code.addLine(prefixTabs
- + "\t"
- + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
+ code.addLine(prefixTabs + "\t" + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
// CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
- code.addLine(prefixTabs
- + "\t"
- + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
- + SpecNaming.AnnoInterfaceInfoInst,
- SpecNaming.CreateInterfaceBeginAnnoFunc
- + Brace(SpecNaming.AppendStr(name))));
+ 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"));
+ 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(prefixTabs + "\t" + construct.getFunctionHeader().getRenamedCall() + ";");
code.addLine("");
// Initialize the value struct
- code.addLine(prefixTabs + "\t"
- + ShortComment("Initialize the value struct"));
+ code.addLine(prefixTabs + "\t" + ShortComment("Initialize the value struct"));
// The very first assignment "
- code.addLine(prefixTabs + "\t"
- + DeclareDefine(name, "*value", SpecNaming.New + Brace(name)));
+ code.addLine(prefixTabs + "\t" + DeclareDefine(name, "*value", SpecNaming.New + Brace(name)));
// Don't leave out the RET field
if (!construct.getFunctionHeader().isReturnVoid())
- code.addLine(prefixTabs + "\t"
- + AssignToPtr("value", SpecNaming.RET, SpecNaming.RET));
+ 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(prefixTabs + "\t" + AssignToPtr("value", decl.name, decl.name));
code.addLine("");
// Store the value info into the current MethodCall
// _setInterfaceBeginAnnotationValue(info, value);
- code.addLine(prefixTabs
- + "\t"
- + ShortComment("Store the value info into the current MethodCall"));
- code.addLine(prefixTabs + "\t"
- + SpecNaming.SetInterfaceBeginAnnoValueFunc
+ code.addLine(prefixTabs + "\t" + ShortComment("Store the value info into the current MethodCall"));
+ code.addLine(prefixTabs + "\t" + SpecNaming.SetInterfaceBeginAnnoValueFunc
+ Brace(SpecNaming.AnnoInterfaceInfoInst + ", value") + ";");
code.addLine("");
projects / cdsspec-compiler.git / blobdiff