Reorganize codes

diff --git a/funcnode.cc b/funcnode.cc
index efbc824edd8afafbaab1a1bff1dbd1f631fa8093..3f238fc1fdaf53f9559fbf47aa86cfbcff3efe32 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -268,45 +268,8 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                // Generate new branches
                if (!branch_found) {
                        SnapVector<struct half_pred_expr *> half_pred_expressions;
-                       void * loc = next_act->get_location();
-
-                       if (next_act->is_read()) {
-                               if ( loc_act_map.contains(loc) ) {
-                                       ModelAction * last_act = loc_act_map.get(loc);
-                                       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);
-                               } else if ( next_inst->is_single_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)) {
-                                                               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);
-                                                       }
-                                               }
-                                       } 
-                               } else {
-                                       // next_inst is not single location
-                                       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);
-                                       }
-                               }
-                       } else {
-                               // TODO: when next_act is a write action, do anything?
-                       }
-
-                       generate_predicate(&curr_pred, next_inst, &half_pred_expressions);
+                       infer_predicates(next_inst, next_act, &loc_act_map, &half_pred_expressions);
+                       generate_predicates(&curr_pred, next_inst, &half_pred_expressions);
                        continue;
                }
 
@@ -392,8 +355,51 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
        return branch_found;
 }
 
+void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
+       HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map,
+       SnapVector<struct half_pred_expr *> * half_pred_expressions)
+{
+       void * loc = next_act->get_location();
+
+       if (next_inst->is_read()) {
+               if ( loc_act_map->contains(loc) ) {
+                       ModelAction * last_act = loc_act_map->get(loc);
+                       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);
+               } else if ( next_inst->is_single_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)) {
+                                               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);
+                                       }
+                               }
+                       }
+               } else {
+                       // next_inst is not single location
+                       uint64_t read_val = next_act->get_reads_from_value();
+
+                       // only infer 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);
+                       }
+               }
+       } else {
+               // TODO: when next_act is a write action, do anything?
+       }
+}
+
 /* Able to generate complex predicates when there are multiple predciate expressions */
-void FuncNode::generate_predicate(Predicate ** curr_pred, FuncInst * next_inst,
+void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst,
        SnapVector<struct half_pred_expr *> * half_pred_expressions)
 {
        if (half_pred_expressions->size() == 0) {

diff --git a/funcnode.h b/funcnode.h
index db52f4ead88a3d9fde098273c573fce1fc7b2560..53f071f18fb3791d1c59c51ab4aa05ed5f8e40ad 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -34,8 +34,9 @@ public:
        void update_inst_tree(func_inst_list_t * inst_list);
 
        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 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 infer_predicates(FuncInst * next_inst, ModelAction * next_act, HashTable<void *, ModelAction *, uintptr_t, 0> * loc_act_map, SnapVector<struct half_pred_expr *> * half_pred_expressions);
+       void generate_predicates(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++; }