From 5781b9606184c945d081e66a276b0366e10cd41f Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Sun, 20 Mar 2016 15:19:36 -0700 Subject: [PATCH] edits --- .../codeGenerator/CodeGeneratorUtils.java | 68 ++++++++++++++++--- .../specExtraction/InterfaceConstruct.java | 5 ++ .../eecs/specExtraction/SpecExtractor.java | 3 +- .../uci/eecs/specExtraction/SpecNaming.java | 2 + 4 files changed, 69 insertions(+), 9 deletions(-) diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java index 7dcaaa0..6a90a72 100644 --- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java +++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java @@ -408,6 +408,15 @@ public class CodeGeneratorUtils { code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString)); + // JustifyingCondition + tmpFunc = name + "_" + SpecNaming.JustifyingCondition; + if (!construct.justifyingCondition.isEmpty()) + code.addLine(DeclareDefine(SpecNaming.CString, + SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc))); + else + code.addLine(DeclareDefine(SpecNaming.CString, + SpecNaming.AppendStr(tmpFunc), + SpecNaming.EmptyCString)); // PostCondition tmpFunc = name + "_" + SpecNaming.PostCondition; if (!construct.postCondition.isEmpty()) @@ -594,13 +603,14 @@ public class CodeGeneratorUtils { if (!construct.preCondition.isEmpty()) { code.addLine(ShortComment("Define @" + SpecNaming.PreCondition + " for " + name)); - code.addLine("bool _" + name + "_" - + SpecNaming.PreCondition + "(" + SpecNaming.Method - + " " + SpecNaming.Method1 + ") {"); + code.addLine("bool _" + name + "_" + SpecNaming.PreCondition + + "(" + SpecNaming.Method + " " + SpecNaming.Method1 + + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + + ") {"); // Initialize value struct fields fieldsInit = GenerateInterfaceFieldsInitialization( - SpecNaming.Method1, SpecNaming.InterfaceValueInst, + SpecNaming.Method2, SpecNaming.InterfaceValueInst, construct); fieldsInit.align(1); code.addLines(fieldsInit); @@ -616,19 +626,47 @@ public class CodeGeneratorUtils { code.addLine("}"); code.addLine(""); + } + // Define @JustifyingCondition + if (!construct.justifyingCondition.isEmpty()) { + code.addLine(ShortComment("Define @" + + SpecNaming.JustifyingCondition + " for " + name)); + code.addLine("bool _" + name + "_" + SpecNaming.JustifyingCondition + + "(" + 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.justifyingCondition.align(1); + code.addLine(TabbedLine(ShortComment("Execute JustifyingCondition"))); + code.addLines(construct.justifyingCondition); + + // By default, we will return true for @PreCondition + code.addLine(TabbedLine(ShortComment("By default @JustifyingCondition returns true"))); + code.addLine(TabbedLine("return true;")); + + code.addLine("}"); + code.addLine(""); + } // Define @PostCondition if (!construct.postCondition.isEmpty()) { code.addLine(ShortComment("Define @" + SpecNaming.PostCondition + " for " + name)); - code.addLine("bool _" + name + "_" - + SpecNaming.PostCondition + "(" - + SpecNaming.Method + " " + SpecNaming.Method1 + code.addLine("bool _" + name + "_" + SpecNaming.PostCondition + + "(" + SpecNaming.Method + " " + SpecNaming.Method1 + + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ") {"); // Initialize value struct fields fieldsInit = GenerateInterfaceFieldsInitialization( - SpecNaming.Method1, SpecNaming.InterfaceValueInst, + SpecNaming.Method2, SpecNaming.InterfaceValueInst, construct); fieldsInit.align(1); code.addLines(fieldsInit); @@ -791,6 +829,20 @@ public class CodeGeneratorUtils { + "),"; } code.addLine(TabbedLine(line, 2)); + // JustifyingCondition + line = "new " + + SpecNaming.NamedFunction + + "(" + + SpecNaming.AppendStr(name + "_" + + SpecNaming.JustifyingCondition) + ", " + + SpecNaming.JustifyingConditionType + ", (void*) "; + if (construct.justifyingCondition.isEmpty()) { + line = line + SpecNaming.NullFunc + "),"; + } else { + line = line + "_" + name + "_" + SpecNaming.JustifyingCondition + + "),"; + } + code.addLine(TabbedLine(line, 2)); // PostCondition line = "new " + SpecNaming.NamedFunction diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java index 1ff0cb0..e2b0290 100644 --- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java +++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java @@ -30,6 +30,7 @@ public class InterfaceConstruct extends Construct { // have other name conflict private String structName; public final Code preCondition; + public final Code justifyingCondition; public final Code transition; public final Code postCondition; public final Code print; @@ -53,6 +54,7 @@ public class InterfaceConstruct extends Construct { this.name = null; this.structName = null; this.preCondition = new Code(); + this.justifyingCondition = new Code(); this.transition = new Code(); this.postCondition = new Code(); this.print = new Code(); @@ -122,6 +124,7 @@ 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.SideEffect) && !name.equals(SpecNaming.PostCondition) && !name.equals(SpecNaming.PrintValue)) { @@ -178,6 +181,8 @@ 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.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 df0b5f1..f8925fb 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|Transition|PostCondition|Define)"); + .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|JustifyingCondition|Transition|PostCondition|Define)"); Matcher matcher = regexpBegin.matcher(""); String line; @@ -654,6 +654,7 @@ public class SpecExtractor { beginLineNum); } else if (constructName.equals(SpecNaming.Interface) || constructName.equals(SpecNaming.PreCondition) + || constructName.equals(SpecNaming.JustifyingCondition) || constructName.equals(SpecNaming.Transition) || constructName.equals(SpecNaming.PostCondition)) { extractInterfaceConstruct(file, lineReader, line, diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java index 8355b75..5b48c99 100644 --- a/src/edu/uci/eecs/specExtraction/SpecNaming.java +++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java @@ -33,6 +33,7 @@ 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 SideEffect = "SideEffect"; public static final String PostCondition = "PostCondition"; public static final String PrintValue = "Print"; @@ -41,6 +42,7 @@ 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 SideEffectType = "SIDE_EFFECT"; public static final String PostConditionType = "POST_CONDITION"; -- 2.34.1