projects
/
cdsspec-compiler.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
e462c46
)
allow shorter spec --- @Interface is not mandatory
author
Peizhao Ou
<peizhaoo@uci.edu>
Thu, 3 Mar 2016 22:45:46 +0000
(14:45 -0800)
committer
Peizhao Ou
<peizhaoo@uci.edu>
Thu, 3 Mar 2016 22:45:46 +0000
(14:45 -0800)
src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
patch
|
blob
|
history
src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
patch
|
blob
|
history
src/edu/uci/eecs/specExtraction/SpecExtractor.java
patch
|
blob
|
history
diff --git
a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 99c4f2e17ca038260ad55f0e10ff0a6c01c44cea..4100a0a3d5acddb338b9b1ee87605d63ac5e3a63 100644
(file)
--- 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();
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(ShortComment("Declare custom value struct for "
+ name));
- code.addLine("typedef struct " +
n
ame + " {");
+ code.addLine("typedef struct " +
structN
ame + " {");
FunctionHeader funcHeader = construct.getFunctionHeader();
// RET
if (!funcHeader.returnType.equals("void"))
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)));
}
for (VariableDeclaration decl : funcHeader.args) {
code.addLine(TabbedLine(Declare(decl)));
}
- code.addLine("} " +
n
ame + ";");
+ code.addLine("} " +
structN
ame + ";");
code.addLine("");
}
}
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;
+ 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(
code.addLine(TabbedLine(
- DeclareDefine(
rule.method1, "*M1", "(" + rule.method
1
+ DeclareDefine(
structName1, "*M1", "(" + structName
1
+ "*) m1->value"), 2));
code.addLine(TabbedLine(
+ "*) m1->value"), 2));
code.addLine(TabbedLine(
- DeclareDefine(
rule.method2, "*M2", "(" + rule.method
2
+ DeclareDefine(
structName2, "*M2", "(" + structName
2
+ "*) m2->value"), 2));
code.addLine(TabbedLine("return " + rule.condition + ";", 2));
code.addLine(TabbedLine("}"));
+ "*) 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();
// Define interface functions
String name = construct.getName();
+ String structName = construct.getStructName();
code.addLine("/********** " + name
+ " functions **********/");
// Define @Transition for INTERFACE
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 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(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,
// 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();
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);
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"
// 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
// 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 232acaf2b34bc5529db9d64bb10af8547059f1ca..1ff0cb05514cc3c8e7c01d56587cee307c6bcd03 100644
(file)
--- 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 {
*
*/
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;
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 preCondition;
+ public final Code transition;
public final Code postCondition;
public final Code print;
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;
super(file, beginLineNum);
this.endLineNum = endLineNum;
this.name = null;
- this.
transition = new Code()
;
+ this.
structName = null
;
this.preCondition = new Code();
this.preCondition = new Code();
+ this.transition = new Code();
this.postCondition = new Code();
this.print = 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)) {
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)) {
} 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);
// 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) {
// 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 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 d3a2521223e3a3c5a9f918de46de5161fbaf8544..afa42f78033b5d34475c38c5601fa251950563fc 100644
(file)
--- 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
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;
Matcher matcher = regexpBegin.matcher("");
String line;
@@
-652,7
+652,10
@@
public class SpecExtractor {
if (constructName.equals(SpecNaming.DeclareState)) {
extractGlobalConstruct(file, lineReader, line,
beginLineNum);
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)) {
extractInterfaceConstruct(file, lineReader, line,
beginLineNum);
} else if (constructName.equals(SpecNaming.Define)) {