From df978540810be6de9db3248f383d819b21ca1f79 Mon Sep 17 00:00:00 2001
From: weiyu <weiyuluo1232@gmail.com>
Date: Fri, 23 Aug 2019 17:02:08 -0700
Subject: [PATCH] only generate NULLITY predicate when it has ever been NULL;
 able to amend predicates that contain no predicate expressions

---
 funcnode.cc | 56 +++++++++++++++++++++++++++++++++++++++++------------
 funcnode.h  |  3 +--
 2 files changed, 45 insertions(+), 14 deletions(-)

diff --git a/funcnode.cc b/funcnode.cc
index 73363c7f..6402a9ae 100644
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -279,19 +279,23 @@ 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;
-		}
+		// no predicate expressions
+		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
 		if (!branch_found && inst_id_map.contains(next_inst)) {
@@ -330,6 +334,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 						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);
 						}
@@ -337,8 +342,13 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 				} 
 			} else {
 				// next_inst is not single location
-				struct half_pred_expr * expression = new half_pred_expr(NULLITY, NULL);
-				half_pred_expressions.push_back(expression);
+				uint64_t read_val = next_act->get_reads_from_value();
+
+				// only generate 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);
+				}
 			}
 
 			if (half_pred_expressions.size() == 0) {
@@ -477,6 +487,28 @@ void FuncNode::generate_predicate(Predicate ** curr_pred, FuncInst * next_inst,
 	}
 }
 
+/* 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)
 {
diff --git a/funcnode.h b/funcnode.h
index 9cf082bd..e757b650 100644
--- a/funcnode.h
+++ b/funcnode.h
@@ -37,10 +37,10 @@ public:
 	uint64_t query_last_read(void * location, uint32_t tid);
 	void clear_read_map(uint32_t tid);
 
-	/* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */
 	void update_predicate_tree(action_list_t * act_list);
 	bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable<FuncInst *, ModelAction *, uintptr_t, 0>* inst_act_map, SnapVector<Predicate *> * unset_predicates);
 	void generate_predicate(Predicate ** curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
+	bool amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act);
 
 	void incr_exit_count() { exit_count++; }
 	uint32_t get_exit_count() { return exit_count; }
@@ -86,7 +86,6 @@ private:
 	 * 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;
-- 
2.34.1