(<CONST>
{ type = "const"; }
)?
- (((str = <STRUCT>.image | str = <CLASS>.image | str = <UNSIGNED>.image) { type = type + " " + str; })?
+ (
+ ((str = <STRUCT>.image | str = <CLASS>.image | str = <UNSIGNED>.image) {
+ type = type.equals("") ? type + str : type + " " + str;
+ })?
(
name = ParseQualifiedName() {
if (!type.equals(""))
}
static public void main(String[] args) {
-// String[] dirNames = { Environment.REGISTER, Environment.MS_QUEUE,
-// Environment.LINUXRWLOCKS, Environment.MCS_LOCK,
-// Environment.DEQUE };
- String[] dirNames = args;
+ String[] dirNames = { Environment.REGISTER, Environment.MS_QUEUE,
+ Environment.LINUXRWLOCKS, Environment.MCS_LOCK,
+ Environment.DEQUE, Environment.TREIBER_STACK };
+// String[] dirNames = args;
- for (int i = 0; i < dirNames.length; i++) {
+ for (int i = 5; i < dirNames.length; i++) {
String dirName = dirNames[i];
System.out.println("/********** Processing " + dirName
+ " **********/");
code.addLine(TabbedLine("#define " + decl.name + " "
+ SpecNaming.StateInst + "->" + decl.name));
}
- code.addLine(TabbedLine(ShortComment("User-defined intial state code")));
+ if (!globalConstruct.autoGenInitial)
+ code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
+ else
+ // Auto-generated the initialization function
+ code.addLine(TabbedLine(ShortComment("Auto-generated state intialization code")));
// Align the code with one tab
globalConstruct.initState.align(1);
code.addLines(globalConstruct.initState);
fieldsInit.align(1);
code.addLines(fieldsInit);
code.addLine("");
- code.addLine(TabbedLine(ShortComment("Execute the print-out")));
+ if (!globalConstruct.autoGenPrint)
+ code.addLine(TabbedLine(ShortComment("Execute user-defined state printing code")));
+ else
+ // Auto-generated the copy function
+ code.addLine(TabbedLine(ShortComment("Execute auto-generated state printing code")));
+
// Align the code with one tab
globalConstruct.printState.align(1);
code.addLines(globalConstruct.printState);
code.addLines(fieldsInit);
construct.print.align(1);
- code.addLine(TabbedLine(ShortComment("Execute Print")));
+ if (!construct.autoGenPrint)
+ code.addLine(TabbedLine(ShortComment("Execute user-defined value printing code")));
+ else
+ // Auto-generated the value printing function
+ code.addLine(TabbedLine(ShortComment("Execute auto-generated value printing code")));
code.addLines(construct.print);
code.addLine("}");
public final static String LINUXRWLOCKS = "linuxrwlocks";
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 Code printState;
public final ArrayList<CommutativityRule> commutativityRules;
+ // Whether the state declaration is empty
+ public final boolean emptyState;
+ // Whether we have auto-gen the state initialization code
+ public final boolean autoGenInitial;
+ // Whether we have auto-gen the state copying code
public final boolean autoGenCopy;
+ // Whether we have auto-gen the state printing code
+ public final boolean autoGenPrint;
public GlobalConstruct(File file, int beginLineNum,
ArrayList<String> annotations) throws WrongAnnotationException {
processAnnotations(annotations);
- if (copyState.isEmpty()) {
+ emptyState = declState.isEmpty();
+ if (emptyState) {
+ WrongAnnotationException.warning(file, beginLineNum,
+ "The state is empty. Make sure that's what you want!");
+ }
+
+ autoGenInitial = initState.isEmpty();
+ if (autoGenInitial) {
+ Code code = generateAutoInitalFunction();
+ initState.addLines(code);
+ }
+
+ autoGenCopy = copyState.isEmpty();
+ if (autoGenCopy) {
Code code = generateAutoCopyFunction();
copyState.addLines(code);
- autoGenCopy = true;
- } else {
- autoGenCopy = false;
}
+
+ autoGenPrint = printState.isEmpty();
+ if (autoGenPrint) {
+ Code code = generateAutoPrintFunction();
+ printState.addLines(code);
+ }
+ }
+
+ /**
+ * <p>
+ * This function will automatically generate the initial statements for
+ * supported types if the user has not defined the "@Initial" primitive
+ * </p>
+ *
+ * @return The auto-generated state intialization statements
+ * @throws WrongAnnotationException
+ */
+ private Code generateAutoInitalFunction() throws WrongAnnotationException {
+ Code code = new Code();
+ if (emptyState) // Empty state should have empty initial function
+ return code;
+ for (VariableDeclaration decl : declState) {
+ String type = decl.type;
+ String name = decl.name;
+ // Primitive types
+ if (type.equals("int") || type.equals("unsigned")
+ || type.equals("unsigned int")
+ || type.equals("int unsigned") || type.equals("double")
+ || type.equals("double") || type.equals("bool")) {
+ // x = 0;
+ code.addLine(name + " = 0;");
+ } else if (type.equals("IntList") || type.equals("IntSet")
+ || type.equals("IntMap")) {
+ // Supported types
+ // q = IntList();
+ code.addLine(name + " = " + type + "();");
+ } else if (type.equals("IntList *") || type.equals("IntSet *")
+ || type.equals("IntMap *")) {
+ // Supported pointer types
+ // q = new IntList;
+ String originalType = SpecUtils.trimSpace(type
+ .replace('*', ' '));
+ code.addLine(name + " = new " + originalType + "();");
+ } else {
+ WrongAnnotationException
+ .err(file,
+ beginLineNum,
+ "You have types in the state declaration that we do not support auto-gen initial function.");
+ }
+ }
+
+ return code;
}
/**
* supported types if the user has not defined the "@Copy" primitive
* </p>
*
- * @return The auto-generated copy statements
+ * @return The auto-generated state copy statements
* @throws WrongAnnotationException
*/
private Code generateAutoCopyFunction() throws WrongAnnotationException {
Code code = new Code();
+ if (emptyState) // Empty state should have empty copy function
+ return code;
for (VariableDeclaration decl : declState) {
String type = decl.type;
String name = decl.name;
return code;
}
+ /**
+ * <p>
+ * This function will automatically generate the printing statements for
+ * supported types if the user has not defined the "@Print" primitive
+ * </p>
+ *
+ * @return The auto-generated state printing statements
+ * @throws WrongAnnotationException
+ */
+ private Code generateAutoPrintFunction() throws WrongAnnotationException {
+ Code code = new Code();
+ if (emptyState) // Empty state should have empty printing function
+ return code;
+ for (VariableDeclaration decl : declState) {
+ String type = decl.type;
+ String name = decl.name;
+ code.addLines(SpecUtils.generatePrintStatement(type, name));
+ }
+
+ return code;
+ }
+
/**
* <p>
* Assert that the global state primitive is valid; if not, throws an
// arguments of the interface
private FunctionHeader funcHeader;
+ public final boolean autoGenPrint;
+
public InterfaceConstruct(File file, int beginLineNum, int endLineNum,
ArrayList<String> annotations) throws WrongAnnotationException {
super(file, beginLineNum);
this.print = new Code();
processAnnotations(annotations);
+
+ autoGenPrint = print.isEmpty();
}
public FunctionHeader getFunctionHeader() {
return this.name;
}
+ /**
+ * <p>
+ * This function will automatically generate the printing statements for
+ * supported types if the user has not defined the "@Print" primitive
+ * </p>
+ *
+ * @return The auto-generated state printing statements
+ * @throws WrongAnnotationException
+ */
+ private Code generateAutoPrintFunction() {
+ Code code = new Code();
+ // For RET
+ code.addLines(SpecUtils.generatePrintStatement(funcHeader.returnType,
+ SpecNaming.RET));
+ // For arguments
+ for (VariableDeclaration decl : funcHeader.args) {
+ String type = decl.type;
+ String name = decl.name;
+ code.addLines(SpecUtils.generatePrintStatement(type, name));
+ }
+ return code;
+ }
+
/**
* <p>
* Assert that the interface primitive is valid; if not, throws an exception
funcHeader = UtilParser.parseFuncHeader(line);
// Record the original declaration line
funcHeader.setHeaderLine(line);
+
+ // Once we have the compelte function declaration, we can auto-gen the
+ // print-out statements if it's not defined
+ if (autoGenPrint) {
+ print.addLines(generateAutoPrintFunction());
+ }
}
public String toString() {
annotations.add(curLine);
// System.out.println(curLine);
// Initial settings for matching lines
- // "\*/( |\t)*$"
- Pattern regexpEnd = Pattern.compile("\\*/( |\\t)*$");
+ // "\*/\s*$"
+ Pattern regexpEnd = Pattern.compile("\\*/\\s*$");
Matcher matcher = regexpEnd.matcher(curLine);
- if (matcher.find()) { // The beginning line is also the end line
- annotations.add(curLine);
+ if (matcher.find()) {
+ // The beginning line is also the end line
+ // In this case, we have already add the curLine
return annotations;
} else {
try {
// Other CDSSpec functions
public static final String AddInterfaceFunctions = "addInterfaceFunctions";
public static final String CDSAnnotateFunc = "cdsannotate";
+ public static final String PRINT = "PRINT";
+ public static final String PrintContainer = "printContainer";
// Special instances
public static final String Method1 = "_M";
* annotations or the beginning line of the next primitive
* @throws WrongAnnotationException
*/
- public static Primitive extractPrimitive(File file, int beginLineNum, ArrayList<String> annotations, IntObj curIdx)
+ public static Primitive extractPrimitive(File file, int beginLineNum,
+ ArrayList<String> annotations, IntObj curIdx)
throws WrongAnnotationException {
if (curIdx.getVal() == annotations.size()) // The current index points
// to the end
}
// Assert that we must have found one primitive
if (primitive == null) {
- WrongAnnotationException.err(file, curLineNum,
- "Something is wrong! We must have found one primitve here!\n");
+ WrongAnnotationException
+ .err(file, curLineNum,
+ "Something is wrong! We must have found one primitve here!\n");
}
// Process the current "primitive"
primitive.addLine(trimmedCode);
}
} else {
- WrongAnnotationException.err(file, curLineNum,
- "The state annotation should have correct primitive syntax (sub-annotations)");
+ WrongAnnotationException
+ .err(file, curLineNum,
+ "The state annotation should have correct primitive syntax (sub-annotations)");
}
// Deal with other normal line. E.g. y = 1;
if (primitive.contents.size() == 0) { // The content of the primitive is
// empty
- WrongAnnotationException.warning(file, curLineNum, "Primitive " + primitive.name + " is empty.");
+ WrongAnnotationException.warning(file, curLineNum, "Primitive "
+ + primitive.name + " is empty.");
}
return primitive;
}
// FIXME: We only consider the type is either a one-level pointer or a
// struct
String bareType = trimSpace(type.replace('*', ' '));
- return !bareType.equals("int") && !bareType.matches("unsigned\\s+int") && !bareType.equals("unsigned")
- && !bareType.equals("bool") && !bareType.equals("double") && !bareType.equals("float")
+ return !bareType.equals("int") && !bareType.matches("unsigned\\s+int")
+ && !bareType.equals("unsigned") && !bareType.equals("bool")
+ && !bareType.equals("double") && !bareType.equals("float")
&& !bareType.equals("void");
}
String bareType = trimSpace(type.replace('*', ' '));
return bareType;
}
+
+ /**
+ * <p>
+ * This function will automatically generate the printing statements for
+ * supported types when given a type and a name of the declaration.
+ * </p>
+ *
+ * @return The auto-generated state printing statements
+ */
+ public static Code generatePrintStatement(String type, String name) {
+ Code code = new Code();
+ // Primitive types
+ if (type.equals("int") || type.equals("unsigned")
+ || type.equals("unsigned int") || type.equals("int unsigned")
+ || type.equals("double") || type.equals("double")
+ || type.equals("bool")) {
+ // PRINT("\tx=%d\n", x);
+ code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%d\\n\", "
+ + name + ");");
+ } else if (type.equals("int *") || type.equals("unsigned *")
+ || type.equals("unsigned int *")
+ || type.equals("int unsigned *") || type.equals("double *")
+ || type.equals("double *") || type.equals("bool *")) {
+ // Supported pointer types for primitive types
+ // PRINT("\t*x=%d\n", *x);
+ code.addLine(SpecNaming.PRINT + "(\"\\t*" + name + "=%d\\n\", *"
+ + name + ");");
+ } else if (type.equals("IntList") || type.equals("IntSet")
+ || type.equals("IntMap")) {
+ // Supported types
+ // PRINT("\tq: ");
+ // printContainer(&q);
+ // model_print("\n");
+ code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
+ code.addLine(SpecNaming.PrintContainer + "(&" + name + ");");
+ code.addLine(SpecNaming.PRINT + "(\"\\n\");");
+ } else if (type.equals("IntList *") || type.equals("IntSet *")
+ || type.equals("IntMap *")) {
+ // Supported pointer types
+ // PRINT("\tq: ");
+ // printContainer(q);
+ // model_print("\n");
+ code.addLine(SpecNaming.PRINT + "(\"\\t" + name + ": \");");
+ code.addLine(SpecNaming.PrintContainer + "(" + name + ");");
+ code.addLine(SpecNaming.PRINT + "(\"\\n\");");
+ } else if (type.equals("void")) {
+ // Just do nothing!
+ } else {
+ if (type.endsWith("*")) { // If it's an obvious pointer (with a STAR)
+ // Weak support pointer types (just print out the address)
+ // PRINT("\tmutex=%p\n", mutex);
+ code.addLine(SpecNaming.PRINT + "(\"\\t" + name + "=%p\\n\", "
+ + name + ");");
+ } else {
+ code.addLine("// We do not support auto-gen print-out for type: "
+ + type + ".");
+ }
+
+ }
+
+ return code;
+ }
+
}