From 897371c3246cdfaa949c943b9b8a1d075360d6fc Mon Sep 17 00:00:00 2001
From: weiyu <weiyuluo1232@gmail.com>
Date: Thu, 22 Aug 2019 12:53:17 -0700
Subject: [PATCH] deduce which locations may share the same value from
 val_loc_map

---
 funcnode.cc | 62 +++++++++++++++++++++++++++++++++++++++++++----------
 funcnode.h  | 15 ++++++++++---
 2 files changed, 63 insertions(+), 14 deletions(-)

diff --git a/funcnode.cc b/funcnode.cc
index ccb930fa..e79c95df 100644
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -16,8 +16,11 @@ FuncNode::FuncNode(ModelHistory * history) :
 	// memory will be reclaimed after each execution
 	read_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 some snapshotted memories when new executions start */
 void FuncNode::set_new_exec_flag()
 {
 //	for (uint i = 0; i < thrd_read_map.size(); i++)
@@ -30,6 +33,8 @@ void FuncNode::set_new_exec_flag()
 
 	read_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
@@ -158,7 +163,9 @@ void FuncNode::update_tree(action_list_t * act_list)
 		}
 	}
 
-//	model_print("function %s\n", func_name);
+	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);
@@ -487,17 +494,9 @@ 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)
@@ -509,6 +508,30 @@ 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)
+{
+	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);
+	}
+}
 
 void FuncNode::print_predicate_tree()
 {
@@ -517,6 +540,23 @@ void FuncNode::print_predicate_tree()
 	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");
+	}
+}
+
 /* @param tid thread id
  * Print the values read by the last read actions for each memory location
  */
diff --git a/funcnode.h b/funcnode.h
index 6e08fc26..277e5256 100644
--- a/funcnode.h
+++ b/funcnode.h
@@ -49,8 +49,10 @@ public:
 
 	void add_to_val_loc_map(uint64_t val, void * loc);
 	void add_to_val_loc_map(value_set_t * values, void * loc);
+	void update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations);
 
 	void print_predicate_tree();
+	void print_val_loc_map();
 	void print_last_read(uint32_t tid);
 
 	MEMALLOC
@@ -68,20 +70,27 @@ private:
 	 */
 	HashTable<const char *, FuncInst *, uintptr_t, 4, model_malloc, model_calloc, model_free> func_inst_map;
 
-	/* list of all atomic actions in this function */
+	/* List of all atomic actions in this function */
 	func_inst_list_mt inst_list;
 
-	/* possible entry atomic actions in this function */
+	/* Possible entry atomic actions in this function */
 	func_inst_list_mt entry_insts;
 
 	/* Store the values read by atomic read actions per memory location for each thread */
 	//ModelVector<read_map_t *> thrd_read_map;
 
-	/* store action_lists when calls to update_tree are deferred */
+	/* Store action_lists when calls to update_tree are deferred */
 	ModelList<action_list_t *> action_list_buffer;
 
+	/* read_locations: set of locations read by this FuncNode
+	 * val_loc_map: keep track of locations that have the same values written to;
+	 * loc_may_equal_map: deduced from val_loc_map;
+	 */
+
 	loc_set_t * read_locations;
 	HashTable<uint64_t, loc_set_t *, uint64_t, 0> * val_loc_map;
+	HashTable<void *, loc_set_t *, uintptr_t, 0> * loc_may_equal_map;
+	value_set_t * values_may_read_from;
 };
 
 #endif /* __FUNCNODE_H__ */
-- 
2.34.1