restructure code and working on deconstructors

diff --git a/funcnode.cc b/funcnode.cc
index 26dfe5c9723c36d02f01cc25ad7a8011ca7bcf11..aa99e9728c61f9cd6acbbe1583541487f2a6a7d4 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -317,95 +317,27 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                }
 
                if (!branch_found) {
-                       if ( loc_act_map.contains(next_act->get_location()) ) {
-                               ModelAction * last_act = loc_act_map.get(next_act->get_location());
-                               FuncInst * last_inst = get_inst(last_act);
-
-                               Predicate * new_pred1 = new Predicate(next_inst);
-                               new_pred1->add_predicate_expr(EQUALITY, last_inst, true);
-
-                               Predicate * new_pred2 = new Predicate(next_inst);
-                               new_pred2->add_predicate_expr(EQUALITY, last_inst, 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 last_read = last_act->get_reads_from_value();
-                               uint64_t next_read = next_act->get_reads_from_value();
-
-                               if ( last_read == next_read )
-                                       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 {
-                               bool test = false;
-                               void * loc = next_act->get_location();
-                               loc_set_t * loc_may_equal = loc_may_equal_map->get(loc);
-                               if (loc_may_equal != NULL) {
-                                       loc_set_iter * loc_it = loc_may_equal->iterator();
-                                       while (loc_it->hasNext()) {
-                                               void * neighbor = loc_it->next();
-                                               if (loc_act_map.contains(neighbor)) {
-                                                       model_print("loc %p may eqaul to loc %p\n", loc, neighbor);
-                                                       ModelAction * last_act = loc_act_map.get(neighbor);
-
-                                                       FuncInst * last_inst = get_inst(last_act);
-
-                                                       Predicate * new_pred1 = new Predicate(next_inst);
-                                                       new_pred1->add_predicate_expr(EQUALITY, last_inst, true);
-
-                                                       Predicate * new_pred2 = new Predicate(next_inst);
-                                                       new_pred2->add_predicate_expr(EQUALITY, last_inst, 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 last_read = last_act->get_reads_from_value();
-                                                       uint64_t next_read = next_act->get_reads_from_value();
-
-                                                       if ( last_read == next_read )
-                                                               curr_pred = new_pred1;
-                                                       else
-                                                               curr_pred = new_pred2;
-
-                                                       test = true;
-                                                       break;
-                                               }
+                       bool may_equal = false;
+                       void * loc = next_act->get_location();
+                       loc_set_t * loc_may_equal = loc_may_equal_map->get(loc);
+                       if (loc_may_equal != NULL) {
+                               loc_set_iter * loc_it = loc_may_equal->iterator();
+                               while (loc_it->hasNext()) {
+                                       void * neighbor = loc_it->next();
+                                       if (loc_act_map.contains(neighbor)) {
+                                               model_print("loc %p may eqaul to loc %p\n", loc, neighbor);
+                                               gen_predicate_and_follow(&curr_pred, next_inst, next_act, &loc_act_map, EQUALITY, neighbor);
+                                               may_equal = true;
+                                               break;
                                        }
-                               } 
-
-                               if (!test) {
-                                       Predicate * new_pred = new Predicate(next_inst);
-                                       curr_pred->add_child(new_pred);
-                                       new_pred->set_parent(curr_pred);
-
-                                       if (curr_pred->is_entry_predicate())
-                                               new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
-
-                                       curr_pred = new_pred;
                                }
+                       } 
+
+                       if (!may_equal) {
+                               if (!next_inst->is_single_location())
+                                       gen_predicate_and_follow(&curr_pred, next_inst, next_act, &loc_act_map, NULLITY, NULL);
+                               else
+                                       gen_predicate_and_follow(&curr_pred, next_inst, next_act, &loc_act_map, UNSET, NULL);
                        }
                }
 
@@ -525,6 +457,65 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
        return branch_found;
 }
 
+void FuncNode::gen_predicate_and_follow(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act,
+               HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map, token_t token, void * loc)
+{
+       Predicate * new_pred1 = new Predicate(next_inst);
+       Predicate * new_pred2 = new Predicate(next_inst);
+       new_pred1->set_parent(*curr_pred);
+       new_pred2->set_parent(*curr_pred);
+
+       uint64_t next_read = next_act->get_reads_from_value();
+
+       switch (token) {
+               case UNSET:
+                       if ( (*curr_pred)->is_entry_predicate() )
+                               new_pred1->add_predicate_expr(NOPREDICATE, NULL, true);
+
+                       (*curr_pred)->add_child(new_pred1);
+                       *curr_pred = new_pred1;
+                       delete new_pred2;
+
+                       break;
+               case EQUALITY:
+                       ModelAction * last_act;
+                       FuncInst * last_inst;
+                       uint64_t last_read;
+
+                       last_act = loc_act_map->get(loc);
+                       last_inst = get_inst(last_act);
+                       last_read = last_act->get_reads_from_value();
+
+                       new_pred1->add_predicate_expr(EQUALITY, last_inst, true);
+                       new_pred2->add_predicate_expr(EQUALITY, last_inst, false);
+                       (*curr_pred)->add_child(new_pred1);
+                       (*curr_pred)->add_child(new_pred2);
+
+                       if ( last_read == next_read )
+                               *curr_pred = new_pred1;
+                       else
+                               *curr_pred = new_pred2;
+                       break;
+               case NULLITY:
+                       new_pred1->add_predicate_expr(NULLITY, NULL, true);
+                       new_pred2->add_predicate_expr(NULLITY, NULL, false);
+                       (*curr_pred)->add_child(new_pred1);
+                       (*curr_pred)->add_child(new_pred2);
+
+                       if ( (void*)next_read == NULL )
+                               *curr_pred = new_pred1;
+                       else
+                               *curr_pred = new_pred2;
+                       break;
+               default:
+                       model_print("unknown predicate token\n");
+                       delete new_pred1;
+                       delete new_pred2;
+
+                       break;
+       }
+}
+
 void FuncNode::add_to_val_loc_map(uint64_t val, void * loc)
 {
        loc_set_t * locations = val_loc_map->get(val);

diff --git a/funcnode.h b/funcnode.h
index 277e5256f0495d843ac061ce8f7c81f25f77928e..2a5781bb51da8823cf99b04a9a53bb5847663e45 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -41,6 +41,7 @@ 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 gen_predicate_and_follow(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map, token_t token, void * loc);
 
        void incr_exit_count() { exit_count++; }
        uint32_t get_exit_count() { return exit_count; }

diff --git a/predicate.cc b/predicate.cc
index c8e3989133fddedb009a8bc8544dfe48d893fdb4..5695452853f93cbc5c887c25acdff6c9e63fc4cd 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -9,6 +9,17 @@ Predicate::Predicate(FuncInst * func_inst, bool is_entry) :
        backedges(16)
 {}
 
+Predicate::~Predicate()
+{
+//     if (func_inst)
+//             delete func_inst;
+
+       // parent should not be deleted
+       pred_expressions.reset();
+       backedges.reset();
+       children.clear();
+}
+
 unsigned int pred_expr_hash(struct pred_expr * expr)
 {
         return (unsigned int)((uintptr_t)expr);

diff --git a/predicate.h b/predicate.h
index 732e39abd8b7644d5f5d9d37df1e9a133594b06e..f787983ff6417d7785be83f42d92be773d2bc27b 100644 (file)
--- a/predicate.h
+++ b/predicate.h
@@ -10,7 +10,7 @@ typedef HashSet<struct pred_expr *, uintptr_t, 0, model_malloc, model_calloc, mo
 typedef HSIterator<struct pred_expr *, uintptr_t, 0, model_malloc, model_calloc, model_free, pred_expr_hash, pred_expr_equal> PredExprSetIter;
 
 typedef enum predicate_token {
-       NOPREDICATE, EQUALITY, NULLITY
+       NOPREDICATE, UNSET, EQUALITY, NULLITY
 } token_t;
 
 /* If token is EQUALITY, then the predicate asserts whether