change the way to detect loops

[c11tester.git] / funcnode.cc

diff --git a/funcnode.cc b/funcnode.cc
index 940a8f7844ee17812e2562caf586ee96126942d4..085ab5bd49e2d2e12ebc82402bf42a39da727905 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(),
@@ -119,7 +120,7 @@ void FuncNode::update_tree(action_list_t * act_list)
                        read_act_list.push_back(act);
        }
 
-       model_print("function %s\n", func_name);
+//     model_print("function %s\n", func_name);
        update_inst_tree(&inst_list);
        update_predicate_tree(&read_act_list);
 //     deep_update(predicate_tree_entry);
@@ -223,6 +224,11 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 */
        /* map a FuncInst to the its predicate */
        HashTable<FuncInst *, Predicate *, uintptr_t, 0> inst_pred_map(128);
+
+       // number FuncInsts to detect loops
+       HashTable<FuncInst *, uint32_t, uintptr_t, 0> inst_id_map(128);
+       uint32_t inst_counter = 0;
+
        HashTable<void *, ModelAction *, uintptr_t, 0> loc_act_map(128);
        HashTable<FuncInst *, ModelAction *, uintptr_t, 0> inst_act_map(128);
 
@@ -235,54 +241,31 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 
                bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map, unset_predicates);
 
-               /* no predicate, follow the only branch */
+               // 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];
-
-                       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;
                }
 
                delete unset_predicates;
 
-               // check back edges
-               if (!branch_found) {
-                       bool backedge_found = false;
-                       Predicate * back_pred = curr_pred->get_backedge();
-                       if (back_pred != NULL) {
-                               curr_pred = back_pred;
-                               backedge_found = true;
-                       } else if (inst_pred_map.contains(next_inst)) {
-                               inst_pred_map.remove(curr_pred->get_func_inst());
+               // detect loops
+               if (!branch_found && inst_id_map.contains(next_inst)) {
+                       FuncInst * curr_inst = curr_pred->get_func_inst();
+                       uint32_t curr_id = inst_id_map.get(curr_inst);
+                       uint32_t next_id = inst_id_map.get(next_inst);
+
+                       if (curr_id >= next_id) {
                                Predicate * old_pred = inst_pred_map.get(next_inst);
-                               back_pred = old_pred->get_parent();
+                               Predicate * back_pred = old_pred->get_parent();
 
-                               curr_pred->set_backedge(back_pred);
+                               curr_pred->add_backedge(back_pred);
                                curr_pred = back_pred;
-                               backedge_found = true;
-                       }
 
-                       if (backedge_found)
                                continue;
+                       }
                }
 
                if (!branch_found) {
@@ -308,6 +291,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);
@@ -320,8 +321,9 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                        }
                }
 
-               if (!inst_pred_map.contains(next_inst))
-                       inst_pred_map.put(next_inst, curr_pred);
+               inst_pred_map.put(next_inst, curr_pred);
+               if (!inst_id_map.contains(next_inst))
+                       inst_id_map.put(next_inst, inst_counter++);
 
                loc_act_map.put(next_act->get_location(), next_act);
                inst_act_map.put(next_inst, next_act);
@@ -353,7 +355,6 @@ void FuncNode::deep_update(Predicate * curr_pred)
 
                        Predicate * parent = curr_pred->get_parent();
                        parent->add_child(another_branch);
-//                     another_branch.add_children(i);
                }
        }