X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=funcnode.cc;h=b28fbd5bb5c8b925af9cc0573be8cecec1cd16b6;hp=e05e84f7367c418eb33296fcf459d35a74149382;hb=c0c4fcf47d8209da26e686b308d8c20ffc8220d3;hpb=9c8fe6c437d1a43d2d6170ea2842f52555b62a11

diff --git a/funcnode.cc b/funcnode.cc
index e05e84f7..b28fbd5b 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),
@@ -31,11 +33,6 @@ 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();
@@ -66,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();
@@ -139,7 +139,7 @@ void FuncNode::update_tree(action_list_t * act_list)
 	if (act_list == NULL || act_list->size() == 0)
 		return;
 
-	HashTable<void *, value_set_t *, uintptr_t, 4> * write_history = history->getWriteHistory();
+	HashTable<void *, value_set_t *, uintptr_t, 0> * write_history = history->getWriteHistory();
 
 	/* build inst_list from act_list for later processing */
 	func_inst_list_t inst_list;
@@ -181,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);
 			}
 		}
 	}
@@ -640,6 +640,51 @@ void FuncNode::add_out_edge(FuncNode * 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.
+ */
+int FuncNode::compute_distance(FuncNode * target, int max_step)
+{
+	if (target == NULL)
+		return -1;
+	else if (target == this)
+		return 0;
+
+	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;
+
+				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);