From ae001970e291857b3fc716f1a1e1472139a4faa6 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Mon, 11 Jul 2016 18:03:30 -0700 Subject: [PATCH] edits --- .../uci/eecs/codeGenerator/CodeGenerator.java | 4 +- .../codeGenerator/CodeGeneratorUtils.java | 108 +++++++++++++----- .../uci/eecs/codeGenerator/Environment.java | 24 ++-- .../eecs/specExtraction/FunctionHeader.java | 2 +- .../specExtraction/InterfaceConstruct.java | 19 +-- .../eecs/specExtraction/SpecExtractor.java | 5 +- .../uci/eecs/specExtraction/SpecNaming.java | 9 +- 7 files changed, 118 insertions(+), 53 deletions(-) diff --git a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java index 22e3908..a77855a 100644 --- a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java @@ -327,8 +327,8 @@ public class CodeGenerator { static public void main(String[] args) { - String[] dirNames = args; -// String[] dirNames = Environment.Benchmarks; +// 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 6a90a72..e6fd383 100644 --- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java +++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java @@ -214,10 +214,15 @@ public class CodeGeneratorUtils { + 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.RET))); + SpecNaming.C_RET))); + code.addLine(TabbedLine(Declare(funcHeader.returnType, + SpecNaming.S_RET))); + } // Arguments for (VariableDeclaration decl : funcHeader.args) { code.addLine(TabbedLine(Declare(decl))); @@ -408,9 +413,18 @@ public class CodeGeneratorUtils { code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString)); - // JustifyingCondition - tmpFunc = name + "_" + SpecNaming.JustifyingCondition; - if (!construct.justifyingCondition.isEmpty()) + // JustifyingPrecondition + tmpFunc = name + "_" + SpecNaming.JustifyingPrecondition; + if (!construct.justifyingPrecondition.isEmpty()) + code.addLine(DeclareDefine(SpecNaming.CString, + SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc))); + else + code.addLine(DeclareDefine(SpecNaming.CString, + SpecNaming.AppendStr(tmpFunc), + SpecNaming.EmptyCString)); + // JustifyingPostcondition + tmpFunc = name + "_" + SpecNaming.JustifyingPostcondition; + if (!construct.justifyingPostcondition.isEmpty()) code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc))); else @@ -627,11 +641,11 @@ public class CodeGeneratorUtils { code.addLine(""); } - // Define @JustifyingCondition - if (!construct.justifyingCondition.isEmpty()) { + // Define @JustifyingPrecondition + if (!construct.justifyingPrecondition.isEmpty()) { code.addLine(ShortComment("Define @" - + SpecNaming.JustifyingCondition + " for " + name)); - code.addLine("bool _" + name + "_" + SpecNaming.JustifyingCondition + + SpecNaming.JustifyingPrecondition + " for " + name)); + code.addLine("bool _" + name + "_" + SpecNaming.JustifyingPrecondition + "(" + SpecNaming.Method + " " + SpecNaming.Method1 + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ") {"); @@ -643,12 +657,40 @@ public class CodeGeneratorUtils { fieldsInit.align(1); code.addLines(fieldsInit); - construct.justifyingCondition.align(1); - code.addLine(TabbedLine(ShortComment("Execute JustifyingCondition"))); - code.addLines(construct.justifyingCondition); + construct.justifyingPrecondition.align(1); + code.addLine(TabbedLine(ShortComment("Execute JustifyingPrecondition"))); + code.addLines(construct.justifyingPrecondition); - // By default, we will return true for @PreCondition - code.addLine(TabbedLine(ShortComment("By default @JustifyingCondition returns true"))); + // 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("}"); @@ -829,17 +871,31 @@ public class CodeGeneratorUtils { + "),"; } code.addLine(TabbedLine(line, 2)); - // JustifyingCondition + // 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.JustifyingCondition) + ", " - + SpecNaming.JustifyingConditionType + ", (void*) "; - if (construct.justifyingCondition.isEmpty()) { + + SpecNaming.JustifyingPostcondition) + ", " + + SpecNaming.JustifyingPostconditionType + ", (void*) "; + if (construct.justifyingPostcondition.isEmpty()) { line = line + SpecNaming.NullFunc + "),"; } else { - line = line + "_" + name + "_" + SpecNaming.JustifyingCondition + line = line + "_" + name + "_" + SpecNaming.JustifyingPostcondition + "),"; } code.addLine(TabbedLine(line, 2)); @@ -974,10 +1030,10 @@ public class CodeGeneratorUtils { // 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) { @@ -1124,7 +1180,7 @@ public class CodeGeneratorUtils { // 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(""); @@ -1138,12 +1194,12 @@ public class CodeGeneratorUtils { + 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 @@ -1174,7 +1230,7 @@ public class CodeGeneratorUtils { // 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; diff --git a/src/edu/uci/eecs/codeGenerator/Environment.java b/src/edu/uci/eecs/codeGenerator/Environment.java index bbdfa9e..f9665b7 100644 --- a/src/edu/uci/eecs/codeGenerator/Environment.java +++ b/src/edu/uci/eecs/codeGenerator/Environment.java @@ -37,19 +37,19 @@ public class Environment { public final static String MPMC = "mpmc-queue"; public final static String[] Benchmarks = { - REGISTER_ACQREL, - REGISTER_RELAXED, +// REGISTER_ACQREL, +// REGISTER_RELAXED, MS_QUEUE, - LINUXRWLOCKS, - MCS_LOCK, - DEQUE, - TREIBER_STACK, - TICKET_LOCK, - SEQLOCK, - READ_COPY_UPDATE, - CONCURRENT_MAP, - SPSC, - MPMC +// LINUXRWLOCKS, +// MCS_LOCK, +// DEQUE, +// TREIBER_STACK, +// TICKET_LOCK, +// SEQLOCK, +// READ_COPY_UPDATE, +// CONCURRENT_MAP, +// SPSC, +// MPMC }; } diff --git a/src/edu/uci/eecs/specExtraction/FunctionHeader.java b/src/edu/uci/eecs/specExtraction/FunctionHeader.java index b79d65b..d07a0a1 100644 --- a/src/edu/uci/eecs/specExtraction/FunctionHeader.java +++ b/src/edu/uci/eecs/specExtraction/FunctionHeader.java @@ -164,7 +164,7 @@ public class FunctionHeader { public String getRenamedCall(String prefix) { String res = ""; if (!isReturnVoid()) { - res = res + returnType + " " + SpecNaming.RET + " = "; + res = res + returnType + " " + SpecNaming.C_RET + " = "; } res = res + prefix + "_" + funcName.fullName + "("; if (args.size() >= 1) { diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java index e2b0290..ddc2614 100644 --- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java +++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java @@ -30,8 +30,9 @@ public class InterfaceConstruct extends Construct { // have other name conflict private String structName; public final Code preCondition; - public final Code justifyingCondition; + public final Code justifyingPrecondition; public final Code transition; + public final Code justifyingPostcondition; public final Code postCondition; public final Code print; @@ -54,8 +55,9 @@ public class InterfaceConstruct extends Construct { this.name = null; this.structName = null; this.preCondition = new Code(); - this.justifyingCondition = new Code(); + this.justifyingPrecondition = new Code(); this.transition = new Code(); + this.justifyingPostcondition = new Code(); this.postCondition = new Code(); this.print = new Code(); @@ -94,9 +96,9 @@ public class InterfaceConstruct extends Construct { */ private Code generateAutoPrintFunction() { Code code = new Code(); - // For RET + // For C_RET code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType, - SpecNaming.RET)); + SpecNaming.C_RET)); // For arguments for (VariableDeclaration decl : funcHeader.args) { String type = decl.type; @@ -124,8 +126,9 @@ public class InterfaceConstruct extends Construct { if (!name.equals(SpecNaming.Interface) && !name.equals(SpecNaming.Transition) && !name.equals(SpecNaming.PreCondition) - && !name.equals(SpecNaming.JustifyingCondition) + && !name.equals(SpecNaming.JustifyingPrecondition) && !name.equals(SpecNaming.SideEffect) + && !name.equals(SpecNaming.JustifyingPostcondition) && !name.equals(SpecNaming.PostCondition) && !name.equals(SpecNaming.PrintValue)) { WrongAnnotationException.err(file, lineNum, name @@ -181,8 +184,10 @@ 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.JustifyingCondition)) { - this.justifyingCondition.addLines(primitive.contents); + } else if (name.equals(SpecNaming.JustifyingPrecondition)) { + this.justifyingPrecondition.addLines(primitive.contents); + } else if (name.equals(SpecNaming.JustifyingPostcondition)) { + this.justifyingPostcondition.addLines(primitive.contents); } else if (name.equals(SpecNaming.PostCondition)) { this.postCondition.addLines(primitive.contents); } else if (name.equals(SpecNaming.PrintValue)) { diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java index f8925fb..a12ce25 100644 --- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java +++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java @@ -624,7 +624,7 @@ public class SpecExtractor { lineReader = new LineNumberReader(br); // "/\*\*\s*@(DeclareState|Interface)" Pattern regexpBegin = Pattern - .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingCondition|Transition|PostCondition|Define)"); + .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingCondition|Transition|JustifyingPostcondition|PostCondition|Define)"); Matcher matcher = regexpBegin.matcher(""); String line; @@ -654,8 +654,9 @@ public class SpecExtractor { beginLineNum); } else if (constructName.equals(SpecNaming.Interface) || constructName.equals(SpecNaming.PreCondition) - || constructName.equals(SpecNaming.JustifyingCondition) + || constructName.equals(SpecNaming.JustifyingPrecondition) || constructName.equals(SpecNaming.Transition) + || constructName.equals(SpecNaming.JustifyingPostcondition) || constructName.equals(SpecNaming.PostCondition)) { extractInterfaceConstruct(file, lineReader, line, beginLineNum); diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java index 5b48c99..9f1c5dd 100644 --- a/src/edu/uci/eecs/specExtraction/SpecNaming.java +++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java @@ -33,8 +33,9 @@ public class SpecNaming { public static final String Interface = "Interface"; public static final String Transition = "Transition"; public static final String PreCondition = "PreCondition"; - public static final String JustifyingCondition = "JustifyingCondition"; + public static final String JustifyingPrecondition = "JustifyingPrecondition"; public static final String SideEffect = "SideEffect"; + public static final String JustifyingPostcondition = "JustifyingPostcondition"; public static final String PostCondition = "PostCondition"; public static final String PrintValue = "Print"; @@ -42,8 +43,9 @@ public class SpecNaming { public static final String PrintValueType = "PRINT_VALUE"; public static final String TransitionType = "TRANSITION"; public static final String PreConditionType = "PRE_CONDITION"; - public static final String JustifyingConditionType = "JUSTIFYING_CONDITION"; + public static final String JustifyingPreconditionType = "JUSTIFYING_PRECONDITION"; public static final String SideEffectType = "SIDE_EFFECT"; + public static final String JustifyingPostconditionType = "JUSTIFYING_POSTCONDITION"; public static final String PostConditionType = "POST_CONDITION"; // Ordering point construct @@ -194,7 +196,8 @@ public class SpecNaming { public static final String OldStateInst = "OLD"; public static final String NewStateInst = "NEW"; // Specification types and macros - public static final String RET = "RET"; + public static final String C_RET = "C_RET"; + public static final String S_RET = "S_RET"; public static final String InterfaceValueInst = "__value"; // The fake ordering point operation -- 2.34.1