From f2d6efad8b1ee05ef5dd12175af9e59e61c7b8f8 Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 31 Oct 2013 18:01:28 -0700
Subject: [PATCH] fixed bugs

---
 benchmark/ms-queue/my_queue.h                 |   6 +-
 grammer/spec.txt                              | 190 ------------------
 grammer/spec_compiler.jj                      |  40 ++--
 .../codeGenerator/CodeGenerator.java          |  33 ++-
 .../codeGenerator/CodeVariables.java          |  69 +++++--
 .../codeGenerator/Environment.java            |   1 +
 .../SequentialDefineSubConstruct.java         |  10 +-
 .../specExtraction/SourceFileInfo.java        |  27 +++
 .../specExtraction/SpecExtractor.java         |   1 +
 9 files changed, 130 insertions(+), 247 deletions(-)

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 3a344d6..4161b33 100644
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -30,7 +30,7 @@ void init_queue(queue_t *q, int num_threads);
 /**
 	@Begin
 	@Global_define:
-		@DeclareVar:
+		@DeclareStruct:
 		typedef struct tag_elem {
 			Tag id;
 			unsigned int data;
@@ -40,7 +40,7 @@ void init_queue(queue_t *q, int num_threads);
 				data = _data;
 			}
 		} tag_elem_t;
-
+		@DeclareVar:
 		spec_queue<tag_elem_t> queue;
 		Tag tag;
 		@InitVar:
@@ -64,7 +64,6 @@ void init_queue(queue_t *q, int num_threads);
 	@Action:
 		# __ID__ is an internal macro that refers to the id of the current
 		# interface call
-		@Code:
 		__sequential.queue.enqueue(tag_elem_t(__ID__, val));
 	@End
 */
@@ -76,7 +75,6 @@ void enqueue(queue_t *q, unsigned int val);
 	@Commit_point_set: Dequeue_Success_Point
 	@ID: __sequential.queue.peak().tag
 	@Action:
-		@Code:
 		unsigned int _Old_Val = __sequential.queue.dequeue().data;
 	@Post_check:
 		_Old_Val == __RET__
diff --git a/grammer/spec.txt b/grammer/spec.txt
index 634a051..ed30de8 100644
--- a/grammer/spec.txt
+++ b/grammer/spec.txt
@@ -1,191 +1 @@
-#include <threads.h>
-#include <stdlib.h>
-#include "librace.h"
-#include "model-assert.h"
-
-#include "my_queue.h"
-
-#define relaxed memory_order_relaxed
-#define release memory_order_release
-#define acquire memory_order_acquire
-
-#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
-#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
-
-#define POISON_IDX 0x666
-
-static unsigned int (*free_lists)[MAX_FREELIST];
-
-/* Search this thread's free list for a "new" node */
-static unsigned int new_node()
-{
-	int i;
-	int t = get_thread_num();
-	for (i = 0; i < MAX_FREELIST; i++) {
-		unsigned int node = load_32(&free_lists[t][i]);
-		if (node) {
-			store_32(&free_lists[t][i], 0);
-			return node;
-		}
-	}
-	/* free_list is empty? */
-	MODEL_ASSERT(0);
-	return 0;
-}
-
-/* Place this node index back on this thread's free list */
-static void reclaim(unsigned int node)
-{
-	int i;
-	int t = get_thread_num();
-
-	/* Don't reclaim NULL node */
-	MODEL_ASSERT(node);
-
-	for (i = 0; i < MAX_FREELIST; i++) {
-		/* Should never race with our own thread here */
-		unsigned int idx = load_32(&free_lists[t][i]);
-
-		/* Found empty spot in free list */
-		if (idx == 0) {
-			store_32(&free_lists[t][i], node);
-			return;
-		}
-	}
-	/* free list is full? */
-	MODEL_ASSERT(0);
-}
-
-void init_queue(queue_t *q, int num_threads)
-{
-	/**
-		@Begin
-		@Entry_point
-		@End
-	*/
-
-	int i, j;
-
-	/* Initialize each thread's free list with INITIAL_FREE pointers */
-	/* The actual nodes are initialized with poison indexes */
-	free_lists = malloc(num_threads * sizeof(*free_lists));
-	for (i = 0; i < num_threads; i++) {
-		for (j = 0; j < INITIAL_FREE; j++) {
-			free_lists[i][j] = 2 + i * MAX_FREELIST + j;
-			atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
-		}
-	}
-
-	/* initialize queue */
-	atomic_init(&q->head, MAKE_POINTER(1, 0));
-	atomic_init(&q->tail, MAKE_POINTER(1, 0));
-	atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
-}
-
-/**
-	@Begin
-	@Interface_define: Enqueue
-	@End
-*/
 void enqueue(queue_t *q, unsigned int val)
-{
-	int success = 0;
-	unsigned int node;
-	pointer tail;
-	pointer next;
-	pointer tmp;
-
-	node = new_node();
-	store_32(&q->nodes[node].value, val);
-	tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
-	set_ptr(&tmp, 0); // NULL
-	atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
-
-	while (!success) {
-		tail = atomic_load_explicit(&q->tail, acquire);
-		next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
-		if (tail == atomic_load_explicit(&q->tail, relaxed)) {
-
-			/* Check for uninitialized 'next' */
-			MODEL_ASSERT(get_ptr(next) != POISON_IDX);
-
-			if (get_ptr(next) == 0) { // == NULL
-				pointer value = MAKE_POINTER(node, get_count(next) + 1);
-				success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
-						&next, value, release, release);
-			}
-			if (!success) {
-				unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
-				pointer value = MAKE_POINTER(ptr,
-						get_count(tail) + 1);
-				int commit_success = 0;
-				commit_success = atomic_compare_exchange_strong_explicit(&q->tail,
-						&tail, value, release, release);
-				/**
-					@Begin
-					@Commit_point_define_check: __ATOMIC_RET__ == true
-					@Label: Enqueue_Success_Point
-					@End
-				*/
-				thrd_yield();
-			}
-		}
-	}
-	atomic_compare_exchange_strong_explicit(&q->tail,
-			&tail,
-			MAKE_POINTER(node, get_count(tail) + 1),
-			release, release);
-}
-
-
-/**
-	@Begin
-	@Interface_define: Dequeue
-	@End
-*/
-unsigned int dequeue(queue_t *q)
-{
-	unsigned int value;
-	int success = 0;
-	pointer head;
-	pointer tail;
-	pointer next;
-
-	while (!success) {
-		head = atomic_load_explicit(&q->head, acquire);
-		tail = atomic_load_explicit(&q->tail, relaxed);
-		next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
-		if (atomic_load_explicit(&q->head, relaxed) == head) {
-			if (get_ptr(head) == get_ptr(tail)) {
-
-				/* Check for uninitialized 'next' */
-				MODEL_ASSERT(get_ptr(next) != POISON_IDX);
-
-				if (get_ptr(next) == 0) { // NULL
-					return 0; // NULL
-				}
-				atomic_compare_exchange_strong_explicit(&q->tail,
-						&tail,
-						MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
-						release, release);
-				thrd_yield();
-			} else {
-				value = load_32(&q->nodes[get_ptr(next)].value);
-				success = atomic_compare_exchange_strong_explicit(&q->head,
-						&head,
-						MAKE_POINTER(get_ptr(next), get_count(head) + 1),
-						release, release);
-				/**
-					@Begin
-					@Commit_point_define_check: __ATOMIC_RET__ == true
-					@Label: Dequeue_Success_Point
-					@End
-				*/
-				if (!success)
-					thrd_yield();
-			}
-		}
-	}
-	reclaim(get_ptr(head));
-	return value;
-}
diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj
index 22fada8..93a5d8b 100644
--- a/grammer/spec_compiler.jj
+++ b/grammer/spec_compiler.jj
@@ -16,6 +16,7 @@
 		# entry point.
 		LANG = C;
 	@Global_define:
+		@DeclareStruct:
 		@DeclareVar:
 		@InitVar:
 		@DefineFunc:
@@ -124,7 +125,7 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
 				File f = new File("./grammer/spec.txt");
 				FileInputStream fis = new FileInputStream(f);
 				SpecParser parser = new SpecParser(fis);
-				
+				/*
 				ArrayList<String> content = new ArrayList<String>();
 				ArrayList<Construct> constructs = new ArrayList<Construct>();
 				ArrayList<String> headers = new ArrayList<String>();
@@ -136,8 +137,9 @@ import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
 				for (int i = 0; i < constructs.size(); i++) {
 					System.out.println(constructs.get(i));
 				}
+				*/
 				
-				//parser.Test();
+				parser.Test();
 				System.out.println("Parsing finished!");
 			} catch (FileNotFoundException e) {
 				e.printStackTrace();
@@ -241,6 +243,8 @@ SKIP : {
 	<OPTIONS: "@Options:">
 |
 	<GLOBAL_DEFINE: "@Global_define:">
+|
+	<DECLARE_STRUCT: "@DeclareStruct:">
 |
 	<DECLARE_VAR: "@DeclareVar:">
 |
@@ -301,6 +305,8 @@ SKIP : {
 	<STRUCT: "struct">
 |
 	<CLASS: "class">
+|
+	<UNSIGNED: "unsigned">
 |
 	<TEMPLATE: "template">
 |
@@ -459,7 +465,7 @@ String Type() :
 	("const"
 	{ type = "const"; }
 	)?
-	(((str = <STRUCT>.image | str = <CLASS>.image) { type = type + " " + str; })? 
+	(((str = <STRUCT>.image | str = <CLASS>.image | str = <UNSIGNED>.image) { type = type + " " + str; })? 
 	(
 	name = ParseQualifiedName() {
 		if (!type.equals(""))
@@ -508,6 +514,8 @@ void Test() :
 	{
 		System.out.println(func);
 	}
+
+	
 }
 
 String ParameterizedName() :
@@ -629,9 +637,12 @@ ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
 	(
 	LOOKAHEAD(2)
 	(
-	t = <CONST> | t = <STRUCT> | t = <CLASS> |
+	t = <CONST> | t = <STRUCT> | t = <CLASS> | t = <UNSIGNED> |
 	(t = <TEMPLATE> { inTemplate = true;  })|
-	(header = <INCLUDE>.image {
+	(t = <INCLUDE>
+	{
+		header = t.image;
+		newLine = true;
 		if (headers != null) {
 			headers.add(header.substring(header.lastIndexOf(' ') + 1));
 		}
@@ -665,6 +676,9 @@ ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
 	)+
 
 	{
+		if (content.size() == 0) {
+			content.add(text);
+		}
 		return content;
 	}
 }
@@ -747,26 +761,30 @@ GlobalConstruct Global_construct() :
 
 SequentialDefineSubConstruct Global_define() :
 {
-	ArrayList<String> initVar, defineFunc, code;
+	ArrayList<String> initVar, defineFunc, code, declareStruct;
 	ArrayList<ArrayList<String>> defineFuncs;
 	ArrayList<VariableDeclaration> declareVars;
+	ArrayList<ArrayList<String>> declareStructs;
 	VariableDeclaration declareVar;
 
 }
 {
 	{
-		declareVars = null;
+		declareVars = new ArrayList<VariableDeclaration>();
 		initVar = null;
 		defineFuncs = new ArrayList<ArrayList<String>>();
+		declareStructs = new ArrayList<ArrayList<String>>();
 	}
 	<GLOBAL_DEFINE>
+	(<DECLARE_STRUCT> (declareStruct = C_CPP_CODE(null) {
+		declareStructs.add(declareStruct); }))*
 		(<DECLARE_VAR> ((declareVar = TypeParam() ";" {
 			declareVars.add(declareVar); } )*))?
 	(<INIT_VAR> (code = C_CPP_CODE(null) { initVar = code; } ))?
 	(<DEFINE_FUNC> (defineFunc = C_CPP_CODE(null) { defineFuncs.add(defineFunc); }))*
 	{
 		SequentialDefineSubConstruct res = new
-			SequentialDefineSubConstruct(declareVars, initVar, defineFuncs);
+			SequentialDefineSubConstruct(declareStructs, declareVars, initVar, defineFuncs);
 		//System.out.println(res);
 		return res;
 	}
@@ -835,16 +853,14 @@ InterfaceConstruct Interface() :
 {
 	{
 		res = null;
-		action = null;
+		action = new ArrayList<String>();
 		condition = "";
 		idCode = "";
 		check = "";
 		postCheck = "";
 		commitPointSet = new ArrayList<String>();
 		hbConditions = new HashMap<String, String>();
-
-		action = null;
-		postAction = null;
+		postAction = new ArrayList<String>();
 	}
 		<BEGIN>
 			<INTERFACE> (interfaceName = <IDENTIFIER>.image)
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index e78624c..d652584 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -79,14 +79,14 @@ public class CodeGenerator {
 		codeAdditions.get(construct.file).add(addition);
 		newCode = CodeVariables.generateStaticVarDefine(_semantics, construct);
 		if (newCode.size() > 0) {
-			addition = new CodeAddition(_semantics.getClassEndConstruct().beginLineNum, newCode);
+			addition = new CodeAddition(
+					_semantics.getClassEndConstruct().beginLineNum, newCode);
 			codeAdditions.get(construct.file).add(addition);
 		}
 	}
 
 	// Mainly rename and wrap the interface
-	private void interface2Code(InterfaceConstruct construct)
-			throws InterfaceWrongFormatException {
+	private void interface2Code(InterfaceConstruct construct) {
 		ArrayList<String> newCode = CodeVariables.generateInterfaceWrapper(
 				_semantics, construct);
 		int lineNum = construct.beginLineNum;
@@ -112,7 +112,8 @@ public class CodeGenerator {
 
 	private void CPDefine2Code(CPDefineConstruct construct) {
 		int lineNum = construct.beginLineNum;
-		ArrayList<String> newCode = CodeVariables.generateCPDefine(_semantics, construct);
+		ArrayList<String> newCode = CodeVariables.generateCPDefine(_semantics,
+				construct);
 
 		CodeAddition addition = new CodeAddition(lineNum, newCode);
 		if (!codeAdditions.containsKey(construct.file)) {
@@ -123,7 +124,8 @@ public class CodeGenerator {
 
 	private void CPDefineCheck2Code(CPDefineCheckConstruct construct) {
 		int lineNum = construct.beginLineNum;
-		ArrayList<String> newCode = CodeVariables.generateCPDefineCheck(_semantics, construct);
+		ArrayList<String> newCode = CodeVariables.generateCPDefineCheck(
+				_semantics, construct);
 
 		CodeAddition addition = new CodeAddition(lineNum, newCode);
 		if (!codeAdditions.containsKey(construct.file)) {
@@ -131,11 +133,11 @@ public class CodeGenerator {
 		}
 		codeAdditions.get(construct.file).add(addition);
 	}
-	
+
 	private void EntryPoint2Code(EntryPointConstruct construct) {
 		int lineNum = construct.beginLineNum;
 		ArrayList<String> newCode = new ArrayList<String>();
-		newCode.add(")
+		newCode.addAll(CodeVariables.generateEntryPointInitCall());
 
 		CodeAddition addition = new CodeAddition(lineNum, newCode);
 		if (!codeAdditions.containsKey(construct.file)) {
@@ -143,7 +145,6 @@ public class CodeGenerator {
 		}
 		codeAdditions.get(construct.file).add(addition);
 	}
-	
 
 	public void generateCode() {
 		for (int i = 0; i < _semantics.constructs.size(); i++) {
@@ -151,17 +152,13 @@ public class CodeGenerator {
 			if (construct instanceof GlobalConstruct) {
 				globalConstruct2Code((GlobalConstruct) construct);
 			} else if (construct instanceof InterfaceConstruct) {
-				try {
-					interface2Code((InterfaceConstruct) construct);
-				} catch (InterfaceWrongFormatException e) {
-					e.printStackTrace();
-				}
+				interface2Code((InterfaceConstruct) construct);
 			} else if (construct instanceof PotentialCPDefineConstruct) {
-				// potentialCP2Code(inst);
+				potentialCPDefine2Code((PotentialCPDefineConstruct) construct);
 			} else if (construct instanceof CPDefineConstruct) {
-				// CPDefine2Code(inst);
+				CPDefine2Code((CPDefineConstruct) construct);
 			} else if (construct instanceof CPDefineCheckConstruct) {
-				// CPDefineCheck2Code(inst);
+				CPDefineCheck2Code((CPDefineCheckConstruct) construct);
 			}
 		}
 	}
@@ -172,8 +169,8 @@ public class CodeGenerator {
 		// 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/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 dd815db..8e87cd5 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -163,7 +163,7 @@ public class CodeVariables {
 			String idCode) {
 		ArrayList<String> code = new ArrayList<String>();
 		code.add("static " + IDType + " " + interfaceName + "_id() {");
-		if (idCode != null) {
+		if (!idCode.equals("")) {
 			code.add(DECLARE_DEFINE(IDType, MACRO_ID, idCode));
 		} else {
 			code.add(DECLARE_DEFINE(IDType, MACRO_ID, DEFAULT_ID));
@@ -177,7 +177,7 @@ public class CodeVariables {
 			InterfaceConstruct construct, FunctionHeader header) {
 		String interfaceName = construct.name;
 		ArrayList<String> code = new ArrayList<String>();
-		code.add("bool " + interfaceName + "_check_action(void *info, "
+		code.add("static bool " + interfaceName + "_check_action(void *info, "
 				+ IDType + " " + MACRO_ID + ") {");
 		code.add(DECLARE("bool", "check_passed"));
 		String infoStructType = interfaceName + "_info", infoStructName = "theInfo";
@@ -192,17 +192,28 @@ public class CodeVariables {
 		}
 		code.add("");
 		// __COND_SAT
-		code.add(DECLARE_DEFINE("bool", MACRO_COND, construct.condition));
+		if (!construct.condition.equals("")) {
+			code.add(DECLARE_DEFINE("bool", MACRO_COND, construct.condition));
+		}
 		// Check
-		code.add(ASSIGN("check_passed", construct.check));
-		code.add("if (!check_passed) return false;");
+		if (!construct.check.equals("")) {
+			code.add(ASSIGN("check_passed", construct.check));
+			code.add("if (!check_passed) return false;");
+		}
 		// Action
-		code.addAll(construct.action);
+		if (construct.action.size() > 0) {
+			code.addAll(construct.action);
+		}
 		// Post_check
-		code.add(ASSIGN("check_passed", construct.postCheck));
-		code.add("if (!check_passed) return false;");
+		if (!construct.postCheck.equals("")) {
+			code.add(ASSIGN("check_passed", construct.postCheck));
+			code.add("if (!check_passed) return false;");
+		}
 		// Post_action
-		code.addAll(construct.postAction);
+		if (construct.postAction.size() > 0) {
+			code.addAll(construct.postAction);
+		}
+
 		code.add("}");
 
 		return code;
@@ -223,12 +234,9 @@ public class CodeVariables {
 		funcDefine.set(0, headLine);
 	}
 
-	private static void makeVariablesStatic(ArrayList<String> varDecls) {
-		for (int i = 0; i < varDecls.size(); i++) {
-			String varDecl = varDecls.get(i);
-			varDecl = "static " + varDecl;
-			varDecls.set(i, varDecl);
-		}
+	private static String makeVariablesStatic(VariableDeclaration varDecl) {
+		String res = "static " + varDecl.type + " " + varDecl.name + ";";
+		return res;
 	}
 
 	private static FunctionHeader getFunctionHeader(SemanticsChecker semantics,
@@ -238,6 +246,7 @@ public class CodeVariables {
 		if (headerLine.startsWith("template")) {
 			headerLine = content.get(construct.beginLineNum + 1);
 		}
+		headerLine = headerLine.substring(0, headerLine.indexOf(')') + 1);
 		try {
 			return SpecParser.parseFuncHeader(headerLine);
 		} catch (ParseException e) {
@@ -252,7 +261,7 @@ public class CodeVariables {
 		HashSet<String> allHeaders = getAllHeaders(semantics);
 
 		// All headers needed by the interface decalration
-		newCode.add(COMMENT("/* Include all the header files that contains the interface declaration */"));
+		newCode.add(COMMENT("Include all the header files that contains the interface declaration"));
 		for (String header : allHeaders) {
 			newCode.add(INCLUDE(header));
 		}
@@ -264,6 +273,14 @@ public class CodeVariables {
 		newCode.add("");
 
 		SequentialDefineSubConstruct code = construct.code;
+		// User-defined structs first
+		newCode.add(COMMENT("All other user-defined structs"));
+		ArrayList<ArrayList<String>> declareStructs = code.declareStructs;
+		for (int i = 0; i < declareStructs.size(); i++) {
+			ArrayList<String> declareStruct = declareStructs.get(i);
+			newCode.addAll(declareStruct);
+			newCode.add("");
+		}
 		// User-defined functions
 		newCode.add(COMMENT("All other user-defined functions"));
 		ArrayList<ArrayList<String>> defineFuncs = code.defineFuncs;
@@ -309,7 +326,8 @@ public class CodeVariables {
 		ArrayList<VariableDeclaration> varDecls = code.declareVar;
 		for (int i = 0; i < varDecls.size(); i++) {
 			VariableDeclaration varDecl = varDecls.get(i);
-			newCode.add(DECLARE(varDecl.type, varDecl.name));
+			// Don't forget to make them static
+			newCode.add(makeVariablesStatic(varDecl));
 		}
 
 		newCode.add("");
@@ -335,7 +353,7 @@ public class CodeVariables {
 		newCode.add("}");
 		newCode.add(COMMENT("End of Global construct generation in class"));
 
-		// printCode(newCode);
+		printCode(newCode);
 		return newCode;
 	}
 
@@ -413,6 +431,12 @@ public class CodeVariables {
 		return newCode;
 	}
 
+	public static ArrayList<String> generateEntryPointInitCall() {
+		ArrayList<String> newCode = new ArrayList<String>(1);
+		newCode.add("__sequential_init();");
+		return newCode;
+	}
+
 	public static ArrayList<String> generateInterfaceWrapper(
 			SemanticsChecker semantics, InterfaceConstruct construct) {
 		ArrayList<String> newCode = new ArrayList<String>();
@@ -428,11 +452,12 @@ public class CodeVariables {
 				.get(construct.name));
 		// Rename the interface
 		renameInterface(semantics, construct);
-		InterfaceDefineConstruct defineConstruct = semantics.interfaceName2DefineConstruct.get(interfaceName);
+		InterfaceDefineConstruct defineConstruct = semantics.interfaceName2DefineConstruct
+				.get(interfaceName);
 		if (defineConstruct != null) {
 			renameInterface(semantics, defineConstruct);
 		}
-		
+
 		// Generate wrapper header
 		newCode.add(header.toString() + " {");
 		// Wrapper function body
@@ -544,7 +569,7 @@ public class CodeVariables {
 		newCode.add("}");
 		return newCode;
 	}
-	
+
 	public static ArrayList<String> generateCPDefineCheck(
 			SemanticsChecker semantics, CPDefineCheckConstruct construct) {
 		ArrayList<String> newCode = new ArrayList<String>();
@@ -573,7 +598,7 @@ public class CodeVariables {
 		newCode.add("}");
 		return newCode;
 	}
-	
+
 	public static ArrayList<String> generateCPDefine(
 			SemanticsChecker semantics, CPDefineConstruct construct) {
 		ArrayList<String> newCode = new ArrayList<String>();
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java b/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
index f4e75cc..6d1c41e 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java
@@ -2,4 +2,5 @@ package edu.uci.eecs.specCompiler.codeGenerator;
 
 public class Environment {
 	public static String HOME_DIRECTORY = System.getProperty("user.dir");
+	public static String GENERATED_FILE_DIR = HOME_DIRECTORY + "/" + "output";
 }
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java
index 29080a8..bb6b8e5 100644
--- a/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java
@@ -6,9 +6,13 @@ public class SequentialDefineSubConstruct {
 	public final ArrayList<String> initVar;
 	public final ArrayList<ArrayList<String>> defineFuncs;
 	public final ArrayList<VariableDeclaration> declareVar;
+	public final ArrayList<ArrayList<String>> declareStructs;
 
-	public SequentialDefineSubConstruct(ArrayList<VariableDeclaration> declareVar,
+	public SequentialDefineSubConstruct(
+			ArrayList<ArrayList<String>> declareStruct,
+			ArrayList<VariableDeclaration> declareVar,
 			ArrayList<String> initVar, ArrayList<ArrayList<String>> defineFuncs) {
+		this.declareStructs = declareStruct;
 		this.declareVar = declareVar;
 		this.initVar = initVar;
 		this.defineFuncs = defineFuncs;
@@ -17,6 +21,10 @@ public class SequentialDefineSubConstruct {
 	public String toString() {
 		StringBuffer res = new StringBuffer();
 		res.append("@Sequential_define:\n");
+		res.append("@DeclareStruct:\n");
+		for (int i = 0; i < defineFuncs.size(); i++) {
+			res.append(ParserUtils.array2Str(declareStructs.get(i)) + "\n");
+		}
 		res.append("@DeclareVar:\n");
 		res.append(ParserUtils.array2Str(declareVar));
 		res.append("@InitVar:\n");
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java b/src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java
index 85f3422..2b9af87 100644
--- a/src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java
@@ -1,8 +1,13 @@
 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;
+
 public class SourceFileInfo {
 	public final File file;
 	public final ArrayList<String> content;
@@ -23,4 +28,26 @@ 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 a130d97..8d7a229 100644
--- a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
@@ -60,6 +60,7 @@ public class SpecExtractor {
 		SourceFileInfo srcFileInfo;
 		try {
 			srcFileInfo = SpecParser.ParseFile(file);
+			srcFileInfo.write2File();
 			srcFilesInfo.put(file, srcFileInfo);
 		} catch (ParseException e) {
 			e.printStackTrace();
-- 
2.34.1