defer the initial update of predicate tree for a better quality tree; generate nullit...

diff --git a/funcnode.cc b/funcnode.cc
index 940a8f7844ee17812e2562caf586ee96126942d4..3a7e4dbe014d116fbd95ba9b649cd6efa31ed361 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -3,6 +3,7 @@
 FuncNode::FuncNode() :
        predicate_tree_initialized(false),
        predicate_tree_entry(new Predicate(NULL, true)),
+       exit_count(0),
        func_inst_map(),
        inst_list(),
        entry_insts(),
@@ -239,25 +240,6 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                if (!branch_found && unset_predicates->size() != 0) {
                        ASSERT(unset_predicates->size() == 1);
                        Predicate * one_branch = (*unset_predicates)[0];
-
-                       if (!next_inst->is_single_location()) {
-                               Predicate * another_branch = new Predicate(next_inst);
-                               // another_branch->copy_predicate_expr(one_branch);
-
-                               uint64_t next_read = next_act->get_reads_from_value();
-                               bool isnull = ((void*)next_read == NULL);
-                               if (isnull) {
-                                       one_branch->add_predicate_expr(NULLITY, NULL, 1);
-                                       another_branch->add_predicate_expr(NULLITY, NULL, 0);
-                               } else {
-                                       another_branch->add_predicate_expr(NULLITY, NULL, 1);
-                                       one_branch->add_predicate_expr(NULLITY, NULL, 0);
-                               }
-
-                               curr_pred->add_child(another_branch);
-                               another_branch->set_parent(curr_pred);
-                       }
-
                        curr_pred = one_branch;
                        branch_found = true;
                }
@@ -308,6 +290,24 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                                        curr_pred = new_pred1;
                                else
                                        curr_pred = new_pred2;
+                       } else if (!next_inst->is_single_location()) {
+                               Predicate * new_pred1 = new Predicate(next_inst);
+                               new_pred1->add_predicate_expr(NULLITY, NULL, true);
+
+                               Predicate * new_pred2 = new Predicate(next_inst);
+                               new_pred2->add_predicate_expr(NULLITY, NULL, false);
+
+                               curr_pred->add_child(new_pred1);
+                               curr_pred->add_child(new_pred2);
+                               new_pred1->set_parent(curr_pred);
+                               new_pred2->set_parent(curr_pred);
+
+                               uint64_t next_read = next_act->get_reads_from_value();
+                               bool isnull = ((void*)next_read == NULL);
+                               if (isnull)
+                                       curr_pred = new_pred1;
+                               else
+                                       curr_pred = new_pred2;
                        } else {
                                Predicate * new_pred = new Predicate(next_inst);
                                curr_pred->add_child(new_pred);
@@ -353,7 +353,6 @@ void FuncNode::deep_update(Predicate * curr_pred)
 
                        Predicate * parent = curr_pred->get_parent();
                        parent->add_child(another_branch);
-//                     another_branch.add_children(i);
                }
        }
 

diff --git a/funcnode.h b/funcnode.h
index c4bf9fed6b1f97e7f21314e60dbf598d36751221..bbc14db11617cfaa14b1ec7248c891b06ef47265 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -39,8 +39,13 @@ public:
        void update_predicate_tree(action_list_t * act_list);
        void deep_update(Predicate * pred);
        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 print_predicate_tree();
 
+       void incr_exit_count() { exit_count++; }
+       uint32_t get_exit_count() { return exit_count; }
+
+       ModelList<action_list_t *> * get_action_list_buffer() { return &action_list_buffer; }
+
+       void print_predicate_tree();
        void print_last_read(uint32_t tid);
 
        MEMALLOC
@@ -50,6 +55,8 @@ private:
        bool predicate_tree_initialized;
        Predicate * predicate_tree_entry;       // a dummy node whose children are the real entries
 
+       uint32_t exit_count;
+
        /* Use source line number as the key of hashtable, to check if
         * atomic operation with this line number has been added or not
         */
@@ -63,6 +70,8 @@ private:
 
        /* Store the values read by atomic read actions per memory location for each thread */
        ModelVector<read_map_t *> thrd_read_map;
+
+       ModelList<action_list_t *> action_list_buffer;
 };
 
 #endif /* __FUNCNODE_H__ */

diff --git a/history.cc b/history.cc
index 89d111199d95bf3e7e491fc4192adc68c7651529..0f90e12662648be6995bef48933d153223b40bf1 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -65,9 +65,23 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
                FuncNode * func_node = func_nodes[func_id];
                func_node->clear_read_map(tid);
 
-               // model_print("hello function %s and thread %d\n", func_node->get_func_name(), tid);
                action_list_t * curr_act_list = func_act_lists->back();
-               func_node->update_tree(curr_act_list);
+               func_node->incr_exit_count();
+
+               /* defer the processing of curr_act_list until the function has exits a few times 
+                * (currently 2 times) so that more information can be gathered to infer nullity predicates.
+                */
+               if (func_node->get_exit_count() >= 2) {
+                       ModelList<action_list_t *> * action_list_buffer = func_node->get_action_list_buffer();
+                       while (action_list_buffer->size() > 0) {
+                               action_list_t * act_list = action_list_buffer->back();
+                               action_list_buffer->pop_back();
+                               func_node->update_tree(act_list);
+                       }
+
+                       func_node->update_tree(curr_act_list);
+               } else
+                       func_node->get_action_list_buffer()->push_front(curr_act_list);
 
                (*thrd_func_list)[id].pop_back();
                func_act_lists->pop_back();