From: Peizhao Ou Date: Thu, 3 Mar 2016 22:45:46 +0000 (-0800) Subject: allow shorter spec --- @Interface is not mandatory X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=d9e508585c6a61b781f2cc6beeac3b8e7ecc402c allow shorter spec --- @Interface is not mandatory --- diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java index 99c4f2e..4100a0a 100644 --- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java +++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java @@ -197,9 +197,10 @@ public class CodeGeneratorUtils { for (InterfaceConstruct construct : list) { // Declare custom value struct for the interface String name = construct.getName(); + String structName = construct.getStructName(); code.addLine(ShortComment("Declare custom value struct for " + name)); - code.addLine("typedef struct " + name + " {"); + code.addLine("typedef struct " + structName + " {"); FunctionHeader funcHeader = construct.getFunctionHeader(); // RET if (!funcHeader.returnType.equals("void")) @@ -209,7 +210,7 @@ public class CodeGeneratorUtils { for (VariableDeclaration decl : funcHeader.args) { code.addLine(TabbedLine(Declare(decl))); } - code.addLine("} " + name + ";"); + code.addLine("} " + structName + ";"); code.addLine(""); } } @@ -498,11 +499,15 @@ public class CodeGeneratorUtils { + SpecNaming.AppendStr(rule.method2) + ") {")); // Initialize M1 & M2 in commutativity rule // e.g. ENQ *M1 = (ENQ*) m1->value; + String structName1 = InterfaceConstruct + .createStructName(rule.method1); + String structName2 = InterfaceConstruct + .createStructName(rule.method2); code.addLine(TabbedLine( - DeclareDefine(rule.method1, "*M1", "(" + rule.method1 + DeclareDefine(structName1, "*M1", "(" + structName1 + "*) m1->value"), 2)); code.addLine(TabbedLine( - DeclareDefine(rule.method2, "*M2", "(" + rule.method2 + DeclareDefine(structName2, "*M2", "(" + structName2 + "*) m2->value"), 2)); code.addLine(TabbedLine("return " + rule.condition + ";", 2)); code.addLine(TabbedLine("}")); @@ -520,6 +525,7 @@ public class CodeGeneratorUtils { // Define interface functions String name = construct.getName(); + String structName = construct.getStructName(); code.addLine("/********** " + name + " functions **********/"); // Define @Transition for INTERFACE @@ -861,10 +867,11 @@ public class CodeGeneratorUtils { String inst, InterfaceConstruct construct) { Code res = new Code(); String name = construct.getName(); + String structName = construct.getStructName(); res.addLine(ShortComment("Initialize fields for " + name)); // The very first assignment " - res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) " - + methodInst + "->" + SpecNaming.MethodValueField)); + res.addLine(DeclareDefine(structName, "*" + inst, "(" + structName + + "*) " + methodInst + "->" + SpecNaming.MethodValueField)); // Don't leave out the RET field if (!construct.getFunctionHeader().isReturnVoid()) { res.addLine(DeclareDefine(construct.getFunctionHeader().returnType, @@ -975,6 +982,7 @@ public class CodeGeneratorUtils { Code code = new Code(); String name = construct.getName(); + String structName = construct.getStructName(); String beginLine = construct.getFunctionHeader().getHeaderLine(); Pattern regexpSpace = Pattern.compile("^(\\s*)\\S.*$"); Matcher matcherSpace = regexpSpace.matcher(beginLine); @@ -1017,8 +1025,9 @@ public class CodeGeneratorUtils { // The very first assignment " code.addLine(prefixTabs + "\t" - + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst, - SpecNaming.New + Brace(name))); + + DeclareDefine(structName, + "*" + SpecNaming.InterfaceValueInst, SpecNaming.New + + Brace(structName))); // Don't leave out the RET field if (!construct.getFunctionHeader().isReturnVoid()) code.addLine(prefixTabs diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java index 232acaf..1ff0cb0 100644 --- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java +++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java @@ -21,9 +21,16 @@ import edu.uci.eecs.utilParser.UtilParser; * */ public class InterfaceConstruct extends Construct { + // The interface label of the current interface; If not specified, we use + // the actual interface name to represent this interface private String name; - public final Code transition; + // Each interface interface will have an auto-generated struct that + // represents the return value and the arguments of that interface method + // call. We will mangle the interface label name to get this name in case we + // have other name conflict + private String structName; public final Code preCondition; + public final Code transition; public final Code postCondition; public final Code print; @@ -44,8 +51,9 @@ public class InterfaceConstruct extends Construct { super(file, beginLineNum); this.endLineNum = endLineNum; this.name = null; - this.transition = new Code(); + this.structName = null; this.preCondition = new Code(); + this.transition = new Code(); this.postCondition = new Code(); this.print = new Code(); @@ -164,7 +172,8 @@ public class InterfaceConstruct extends Construct { if (primitive.contents.size() == 0) continue; if (name.equals(SpecNaming.Interface)) { - this.name = extractInterfaceName(file, primitive); + String interName = extractInterfaceName(file, primitive); + setNames(interName); } else if (name.equals(SpecNaming.Transition)) { this.transition.addLines(primitive.contents); } else if (name.equals(SpecNaming.PreCondition)) { @@ -195,6 +204,12 @@ public class InterfaceConstruct extends Construct { // Record the original declaration line funcHeader.setHeaderLine(line); + // If users have not defined @Interface, we should use the function name + // as the interface label + if (name == null) { + setNames(funcHeader.funcName.bareName); + } + // Once we have the compelte function declaration, we can auto-gen the // print-out statements if it's not defined if (autoGenPrint) { @@ -226,4 +241,19 @@ public class InterfaceConstruct extends Construct { public void setEndLineNumFunction(int endLineNumFunction) { this.endLineNumFunction = endLineNumFunction; } + + public String getStructName() { + return structName; + } + + private void setNames(String name) { + this.name = name; + if (name == null) + return; + structName = createStructName(name); + } + + static public String createStructName(String labelName) { + return "__struct_" + labelName + "__"; + } } diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java index d3a2521..afa42f7 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|Define)"); + .compile("/\\*\\*\\s*@(DeclareState|Interface|PreCondition|Transition|PostCondition|Define)"); Matcher matcher = regexpBegin.matcher(""); String line; @@ -652,7 +652,10 @@ public class SpecExtractor { if (constructName.equals(SpecNaming.DeclareState)) { extractGlobalConstruct(file, lineReader, line, beginLineNum); - } else if (constructName.equals(SpecNaming.Interface)) { + } else if (constructName.equals(SpecNaming.Interface) + || constructName.equals(SpecNaming.PreCondition) + || constructName.equals(SpecNaming.Transition) + || constructName.equals(SpecNaming.PostCondition)) { extractInterfaceConstruct(file, lineReader, line, beginLineNum); } else if (constructName.equals(SpecNaming.Define)) {