X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=funcnode.cc;h=e08ca1b850f8a0f3239bdef7fd785677acbd0745;hp=19601fac5c4f3bd62882f8ba8456afb8ad36af0f;hb=35ebf30f42f46d47fbec1db62acc453733dfb2e1;hpb=3594ff85c07e29afe077fd9005200e0342991787

diff --git a/funcnode.cc b/funcnode.cc
index 19601fac..e08ca1b8 100644
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -2,19 +2,21 @@
 
 FuncNode::FuncNode(ModelHistory * history) :
 	history(history),
-	predicate_tree_initialized(false),
 	exit_count(0),
 	func_inst_map(),
 	inst_list(),
 	entry_insts(),
-	predicate_tree_position()
+	predicate_tree_position(),
+	edge_table(32),
+	out_edges()
 {
 	predicate_tree_entry = new Predicate(NULL, true);
 	predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
 
-	// memories that are 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>();
 	thrd_inst_act_map = new SnapVector<inst_act_map_t *>();
@@ -32,6 +34,7 @@ void FuncNode::set_new_exec_flag()
 
 	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 *>();
@@ -142,23 +145,28 @@ void FuncNode::update_tree(action_list_t * 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;
 
-		/* NOTE: for rmw actions, func_inst and act may have different
-		 * action types because of action type conversion in ModelExecution
-		 * func_inst->is_write() <==> pure writes (excluding rmw) */
-		if (func_inst->is_write()) {
-			// model_print("write detected\n");
+		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);
+			}
+
 		}
 
-		/* func_inst->is_read() <==> read + rmw */
-		if (func_inst->is_read()) {
-			rw_act_list.push_back(act);
+		if (act->is_read()) {
+			if (!act_added)
+				rw_act_list.push_back(act);
+
 			/* If func_inst may only read_from a single location, then:
 			 *
 			 * The first time an action reads from some location,
@@ -166,12 +174,11 @@ void FuncNode::update_tree(action_list_t * act_list)
 			 * location from ModelHistory and notify ModelHistory
 			 * that this FuncNode may read from this location.
 			 */
-			void * loc = act->get_location();
 			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_func_nodes_map(loc, this);
 			}
 		}
 	}
@@ -223,13 +230,14 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 	if (act_list == NULL || act_list->size() == 0)
 		return;
 
-	/* 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);
 
@@ -284,12 +292,15 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 		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();
 	}
 }
@@ -464,6 +475,12 @@ void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst,
 		(*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 */
@@ -603,6 +620,22 @@ inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid)
 	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);
+	}
+}
+
 void FuncNode::print_predicate_tree()
 {
 	model_print("digraph function_%s {\n", func_name);