From: Peizhao Ou <peizhaoo@uci.edu>
Date: Tue, 25 Mar 2014 19:10:03 +0000 (-0700)
Subject: fix cp clear
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=b69f55ac12d851bb3f77b52d077e12802d0f3046

fix cp clear
---

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 0a1a7b2..a4e58b6 100644
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -269,7 +269,7 @@ static inline void read_unlock(rwlock_t *rw)
 /**
 	@Begin
 	@Interface: Write_Unlock
-	@Commit_point_set: Write_Unlock_Point
+	@Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
 	@Check:
 		reader_lock_cnt == 0 && writer_lock_acquired
 	@Action: 
@@ -285,6 +285,13 @@ static inline void write_unlock(rwlock_t *rw)
 		@Label: Write_Unlock_Point
 		@End
 	*/
+
+	/**
+		//@Begin
+		@Commit_point_clear: true
+		@Label: Write_Unlock_Clear
+		@End
+	*/
 }
 
 rwlock_t mylock;
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index fb1b520..4c4fc87 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -49,6 +49,7 @@ public class CodeVariables {
 	public static final String SPEC_ANNO_TYPE_INTERFACE_END = "INTERFACE_END";
 	public static final String SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE = "POTENTIAL_CP_DEFINE";
 	public static final String SPEC_ANNO_TYPE_CP_DEFINE_CHECK = "CP_DEFINE_CHECK";
+	public static final String SPEC_ANNO_TYPE_CP_CLEAR = "CP_CLEAR";
 	public static final String SPEC_ANNO_TYPE_CP_DEFINE = "CP_DEFINE";
 	public static final String SPEC_ANNOTATION = "spec_annotation";
 	public static final String SPEC_ANNOTATION_FIELD_TYPE = "type";
@@ -855,7 +856,7 @@ public class CodeVariables {
 		newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
 		newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
 		newCode.add("\t\t"
-				+ ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK));
+				+ ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_CLEAR));
 		newCode.add("\t\t" + ASSIGN_TO_PTR(anno, "annotation", structName));
 		newCode.add("\t\t" + ANNOTATE(semantics, anno));
 		newCode.add("\t" + "}");
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
index e5b5f9d..23dad2f 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
@@ -6,6 +6,7 @@ import java.util.HashMap;
 import java.util.HashSet;
 
 import edu.uci.eecs.specCompiler.grammerParser.ParseException;
+import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ClassBeginConstruct;
@@ -270,6 +271,15 @@ public class SemanticsChecker {
 				commitPointLabel2Num.put(label, _commitPointNum++);
 				num2CommitPointLabel.put(_commitPointNum, label);
 
+				CPLabel2Construct.put(label, construct);
+			} else if (construct instanceof CPClearConstruct) {
+				CPClearConstruct theConstruct = (CPClearConstruct) construct;
+				label = theConstruct.label;
+				checkLabelDuplication(construct, label);
+				// Number the commit point define check label
+				commitPointLabel2Num.put(label, _commitPointNum++);
+				num2CommitPointLabel.put(_commitPointNum, label);
+
 				CPLabel2Construct.put(label, construct);
 			} else if (construct instanceof CPDefineConstruct) {
 				CPDefineConstruct theConstruct = (CPDefineConstruct) construct;