From 24022553f123d8f8a796b257410b4c1c1b9ef8ee Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Fri, 1 Nov 2013 17:36:58 -0700
Subject: [PATCH] more bug fix

---
 .../simplified_cliffc_hashtable.h             | 18 ++--
 benchmark/linuxrwlocks/linuxrwlocks.c         | 35 +++-----
 grammer/spec.txt                              | 56 +++++++++++-
 grammer/spec_compiler.jj                      | 30 +++++--
 .../codeGenerator/CodeAddition.java           |  9 +-
 .../codeGenerator/CodeGenerator.java          | 48 ++++++++--
 .../codeGenerator/CodeVariables.java          | 87 ++++++++++++-------
 .../codeGenerator/SemanticsChecker.java       |  6 --
 .../specExtraction/ParserUtils.java           | 27 ++++++
 .../specExtraction/SourceFileInfo.java        | 22 -----
 .../specExtraction/SpecExtractor.java         |  2 +-
 test.c                                        |  9 +-
 12 files changed, 237 insertions(+), 112 deletions(-)

diff --git a/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h b/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
index 299e7a3..c02c0a3 100644
--- a/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
@@ -95,7 +95,6 @@ class cliffc_hashtable {
 				map = spec_hashtable<TypeK, TypeV*>();
 				id_map = spec_hashtable<TypeK, TypeV*>();
 				tag = Tag();
-			@DefineFunc:
 			static bool equals_val(TypeV *ptr1, TypeV *ptr2) {
 				// ...
 			}
@@ -369,7 +368,7 @@ friend class CHM;
 		@Commit_point_set: Read_Val_Point1 | Read_Val_Point2 | Read_Val_Point3
 		@ID: __sequential.getKeyTag(key)
 		@Action:
-			@DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
+			TypeV *_Old_Val = __sequential.map.get(key)
 		@Post_check:
 			__sequential.equals_val(_Old_Val, __RET__)
 		@End
@@ -391,8 +390,8 @@ friend class CHM;
 		@ID: __sequential.getKeyTag(key)
 		@Action:
 			# Remember this old value at checking point
-			@DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
-			@Code: __sequential.map.put(key, &val);
+			TypeV *_Old_Val = __sequential.map.get(key)
+			__sequential.map.put(key, &val);
 		@Post_check:
 			__sequential.equals_val(__RET__, _Old_Val)
 		@End
@@ -411,8 +410,7 @@ friend class CHM;
 			COND_PutIfAbsentSucc :: __RET__ == NULL
 		@ID: __sequential.getKeyTag(key)
 		@Action:
-			@DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
-			@Code:
+			TypeV *_Old_Val = __sequential.map.get(key)
 			if (__COND_SAT__)
 				__sequential.map.put(key, &value);
 		@Post_check:
@@ -429,8 +427,8 @@ friend class CHM;
 		@Commit_point_set: Write_Val_Point
 		@ID: __sequential.getKeyTag(key)
 		@Action:
-			@DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
-			@Code: __sequential.map.put(key, NULL);
+			TypeV *_Old_Val = __sequential.map.get(key)
+			__sequential.map.put(key, NULL);
 		@Post_check:
 			__sequential.equals_val(__RET__, _Old_Val)
 		@End
@@ -450,7 +448,6 @@ friend class CHM;
 			COND_RemoveIfMatchSucc :: __RET__ == true
 		@ID: __sequential.getKeyTag(key)
 		@Action:
-			@Code:
 			if (__COND_SAY__)
 				__sequential.map.put(key, NULL);
 		@Post_check:
@@ -470,7 +467,7 @@ friend class CHM;
 			Write_Val_Point
 		@ID: __sequential.getKeyTag(key)
 		@Action:
-			@DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
+			TypeV *_Old_Val = __sequential.map.get(key)
 		@Post_check:
 			__sequential.equals_val(__RET__, _Old_Val)
 		@End
@@ -490,7 +487,6 @@ friend class CHM;
 			COND_ReplaceIfMatchSucc :: __RET__ == true
 		@ID: __sequential.getKeyTag(key)
 		@Action:
-			@Code:
 			if (__COND_SAY__)
 				__sequential.map.put(key, &newval);
 		@Post_check:
diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 9dd2bf8..1cbe525 100644
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -45,7 +45,6 @@
 		@InitVar:
 			writer_lock_acquired = false;
 			reader_lock_cnt = 0;
-		@DefineFunc:
 	@Happens_before:
 		# Since commit_point_set has no ID attached, A -> B means that for any B,
 		# the previous A happens before B.
@@ -84,10 +83,9 @@ static inline int write_can_lock(rwlock_t *lock)
 	@Commit_point_set:
 		Read_Lock_Success_1 | Read_Lock_Success_2
 	@Check:
-		!__sequential.writer_lock_acquired
+		!writer_lock_acquired
 	@Action:
-		@Code:
-		__sequential.reader_lock_cnt++;
+		reader_lock_cnt++;
 	@End
 */
 static inline void read_lock(rwlock_t *rw)
@@ -121,10 +119,9 @@ static inline void read_lock(rwlock_t *rw)
 	@Commit_point_set:
 		Write_Lock_Success_1 | Write_Lock_Success_2
 	@Check:
-		!__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
+		!writer_lock_acquired && reader_lock_cnt == 0
 	@Action:
-		@Code:
-		__sequential.writer_lock_acquired = true;
+		writer_lock_acquired = true;
 	@End
 */
 static inline void write_lock(rwlock_t *rw)
@@ -157,15 +154,14 @@ static inline void write_lock(rwlock_t *rw)
 	@Commit_point_set:
 		Read_Trylock_Point
 	@Condition:
-		__sequential.writer_lock_acquired == false
+		writer_lock_acquired == false
 	@HB_condition:
 		HB_Read_Trylock_Succ :: __RET__ == 1
 	@Action:
-		@Code:
-		if (__COND_SAY__)
-			__sequential.reader_lock_cnt++;
+		if (__COND_SAT__)
+			reader_lock_cnt++;
 	@Post_check:
-		__COND_SAY__ ? __RET__ == 1 : __RET__ == 0
+		__COND_SAT__ ? __RET__ == 1 : __RET__ == 0
 	@End
 */
 static inline int read_trylock(rwlock_t *rw)
@@ -190,15 +186,14 @@ static inline int read_trylock(rwlock_t *rw)
 	@Commit_point_set:
 		Write_Trylock_Point
 	@Condition:
-		!__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
+		!writer_lock_acquired && reader_lock_cnt == 0
 	@HB_condition:
 		HB_Write_Trylock_Succ :: __RET__ == 1
 	@Action:
-		@Code:
-		if (__COND_SAY__)
-			__sequential.writer_lock_acquired = true;
+		if (__COND_SAT__)
+			writer_lock_acquired = true;
 	@Post_check:
-		__COND_SAY__ ? __RET__ == 1 : __RET__ == 0
+		__COND_SAT__ ? __RET__ == 1 : __RET__ == 0
 	@End
 */
 static inline int write_trylock(rwlock_t *rw)
@@ -222,9 +217,8 @@ static inline int write_trylock(rwlock_t *rw)
 	@Interface: Read_Unlock
 	@Commit_point_set: Read_Unlock_Point
 	@Check:
-		__sequential.reader_lock_cnt > 0 && !__sequential.writer_lock_acquired
+		reader_lock_cnt > 0 && !writer_lock_acquired
 	@Action: 
-		@Code:
 		reader_lock_cnt--;
 	@End
 */
@@ -246,8 +240,7 @@ static inline void read_unlock(rwlock_t *rw)
 	@Check:
 		reader_lock_cnt == 0 && writer_lock_acquired
 	@Action: 
-		@Code:
-		__sequential.writer_lock_acquired = false;
+		writer_lock_acquired = false;
 	@End
 */
 
diff --git a/grammer/spec.txt b/grammer/spec.txt
index ed30de8..1ac8dc1 100644
--- a/grammer/spec.txt
+++ b/grammer/spec.txt
@@ -1 +1,55 @@
-void enqueue(queue_t *q, unsigned int val)
+/**
+@Begin
+		@Options:
+			LANG = C;
+			CLASS = cliffc_hashtable;
+		@Global_define:
+			@DeclareVar:
+			spec_hashtable<TypeK, TypeV*> map;
+			spec_hashtable<TypeK, Tag> id_map;
+			Tag tag;
+			@InitVar:
+				map = spec_hashtable<TypeK, TypeV*>();
+				id_map = spec_hashtable<TypeK, TypeV*>();
+				tag = Tag();
+			@DefineFunc:
+			static bool equals_val(TypeV *ptr1, TypeV *ptr2) {
+				// ...
+			}
+			
+			# Update the tag for the current key slot if the corresponding tag
+			# is NULL, otherwise just return that tag. It will update the next
+			# available tag too if it requires a new tag for that key slot.
+			static Tag getKeyTag(TypeK &key) {
+				if (id_map.get(key) == NULL) {
+					Tag cur_tag = tag.current();
+					id_map.put(key, cur_tag);
+					tag.next();
+					return cur_tag;
+				} else {
+					return id_map.get(key);
+				}
+			}
+		
+		@Interface_cluster:
+			Read_interface = {
+				Get,
+				PutIfAbsent,
+				RemoveAny,
+				RemoveIfMatch,
+				ReplaceAny,
+				ReplaceIfMatch
+			}
+			
+			Write_interface = {
+				Put,
+				PutIfAbsent(COND_PutIfAbsentSucc),
+				RemoveAny,
+				RemoveIfMatch(COND_RemoveIfMatchSucc),
+				ReplaceAny,
+				ReplaceIfMatch(COND_ReplaceIfMatchSucc)
+			}
+		@Happens_before:
+			Write_interface -> Read_interface
+		@End
+	*/
diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj
index 93a5d8b..6a4f61b 100644
--- a/grammer/spec_compiler.jj
+++ b/grammer/spec_compiler.jj
@@ -179,6 +179,8 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
 
 		public static String stringArray2String(ArrayList<String> content) {
 			StringBuilder sb = new StringBuilder();
+			if (content.size() == 1)
+				return content.get(0);
 			for (int i = 0; i < content.size(); i++) {
 				sb.append(content.get(i) + "\n");
 			}
@@ -309,6 +311,10 @@ SKIP : {
 	<UNSIGNED: "unsigned">
 |
 	<TEMPLATE: "template">
+|
+	<INLINE: "inline">
+|
+	<STATIC: "static">
 |
 	<#DIGIT: ["0"-"9"]>
 |
@@ -514,7 +520,6 @@ void Test() :
 	{
 		System.out.println(func);
 	}
-
 	
 }
 
@@ -525,8 +530,8 @@ String ParameterizedName() :
 }
 {
 	(str = <IDENTIFIER>.image {res = str;})
-	("<" str = <IDENTIFIER>.image { res = res + "<" + str; }
-	("," str = <IDENTIFIER>.image { res = res + ", " + str; })* ">"
+	("<" str = Type() { res = res + "<" + str; }
+	("," str = Type() { res = res + ", " + str; })* ">"
 	{ res = res + ">"; }
 	)?
 	{
@@ -541,6 +546,7 @@ FunctionHeader FuncDecl() :
 	ArrayList<VariableDeclaration> args;
 }
 {
+	(<STATIC> | <INLINE>)*
 	ret = Type() 
 	funcName = ParseQualifiedName() 
 	args = FormalParamList() 
@@ -639,6 +645,7 @@ ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
 	(
 	t = <CONST> | t = <STRUCT> | t = <CLASS> | t = <UNSIGNED> |
 	(t = <TEMPLATE> { inTemplate = true;  })|
+	t = <STATIC> | t = <INLINE> |
 	(t = <INCLUDE>
 	{
 		header = t.image;
@@ -666,11 +673,16 @@ ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
 	(t = <DEFINE> { newLine = true; } )
 	)
 	{
-		text = text + " " + t.image;
+		if (text.equals("")) {
+			text = t.image;
+		} else {
+			text = text + " " + t.image;
+		}
 		if (newLine) {
 			content.add(text);
 			text = "";
 			newLine = false;
+			inTemplate = false;
 		}
 	}
 	)+
@@ -798,8 +810,8 @@ ConditionalInterface Conditional_interface() :
 	{
 		hbConditionLabel = "";
 	}
-	interfaceName = <IDENTIFIER>.image (<OPEN_BRACKET> hbConditionLabel =
-	<IDENTIFIER>.image <CLOSE_BRACKET>)?
+	interfaceName = <IDENTIFIER>.image (<OPEN_PAREN> hbConditionLabel =
+	<IDENTIFIER>.image <CLOSE_PAREN>)?
 	{
 		return new ConditionalInterface(interfaceName, hbConditionLabel);
 	}
@@ -812,14 +824,14 @@ void Interface_cluster(GlobalConstruct inst) :
 }
 {
 	(clusterName= <IDENTIFIER>.image)
-	<EQUALS> <OPEN_PAREN>
+	<EQUALS> <OPEN_BRACE>
 		(condInterface = Conditional_interface()
 		{ inst.addInterface2Cluster(clusterName, condInterface); } 
 		)
 		(<COMMA> condInterface = Conditional_interface()
 		{ inst.addInterface2Cluster(clusterName, condInterface); } 
 		)*
-	<CLOSE_PAREN>
+	<CLOSE_BRACE>
 }
 
 void Interface_clusters(GlobalConstruct inst) :
@@ -882,7 +894,7 @@ InterfaceConstruct Interface() :
 			(<CONDITION> (content = C_CPP_CODE(null) { condition = stringArray2String(content); }))?
 			(
 				<HB_CONDITION>
-				(hbLabel = <IDENTIFIER>.image)
+				(hbLabel = <IDENTIFIER>.image) <DOUBLECOLON>
 				(content = C_CPP_CODE(null) { hbCondition = stringArray2String(content); })
 				{
 					if (hbConditions.containsKey(hbLabel)) {
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java
index f127772..a0bc957 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java
@@ -1,11 +1,14 @@
 package edu.uci.eecs.specCompiler.codeGenerator;
 
 import java.util.ArrayList;
+import java.util.Comparator;
 
 public class CodeAddition {
-	public static class CodeAdditionComparator<CodeAddition> {
-		
-	}
+	public static Comparator<CodeAddition> lineNumComparator = new Comparator<CodeAddition>() {
+		public int compare(CodeAddition addition1, CodeAddition addition2) {
+			return addition1.lineNum - addition2.lineNum;
+		}
+	};
 	
 	public final int lineNum;
 	public final ArrayList<String> newCode;
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index d652584..20f6e53 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -6,6 +6,7 @@ import java.io.FileNotFoundException;
 import java.io.FileReader;
 import java.io.IOException;
 import java.util.ArrayList;
+import java.util.Collections;
 import java.util.HashMap;
 import java.util.Iterator;
 
@@ -19,6 +20,7 @@ import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.IDExtractor;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ParserUtils;
 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
@@ -146,6 +148,25 @@ public class CodeGenerator {
 		codeAdditions.get(construct.file).add(addition);
 	}
 
+	private ArrayList<String> insertAnnotation2Src(
+			ArrayList<CodeAddition> additions, ArrayList<String> content) {
+		int totalSize = content.size();
+		for (int i = 0; i < additions.size(); i++) {
+			totalSize += additions.size();
+		}
+		ArrayList<String> newContent = new ArrayList<String>(totalSize);
+		int curSrcLine = 0;
+		for (int i = 0; i < additions.size(); i++) {
+			CodeAddition addition = additions.get(i);
+			if (curSrcLine <  addition.lineNum) {
+				newContent.addAll(content.subList(curSrcLine, addition.lineNum - 1));
+				curSrcLine = addition.lineNum;
+			}
+			newContent.addAll(addition.newCode);
+		}
+		return newContent;
+	}
+
 	public void generateCode() {
 		for (int i = 0; i < _semantics.constructs.size(); i++) {
 			Construct construct = _semantics.constructs.get(i);
@@ -159,18 +180,35 @@ public class CodeGenerator {
 				CPDefine2Code((CPDefineConstruct) construct);
 			} else if (construct instanceof CPDefineCheckConstruct) {
 				CPDefineCheck2Code((CPDefineCheckConstruct) construct);
+			} else if (construct instanceof EntryPointConstruct) {
+				EntryPoint2Code((EntryPointConstruct) construct);
 			}
 		}
+		// Sort code additions
+		for (File file : codeAdditions.keySet()) {
+			ArrayList<CodeAddition> additions = codeAdditions.get(file);
+			if (additions.size() == 0) // Simply do nothing, already written
+										// once
+				continue;
+			ArrayList<String> content = _semantics.srcFilesInfo.get(file).content;
+			Collections.sort(additions, CodeAddition.lineNumComparator);
+			// Insert generated annotation to the source files
+			ArrayList<String> newContent = insertAnnotation2Src(additions,
+					content);
+			// Write it back to file
+			ParserUtils.write2File(file, newContent);
+		}
+
 	}
 
 	public static void main(String[] argvs) {
 		String homeDir = Environment.HOME_DIRECTORY;
 		File[] srcFiles = {
-		// new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c"),
-		new File(homeDir
-				+ "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
-//		 new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
-//		 new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
+		 new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+//		new File(homeDir
+//				+ "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"), };
+		// new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+		// new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
 		CodeGenerator gen = new CodeGenerator(srcFiles);
 		gen.generateCode();
 	}
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index 8e87cd5..980e420 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -23,6 +23,7 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
 
 public class CodeVariables {
 	// C++ code or library
+	public static final String HEADER_STDLIB = "<stdlib.h>";
 	public static final String HEADER_THREADS = "<threads.h>";
 	public static final String HEADER_STDINT = "<stdint.h>";
 	public static final String ThreadIDType = "thrd_t";
@@ -148,12 +149,14 @@ public class CodeVariables {
 	}
 
 	private static ArrayList<String> DEFINE_INFO_STRUCT(String interfaceName,
-			FunctionHeader funcDecl) {
+			FunctionHeader header) {
 		ArrayList<String> code = new ArrayList<String>();
 		code.add("typedef struct " + interfaceName + "_info {");
-		code.add(DECLARE(funcDecl.returnType, MACRO_RETURN));
-		for (int i = 0; i < funcDecl.args.size(); i++) {
-			code.add(DECLARE(funcDecl.args.get(i)));
+		if (!header.returnType.equals("void")) {
+			code.add(DECLARE(header.returnType, MACRO_RETURN));
+		}
+		for (int i = 0; i < header.args.size(); i++) {
+			code.add(DECLARE(header.args.get(i)));
 		}
 		code.add("} " + interfaceName + "_info {");
 		return code;
@@ -180,17 +183,22 @@ public class CodeVariables {
 		code.add("static bool " + interfaceName + "_check_action(void *info, "
 				+ IDType + " " + MACRO_ID + ") {");
 		code.add(DECLARE("bool", "check_passed"));
-		String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
-		code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
-				BRACE(infoStructType) + "info"));
-		code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
-				GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
-		for (int i = 0; i < header.args.size(); i++) {
-			String type = header.args.get(i).type, var = header.args.get(i).name;
-			code.add((DECLARE_DEFINE(type, var,
-					GET_FIELD_BY_PTR(infoStructName, var))));
+		// Read info struct
+		if (!header.returnType.equals("void") || header.args.size() != 0) {
+			String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
+			code.add(DECLARE_DEFINE(infoStructType + "*", infoStructName,
+					BRACE(infoStructType) + "info"));
+			if (!header.returnType.equals("void")) {
+				code.add((DECLARE_DEFINE(header.returnType, MACRO_RETURN,
+						GET_FIELD_BY_PTR(infoStructName, MACRO_RETURN))));
+			}
+			for (int i = 0; i < header.args.size(); i++) {
+				String type = header.args.get(i).type, var = header.args.get(i).name;
+				code.add((DECLARE_DEFINE(type, var,
+						GET_FIELD_BY_PTR(infoStructName, var))));
+			}
+			code.add("");
 		}
-		code.add("");
 		// __COND_SAT
 		if (!construct.condition.equals("")) {
 			code.add(DECLARE_DEFINE("bool", MACRO_COND, construct.condition));
@@ -296,12 +304,14 @@ public class CodeVariables {
 					.get(interfaceName);
 			FunctionHeader funcHeader = getFunctionHeader(semantics, iConstruct);
 			// Define necessary info structure
-			newCode.add(COMMENT("Definition of interface info struct: "
-					+ interfaceName));
-			newCode.addAll(DEFINE_INFO_STRUCT(interfaceName, funcHeader));
-			newCode.add(COMMENT("End of info struct definition: "
-					+ interfaceName));
-			newCode.add("");
+			if (!funcHeader.returnType.equals("void") || funcHeader.args.size() > 0) {
+				newCode.add(COMMENT("Definition of interface info struct: "
+						+ interfaceName));
+				newCode.addAll(DEFINE_INFO_STRUCT(interfaceName, funcHeader));
+				newCode.add(COMMENT("End of info struct definition: "
+						+ interfaceName));
+				newCode.add("");
+			}
 
 			// Define ID function
 			newCode.add(COMMENT("ID function of interface: " + interfaceName));
@@ -442,6 +452,7 @@ public class CodeVariables {
 		ArrayList<String> newCode = new ArrayList<String>();
 		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));
@@ -472,12 +483,16 @@ public class CodeVariables {
 		newCode.add(ASSIGN_PTR(structName, "annotation", structName));
 		newCode.add(ANNOTATE(anno));
 		// Call original renamed function
-		newCode.add(DECLARE_DEFINE(header.returnType, MACRO_RETURN,
-				header.getRenamedCall(SPEC_INTERFACE_WRAPPER)));
+		if (header.returnType.equals("void")) {
+			newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER));
+		} else {
+			newCode.add(DECLARE_DEFINE(header.returnType, MACRO_RETURN,
+					header.getRenamedCall(SPEC_INTERFACE_WRAPPER)));
+		}
 		// HB conditions
 		for (String label : construct.hbConditions.keySet()) {
 			String condition = construct.hbConditions.get(label);
-			String hbCondNum = Integer.toString(semantics.interface2Num
+			String hbCondNum = Integer.toString(semantics.hbLabel2Num
 					.get(label));
 			newCode.add("if " + BRACE(condition) + " {");
 			structName = "hb_condition";
@@ -490,16 +505,26 @@ public class CodeVariables {
 			newCode.add(ASSIGN(anno, "type", SPEC_ANNO_TYPE_HB_CONDITION));
 			newCode.add(ASSIGN_PTR(anno, "annotation", structName));
 			newCode.add(ANNOTATE(anno));
+			newCode.add("}");
+			newCode.add("");
 		}
 		// Interface end
-		String infoStructType = interfaceName + "_info", infoName = "info";
-		newCode.add(DECLARE_DEFINE(infoStructType, infoName,
-				BRACE(infoStructType + "*") + " malloc(sizeof("
-						+ infoStructType + "))"));
-		newCode.add(ASSIGN_TO_PTR(infoName, MACRO_RETURN, MACRO_RETURN));
-		for (int i = 0; i < header.args.size(); i++) {
-			String argName = header.args.get(i).name;
-			newCode.add(ASSIGN_TO_PTR(infoName, argName, argName));
+		String infoStructType = null, infoName = null;
+		if (!header.returnType.equals("void") || header.args.size() > 0) {
+			infoStructType = interfaceName + "_info";
+			infoName = "info";
+			newCode.add(DECLARE_DEFINE(infoStructType, infoName,
+					BRACE(infoStructType + "*") + " malloc(sizeof("
+							+ infoStructType + "))"));
+			if (!header.returnType.equals("void")) {
+				newCode.add(ASSIGN_TO_PTR(infoName, MACRO_RETURN, MACRO_RETURN));
+			}
+			for (int i = 0; i < header.args.size(); i++) {
+				String argName = header.args.get(i).name;
+				newCode.add(ASSIGN_TO_PTR(infoName, argName, argName));
+			}
+		} else {
+			infoName = "NULL";
 		}
 		structName = "interface_end";
 		anno = "annoation_interface_end";
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
index 26647f6..ae53d3b 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
@@ -121,12 +121,6 @@ public class SemanticsChecker {
 						+ label + "!");
 			}
 
-			// No HB condition label can duplicate!
-			if (hbLabel2Num.containsKey(label)) {
-				throw new SemanticsCheckerException("Happens-before label: "
-						+ label + " duplicates!");
-			}
-
 			// Number the HB-condition label
 			hbLabel2Num.put(label, _hbLabelNum++);
 		}
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/ParserUtils.java b/src/edu/uci/eecs/specCompiler/specExtraction/ParserUtils.java
index 61d0da7..2cae9b5 100644
--- a/src/edu/uci/eecs/specCompiler/specExtraction/ParserUtils.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/ParserUtils.java
@@ -1,7 +1,12 @@
 package edu.uci.eecs.specCompiler.specExtraction;
 
+import java.io.BufferedWriter;
+import java.io.File;
+import java.io.FileWriter;
+import java.io.IOException;
 import java.util.ArrayList;
 
+import edu.uci.eecs.specCompiler.codeGenerator.Environment;
 import edu.uci.eecs.specCompiler.codeGenerator.SemanticsChecker;
 import edu.uci.eecs.specCompiler.grammerParser.ParseException;
 import edu.uci.eecs.specCompiler.grammerParser.SpecParser;
@@ -54,4 +59,26 @@ public class ParserUtils {
 		}
 		return templateStr;
 	}
+	
+	public static void write2File(File file, ArrayList<String> content) {
+		String newFileName = Environment.GENERATED_FILE_DIR + "/" + file.getName();
+		File newFile = new File(newFileName);
+		newFile.getParentFile().mkdirs();
+		if (!newFile.exists()) {
+			try {
+				newFile.createNewFile();
+			} catch (IOException e) {
+				e.printStackTrace();
+			}
+		}
+		try {
+			BufferedWriter bw = new BufferedWriter(new FileWriter(newFile));
+			for (int i = 0; i < content.size(); i++) {
+				bw.write(content.get(i) + "\n");
+			}
+			bw.flush();
+		} catch (IOException e) {
+			e.printStackTrace();
+		}
+	}
 }
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java b/src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java
index 2b9af87..0ac075f 100644
--- a/src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java
@@ -28,26 +28,4 @@ public class SourceFileInfo {
 		SourceFileInfo another = (SourceFileInfo) o;
 		return another.file.equals(file);
 	}
-	
-	public void write2File() {
-		String newFileName = Environment.GENERATED_FILE_DIR + "/" + file.getName();
-		File newFile = new File(newFileName);
-		newFile.getParentFile().mkdirs();
-		if (!newFile.exists()) {
-			try {
-				newFile.createNewFile();
-			} catch (IOException e) {
-				e.printStackTrace();
-			}
-		}
-		try {
-			BufferedWriter bw = new BufferedWriter(new FileWriter(newFile));
-			for (int i = 0; i < content.size(); i++) {
-				bw.write(content.get(i) + "\n");
-			}
-			bw.flush();
-		} catch (IOException e) {
-			e.printStackTrace();
-		}
-	}
 }
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
index 8d7a229..52862f4 100644
--- a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
@@ -60,7 +60,7 @@ public class SpecExtractor {
 		SourceFileInfo srcFileInfo;
 		try {
 			srcFileInfo = SpecParser.ParseFile(file);
-			srcFileInfo.write2File();
+			ParserUtils.write2File(srcFileInfo.file, srcFileInfo.content);
 			srcFilesInfo.put(file, srcFileInfo);
 		} catch (ParseException e) {
 			e.printStackTrace();
diff --git a/test.c b/test.c
index 65c412a..b279809 100644
--- a/test.c
+++ b/test.c
@@ -2,9 +2,14 @@
 #include <stdlib.h>
 #include <stdint.h>
 
+typedef struct A {
+
+} A;
+
 int main() {
 	uint64_t i64 = (uint64_t) NULL;
-	if (i64)
-		printf("True\n");
+	A *a = (A*) malloc (sizeof(A));
+	printf("%d\n", sizeof(A));
+	printf("%d\n", a);
 	return 1;
 }
-- 
2.34.1