X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=funcnode.cc;h=5333bce757eb2f863930e6ad03687c95fd175a21;hb=2ddb5d2c8170fe40d0f056d86e98f22c87c8c722;hp=ccb930fa2581def84d39175859124735f8874dfc;hpb=533aa98d0e7df1435defd4b0698aedf5300a1ad3;p=c11tester.git

diff --git a/funcnode.cc b/funcnode.cc
index ccb930fa..5333bce7 100644
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -1,35 +1,45 @@
+#include "action.h"
+#include "history.h"
 #include "funcnode.h"
+#include "funcinst.h"
+#include "predicate.h"
+#include "concretepredicate.h"
+
+#include "model.h"
 
 FuncNode::FuncNode(ModelHistory * history) :
 	history(history),
-	predicate_tree_initialized(false),
 	exit_count(0),
 	func_inst_map(),
 	inst_list(),
 	entry_insts(),
-//	thrd_read_map(),
-	action_list_buffer()
+	predicate_tree_position(),
+	edge_table(32),
+	out_edges()
 {
 	predicate_tree_entry = new Predicate(NULL, true);
 	predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
 
-	// memory will be reclaimed after each execution
+	// Memories that are reclaimed after each execution
+	action_list_buffer = new SnapList<action_list_t *>();
 	read_locations = new loc_set_t();
+	write_locations = new loc_set_t();
 	val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
+	loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
+
+	//values_may_read_from = new value_set_t();
 }
 
+/* Reallocate snapshotted memories when new executions start */
 void FuncNode::set_new_exec_flag()
 {
-//	for (uint i = 0; i < thrd_read_map.size(); i++)
-//		thrd_read_map[i] = new read_map_t();
-
-	for (mllnode<FuncInst *> * it = inst_list.begin(); it != NULL; it = it->getNext()) {
-		FuncInst * inst = it->getVal();
-		inst->reset_location();
-	}
-
+	action_list_buffer = new SnapList<action_list_t *>();
 	read_locations = new loc_set_t();
+	write_locations = new loc_set_t();
 	val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
+	loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
+
+	//values_may_read_from = new value_set_t();
 }
 
 /* Check whether FuncInst with the same type, position, and location
@@ -53,10 +63,13 @@ void FuncNode::add_inst(ModelAction *act)
 		FuncInst * inst = func_inst_map.get(position);
 
 		ASSERT(inst->get_type() == act->get_type());
+		int curr_execution_number = model->get_execution_number();
 
-		// locations are set to NULL when new executions start
-		if (inst->get_location() == NULL)
+		/* Reset locations when new executions start */
+		if (inst->get_execution_number() != curr_execution_number) {
 			inst->set_location(act->get_location());
+			inst->set_execution_number(curr_execution_number);
+		}
 
 		if (inst->get_location() != act->get_location())
 			inst->not_single_location();
@@ -130,38 +143,54 @@ void FuncNode::update_tree(action_list_t * act_list)
 
 	/* build inst_list from act_list for later processing */
 	func_inst_list_t inst_list;
-	action_list_t read_act_list;
+	action_list_t rw_act_list;
 
 	for (sllnode<ModelAction *> * it = act_list->begin(); it != NULL; it = it->getNext()) {
 		ModelAction * act = it->getVal();
 		FuncInst * func_inst = get_inst(act);
+		void * loc = act->get_location();
 
 		if (func_inst == NULL)
 			continue;
 
 		inst_list.push_back(func_inst);
+		bool act_added = false;
+
+		if (act->is_write()) {
+			rw_act_list.push_back(act);
+			act_added = true;
+			if (!write_locations->contains(loc)) {
+				write_locations->add(loc);
+				history->update_loc_wr_func_nodes_map(loc, this);
+			}
+
+		}
 
-		if (func_inst->is_read()) {
-			read_act_list.push_back(act);
+		if (act->is_read()) {
+			if (!act_added)
+				rw_act_list.push_back(act);
 
-			/* the first time an action reads from some location, import all the values that have
-			 * been written to this location from ModelHistory and notify ModelHistory that this
-			 * FuncNode may read from this location. 
+			/* If func_inst may only read_from a single location, then:
+			 *
+			 * The first time an action reads from some location,
+			 * import all the values that have been written to this
+			 * location from ModelHistory and notify ModelHistory
+			 * that this FuncNode may read from this location.
 			 */
-			void * loc = act->get_location();
-			if (!read_locations->contains(loc)) {
+			if (!read_locations->contains(loc) && func_inst->is_single_location()) {
 				read_locations->add(loc);
 				value_set_t * write_values = write_history->get(loc);
 				add_to_val_loc_map(write_values, loc);
-				history->add_to_loc_func_nodes_map(loc, this);
+				history->update_loc_rd_func_nodes_map(loc, this);
 			}
 		}
 	}
 
 //	model_print("function %s\n", func_name);
+//	print_val_loc_map();
+
 	update_inst_tree(&inst_list);
-	update_predicate_tree(&read_act_list);
-//	deep_update(predicate_tree_entry);
+	update_predicate_tree(&rw_act_list);
 
 //	print_predicate_tree();
 }
@@ -199,77 +228,19 @@ void FuncNode::update_inst_tree(func_inst_list_t * inst_list)
 	}
 }
 
-/* @param tid thread id
- * Store the values read by atomic read actions into thrd_read_map */
-void FuncNode::store_read(ModelAction * act, uint32_t tid)
-{
-/*
-	ASSERT(act);
-
-	void * location = act->get_location();
-	uint64_t read_from_val = act->get_reads_from_value();
-
-	// resize and initialize
-	uint32_t old_size = thrd_read_map.size();
-	if (old_size <= tid) {
-		thrd_read_map.resize(tid + 1);
-		for (uint32_t i = old_size; i < tid + 1;i++)
-			thrd_read_map[i] = new read_map_t();
-	}
-
-	read_map_t * read_map = thrd_read_map[tid];
-	read_map->put(location, read_from_val);
-*/
-}
-
-uint64_t FuncNode::query_last_read(void * location, uint32_t tid)
-{
-/*
-	if (thrd_read_map.size() <= tid)
-		return VALUE_NONE;
-
-	read_map_t * read_map = thrd_read_map[tid];
-
-	// last read value not found
-	if ( !read_map->contains(location) )
-		return VALUE_NONE;
-
-	uint64_t read_val = read_map->get(location);
-	return read_val;
-*/
-}
-
-/* @param tid thread id
- * Reset read map for a thread. This function shall only be called
- * when a thread exits a function
- */
-void FuncNode::clear_read_map(uint32_t tid)
-{
-/*
-	if (thrd_read_map.size() <= tid)
-		return;
-
-	thrd_read_map[tid]->reset();
-*/
-}
-
 void FuncNode::update_predicate_tree(action_list_t * act_list)
 {
 	if (act_list == NULL || act_list->size() == 0)
 		return;
-/*
-	if (predicate_tree_initialized) {
-		return;
-	}
-	predicate_tree_initialized = true;
-*/
-	/* map a FuncInst to the its predicate */
+
+	/* Map a FuncInst to the its predicate */
 	HashTable<FuncInst *, Predicate *, uintptr_t, 0> inst_pred_map(128);
 
-	// number FuncInsts to detect loops
+	// Number FuncInsts to detect loops
 	HashTable<FuncInst *, uint32_t, uintptr_t, 0> inst_id_map(128);
 	uint32_t inst_counter = 0;
 
+	/* Only need to store the locations of read actions */
 	HashTable<void *, ModelAction *, uintptr_t, 0> loc_act_map(128);
 	HashTable<FuncInst *, ModelAction *, uintptr_t, 0> inst_act_map(128);
 
@@ -278,21 +249,25 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 	while (it != NULL) {
 		ModelAction * next_act = it->getVal();
 		FuncInst * next_inst = get_inst(next_act);
-		SnapVector<Predicate *> * unset_predicates = new SnapVector<Predicate *>();
 
-		bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map, unset_predicates);
+		SnapVector<Predicate *> unset_predicates = SnapVector<Predicate *>();
+		bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map, &unset_predicates);
 
-		// no predicate expressions, follow the only branch
-		if (!branch_found && unset_predicates->size() != 0) {
-			ASSERT(unset_predicates->size() == 1);
-			Predicate * one_branch = (*unset_predicates)[0];
-			curr_pred = one_branch;
-			branch_found = true;
-		}
+		// A branch with unset predicate expression is detected
+		if (!branch_found && unset_predicates.size() != 0) {
+			ASSERT(unset_predicates.size() == 1);
+			Predicate * one_branch = unset_predicates[0];
 
-		delete unset_predicates;
+			bool amended = amend_predicate_expr(&curr_pred, next_inst, next_act);
+			if (amended)
+				continue;
+			else {
+				curr_pred = one_branch;
+				branch_found = true;
+			}
+		}
 
-		// detect loops
+		// Detect loops
 		if (!branch_found && inst_id_map.contains(next_inst)) {
 			FuncInst * curr_inst = curr_pred->get_func_inst();
 			uint32_t curr_id = inst_id_map.get(curr_inst);
@@ -309,103 +284,30 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 			}
 		}
 
+		// Generate new branches
 		if (!branch_found) {
-			if ( loc_act_map.contains(next_act->get_location()) ) {
-				ModelAction * last_act = loc_act_map.get(next_act->get_location());
-				FuncInst * last_inst = get_inst(last_act);
-
-				Predicate * new_pred1 = new Predicate(next_inst);
-				new_pred1->add_predicate_expr(EQUALITY, last_inst, true);
-
-				Predicate * new_pred2 = new Predicate(next_inst);
-				new_pred2->add_predicate_expr(EQUALITY, last_inst, false);
-
-				curr_pred->add_child(new_pred1);
-				curr_pred->add_child(new_pred2);
-				new_pred1->set_parent(curr_pred);
-				new_pred2->set_parent(curr_pred);
-
-				uint64_t last_read = last_act->get_reads_from_value();
-				uint64_t next_read = next_act->get_reads_from_value();
-
-				if ( last_read == next_read )
-					curr_pred = new_pred1;
-				else
-					curr_pred = new_pred2;
-			} else if (!next_inst->is_single_location()) {
-				Predicate * new_pred1 = new Predicate(next_inst);
-				new_pred1->add_predicate_expr(NULLITY, NULL, true);
-
-				Predicate * new_pred2 = new Predicate(next_inst);
-				new_pred2->add_predicate_expr(NULLITY, NULL, false);
-
-				curr_pred->add_child(new_pred1);
-				curr_pred->add_child(new_pred2);
-				new_pred1->set_parent(curr_pred);
-				new_pred2->set_parent(curr_pred);
-
-				uint64_t next_read = next_act->get_reads_from_value();
-				bool isnull = ((void*)next_read == NULL);
-				if (isnull)
-					curr_pred = new_pred1;
-				else
-					curr_pred = new_pred2;
-			} else {
-				Predicate * new_pred = new Predicate(next_inst);
-				curr_pred->add_child(new_pred);
-				new_pred->set_parent(curr_pred);
-
-				if (curr_pred->is_entry_predicate())
-					new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
-
-				curr_pred = new_pred;
-			}
+			SnapVector<struct half_pred_expr *> half_pred_expressions;
+			infer_predicates(next_inst, next_act, &loc_act_map, &half_pred_expressions);
+			generate_predicates(&curr_pred, next_inst, &half_pred_expressions);
+			continue;
+		}
+
+		if (next_act->is_write())
+			curr_pred->set_write(true);
+
+		if (next_act->is_read()) {
+			loc_act_map.put(next_act->get_location(), next_act);
 		}
 
+		inst_act_map.put(next_inst, next_act);
 		inst_pred_map.put(next_inst, curr_pred);
 		if (!inst_id_map.contains(next_inst))
 			inst_id_map.put(next_inst, inst_counter++);
 
-		loc_act_map.put(next_act->get_location(), next_act);
-		inst_act_map.put(next_inst, next_act);
 		it = it->getNext();
 	}
 }
 
-void FuncNode::deep_update(Predicate * curr_pred)
-{
-	FuncInst * func_inst = curr_pred->get_func_inst();
-	if (func_inst != NULL && !func_inst->is_single_location()) {
-		bool has_null_pred = false;
-		PredExprSet * pred_expressions = curr_pred->get_pred_expressions();
-		PredExprSetIter * pred_expr_it = pred_expressions->iterator();
-		while (pred_expr_it->hasNext()) {
-			pred_expr * pred_expression = pred_expr_it->next();
-			if (pred_expression->token == NULLITY) {
-				has_null_pred = true;
-				break;
-			}
-		}
-
-		if (!has_null_pred) {
-//			func_inst->print();
-			Predicate * another_branch = new Predicate(func_inst);
-			another_branch->copy_predicate_expr(curr_pred);
-			another_branch->add_predicate_expr(NULLITY, NULL, 1);
-			curr_pred->add_predicate_expr(NULLITY, NULL, 0);
-
-			Predicate * parent = curr_pred->get_parent();
-			parent->add_child(another_branch);
-		}
-	}
-
-	ModelVector<Predicate *> * branches = curr_pred->get_children();
-	for (uint i = 0; i < branches->size(); i++) {
-		Predicate * branch = (*branches)[i];
-		deep_update(branch);
-	}
-}
-
 /* Given curr_pred and next_inst, find the branch following curr_pred that
  * contains next_inst and the correct predicate. 
  * @return true if branch found, false otherwise.
@@ -422,43 +324,37 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
 		if (branch->get_func_inst() != next_inst)
 			continue;
 
-		/* check against predicate expressions */
+		/* Check against predicate expressions */
 		bool predicate_correct = true;
 		PredExprSet * pred_expressions = branch->get_pred_expressions();
-		PredExprSetIter * pred_expr_it = pred_expressions->iterator();
 
+		/* Only read and rmw actions my have unset predicate expressions */
 		if (pred_expressions->getSize() == 0) {
 			predicate_correct = false;
 			unset_predicates->push_back(branch);
 		}
 
-		while (pred_expr_it->hasNext()) {
-			pred_expr * pred_expression = pred_expr_it->next();
-			uint64_t last_read, next_read;
+		ConcretePredicate * concrete_pred = branch->evaluate(inst_act_map, next_act->get_tid());
+		SnapVector<struct concrete_pred_expr> * concrete_exprs = concrete_pred->getExpressions();
+		for (uint i = 0; i < concrete_exprs->size(); i++) {
+			struct concrete_pred_expr concrete = (*concrete_exprs)[i];
+			uint64_t next_read;
 			bool equality;
 
-			switch(pred_expression->token) {
+			switch (concrete.token) {
 				case NOPREDICATE:
 					predicate_correct = true;
 					break;
 				case EQUALITY:
-					FuncInst * to_be_compared;
-					ModelAction * last_act;
-
-					to_be_compared = pred_expression->func_inst;
-					last_act = inst_act_map->get(to_be_compared);
-
-					last_read = last_act->get_reads_from_value();
 					next_read = next_act->get_reads_from_value();
-					equality = (last_read == next_read);
-					if (equality != pred_expression->value)
+					equality = (next_read == concrete.value);
+					if (equality != concrete.equality)
 						predicate_correct = false;
-
 					break;
 				case NULLITY:
 					next_read = next_act->get_reads_from_value();
 					equality = ((void*)next_read == NULL);
-					if (equality != pred_expression->value)
+					if (equality != concrete.equality)
 						predicate_correct = false;
 					break;
 				default:
@@ -467,6 +363,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
 					break;
 			}
 		}
+		delete concrete_pred;
 
 		if (predicate_correct) {
 			*curr_pred = branch;
@@ -478,6 +375,134 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
 	return branch_found;
 }
 
+/* Infer predicate expressions, which are generated in FuncNode::generate_predicates */
+void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
+	HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map,
+	SnapVector<struct half_pred_expr *> * half_pred_expressions)
+{
+	void * loc = next_act->get_location();
+
+	if (next_inst->is_read()) {
+		/* read + rmw */
+		if ( loc_act_map->contains(loc) ) {
+			ModelAction * last_act = loc_act_map->get(loc);
+			FuncInst * last_inst = get_inst(last_act);
+			struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
+			half_pred_expressions->push_back(expression);
+		} else if ( next_inst->is_single_location() ){
+			loc_set_t * loc_may_equal = loc_may_equal_map->get(loc);
+
+			if (loc_may_equal != NULL) {
+				loc_set_iter * loc_it = loc_may_equal->iterator();
+				while (loc_it->hasNext()) {
+					void * neighbor = loc_it->next();
+					if (loc_act_map->contains(neighbor)) {
+						ModelAction * last_act = loc_act_map->get(neighbor);
+						FuncInst * last_inst = get_inst(last_act);
+
+						struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
+						half_pred_expressions->push_back(expression);
+					}
+				}
+			}
+		} else {
+			// next_inst is not single location
+			uint64_t read_val = next_act->get_reads_from_value();
+
+			// only infer NULLITY predicate when it is actually NULL.
+			if ( (void*)read_val == NULL) {
+				struct half_pred_expr * expression = new half_pred_expr(NULLITY, NULL);
+				half_pred_expressions->push_back(expression);
+			}
+		}
+	} else {
+		/* Pure writes */
+		// TODO: do anything here?
+	}
+}
+
+/* Able to generate complex predicates when there are multiple predciate expressions */
+void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst,
+	SnapVector<struct half_pred_expr *> * half_pred_expressions)
+{
+	if (half_pred_expressions->size() == 0) {
+		Predicate * new_pred = new Predicate(next_inst);
+		(*curr_pred)->add_child(new_pred);
+		new_pred->set_parent(*curr_pred);
+
+		/* entry predicates and predicates containing pure write actions
+		 * have no predicate expressions */
+		if ( (*curr_pred)->is_entry_predicate() )
+			new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
+		else if (next_inst->is_write()) {
+			/* next_inst->is_write() <==> pure writes */
+			new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
+		}
+
+		return;
+	}
+
+	SnapVector<Predicate *> predicates;
+
+	struct half_pred_expr * half_expr = (*half_pred_expressions)[0];
+	predicates.push_back(new Predicate(next_inst));
+	predicates.push_back(new Predicate(next_inst));
+
+	predicates[0]->add_predicate_expr(half_expr->token, half_expr->func_inst, true);
+	predicates[1]->add_predicate_expr(half_expr->token, half_expr->func_inst, false);
+
+	for (uint i = 1; i < half_pred_expressions->size(); i++) {
+		half_expr = (*half_pred_expressions)[i];
+
+		uint old_size = predicates.size();
+		for (uint j = 0; j < old_size; j++) {
+			Predicate * pred = predicates[j];
+			Predicate * new_pred = new Predicate(next_inst);
+			new_pred->copy_predicate_expr(pred);
+
+			pred->add_predicate_expr(half_expr->token, half_expr->func_inst, true);
+			new_pred->add_predicate_expr(half_expr->token, half_expr->func_inst, false);
+
+			predicates.push_back(new_pred);
+		}
+	}
+
+	for (uint i = 0; i < predicates.size(); i++) {
+		Predicate * pred= predicates[i];
+		(*curr_pred)->add_child(pred);
+		pred->set_parent(*curr_pred);
+	}
+
+	/* Free memories allocated by infer_predicate */
+	for (uint i = 0; i < half_pred_expressions->size(); i++) {
+		struct half_pred_expr * tmp = (*half_pred_expressions)[i];
+		snapshot_free(tmp);
+	}
+}
+
+/* Amend predicates that contain no predicate expressions. Currenlty only amend with NULLITY predicates */
+bool FuncNode::amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act)
+{
+	// there should only be only child
+	Predicate * unset_pred = (*curr_pred)->get_children()->back();
+	uint64_t read_val = next_act->get_reads_from_value();
+
+	// only generate NULLITY predicate when it is actually NULL.
+	if ( !next_inst->is_single_location() && (void*)read_val == NULL ) {
+		Predicate * new_pred = new Predicate(next_inst);
+
+		(*curr_pred)->add_child(new_pred);
+		new_pred->set_parent(*curr_pred);
+
+		unset_pred->add_predicate_expr(NULLITY, NULL, false);
+		new_pred->add_predicate_expr(NULLITY, NULL, true);
+
+		return true;
+	}
+
+	return false;
+}
+
 void FuncNode::add_to_val_loc_map(uint64_t val, void * loc)
 {
 	loc_set_t * locations = val_loc_map->get(val);
@@ -487,21 +512,16 @@ void FuncNode::add_to_val_loc_map(uint64_t val, void * loc)
 		val_loc_map->put(val, locations);
 	}
 
+	update_loc_may_equal_map(loc, locations);
 	locations->add(loc);
-
-/*
-	model_print("val %llx: ", val);
-	loc_set_iter * it = locations->iterator();
-	while (it->hasNext()) {
-		void * location = it->next();
-		model_print("%p ", location);
-	}
-	model_print("\n");
-*/
+	// values_may_read_from->add(val);
 }
 
 void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc)
 {
+	if (values == NULL)
+		return;
+
 	value_set_iter * it = values->iterator();
 	while (it->hasNext()) {
 		uint64_t val = it->next();
@@ -509,30 +529,184 @@ void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc)
 	}
 }
 
+void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations)
+{
+	if ( old_locations->contains(new_loc) )
+		return;
 
-void FuncNode::print_predicate_tree()
+	loc_set_t * neighbors = loc_may_equal_map->get(new_loc);
+
+	if (neighbors == NULL) {
+		neighbors = new loc_set_t();
+		loc_may_equal_map->put(new_loc, neighbors);
+	}
+
+	loc_set_iter * loc_it = old_locations->iterator();
+	while (loc_it->hasNext()) {
+		// new_loc: { old_locations, ... }
+		void * member = loc_it->next();
+		neighbors->add(member);
+
+		// for each i in old_locations, i : { new_loc, ... }
+		loc_set_t * _neighbors = loc_may_equal_map->get(member);
+		if (_neighbors == NULL) {
+			_neighbors = new loc_set_t();
+			loc_may_equal_map->put(member, _neighbors);
+		}
+		_neighbors->add(new_loc);
+	}
+}
+
+/* Every time a thread enters a function, set its position to the predicate tree entry */
+void FuncNode::init_predicate_tree_position(thread_id_t tid)
 {
-	model_print("digraph function_%s {\n", func_name);
-	predicate_tree_entry->print_pred_subtree();
-	model_print("}\n");	// end of graph
+	int thread_id = id_to_int(tid);
+	if (predicate_tree_position.size() <= (uint) thread_id)
+		predicate_tree_position.resize(thread_id + 1);
+
+	predicate_tree_position[thread_id] = predicate_tree_entry;
+}
+
+void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred)
+{
+	int thread_id = id_to_int(tid);
+	predicate_tree_position[thread_id] = pred;
+}
+
+/* @return The position of a thread in a predicate tree */
+Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid)
+{
+	int thread_id = id_to_int(tid);
+	return predicate_tree_position[thread_id];
+}
+
+/* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */
+void FuncNode::init_inst_act_map(thread_id_t tid)
+{
+	int thread_id = id_to_int(tid);
+	SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
+	uint old_size = thrd_inst_act_map->size();
+
+	if (thrd_inst_act_map->size() <= (uint) thread_id) {
+		uint new_size = thread_id + 1;
+		thrd_inst_act_map->resize(new_size);
+
+		for (uint i = old_size; i < new_size; i++)
+			(*thrd_inst_act_map)[i] = new inst_act_map_t(128);
+	}
+}
+
+/* Reset elements of thrd_inst_act_map when threads exit functions */
+void FuncNode::reset_inst_act_map(thread_id_t tid)
+{
+	int thread_id = id_to_int(tid);
+	SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
+
+	inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
+	map->reset();
+}
+
+void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act)
+{
+	int thread_id = id_to_int(tid);
+	SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
+
+	inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
+	FuncInst * read_inst = get_inst(read_act);
+	map->put(read_inst, read_act);
 }
 
-/* @param tid thread id
- * Print the values read by the last read actions for each memory location
+inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid)
+{
+	int thread_id = id_to_int(tid);
+	SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
+
+	return (*thrd_inst_act_map)[thread_id];
+}
+
+/* Add FuncNodes that this node may follow */
+void FuncNode::add_out_edge(FuncNode * other)
+{
+	if ( !edge_table.contains(other) ) {
+		edge_table.put(other, OUT_EDGE);
+		out_edges.push_back(other);
+		return;
+	}
+
+	edge_type_t edge = edge_table.get(other);
+	if (edge == IN_EDGE) {
+		edge_table.put(other, BI_EDGE);
+		out_edges.push_back(other);
+	}
+}
+
+/* Compute the distance between this FuncNode and the target node.
+ * Return -1 if the target node is unreachable or the actual distance
+ * is greater than max_step.
  */
-/*
-void FuncNode::print_last_read(uint32_t tid)
+int FuncNode::compute_distance(FuncNode * target, int max_step)
 {
-	ASSERT(thrd_read_map.size() > tid);
-	read_map_t * read_map = thrd_read_map[tid];
+	if (target == NULL)
+		return -1;
+	else if (target == this)
+		return 0;
 
-	mllnode<void *> * it;
-	for (it = read_locations.begin();it != NULL;it=it->getNext()) {
-		if ( !read_map->contains(it->getVal()) )
-			break;
+	SnapList<FuncNode *> queue;
+	HashTable<FuncNode *, int, uintptr_t, 0> distances(128);
+
+	queue.push_back(this);
+	distances.put(this, 0);
+
+	while (!queue.empty()) {
+		FuncNode * curr = queue.front();
+		queue.pop_front();
+		int dist = distances.get(curr);
+
+		if (max_step <= dist)
+			return -1;
+
+		ModelList<FuncNode *> * outEdges = curr->get_out_edges();
+		mllnode<FuncNode *> * it;
+		for (it = outEdges->begin(); it != NULL; it = it->getNext()) {
+			FuncNode * out_node = it->getVal();
+
+			/* This node has not been visited before */
+			if ( !distances.contains(out_node) ) {
+				if (out_node == target)
+					return dist + 1;
 
-		uint64_t read_val = read_map->get(it->getVal());
-		model_print("last read of thread %d at %p: 0x%x\n", tid, it->getVal(), read_val);
+				queue.push_back(out_node);
+				distances.put(out_node, dist + 1);
+			}
+		}
 	}
+
+	/* Target node is unreachable */
+	return -1;
+}
+
+void FuncNode::print_predicate_tree()
+{
+	model_print("digraph function_%s {\n", func_name);
+	predicate_tree_entry->print_pred_subtree();
+	model_print("}\n");	// end of graph
 }
+
+void FuncNode::print_val_loc_map()
+{
+/*
+	value_set_iter * val_it = values_may_read_from->iterator();
+	while (val_it->hasNext()) {
+		uint64_t value = val_it->next();
+		model_print("val %llx: ", value);
+
+		loc_set_t * locations = val_loc_map->get(value);
+		loc_set_iter * loc_it = locations->iterator();
+		while (loc_it->hasNext()) {
+			void * location = loc_it->next();
+			model_print("%p ", location);
+		}
+		model_print("\n");
+	}
 */
+}