From 3f2abaf79b5d1cb74a405eb6a8c4f0471e41daa6 Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 25 Feb 2016 17:27:41 -0800
Subject: [PATCH] add destructors

---
 .../uci/eecs/codeGenerator/CodeGenerator.java |   9 +-
 .../codeGenerator/CodeGeneratorUtils.java     | 601 +++++++++---------
 .../uci/eecs/codeGenerator/Environment.java   |  23 +
 .../eecs/specExtraction/GlobalConstruct.java  |  42 ++
 .../specExtraction/InterfaceConstruct.java    |   6 -
 .../uci/eecs/specExtraction/SpecNaming.java   |   1 +
 6 files changed, 372 insertions(+), 310 deletions(-)

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
index 41a5bdd..22e3908 100644
--- a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
@@ -326,14 +326,9 @@ public class CodeGenerator {
 	}
 
 	static public void main(String[] args) {
-//		String[] dirNames = { 
-//				Environment.REGISTER, 
-//				Environment.MS_QUEUE,
-//				Environment.LINUXRWLOCKS,
-//				Environment.MCS_LOCK,
-//				Environment.DEQUE, 
-//				Environment.TREIBER_STACK };
+	
 		String[] dirNames = args;
+//		String[] dirNames = Environment.Benchmarks;
 
 		for (int i = 0; i < dirNames.length; i++) {
 			String dirName = dirNames[i];
diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 73176b9..694695c 100644
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -140,8 +140,12 @@ public class CodeGeneratorUtils {
 		code.addLine("*/");
 		code.addLine("");
 
-		code.addLine("#ifndef _" + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-', '_') + "_H");
-		code.addLine("#define _" + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-', '_') + "_H");
+		code.addLine("#ifndef _"
+				+ SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
+						'_') + "_H");
+		code.addLine("#define _"
+				+ SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
+						'_') + "_H");
 		code.addLine("");
 
 		// FIXME: We have included ad-hoc header files here
@@ -166,9 +170,6 @@ public class CodeGeneratorUtils {
 		code.addLine("");
 
 		code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
-		code.addLine(ShortComment("A special empty string"));
-		code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.EmptyCString));
-		code.addLine("");
 
 		// Interface name strings
 		code.addLine(ShortComment("Interface name strings"));
@@ -176,70 +177,34 @@ public class CodeGeneratorUtils {
 			ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
 			for (InterfaceConstruct construct : list) {
 				String name = construct.getName();
-				code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(name)));
+				code.addLine(Declare("extern " + SpecNaming.CString,
+						SpecNaming.AppendStr(name)));
 			}
 		}
 		code.addLine("");
 
-		// Commutativity rule strings
-		code.addLine(ShortComment("Commutativity rule strings"));
-		for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-			code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.Commutativity + i)));
-		}
-		code.addLine("");
-
 		// Ordering points label strings
 		code.addLine(ShortComment("Ordering points label strings"));
 		for (String label : OPLabelSet) {
-			code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(label)));
+			code.addLine(Declare("extern " + SpecNaming.CString,
+					SpecNaming.AppendStr(label)));
 		}
 		code.addLine("");
 
-		// Special function name strings
-		code.addLine(ShortComment("Special function name strings"));
-		code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.InitalState)));
-		code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.CopyState)));
-		code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.FinalState)));
-		code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.PrintState)));
-		code.addLine("");
-
-		// Interface name strings
-		for (File file : interfaceListMap.keySet()) {
-			ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
-			for (InterfaceConstruct construct : list) {
-				String name = construct.getName();
-				code.addLine(ShortComment(name + " function strings"));
-				// Transition
-				String tmpFunc = name + "_" + SpecNaming.Transition;
-				code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-				// PreCondition
-				tmpFunc = name + "_" + SpecNaming.PreCondition;
-				code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-				// SideEffect
-				tmpFunc = name + "_" + SpecNaming.SideEffect;
-				code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-				// PostCondition
-				tmpFunc = name + "_" + SpecNaming.PostCondition;
-				code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-				// Print
-				tmpFunc = name + "_" + SpecNaming.PrintValue;
-				code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-				code.addLine("");
-			}
-		}
-
 		// Declare customized value struct
 		for (File file : interfaceListMap.keySet()) {
 			ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
 			for (InterfaceConstruct construct : list) {
 				// Declare custom value struct for the interface
 				String name = construct.getName();
-				code.addLine(ShortComment("Declare custom value struct for " + name));
+				code.addLine(ShortComment("Declare custom value struct for "
+						+ name));
 				code.addLine("typedef struct " + name + " {");
 				FunctionHeader funcHeader = construct.getFunctionHeader();
 				// RET
 				if (!funcHeader.returnType.equals("void"))
-					code.addLine(TabbedLine(Declare(funcHeader.returnType, SpecNaming.RET)));
+					code.addLine(TabbedLine(Declare(funcHeader.returnType,
+							SpecNaming.RET)));
 				// Arguments
 				for (VariableDeclaration decl : funcHeader.args) {
 					code.addLine(TabbedLine(Declare(decl)));
@@ -249,75 +214,6 @@ public class CodeGeneratorUtils {
 			}
 		}
 
-		// Declare @Initial
-		code.addLine(ShortComment("Declare @" + SpecNaming.InitalState));
-		code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "(" + SpecNaming.Method + " "
-				+ SpecNaming.Method1 + ");");
-		code.addLine("");
-		// Declare @Copy
-		code.addLine(ShortComment("Declare @" + SpecNaming.CopyState));
-		code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "(" + SpecNaming.Method + " " + "dest, "
-				+ SpecNaming.Method + " src);");
-		code.addLine("");
-		// Declare @Print
-		code.addLine(ShortComment("Declare @" + SpecNaming.PrintState));
-		if (!globalConstruct.printState.isEmpty()) {
-			code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "(" + SpecNaming.Method + " "
-					+ SpecNaming.Method1 + ");");
-			code.addLine("");
-		}
-
-		// Declare @Commutativity
-		code.addLine(ShortComment("Declare commutativity checking functions"));
-		for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-			code.addLine("bool _check" + SpecNaming.Commutativity + i + "(" + SpecNaming.Method + " m1, "
-					+ SpecNaming.Method + " m2);");
-		}
-		code.addLine("");
-
-		// Declare customized interface functions
-		for (File file : interfaceListMap.keySet()) {
-			ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
-			for (InterfaceConstruct construct : list) {
-				// Declare interface functions
-				String name = construct.getName();
-				code.addLine("/**********    " + name + " functions    **********/");
-				// Declare @Transition for INTERFACE
-				code.addLine(ShortComment("Declare @" + SpecNaming.Transition + " for " + name));
-				code.addLine("void _" + name + "_" + SpecNaming.Transition + "(" + SpecNaming.Method + " "
-						+ SpecNaming.Method1 + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ");");
-				code.addLine("");
-				// Declare @PreCondition
-				if (!construct.preCondition.isEmpty()) {
-					code.addLine(ShortComment("Declare @" + SpecNaming.PreCondition + " for " + name));
-					code.addLine("bool _" + name + "_" + SpecNaming.PreCondition + "(" + SpecNaming.Method + " "
-							+ SpecNaming.Method1 + ");");
-					code.addLine("");
-				}
-				// Declare @SideEffect
-				if (!construct.sideEffect.isEmpty()) {
-					code.addLine(ShortComment("Declare @" + SpecNaming.SideEffect + " for " + name));
-					code.addLine("void _" + name + "_" + SpecNaming.SideEffect + "(" + SpecNaming.Method + " "
-							+ SpecNaming.Method1 + ");");
-					code.addLine("");
-				}
-				// Declare @PostCondition
-				if (!construct.postCondition.isEmpty()) {
-					code.addLine(ShortComment("Declare @" + SpecNaming.PostCondition + " for " + name));
-					code.addLine("bool _" + name + "_" + SpecNaming.PostCondition + "(" + SpecNaming.Method + " "
-							+ SpecNaming.Method1 + ");");
-					code.addLine("");
-				}
-				// Declare @Print
-				if (!construct.print.isEmpty()) {
-					code.addLine(ShortComment("Declare @" + SpecNaming.PrintValue + " for " + name));
-					code.addLine("void _" + name + "_" + SpecNaming.PrintValue + "(" + SpecNaming.Method + " "
-							+ SpecNaming.Method1 + ");");
-					code.addLine("");
-				}
-			}
-		}
-
 		// Declare INIT annotation instrumentation function
 		code.addLine(ShortComment("Declare INIT annotation instrumentation function"));
 		code.addLine("void _createInitAnnotation();");
@@ -377,14 +273,31 @@ public class CodeGeneratorUtils {
 			code.addLine(TabbedLine(Declare(decl)));
 		}
 		code.addLine("");
+		// Define state destructor
+		code.addLine(TabbedLine(ShortComment("Define state destructor")));
+		code.addLine(TabbedLine("~" + SpecNaming.StateStruct + "() {"));
+		if (!globalConstruct.autoGenClear) {
+			code.addLine(TabbedLine(
+					ShortComment("Execute user-defined state clear code"), 2));
+		} else {
+			code.addLine(TabbedLine(
+					ShortComment("Execute auto-generated state clear code"), 2));
+		}
+		globalConstruct.clearState.align(2);
+		code.addLines(globalConstruct.clearState);
+		code.addLine(TabbedLine("}"));
+		code.addLine("");
+
 		code.addLine(TabbedLine("SNAPSHOTALLOC"));
+		code.addLine("");
 		code.addLine("} " + SpecNaming.StateStruct + ";");
 		code.addLine("");
 		code.addLine("");
 
 		code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
 		code.addLine(ShortComment("A special empty string"));
-		code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString, "\"\""));
+		code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,
+				"\"\""));
 		code.addLine("");
 
 		// Interface name strings
@@ -393,7 +306,8 @@ public class CodeGeneratorUtils {
 			ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
 			for (InterfaceConstruct construct : list) {
 				String name = construct.getName();
-				code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(name), Quote(name)));
+				code.addLine(DeclareDefine(SpecNaming.CString,
+						SpecNaming.AppendStr(name), Quote(name)));
 			}
 		}
 		code.addLine("");
@@ -401,8 +315,10 @@ public class CodeGeneratorUtils {
 		// Commutativity rule strings
 		code.addLine(ShortComment("Commutativity rule strings"));
 		for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-			CommutativityRule rule = globalConstruct.commutativityRules.get(i - 1);
-			code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.Commutativity + i),
+			CommutativityRule rule = globalConstruct.commutativityRules
+					.get(i - 1);
+			code.addLine(DeclareDefine(SpecNaming.CString,
+					SpecNaming.AppendStr(SpecNaming.Commutativity + i),
 					Quote(rule.toString())));
 		}
 		code.addLine("");
@@ -410,20 +326,28 @@ public class CodeGeneratorUtils {
 		// Ordering points label strings
 		code.addLine(ShortComment("Ordering points label strings"));
 		for (String label : OPLabelSet) {
-			code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(label), Quote(label)));
+			code.addLine(DeclareDefine(SpecNaming.CString,
+					SpecNaming.AppendStr(label), Quote(label)));
 		}
 		code.addLine("");
 
 		// Special function name strings
 		code.addLine(ShortComment("Special function name strings"));
-		code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.InitalState),
-				Quote("_" + SpecNaming.InitalState.toLowerCase())));
-		code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.CopyState),
-				Quote("_" + SpecNaming.CopyState.toLowerCase())));
-		code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.FinalState),
-				Quote("_" + SpecNaming.FinalState.toLowerCase())));
-		code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.PrintState),
-				Quote("_" + SpecNaming.PrintState.toLowerCase())));
+		code.addLine(DeclareDefine(SpecNaming.CString,
+				SpecNaming.AppendStr(SpecNaming.InitalState), Quote("_"
+						+ SpecNaming.InitalState.toLowerCase())));
+		code.addLine(DeclareDefine(SpecNaming.CString,
+				SpecNaming.AppendStr(SpecNaming.CopyState), Quote("_"
+						+ SpecNaming.CopyState.toLowerCase())));
+		code.addLine(DeclareDefine(SpecNaming.CString,
+				SpecNaming.AppendStr(SpecNaming.ClearState), Quote("_"
+						+ SpecNaming.ClearState.toLowerCase())));
+		code.addLine(DeclareDefine(SpecNaming.CString,
+				SpecNaming.AppendStr(SpecNaming.FinalState), Quote("_"
+						+ SpecNaming.FinalState.toLowerCase())));
+		code.addLine(DeclareDefine(SpecNaming.CString,
+				SpecNaming.AppendStr(SpecNaming.PrintState), Quote("_"
+						+ SpecNaming.PrintState.toLowerCase())));
 		code.addLine("");
 
 		// Interface name strings
@@ -434,52 +358,49 @@ public class CodeGeneratorUtils {
 				code.addLine(ShortComment(name + " function strings"));
 				// Transition
 				String tmpFunc = name + "_" + SpecNaming.Transition;
-				code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+				code.addLine(DeclareDefine(SpecNaming.CString,
+						SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
 				// PreCondition
 				tmpFunc = name + "_" + SpecNaming.PreCondition;
 				if (!construct.preCondition.isEmpty())
-					code.addLine(
-							DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+					code.addLine(DeclareDefine(SpecNaming.CString,
+							SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
 				else
-					code.addLine(
-							DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
-				// SideEffect
-				tmpFunc = name + "_" + SpecNaming.SideEffect;
-				if (!construct.sideEffect.isEmpty())
-					code.addLine(
-							DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
-				else
-					code.addLine(
-							DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
+					code.addLine(DeclareDefine(SpecNaming.CString,
+							SpecNaming.AppendStr(tmpFunc),
+							SpecNaming.EmptyCString));
 				// PostCondition
 				tmpFunc = name + "_" + SpecNaming.PostCondition;
 				if (!construct.postCondition.isEmpty())
-					code.addLine(
-							DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+					code.addLine(DeclareDefine(SpecNaming.CString,
+							SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
 				else
-					code.addLine(
-							DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
+					code.addLine(DeclareDefine(SpecNaming.CString,
+							SpecNaming.AppendStr(tmpFunc),
+							SpecNaming.EmptyCString));
 				// Print
 				tmpFunc = name + "_" + SpecNaming.PrintValue;
 				if (!construct.print.isEmpty())
-					code.addLine(
-							DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+					code.addLine(DeclareDefine(SpecNaming.CString,
+							SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
 				else
-					code.addLine(
-							DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
+					code.addLine(DeclareDefine(SpecNaming.CString,
+							SpecNaming.AppendStr(tmpFunc),
+							SpecNaming.EmptyCString));
 				code.addLine("");
 			}
 		}
 
 		// Define @Initial
 		code.addLine(ShortComment("Define @" + SpecNaming.InitalState));
-		code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "(" + SpecNaming.Method + " "
-				+ SpecNaming.Method1 + ") {");
-		code.addLine(TabbedLine(
-				DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
+		code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
+				+ SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
+		code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+				+ SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
 		// Define macros
 		for (VariableDeclaration decl : globalConstruct.declState) {
-			code.addLine(TabbedLine("#define " + decl.name + " " + SpecNaming.StateInst + "->" + decl.name));
+			code.addLine(TabbedLine("#define " + decl.name + " "
+					+ SpecNaming.StateInst + "->" + decl.name));
 		}
 		if (!globalConstruct.autoGenInitial)
 			code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
@@ -494,20 +415,23 @@ public class CodeGeneratorUtils {
 			code.addLine(TabbedLine("#undef " + decl.name));
 		}
 		code.addLine("");
-		code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1, SpecNaming.StateInst, SpecNaming.StateInst)));
+		code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1,
+				SpecNaming.StateInst, SpecNaming.StateInst)));
 		code.addLine("}");
 		code.addLine("");
 
 		// Define @Copy
 		code.addLine(ShortComment("Define @" + SpecNaming.CopyState));
-		code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "(" + SpecNaming.Method + " " + "dest, "
-				+ SpecNaming.Method + " src) {");
+		code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
+				+ SpecNaming.Method + " " + "dest, " + SpecNaming.Method
+				+ " src) {");
 		// StateStruct *OLD = (StateStruct*) src->state;
-		code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.OldStateInst,
-				Brace(SpecNaming.StateStruct + "*") + " src->" + SpecNaming.StateInst)));
+		code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+				+ SpecNaming.OldStateInst, Brace(SpecNaming.StateStruct + "*")
+				+ " src->" + SpecNaming.StateInst)));
 		// StateStruct *NEW = new StateStruct;
-		code.addLine(TabbedLine(
-				DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
+		code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+				+ SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
 		if (!globalConstruct.autoGenCopy)
 			code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
 		else
@@ -516,19 +440,35 @@ public class CodeGeneratorUtils {
 		globalConstruct.copyState.align(1);
 		code.addLines(globalConstruct.copyState);
 		code.addLine("");
-		code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst, SpecNaming.NewStateInst)));
+		code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst,
+				SpecNaming.NewStateInst)));
+		code.addLine("}");
+		code.addLine("");
+
+		// Define @Clear
+		code.addLine(ShortComment("Define @" + SpecNaming.ClearState));
+		code.addLine("void _" + SpecNaming.ClearState.toLowerCase() + "("
+				+ SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
+		// Retrieve the state
+		code.addLine(TabbedLine(ShortComment("Retrieve the state")));
+		code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+				+ SpecNaming.StateInst, "(" + SpecNaming.StateStruct + "*) "
+				+ SpecNaming.Method1 + "->state")));
+		// Explicitly call the state destructor
+		code.addLine(TabbedLine(ShortComment("Explicitly call the state destructor")));
+		code.addLine(TabbedLine("delete " + SpecNaming.StateInst + ";"));
 		code.addLine("}");
 		code.addLine("");
 
 		// Define @Print
 		if (!globalConstruct.printState.isEmpty()) {
 			code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
-			code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "(" + SpecNaming.Method + " "
-					+ SpecNaming.Method1 + ") {");
+			code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
+					+ SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
 
 			// Initialize state struct fields
-			Code fieldsInit = GenerateStateFieldsInitialization(SpecNaming.Method1, SpecNaming.StateInst,
-					globalConstruct);
+			Code fieldsInit = GenerateStateFieldsInitialization(
+					SpecNaming.Method1, SpecNaming.StateInst, globalConstruct);
 			fieldsInit.align(1);
 			code.addLines(fieldsInit);
 			code.addLine("");
@@ -548,16 +488,23 @@ public class CodeGeneratorUtils {
 		// Define @Commutativity
 		code.addLine(ShortComment("Define commutativity checking functions"));
 		for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-			CommutativityRule rule = globalConstruct.commutativityRules.get(i - 1);
-			code.addLine("bool _check" + SpecNaming.Commutativity + i + "(" + SpecNaming.Method + " m1, "
-					+ SpecNaming.Method + " m2) {");
+			CommutativityRule rule = globalConstruct.commutativityRules
+					.get(i - 1);
+			code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
+					+ SpecNaming.Method + " m1, " + SpecNaming.Method
+					+ " m2) {");
 			// if (m1->name == _ENQ_str && m2->name == _DEQ_str) {
-			code.addLine(TabbedLine("if (m1->name == " + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
+			code.addLine(TabbedLine("if (m1->name == "
+					+ SpecNaming.AppendStr(rule.method1) + " && m2->name == "
 					+ SpecNaming.AppendStr(rule.method2) + ") {"));
 			// Initialize M1 & M2 in commutativity rule
 			// e.g. ENQ *M1 = (ENQ*) m1->value;
-			code.addLine(TabbedLine(DeclareDefine(rule.method1, "*M1", "(" + rule.method1 + "*) m1->value"), 2));
-			code.addLine(TabbedLine(DeclareDefine(rule.method2, "*M2", "(" + rule.method2 + "*) m2->value"), 2));
+			code.addLine(TabbedLine(
+					DeclareDefine(rule.method1, "*M1", "(" + rule.method1
+							+ "*) m1->value"), 2));
+			code.addLine(TabbedLine(
+					DeclareDefine(rule.method2, "*M2", "(" + rule.method2
+							+ "*) m2->value"), 2));
 			code.addLine(TabbedLine("return " + rule.condition + ";", 2));
 			code.addLine(TabbedLine("}"));
 			code.addLine(TabbedLine("return false;"));
@@ -574,14 +521,20 @@ public class CodeGeneratorUtils {
 
 				// Define interface functions
 				String name = construct.getName();
-				code.addLine("/**********    " + name + " functions    **********/");
+				code.addLine("/**********    " + name
+						+ " functions    **********/");
 				// Define @Transition for INTERFACE
-				code.addLine(ShortComment("Define @" + SpecNaming.Transition + " for " + name));
-				code.addLine("void _" + name + "_" + SpecNaming.Transition + "(" + SpecNaming.Method + " "
-						+ SpecNaming.Method1 + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ") {");
+				code.addLine(ShortComment("Define @" + SpecNaming.Transition
+						+ " for " + name));
+				code.addLine("void _" + name + "_" + SpecNaming.Transition
+						+ "(" + SpecNaming.Method + " " + SpecNaming.Method1
+						+ ", " + SpecNaming.Method + " " + SpecNaming.Method2
+						+ ") {");
 
 				// Initialize value struct fields
-				fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method2, SpecNaming.InterfaceValueInst, construct);
+				fieldsInit = GenerateInterfaceFieldsInitialization(
+						SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+						construct);
 				fieldsInit.align(1);
 				code.addLines(fieldsInit);
 
@@ -594,12 +547,16 @@ public class CodeGeneratorUtils {
 
 				// Define @PreCondition
 				if (!construct.preCondition.isEmpty()) {
-					code.addLine(ShortComment("Define @" + SpecNaming.PreCondition + " for " + name));
-					code.addLine("bool _" + name + "_" + SpecNaming.PreCondition + "(" + SpecNaming.Method + " "
-							+ SpecNaming.Method1 + ") {");
+					code.addLine(ShortComment("Define @"
+							+ SpecNaming.PreCondition + " for " + name));
+					code.addLine("bool _" + name + "_"
+							+ SpecNaming.PreCondition + "(" + SpecNaming.Method
+							+ " " + SpecNaming.Method1 + ") {");
 
 					// Initialize value struct fields
-					fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
+					fieldsInit = GenerateInterfaceFieldsInitialization(
+							SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+							construct);
 					fieldsInit.align(1);
 					code.addLines(fieldsInit);
 
@@ -611,32 +568,19 @@ public class CodeGeneratorUtils {
 					code.addLine("");
 
 				}
-				// Define @SideEffect
-				if (!construct.sideEffect.isEmpty()) {
-					code.addLine(ShortComment("Define @" + SpecNaming.SideEffect + " for " + name));
-					code.addLine("void _" + name + "_" + SpecNaming.SideEffect + "(" + SpecNaming.Method + " "
-							+ SpecNaming.Method1 + ") {");
-
-					// Initialize value struct fields
-					fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
-					fieldsInit.align(1);
-					code.addLines(fieldsInit);
-
-					construct.sideEffect.align(1);
-					code.addLine(TabbedLine(ShortComment("Execute SideEffect")));
-					code.addLines(construct.sideEffect);
-
-					code.addLine("}");
-					code.addLine("");
-				}
 				// Define @PostCondition
 				if (!construct.postCondition.isEmpty()) {
-					code.addLine(ShortComment("Define @" + SpecNaming.PostCondition + " for " + name));
-					code.addLine("bool _" + name + "_" + SpecNaming.PostCondition + "(" + SpecNaming.Method + " "
-							+ SpecNaming.Method1 + ") {");
+					code.addLine(ShortComment("Define @"
+							+ SpecNaming.PostCondition + " for " + name));
+					code.addLine("bool _" + name + "_"
+							+ SpecNaming.PostCondition + "("
+							+ SpecNaming.Method + " " + SpecNaming.Method1
+							+ ") {");
 
 					// Initialize value struct fields
-					fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
+					fieldsInit = GenerateInterfaceFieldsInitialization(
+							SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+							construct);
 					fieldsInit.align(1);
 					code.addLines(fieldsInit);
 
@@ -649,11 +593,15 @@ public class CodeGeneratorUtils {
 				}
 				// Define @Print
 				if (!construct.print.isEmpty()) {
-					code.addLine(ShortComment("Define @" + SpecNaming.PrintValue + " for " + name));
-					code.addLine("void _" + name + "_" + SpecNaming.PrintValue + "(" + SpecNaming.Method + " "
+					code.addLine(ShortComment("Define @"
+							+ SpecNaming.PrintValue + " for " + name));
+					code.addLine("void _" + name + "_" + SpecNaming.PrintValue
+							+ "(" + SpecNaming.Method + " "
 							+ SpecNaming.Method1 + ") {");
 					// Initialize value struct fields
-					fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
+					fieldsInit = GenerateInterfaceFieldsInitialization(
+							SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+							construct);
 					fieldsInit.align(1);
 					code.addLines(fieldsInit);
 
@@ -677,35 +625,46 @@ public class CodeGeneratorUtils {
 
 		// Init commutativity rules
 		code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
-		code.addLine(TabbedLine(DeclareDefine("int", SpecNaming.CommutativityRuleSizeInst,
+		code.addLine(TabbedLine(DeclareDefine("int",
+				SpecNaming.CommutativityRuleSizeInst,
 				Integer.toString(globalConstruct.commutativityRules.size()))));
-		String tmp = SpecNaming.NewSize + Brace(SpecNaming.CommutativityRule + ", sizeof"
-				+ Brace(SpecNaming.CommutativityRule) + " * " + SpecNaming.CommutativityRuleSizeInst);
-		code.addLine(
-				TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*" + SpecNaming.CommutativityRuleInst, tmp)));
+		String tmp = SpecNaming.NewSize
+				+ Brace(SpecNaming.CommutativityRule + ", sizeof"
+						+ Brace(SpecNaming.CommutativityRule) + " * "
+						+ SpecNaming.CommutativityRuleSizeInst);
+		code.addLine(TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*"
+				+ SpecNaming.CommutativityRuleInst, tmp)));
 		for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-			CommutativityRule rule = globalConstruct.commutativityRules.get(i - 1);
-			code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ") + i));
+			CommutativityRule rule = globalConstruct.commutativityRules
+					.get(i - 1);
+			code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ")
+					+ i));
 			// new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
 			// _Commutativity1_str, _checkCommutativity1)
-			line = "new" + Brace(" &" + SpecNaming.CommutativityRuleInst + "[" + (i - 1) + "] ")
-					+ SpecNaming.CommutativityRule + "(" + SpecNaming.AppendStr(rule.method1) + ", "
-					+ SpecNaming.AppendStr(rule.method2) + ", " + SpecNaming.AppendStr(SpecNaming.Commutativity + i)
-					+ ", " + "_check" + SpecNaming.Commutativity + i + ");";
+			line = "new"
+					+ Brace(" &" + SpecNaming.CommutativityRuleInst + "["
+							+ (i - 1) + "] ") + SpecNaming.CommutativityRule
+					+ "(" + SpecNaming.AppendStr(rule.method1) + ", "
+					+ SpecNaming.AppendStr(rule.method2) + ", "
+					+ SpecNaming.AppendStr(SpecNaming.Commutativity + i) + ", "
+					+ "_check" + SpecNaming.Commutativity + i + ");";
 			code.addLine(TabbedLine(line));
 		}
 
 		// Initialize AnnoInit
 		code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
 		// AnnoInit *init = new AnnoInit(
-		code.addLine(TabbedLine(
-				SpecNaming.AnnoInit + " *" + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit + "("));
+		code.addLine(TabbedLine(SpecNaming.AnnoInit + " *"
+				+ SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit
+				+ "("));
 		// new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
-		code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.InitalState)
-				+ ", " + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
+		code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+				+ SpecNaming.AppendStr(SpecNaming.InitalState) + ", "
+				+ SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
 				+ SpecNaming.InitalState.toLowerCase() + "),", 2));
 		// new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
-		line = "new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
+		line = "new " + SpecNaming.NamedFunction + "("
+				+ SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
 				+ SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
 		if (globalConstruct.finalState.isEmpty()) {
 			line = line + SpecNaming.NullFunc + "),";
@@ -714,26 +673,29 @@ public class CodeGeneratorUtils {
 		}
 		code.addLine(TabbedLine(line, 2));
 		// new NamedFunction(_Copy_str, COPY, (void*) _copy),
-		code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.CopyState)
-				+ ", " + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _" + SpecNaming.CopyState.toLowerCase()
-				+ "),", 2));
+		code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+				+ SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
+				+ SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
+				+ SpecNaming.CopyState.toLowerCase() + "),", 2));
+		// new NamedFunction(_Clear_str, CLEAR, (void*) _clear),
+		code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+				+ SpecNaming.AppendStr(SpecNaming.ClearState) + ", "
+				+ SpecNaming.ClearState.toUpperCase() + ", " + "(void*) _"
+				+ SpecNaming.ClearState.toLowerCase() + "),", 2));
 		// new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
-		line = "new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
-				+ SpecNaming.PrintStateType + ", " + "(void*)";
-		if (globalConstruct.printState.isEmpty()) {
-			line = line + SpecNaming.NullFunc + "),";
-		} else {
-			line = line + "_" + SpecNaming.PrintState.toLowerCase() + "),";
-		}
-		code.addLine(TabbedLine(line, 2));
+		code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+				+ SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
+				+ SpecNaming.PrintStateType + ", " + "(void*) _"
+				+ SpecNaming.PrintState.toLowerCase() + "),", 2));
 		// commuteRules, CommuteRuleSize);
-		code.addLine(
-				TabbedLine(SpecNaming.CommutativityRuleInst + ", " + SpecNaming.CommutativityRuleSizeInst + ");", 2));
+		code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
+				+ SpecNaming.CommutativityRuleSizeInst + ");", 2));
 		code.addLine("");
 
 		// Declare StateFunctions map
 		code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
-		code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*" + SpecNaming.StateFunctionsInst)));
+		code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*"
+				+ SpecNaming.StateFunctionsInst)));
 		code.addLine("");
 
 		// StateFunction for interface
@@ -741,62 +703,72 @@ public class CodeGeneratorUtils {
 			ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
 			for (InterfaceConstruct construct : list) {
 				String name = construct.getName();
-				code.addLine(TabbedLine(ShortComment("StateFunction for " + name)));
+				code.addLine(TabbedLine(ShortComment("StateFunction for "
+						+ name)));
 				// stateFuncs = new StateFunctions(
-				code.addLine(TabbedLine(SpecNaming.StateFunctionsInst + " = new " + SpecNaming.StateFunctions + "("));
+				code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
+						+ " = new " + SpecNaming.StateFunctions + "("));
 				// new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
 				// _ENQ_Transition),
 				// Transition
 				code.addLine(TabbedLine(
-						"new " + SpecNaming.NamedFunction + "("
-								+ SpecNaming.AppendStr(name + "_" + SpecNaming.Transition) + ", "
-								+ SpecNaming.TransitionType + ", (void*) _" + name + "_" + SpecNaming.Transition + "),",
-						2));
+						"new "
+								+ SpecNaming.NamedFunction
+								+ "("
+								+ SpecNaming.AppendStr(name + "_"
+										+ SpecNaming.Transition) + ", "
+								+ SpecNaming.TransitionType + ", (void*) _"
+								+ name + "_" + SpecNaming.Transition + "),", 2));
 				// PreCondition
-				line = "new " + SpecNaming.NamedFunction + "("
-						+ SpecNaming.AppendStr(name + "_" + SpecNaming.PreCondition) + ", "
+				line = "new "
+						+ SpecNaming.NamedFunction
+						+ "("
+						+ SpecNaming.AppendStr(name + "_"
+								+ SpecNaming.PreCondition) + ", "
 						+ SpecNaming.PreConditionType + ", (void*) ";
 				if (construct.preCondition.isEmpty()) {
 					line = line + SpecNaming.NullFunc + "),";
 				} else {
-					line = line + "_" + name + "_" + SpecNaming.PreCondition + "),";
-				}
-				code.addLine(TabbedLine(line, 2));
-				// SideEffect
-				line = "new " + SpecNaming.NamedFunction + "("
-						+ SpecNaming.AppendStr(name + "_" + SpecNaming.SideEffect) + ", " + SpecNaming.SideEffectType
-						+ ", (void*) ";
-				if (construct.sideEffect.isEmpty()) {
-					line = line + SpecNaming.NullFunc + "),";
-				} else {
-					line = line + "_" + name + "_" + SpecNaming.SideEffect + "),";
+					line = line + "_" + name + "_" + SpecNaming.PreCondition
+							+ "),";
 				}
 				code.addLine(TabbedLine(line, 2));
 				// PostCondition
-				line = "new " + SpecNaming.NamedFunction + "("
-						+ SpecNaming.AppendStr(name + "_" + SpecNaming.PostCondition) + ", "
+				line = "new "
+						+ SpecNaming.NamedFunction
+						+ "("
+						+ SpecNaming.AppendStr(name + "_"
+								+ SpecNaming.PostCondition) + ", "
 						+ SpecNaming.PostConditionType + ", (void*) ";
 				if (construct.postCondition.isEmpty()) {
 					line = line + SpecNaming.NullFunc + "),";
 				} else {
-					line = line + "_" + name + "_" + SpecNaming.PostCondition + "),";
+					line = line + "_" + name + "_" + SpecNaming.PostCondition
+							+ "),";
 				}
 				code.addLine(TabbedLine(line, 2));
 				// Print (PrintValue
-				line = "new " + SpecNaming.NamedFunction + "("
-						+ SpecNaming.AppendStr(name + "_" + SpecNaming.PrintValue) + ", " + SpecNaming.PrintValueType
-						+ ", (void*) ";
+				line = "new "
+						+ SpecNaming.NamedFunction
+						+ "("
+						+ SpecNaming.AppendStr(name + "_"
+								+ SpecNaming.PrintValue) + ", "
+						+ SpecNaming.PrintValueType + ", (void*) ";
 				if (construct.print.isEmpty()) {
 					line = line + SpecNaming.NullFunc + ")";
 				} else {
-					line = line + "_" + name + "_" + SpecNaming.PrintValue + ")";
+					line = line + "_" + name + "_" + SpecNaming.PrintValue
+							+ ")";
 				}
 				code.addLine(TabbedLine(line, 2));
 				code.addLine(TabbedLine(");"));
 
 				// init->addInterfaceFunctions(_ENQ_str, stateFuncs);
-				code.addLine(TabbedLine(SpecNaming.AnnoInitInst + "->" + SpecNaming.AddInterfaceFunctions
-						+ Brace(SpecNaming.AppendStr(name) + ", " + SpecNaming.StateFunctionsInst) + ";"));
+				code.addLine(TabbedLine(SpecNaming.AnnoInitInst
+						+ "->"
+						+ SpecNaming.AddInterfaceFunctions
+						+ Brace(SpecNaming.AppendStr(name) + ", "
+								+ SpecNaming.StateFunctionsInst) + ";"));
 				code.addLine("");
 			}
 		}
@@ -804,8 +776,12 @@ public class CodeGeneratorUtils {
 		// Create and instrument with the INIT annotation
 		code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
 		// cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
-		code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc + Brace(SpecNaming.SPEC_ANALYSIS + ", new "
-				+ SpecNaming.SpecAnnotation + Brace(SpecNaming.AnnoTypeInit + ", " + SpecNaming.AnnoInitInst)) + ";"));
+		code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc
+				+ Brace(SpecNaming.SPEC_ANALYSIS
+						+ ", new "
+						+ SpecNaming.SpecAnnotation
+						+ Brace(SpecNaming.AnnoTypeInit + ", "
+								+ SpecNaming.AnnoInitInst)) + ";"));
 
 		code.addLine("}");
 		code.addLine("");
@@ -839,13 +815,16 @@ public class CodeGeneratorUtils {
 	 *            The global state construct
 	 * @return The generated code
 	 */
-	public static Code GenerateStateFieldsInitialization(String methodInst, String inst, GlobalConstruct construct) {
+	public static Code GenerateStateFieldsInitialization(String methodInst,
+			String inst, GlobalConstruct construct) {
 		Code res = new Code();
-		res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct + " fields"));
-		res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst,
-				"(" + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
+		res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct
+				+ " fields"));
+		res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst, "("
+				+ SpecNaming.StateStruct + "*) " + methodInst + "->state"));
 		for (VariableDeclaration decl : construct.declState) {
-			res.addLine(DeclareDefine(decl.type, decl.name, inst + "->" + decl.name));
+			res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
+					+ decl.name));
 		}
 		return res;
 	}
@@ -876,21 +855,23 @@ public class CodeGeneratorUtils {
 	 *            The corresponding interface construct
 	 * @return The generated code
 	 */
-	public static Code GenerateInterfaceFieldsInitialization(String methodInst, String inst,
-			InterfaceConstruct construct) {
+	public static Code GenerateInterfaceFieldsInitialization(String methodInst,
+			String inst, InterfaceConstruct construct) {
 		Code res = new Code();
 		String name = construct.getName();
 		res.addLine(ShortComment("Initialize fields for " + name));
 		// The very first assignment "
-		res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) " + methodInst + "->" + SpecNaming.MethodValueField));
+		res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) "
+				+ methodInst + "->" + SpecNaming.MethodValueField));
 		// Don't leave out the RET field
 		if (!construct.getFunctionHeader().isReturnVoid()) {
-			res.addLine(DeclareDefine(construct.getFunctionHeader().returnType, SpecNaming.RET,
-					inst + "->" + SpecNaming.RET));
+			res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
+					SpecNaming.RET, inst + "->" + SpecNaming.RET));
 		}
 		// For arguments
 		for (VariableDeclaration decl : construct.getFunctionHeader().args) {
-			res.addLine(DeclareDefine(decl.type, decl.name, inst + "->" + decl.name));
+			res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
+					+ decl.name));
 		}
 		return res;
 	}
@@ -920,16 +901,19 @@ public class CodeGeneratorUtils {
 			code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
 			break;
 		case PotentialOP:
-			code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc + "(" + SpecNaming.AppendStr(label) + ");");
+			code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
+					+ "(" + SpecNaming.AppendStr(label) + ");");
 			break;
 		case OPCheck:
-			code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "(" + SpecNaming.AppendStr(label) + ");");
+			code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "("
+					+ SpecNaming.AppendStr(label) + ");");
 			break;
 		case OPClear:
 			code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();");
 			break;
 		case OPClearDefine:
-			code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc + "();");
+			code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
+					+ "();");
 			break;
 		default:
 			break;
@@ -998,7 +982,8 @@ public class CodeGeneratorUtils {
 
 		// Add one line to separate
 		code.addLine("");
-		code.addLine(prefixTabs + ShortComment("Generated wrapper interface for " + name));
+		code.addLine(prefixTabs
+				+ ShortComment("Generated wrapper interface for " + name));
 		if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
 											// of the line
 			code.addLine(beginLine + " {");
@@ -1006,34 +991,56 @@ public class CodeGeneratorUtils {
 			code.addLine(beginLine);
 		}
 		// Instrument with the INTERFACE_BEGIN annotations
-		code.addLine(prefixTabs + "\t" + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
+		code.addLine(prefixTabs
+				+ "\t"
+				+ ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
 		// CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
-		code.addLine(
-				prefixTabs + "\t" + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*" + SpecNaming.AnnoInterfaceInfoInst,
-						SpecNaming.CreateInterfaceBeginAnnoFunc + Brace(SpecNaming.AppendStr(name))));
+		code.addLine(prefixTabs
+				+ "\t"
+				+ DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
+						+ SpecNaming.AnnoInterfaceInfoInst,
+						SpecNaming.CreateInterfaceBeginAnnoFunc
+								+ Brace(SpecNaming.AppendStr(name))));
 		// Call the actual function
-		code.addLine(prefixTabs + "\t" + ShortComment("Call the actual function"));
+		code.addLine(prefixTabs + "\t"
+				+ ShortComment("Call the actual function"));
 		// bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
-		code.addLine(prefixTabs + "\t" + construct.getFunctionHeader().getRenamedCall() + ";");
+		code.addLine(prefixTabs + "\t"
+				+ construct.getFunctionHeader().getRenamedCall() + ";");
 		code.addLine("");
 
 		// Initialize the value struct
-		code.addLine(prefixTabs + "\t" + ShortComment("Initialize the value struct"));
+		code.addLine(prefixTabs + "\t"
+				+ ShortComment("Initialize the value struct"));
 		// The very first assignment "
-		code.addLine(prefixTabs + "\t" + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst, SpecNaming.New + Brace(name)));
+		code.addLine(prefixTabs
+				+ "\t"
+				+ DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst,
+						SpecNaming.New + Brace(name)));
 		// Don't leave out the RET field
 		if (!construct.getFunctionHeader().isReturnVoid())
-			code.addLine(prefixTabs + "\t" + AssignToPtr(SpecNaming.InterfaceValueInst, SpecNaming.RET, SpecNaming.RET));
+			code.addLine(prefixTabs
+					+ "\t"
+					+ AssignToPtr(SpecNaming.InterfaceValueInst,
+							SpecNaming.RET, SpecNaming.RET));
 		// For arguments
 		for (VariableDeclaration decl : construct.getFunctionHeader().args)
-			code.addLine(prefixTabs + "\t" + AssignToPtr(SpecNaming.InterfaceValueInst, decl.name, decl.name));
+			code.addLine(prefixTabs
+					+ "\t"
+					+ AssignToPtr(SpecNaming.InterfaceValueInst, decl.name,
+							decl.name));
 		code.addLine("");
 
 		// Store the value info into the current MethodCall
 		// _setInterfaceBeginAnnotationValue(info, value);
-		code.addLine(prefixTabs + "\t" + ShortComment("Store the value info into the current MethodCall"));
-		code.addLine(prefixTabs + "\t" + SpecNaming.SetInterfaceBeginAnnoValueFunc
-				+ Brace(SpecNaming.AnnoInterfaceInfoInst + ", " + SpecNaming.InterfaceValueInst) + ";");
+		code.addLine(prefixTabs
+				+ "\t"
+				+ ShortComment("Store the value info into the current MethodCall"));
+		code.addLine(prefixTabs
+				+ "\t"
+				+ SpecNaming.SetInterfaceBeginAnnoValueFunc
+				+ Brace(SpecNaming.AnnoInterfaceInfoInst + ", "
+						+ SpecNaming.InterfaceValueInst) + ";");
 		code.addLine("");
 
 		// Return if necessary
diff --git a/src/edu/uci/eecs/codeGenerator/Environment.java b/src/edu/uci/eecs/codeGenerator/Environment.java
index 84fc4ee..563babb 100644
--- a/src/edu/uci/eecs/codeGenerator/Environment.java
+++ b/src/edu/uci/eecs/codeGenerator/Environment.java
@@ -1,5 +1,7 @@
 package edu.uci.eecs.codeGenerator;
 
+import java.util.ArrayList;
+
 /**
  * <p>
  * This class contains some constant strings related to the code generation
@@ -26,5 +28,26 @@ public class Environment {
 	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 static String TICKET_LOCK = "ticket-lock";
+	public final static String SEQLOCK = "seqlock";
+	public final static String READ_COPY_UPDATE = "read-copy-update";
+	public final static String CONCURRENT_MAP = "concurrent-hashmap";
+	public final static String SPSC = "spsc-bugfix";
+	public final static String MPMC = "mpmc-queue";
+	
+	public final static String[] Benchmarks = {
+		REGISTER,
+		MS_QUEUE,
+		LINUXRWLOCKS,
+		MCS_LOCK,
+		DEQUE,
+		TREIBER_STACK,
+		TICKET_LOCK,
+		SEQLOCK,
+		READ_COPY_UPDATE,
+		CONCURRENT_MAP,
+		SPSC,
+		MPMC
+	}; 
 
 }
diff --git a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
index b2e52a0..d8f6dd4 100644
--- a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
@@ -21,6 +21,7 @@ public class GlobalConstruct extends Construct {
 	public final ArrayList<VariableDeclaration> declState;
 	public final Code initState;
 	public final Code copyState;
+	public final Code clearState;
 	public final Code finalState;
 	public final Code printState;
 	public final ArrayList<CommutativityRule> commutativityRules;
@@ -31,6 +32,8 @@ public class GlobalConstruct extends Construct {
 	public final boolean autoGenInitial;
 	// Whether we have auto-gen the state copying code
 	public final boolean autoGenCopy;
+	// Whether we have auto-gen the state clearing code
+	public final boolean autoGenClear;
 	// Whether we have auto-gen the state printing code
 	public final boolean autoGenPrint;
 
@@ -40,6 +43,7 @@ public class GlobalConstruct extends Construct {
 		declState = new ArrayList<VariableDeclaration>();
 		initState = new Code();
 		copyState = new Code();
+		clearState = new Code();
 		finalState = new Code();
 		printState = new Code();
 		commutativityRules = new ArrayList<CommutativityRule>();
@@ -64,6 +68,12 @@ public class GlobalConstruct extends Construct {
 			copyState.addLines(code);
 		}
 
+		autoGenClear = clearState.isEmpty();
+		if (autoGenClear) {
+			Code code = generateAutoClearFunction();
+			clearState.addLines(code);
+		}
+
 		autoGenPrint = printState.isEmpty();
 		if (autoGenPrint) {
 			Code code = generateAutoPrintFunction();
@@ -167,6 +177,35 @@ public class GlobalConstruct extends Construct {
 
 		return code;
 	}
+	
+	/**
+	 * <p>
+	 * This function will automatically generate the clear statements for
+	 * supported types if the user has not defined the "@Clear" primitive
+	 * </p>
+	 * 
+	 * @return The auto-generated state copy statements
+	 * @throws WrongAnnotationException
+	 */
+	private Code generateAutoClearFunction() throws WrongAnnotationException {
+		Code code = new Code();
+		if (emptyState) // Empty state should have empty copy function
+			return code;
+		
+		// FIXME: Just try our best to generate recycling statements
+		for (VariableDeclaration decl : declState) {
+			String type = decl.type;
+			String name = decl.name;
+			if (type.equals("IntList *") || type.equals("IntSet *")
+					|| type.equals("IntMap *")) {
+				// Supported pointer types
+				// if (stack) delete stack;
+				code.addLine("if (" + name + ") delete " + name + ";");
+			}
+		}
+
+		return code;
+	}
 
 	/**
 	 * <p>
@@ -209,6 +248,7 @@ public class GlobalConstruct extends Construct {
 		if (!name.equals(SpecNaming.DeclareState)
 				&& !name.equals(SpecNaming.InitalState)
 				&& !name.equals(SpecNaming.CopyState)
+				&& !name.equals(SpecNaming.ClearState)
 				&& !name.equals(SpecNaming.FinalState)
 				&& !name.equals(SpecNaming.Commutativity)
 				&& !name.equals(SpecNaming.PrintState)) {
@@ -292,6 +332,8 @@ public class GlobalConstruct extends Construct {
 				initState.addLines(primitive.contents);
 			} else if (name.equals(SpecNaming.CopyState)) {
 				copyState.addLines(primitive.contents);
+			} else if (name.equals(SpecNaming.ClearState)) {
+				clearState.addLines(primitive.contents);
 			} else if (name.equals(SpecNaming.FinalState)) {
 				finalState.addLines(primitive.contents);
 			} else if (name.equals(SpecNaming.PrintState)) {
diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
index 6afd5f1..232acaf 100644
--- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
@@ -24,7 +24,6 @@ public class InterfaceConstruct extends Construct {
 	private String name;
 	public final Code transition;
 	public final Code preCondition;
-	public final Code sideEffect;
 	public final Code postCondition;
 	public final Code print;
 
@@ -47,7 +46,6 @@ public class InterfaceConstruct extends Construct {
 		this.name = null;
 		this.transition = new Code();
 		this.preCondition = new Code();
-		this.sideEffect = new Code();
 		this.postCondition = new Code();
 		this.print = new Code();
 
@@ -171,8 +169,6 @@ public class InterfaceConstruct extends Construct {
 				this.transition.addLines(primitive.contents);
 			} else if (name.equals(SpecNaming.PreCondition)) {
 				this.preCondition.addLines(primitive.contents);
-			} else if (name.equals(SpecNaming.SideEffect)) {
-				this.sideEffect.addLines(primitive.contents);
 			} else if (name.equals(SpecNaming.PostCondition)) {
 				this.postCondition.addLines(primitive.contents);
 			} else if (name.equals(SpecNaming.PrintValue)) {
@@ -214,8 +210,6 @@ public class InterfaceConstruct extends Construct {
 			sb.append("@Transition:\n" + transition);
 		if (!preCondition.isEmpty())
 			sb.append("@PreCondition:\n" + preCondition);
-		if (!sideEffect.isEmpty())
-			sb.append("@SideEffect:\n" + sideEffect);
 		if (!postCondition.isEmpty())
 			sb.append("@PostCondition:\n" + postCondition);
 		if (!print.isEmpty())
diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java
index 463d2c9..f1f97ff 100644
--- a/src/edu/uci/eecs/specExtraction/SpecNaming.java
+++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java
@@ -21,6 +21,7 @@ public class SpecNaming {
 	public static final String DeclareState = "DeclareState";
 	public static final String InitalState = "Initial";
 	public static final String CopyState = "Copy";
+	public static final String ClearState = "Clear";
 	public static final String FinalState = "Final";
 	public static final String PrintState = "Print";
 	public static final String Commutativity = "Commutativity";
-- 
2.34.1