From 3f2abaf79b5d1cb74a405eb6a8c4f0471e41daa6 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Thu, 25 Feb 2016 17:27:41 -0800 Subject: [PATCH] add destructors --- .../uci/eecs/codeGenerator/CodeGenerator.java | 9 +- .../codeGenerator/CodeGeneratorUtils.java | 601 +++++++++--------- .../uci/eecs/codeGenerator/Environment.java | 23 + .../eecs/specExtraction/GlobalConstruct.java | 42 ++ .../specExtraction/InterfaceConstruct.java | 6 - .../uci/eecs/specExtraction/SpecNaming.java | 1 + 6 files changed, 372 insertions(+), 310 deletions(-) diff --git a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java index 41a5bdd..22e3908 100644 --- a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java @@ -326,14 +326,9 @@ public class CodeGenerator { } static public void main(String[] args) { -// String[] dirNames = { -// Environment.REGISTER, -// Environment.MS_QUEUE, -// Environment.LINUXRWLOCKS, -// Environment.MCS_LOCK, -// Environment.DEQUE, -// Environment.TREIBER_STACK }; + String[] dirNames = args; +// String[] dirNames = Environment.Benchmarks; for (int i = 0; i < dirNames.length; i++) { String dirName = dirNames[i]; diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java index 73176b9..694695c 100644 --- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java +++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java @@ -140,8 +140,12 @@ public class CodeGeneratorUtils { 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 @@ -166,9 +170,6 @@ public class CodeGeneratorUtils { 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")); @@ -176,70 +177,34 @@ public class CodeGeneratorUtils { ArrayList 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(""); - // 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(""); - - // Interface name strings - for (File file : interfaceListMap.keySet()) { - ArrayList 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 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(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))); @@ -249,75 +214,6 @@ public class CodeGeneratorUtils { } } - // 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 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();"); @@ -377,14 +273,31 @@ public class CodeGeneratorUtils { 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(""); 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 @@ -393,7 +306,8 @@ public class CodeGeneratorUtils { ArrayList 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(""); @@ -401,8 +315,10 @@ public class CodeGeneratorUtils { // 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(""); @@ -410,20 +326,28 @@ public class CodeGeneratorUtils { // 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.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(SpecNaming.PrintState), Quote("_" + + SpecNaming.PrintState.toLowerCase()))); code.addLine(""); // Interface name strings @@ -434,52 +358,49 @@ public class CodeGeneratorUtils { 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)); - // 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)); + 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"))); @@ -494,20 +415,23 @@ public class CodeGeneratorUtils { 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 @@ -516,19 +440,35 @@ public class CodeGeneratorUtils { 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 @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 + ") {"); + 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(""); @@ -548,16 +488,23 @@ public class CodeGeneratorUtils { // 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;")); @@ -574,14 +521,20 @@ public class CodeGeneratorUtils { // 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, SpecNaming.InterfaceValueInst, construct); + fieldsInit = GenerateInterfaceFieldsInitialization( + SpecNaming.Method2, SpecNaming.InterfaceValueInst, + construct); fieldsInit.align(1); code.addLines(fieldsInit); @@ -594,12 +547,16 @@ public class CodeGeneratorUtils { // 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, SpecNaming.InterfaceValueInst, construct); + fieldsInit = GenerateInterfaceFieldsInitialization( + SpecNaming.Method1, SpecNaming.InterfaceValueInst, + construct); fieldsInit.align(1); code.addLines(fieldsInit); @@ -611,32 +568,19 @@ public class CodeGeneratorUtils { 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, SpecNaming.InterfaceValueInst, 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 + ") {"); + 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, SpecNaming.InterfaceValueInst, construct); + fieldsInit = GenerateInterfaceFieldsInitialization( + SpecNaming.Method1, SpecNaming.InterfaceValueInst, + construct); fieldsInit.align(1); code.addLines(fieldsInit); @@ -649,11 +593,15 @@ public class CodeGeneratorUtils { } // 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, SpecNaming.InterfaceValueInst, construct); + fieldsInit = GenerateInterfaceFieldsInitialization( + SpecNaming.Method1, SpecNaming.InterfaceValueInst, + construct); fieldsInit.align(1); code.addLines(fieldsInit); @@ -677,35 +625,46 @@ public class CodeGeneratorUtils { // 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 + "),"; @@ -714,26 +673,29 @@ public class CodeGeneratorUtils { } 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(_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 + "(" + 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)); + 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(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 @@ -741,62 +703,72 @@ public class CodeGeneratorUtils { ArrayList 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 + "),"; - } - 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 + "),"; + line = line + "_" + name + "_" + SpecNaming.PreCondition + + "),"; } 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(""); } } @@ -804,8 +776,12 @@ public class CodeGeneratorUtils { // 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(""); @@ -839,13 +815,16 @@ public class CodeGeneratorUtils { * 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; } @@ -876,21 +855,23 @@ public class CodeGeneratorUtils { * 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 + "->" + SpecNaming.MethodValueField)); + res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) " + + methodInst + "->" + SpecNaming.MethodValueField)); // Don't leave out the RET field if (!construct.getFunctionHeader().isReturnVoid()) { - res.addLine(DeclareDefine(construct.getFunctionHeader().returnType, SpecNaming.RET, - inst + "->" + SpecNaming.RET)); + res.addLine(DeclareDefine(construct.getFunctionHeader().returnType, + SpecNaming.RET, inst + "->" + 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; } @@ -920,16 +901,19 @@ public class CodeGeneratorUtils { code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();"); break; case PotentialOP: - code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc + "(" + SpecNaming.AppendStr(label) + ");"); + code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc + + "(" + SpecNaming.AppendStr(label) + ");"); break; case OPCheck: - code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "(" + SpecNaming.AppendStr(label) + ");"); + code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "(" + + SpecNaming.AppendStr(label) + ");"); break; case OPClear: code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();"); break; case OPClearDefine: - code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc + "();"); + code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc + + "();"); break; default: break; @@ -998,7 +982,8 @@ public class CodeGeneratorUtils { // 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 + " {"); @@ -1006,34 +991,56 @@ public class CodeGeneratorUtils { 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, "*" + SpecNaming.InterfaceValueInst, SpecNaming.New + Brace(name))); + code.addLine(prefixTabs + + "\t" + + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst, + SpecNaming.New + Brace(name))); // Don't leave out the RET field if (!construct.getFunctionHeader().isReturnVoid()) - code.addLine(prefixTabs + "\t" + AssignToPtr(SpecNaming.InterfaceValueInst, SpecNaming.RET, SpecNaming.RET)); + code.addLine(prefixTabs + + "\t" + + AssignToPtr(SpecNaming.InterfaceValueInst, + SpecNaming.RET, SpecNaming.RET)); // For arguments for (VariableDeclaration decl : construct.getFunctionHeader().args) - code.addLine(prefixTabs + "\t" + AssignToPtr(SpecNaming.InterfaceValueInst, 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 // _setInterfaceBeginAnnotationValue(info, value); - code.addLine(prefixTabs + "\t" + ShortComment("Store the value info into the current MethodCall")); - code.addLine(prefixTabs + "\t" + SpecNaming.SetInterfaceBeginAnnoValueFunc - + Brace(SpecNaming.AnnoInterfaceInfoInst + ", " + SpecNaming.InterfaceValueInst) + ";"); + code.addLine(prefixTabs + + "\t" + + ShortComment("Store the value info into the current MethodCall")); + code.addLine(prefixTabs + + "\t" + + SpecNaming.SetInterfaceBeginAnnoValueFunc + + Brace(SpecNaming.AnnoInterfaceInfoInst + ", " + + SpecNaming.InterfaceValueInst) + ";"); code.addLine(""); // Return if necessary diff --git a/src/edu/uci/eecs/codeGenerator/Environment.java b/src/edu/uci/eecs/codeGenerator/Environment.java index 84fc4ee..563babb 100644 --- a/src/edu/uci/eecs/codeGenerator/Environment.java +++ b/src/edu/uci/eecs/codeGenerator/Environment.java @@ -1,5 +1,7 @@ package edu.uci.eecs.codeGenerator; +import java.util.ArrayList; + /** *

* This class contains some constant strings related to the code generation @@ -26,5 +28,26 @@ public class Environment { public final static String MCS_LOCK = "mcs-lock"; public final static String DEQUE = "chase-lev-deque-bugfix"; public final static String TREIBER_STACK = "treiber-stack"; + public final static String TICKET_LOCK = "ticket-lock"; + public final static String SEQLOCK = "seqlock"; + public final static String READ_COPY_UPDATE = "read-copy-update"; + public final static String CONCURRENT_MAP = "concurrent-hashmap"; + public final static String SPSC = "spsc-bugfix"; + public final static String MPMC = "mpmc-queue"; + + public final static String[] Benchmarks = { + REGISTER, + MS_QUEUE, + LINUXRWLOCKS, + MCS_LOCK, + DEQUE, + TREIBER_STACK, + TICKET_LOCK, + SEQLOCK, + READ_COPY_UPDATE, + CONCURRENT_MAP, + SPSC, + MPMC + }; } diff --git a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java index b2e52a0..d8f6dd4 100644 --- a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java +++ b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java @@ -21,6 +21,7 @@ public class GlobalConstruct extends Construct { public final ArrayList declState; public final Code initState; public final Code copyState; + public final Code clearState; public final Code finalState; public final Code printState; public final ArrayList commutativityRules; @@ -31,6 +32,8 @@ public class GlobalConstruct extends Construct { public final boolean autoGenInitial; // Whether we have auto-gen the state copying code public final boolean autoGenCopy; + // Whether we have auto-gen the state clearing code + public final boolean autoGenClear; // Whether we have auto-gen the state printing code public final boolean autoGenPrint; @@ -40,6 +43,7 @@ public class GlobalConstruct extends Construct { declState = new ArrayList(); initState = new Code(); copyState = new Code(); + clearState = new Code(); finalState = new Code(); printState = new Code(); commutativityRules = new ArrayList(); @@ -64,6 +68,12 @@ public class GlobalConstruct extends Construct { copyState.addLines(code); } + autoGenClear = clearState.isEmpty(); + if (autoGenClear) { + Code code = generateAutoClearFunction(); + clearState.addLines(code); + } + autoGenPrint = printState.isEmpty(); if (autoGenPrint) { Code code = generateAutoPrintFunction(); @@ -167,6 +177,35 @@ public class GlobalConstruct extends Construct { return code; } + + /** + *

+ * This function will automatically generate the clear statements for + * supported types if the user has not defined the "@Clear" primitive + *

+ * + * @return The auto-generated state copy statements + * @throws WrongAnnotationException + */ + private Code generateAutoClearFunction() throws WrongAnnotationException { + Code code = new Code(); + if (emptyState) // Empty state should have empty copy function + return code; + + // FIXME: Just try our best to generate recycling statements + for (VariableDeclaration decl : declState) { + String type = decl.type; + String name = decl.name; + if (type.equals("IntList *") || type.equals("IntSet *") + || type.equals("IntMap *")) { + // Supported pointer types + // if (stack) delete stack; + code.addLine("if (" + name + ") delete " + name + ";"); + } + } + + return code; + } /** *

@@ -209,6 +248,7 @@ public class GlobalConstruct extends Construct { if (!name.equals(SpecNaming.DeclareState) && !name.equals(SpecNaming.InitalState) && !name.equals(SpecNaming.CopyState) + && !name.equals(SpecNaming.ClearState) && !name.equals(SpecNaming.FinalState) && !name.equals(SpecNaming.Commutativity) && !name.equals(SpecNaming.PrintState)) { @@ -292,6 +332,8 @@ public class GlobalConstruct extends Construct { initState.addLines(primitive.contents); } else if (name.equals(SpecNaming.CopyState)) { copyState.addLines(primitive.contents); + } else if (name.equals(SpecNaming.ClearState)) { + clearState.addLines(primitive.contents); } else if (name.equals(SpecNaming.FinalState)) { finalState.addLines(primitive.contents); } else if (name.equals(SpecNaming.PrintState)) { diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java index 6afd5f1..232acaf 100644 --- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java +++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java @@ -24,7 +24,6 @@ public class InterfaceConstruct extends Construct { private String name; public final Code transition; public final Code preCondition; - public final Code sideEffect; public final Code postCondition; public final Code print; @@ -47,7 +46,6 @@ public class InterfaceConstruct extends Construct { this.name = null; this.transition = new Code(); this.preCondition = new Code(); - this.sideEffect = new Code(); this.postCondition = new Code(); this.print = new Code(); @@ -171,8 +169,6 @@ public class InterfaceConstruct extends Construct { this.transition.addLines(primitive.contents); } else if (name.equals(SpecNaming.PreCondition)) { this.preCondition.addLines(primitive.contents); - } else if (name.equals(SpecNaming.SideEffect)) { - this.sideEffect.addLines(primitive.contents); } else if (name.equals(SpecNaming.PostCondition)) { this.postCondition.addLines(primitive.contents); } else if (name.equals(SpecNaming.PrintValue)) { @@ -214,8 +210,6 @@ public class InterfaceConstruct extends Construct { sb.append("@Transition:\n" + transition); if (!preCondition.isEmpty()) sb.append("@PreCondition:\n" + preCondition); - if (!sideEffect.isEmpty()) - sb.append("@SideEffect:\n" + sideEffect); if (!postCondition.isEmpty()) sb.append("@PostCondition:\n" + postCondition); if (!print.isEmpty()) diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java index 463d2c9..f1f97ff 100644 --- a/src/edu/uci/eecs/specExtraction/SpecNaming.java +++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java @@ -21,6 +21,7 @@ public class SpecNaming { public static final String DeclareState = "DeclareState"; public static final String InitalState = "Initial"; public static final String CopyState = "Copy"; + public static final String ClearState = "Clear"; public static final String FinalState = "Final"; public static final String PrintState = "Print"; public static final String Commutativity = "Commutativity"; -- 2.34.1