X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=funcnode.cc;h=bf8971bdfbf4de48eba3a53a20323358f3594477;hp=af268aad0d0cf95c3fbca6d8b32f134dc6f2af1a;hb=0acd7ac85bd6004e53e1283a2900ffef7debeed8;hpb=d8706290996922a019a5c084b858d4a7cf82cdda

diff --git a/funcnode.cc b/funcnode.cc
index af268aad..bf8971bd 100644
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -5,6 +5,8 @@
 #include "predicate.h"
 #include "concretepredicate.h"
 
+#include "model.h"
+
 FuncNode::FuncNode(ModelHistory * history) :
 	history(history),
 	exit_count(0),
@@ -24,7 +26,6 @@ FuncNode::FuncNode(ModelHistory * history) :
 	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>();
-	thrd_inst_act_map = new SnapVector<inst_act_map_t *>();
 
 	//values_may_read_from = new value_set_t();
 }
@@ -32,17 +33,11 @@ FuncNode::FuncNode(ModelHistory * history) :
 /* Reallocate snapshotted memories when new executions start */
 void FuncNode::set_new_exec_flag()
 {
-	for (mllnode<FuncInst *> * it = inst_list.begin(); it != NULL; it = it->getNext()) {
-		FuncInst * inst = it->getVal();
-		inst->unset_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>();
-	thrd_inst_act_map = new SnapVector<inst_act_map_t *>();
 
 	//values_may_read_from = new value_set_t();
 }
@@ -68,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();
@@ -183,7 +181,7 @@ void FuncNode::update_tree(action_list_t * act_list)
 				read_locations->add(loc);
 				value_set_t * write_values = write_history->get(loc);
 				add_to_val_loc_map(write_values, loc);
-				history->update_loc_func_nodes_map(loc, this);
+				history->update_loc_rd_func_nodes_map(loc, this);
 			}
 		}
 	}
@@ -365,6 +363,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
 					break;
 			}
 		}
+		delete concrete_pred;
 
 		if (predicate_correct) {
 			*curr_pred = branch;
@@ -585,6 +584,7 @@ Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid)
 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) {
@@ -600,6 +600,8 @@ void FuncNode::init_inst_act_map(thread_id_t tid)
 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();
 }
@@ -607,6 +609,8 @@ void FuncNode::reset_inst_act_map(thread_id_t tid)
 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);
@@ -615,6 +619,8 @@ void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act)
 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];
 }
 
@@ -634,6 +640,40 @@ void FuncNode::add_out_edge(FuncNode * other)
 	}
 }
 
+int FuncNode::compute_distance(FuncNode * target, int max_step)
+{
+	SnapList<FuncNode *> queue;
+	HashTable<FuncNode *, int, uintptr_t, 0> distances;
+
+	int dist = 0;
+	queue.push_back(this);
+	distances.put(this, dist);
+
+	while (!queue.empty()) {
+		FuncNode * curr = queue.front();
+		queue.pop_front();
+
+		if (curr == target)
+			return dist;
+		else if (max_step < dist)
+			return -1;
+
+		dist++;
+		ModelList<FuncNode *> * outEdges = curr->get_out_edges();
+		mllnode<FuncNode *> * it;
+		for (it = outEdges->begin(); it != NULL; it = it->getNext()) {
+			FuncNode * out_node = it->getVal();
+			if ( !distances.contains(out_node) ) {
+				queue.push_back(out_node);
+				distances.put(out_node, dist);
+			}
+		}
+	}
+
+	/* Target node is unreachable */
+	return -1;
+}
+
 void FuncNode::print_predicate_tree()
 {
 	model_print("digraph function_%s {\n", func_name);