only generate NULLITY predicate when it has ever been NULL; able to amend predicates...

diff --git a/funcnode.cc b/funcnode.cc
index 73363c7ffc3fc175eccf1691fd26afabfc62d60d..6402a9aee732fd7c71de36284246e7619c2759a2 100644 (file)
--- 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 9cf082bd723234957b50cf2eb1a03b5ecba24544..e757b650df5770c41fc627551d300c9bab839546 100644 (file)
--- 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;