From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 5 Dec 2013 05:53:03 +0000 (-0800)
Subject: more
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=541ee814ad10bc181abd4d8825397249c6f86ad7;hp=0a6651b877d4303c94fb0a2a9c5632acbd574f32

more
---

diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj
index 24accc9..cbe2e28 100644
--- a/grammer/spec_compiler.jj
+++ b/grammer/spec_compiler.jj
@@ -30,7 +30,7 @@
 	
 	b) Interface construct
 	@Begin
-	@Interface: ...
+	@Interface_decl: ...
 	@Commit_point_set:
 		IDENTIFIER | IDENTIFIER ...
 	@Condition: ... (Optional)
@@ -75,6 +75,25 @@
 	@Begin
 	@Interface_define: <Interface_Name>
 	@End
+
+	g) Interface declare & define construct
+	@Begin
+	@Interface_decl_define: <Interface_Name>
+	@Commit_point_set:
+		IDENTIFIER | IDENTIFIER ...
+	@Condition: ... (Optional)
+	@HB_Condition:
+		IDENTIFIER :: <C_CPP_Condition>
+	@HB_Condition: ...
+	@ID: ... (Optional, use default ID)
+	@Check: (Optional)
+		...
+	@Action: (Optional)
+		...
+	@Post_action: (Optional)
+	@Post_check: (Optional)
+	@End
+
 */
 
 
@@ -564,11 +583,13 @@ String ParameterizedName() :
 
 FunctionHeader FuncDecl() :
 {
+	ArrayList<VariableDeclaration> templateList;
 	String ret;
 	QualifiedName funcName;
 	ArrayList<VariableDeclaration> args;
 }
 {
+aa
 	(<STATIC> | <INLINE>)*
 	ret = Type() 
 	funcName = ParseQualifiedName() 
@@ -596,22 +617,31 @@ QualifiedName ParseQualifiedName() :
 	}
 }
 
-ArrayList<String> TemplateParamList() :
+ArrayList<VariableDeclaration> TemplateParamList() :
 {
-	ArrayList<String> params;
-	String str;
+	ArrayList<VariableDeclaration> params;
+	String type;
+	String name;
 }
 {
 	{
-		params = new ArrayList<String>();
+		params = new ArrayList<VariableDeclaration>();
 	}
 	<TEMPLATE>
 	"<"
-	(str = <IDENTIFIER>.image 
-	str = <IDENTIFIER>.image {params.add(str);})
+	(type = <IDENTIFIER>.image 
+	name = <IDENTIFIER>.image
+	{
+		params.add(new VariableDeclaration(type, name));
+	}
+	)
 
-	("," str = <IDENTIFIER>.image 
-	str = <IDENTIFIER>.image {params.add(str);})*
+	("," type = <IDENTIFIER>.image 
+	name = <IDENTIFIER>.image
+	{
+		params.add(new VariableDeclaration(type, name));
+	}
+	)*
 	">"
 	{
 		//System.out.println(params);
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index f98250d..e6dfc1d 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -482,7 +482,6 @@ public class CodeVariables {
 		String interfaceName = construct.name;
 		// Generate necessary header file (might be redundant but never mind)
 		newCode.add(INCLUDE(HEADER_STDLIB));
-		newCode.add(INCLUDE(HEADER_THREADS));
 		newCode.add(INCLUDE(HEADER_CDSANNOTATE));
 		newCode.add(INCLUDE(HEADER_SPECANNOTATION));
 		newCode.add(INCLUDE(HEADER_SPEC_LIB));
@@ -596,6 +595,7 @@ public class CodeVariables {
 		return newCode;
 	}
 
+	// Rename the interface depending on if it's declaration or definition
 	public static void renameInterface(SemanticsChecker semantics,
 			Construct construct) {
 		FunctionHeader header = getFunctionHeader(semantics, construct);
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java b/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
index 654e579..d48462a 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
@@ -4,6 +4,11 @@ public class Environment {
 	public static String HOME_DIRECTORY = System.getProperty("user.dir");
 	public static String GENERATED_FILE_DIR = HOME_DIRECTORY + "/" + "output";
 	public static String MODEL_CHECKER_HOME_DIR = System
-			.getProperty("user.home") + "/model-checker-priv";
+			.getProperty("user.home") + "/test/model-checker-priv";
 	public static String MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_HOME_DIR + "/test";
+	
+	public static String MS_QUEUE = MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_TEST_DIR + "/ms-queue";
+	public static String LINUXRWLOCKS = MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_TEST_DIR + "/linuxrwlocks";
+	public static String CLIFFC_HASHTABLE = MODEL_CHECKER_TEST_DIR = MODEL_CHECKER_TEST_DIR + "/cliffc-hashtable";
+			
 }
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java b/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
index f8e84bc..60f7700 100644
--- a/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
@@ -3,12 +3,15 @@ package edu.uci.eecs.specCompiler.specExtraction;
 import java.util.ArrayList;
 
 public class FunctionHeader {
+	public final ArrayList<VariableDeclaration> templateList;
+	
 	public final String returnType;
 	public final QualifiedName qualifiedName;
 	public final ArrayList<VariableDeclaration> args;
 
-	public FunctionHeader(String returnType, QualifiedName qualifiedName,
+	public FunctionHeader(ArrayList<VariableDeclaration> templateList, String returnType, QualifiedName qualifiedName,
 			ArrayList<VariableDeclaration> args) {
+		this.templateList = templateList;
 		this.returnType = returnType;
 		this.qualifiedName = qualifiedName;
 		this.args = args;
@@ -29,7 +32,7 @@ public class FunctionHeader {
 	public FunctionHeader getRenamedHeader(String prefix) {
 		String newFullName = qualifiedName.qualifiedName + prefix + "_"
 				+ qualifiedName.bareName;
-		FunctionHeader newHeader = new FunctionHeader(returnType,
+		FunctionHeader newHeader = new FunctionHeader(templateList, returnType,
 				new QualifiedName(newFullName), args);
 		return newHeader;
 	}
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java
index 8231c18..657b270 100644
--- a/src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java
@@ -4,7 +4,6 @@ import java.io.File;
 
 public class InterfaceDefineConstruct extends Construct {
 	public final String name;
-	private String funcDecl;
 
 	public InterfaceDefineConstruct(File file, int beginLineNum, String name) {
 		super(file, beginLineNum);