Incorporate failed predicates in weights

diff --git a/funcnode.cc b/funcnode.cc
index 94ef8c93b6b1baf96737d36029a65c5872c8947c..26e8f59e84cb22a20f18576b29bd23c13c2011c9 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -22,6 +22,7 @@ FuncNode::FuncNode(ModelHistory * history) :
        predicate_leaves(),
        leaves_tmp_storage(),
        weight_debug_vec(),
+       failed_predicates(),
        edge_table(32),
        out_edges()
 {
@@ -761,6 +762,11 @@ int FuncNode::compute_distance(FuncNode * target, int max_step)
        return -1;
 }
 
+void FuncNode::add_failed_predicate(Predicate * pred)
+{
+       failed_predicates.add(pred);
+}
+
 /* Implement quick sort to sort leaves before assigning base scores */
 template<typename _Tp>
 static int partition(ModelVector<_Tp *> * arr, int low, int high)
@@ -803,7 +809,7 @@ void FuncNode::assign_initial_weight()
 
        while (it->hasNext()) {
                Predicate * pred = it->next();
-               double weight = 100.0 / sqrt(pred->get_expl_count() + 1);
+               double weight = 100.0 / sqrt(pred->get_expl_count() + pred->get_fail_count() + 1);
                pred->set_weight(weight);
                leaves_tmp_storage.push_back(pred);
        }
@@ -861,10 +867,18 @@ void FuncNode::update_predicate_tree_weight()
 
        weight_debug_vec.clear();
 
+       PredSetIter * it = failed_predicates.iterator();
+       while (it->hasNext()) {
+               Predicate * pred = it->next();
+               leaves_tmp_storage.push_back(pred);
+       }
+       delete it;
+       failed_predicates.reset();
+
        quickSort(&leaves_tmp_storage, 0, leaves_tmp_storage.size() - 1);
        for (uint i = 0; i < leaves_tmp_storage.size(); i++) {
                Predicate * pred = leaves_tmp_storage[i];
-               double weight = 100.0 / sqrt(pred->get_expl_count() + 1);
+               double weight = 100.0 / sqrt(pred->get_expl_count() + pred->get_fail_count() + 1);
                pred->set_weight(weight);
        }
 

diff --git a/funcnode.h b/funcnode.h
index 7aec0bd047e8f21fa672c3a8efbc928d42971769..a0eb6233988c1d082de9e88a734ee084772209c4 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -60,6 +60,8 @@ public:
        ModelList<FuncNode *> * get_out_edges() { return &out_edges; }
        int compute_distance(FuncNode * target, int max_step = MAX_DIST);
 
+       void add_failed_predicate(Predicate * pred);
+
        void print_predicate_tree();
 
        MEMALLOC
@@ -122,6 +124,7 @@ private:
        PredSet predicate_leaves;
        ModelVector<Predicate *> leaves_tmp_storage;
        ModelVector<Predicate *> weight_debug_vec;
+       PredSet failed_predicates;
 
        /* Store the relation between this FuncNode and other FuncNodes */
        HashTable<FuncNode *, edge_type_t, uintptr_t, 0, model_malloc, model_calloc, model_free> edge_table;

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 6d90f5fd62c460e0946c5e0c9c6034aa0636a62f..e2e057d890e3282129f8e3e0edc164e688db4019 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -54,7 +54,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                if (curr_pred != NULL)  {
                        Predicate * selected_branch = NULL;
 
-                       if (check_store_visibility(curr_pred, read_inst, inst_act_map, rf_set))
+                       if (check_branch_inst(curr_pred, read_inst, inst_act_map, rf_set))
                                selected_branch = selectBranch(tid, curr_pred, read_inst);
                        else {
                                // no child of curr_pred matches read_inst, check back edges
@@ -63,7 +63,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
 
                                while (it->hasNext()) {
                                        curr_pred = it->next();
-                                       if (check_store_visibility(curr_pred, read_inst, inst_act_map, rf_set)) {
+                                       if (check_branch_inst(curr_pred, read_inst, inst_act_map, rf_set)) {
                                                selected_branch = selectBranch(tid, curr_pred, read_inst);
                                                break;
                                        }
@@ -85,7 +85,12 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
        // The chosen branch fails, reselect new branches
        while ( rf_set->size() == 0 ) {
                Predicate * selected_branch = get_selected_child_branch(tid);
+               FuncNode * func_node = history->get_curr_func_node(tid);
+
+               // Add failed predicate to NewFuzzer and FuncNode
                failed_predicates.put(selected_branch, true);
+               func_node->add_failed_predicate(selected_branch);
+               selected_branch->incr_fail_count();
 
                //model_print("the %d read action of thread %d at %p is unsuccessful\n", read->get_seq_number(), read_thread->get_id(), read->get_location());
 
@@ -99,7 +104,6 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                FuncInst * read_inst = thrd_last_func_inst[thread_id];
                selected_branch = selectBranch(tid, curr_pred, read_inst);
 
-               FuncNode * func_node = history->get_curr_func_node(tid);
                inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
                prune_writes(tid, selected_branch, rf_set, inst_act_map);
 
@@ -111,13 +115,10 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
        return random_index;
 }
 
-/* For children of curr_pred that matches read_inst.
- * If any store in rf_set satisfies the a child's predicate,
- * increment the store visibility count for it.
- *
+/* Check if children of curr_pred match read_inst.
  * @return False if no child matches read_inst
  */
-bool NewFuzzer::check_store_visibility(Predicate * curr_pred, FuncInst * read_inst,
+bool NewFuzzer::check_branch_inst(Predicate * curr_pred, FuncInst * read_inst,
 inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set)
 {
        available_branches_tmp_storage.clear();
@@ -136,6 +137,7 @@ inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set)
                /* The children predicates may have different FuncInsts */
                if (branch->get_func_inst() == read_inst) {
                        any_child_match = true;
+                       branch->incr_total_checking_count();
                        available_branches_tmp_storage.push_back(branch);
                }
        }

diff --git a/newfuzzer.h b/newfuzzer.h
index d3fc460e63eba02a67b2284bd9a67de8ef0db19c..8e506ad7569e9ba037d7d4c8315c37659f6c7df8 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -49,7 +49,7 @@ private:
        SnapVector<Predicate *> thrd_selected_child_branch;
        SnapVector< SnapVector<ModelAction *> *> thrd_pruned_writes;
 
-       bool check_store_visibility(Predicate * curr_pred, FuncInst * read_inst, inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set);
+       bool check_branch_inst(Predicate * curr_pred, FuncInst * read_inst, inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set);
        Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst);
        bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map);
        int choose_branch_index(SnapVector<Predicate *> * branches);

diff --git a/predicate.cc b/predicate.cc
index 35bc032fcbb2f860c0a477fa723a3ff1da8bac71..e87c695bedadccfd908c31aa4524c56082833142 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -177,7 +177,7 @@ void Predicate::print_predicate()
 
        double prob = (double) store_visible_count / total_checking_count;
        model_print("Total checks: %d, visible count: %d; prob: %f\n", total_checking_count, store_visible_count, prob);
-       model_print("Exploration count: %d", exploration_count);
+       model_print("Exploration count: %d, failure count: %d", exploration_count, failure_count);
        model_print("\"];\n");
 
        delete it;

diff --git a/predicate.h b/predicate.h
index 8afc24be0839ff5da5c11e05a1b0c910a7fa1133..df46ca1052551dc04b0423e5d3a394261c669f1c 100644 (file)
--- a/predicate.h
+++ b/predicate.h
@@ -45,10 +45,12 @@ public:
        ConcretePredicate * evaluate(inst_act_map_t * inst_act_map, thread_id_t tid);
 
        uint32_t get_expl_count() { return exploration_count; }
+       uint32_t get_fail_count() { return failure_count; }
        uint32_t get_store_visible_count() { return store_visible_count; }
        uint32_t get_total_checking_count() { return total_checking_count; }
 
        void incr_expl_count() { exploration_count++; }
+       void incr_fail_count() { failure_count++; }
        void incr_store_visible_count() { store_visible_count++; }
        void incr_total_checking_count() { total_checking_count++; }
 
@@ -70,6 +72,7 @@ private:
        double weight;
 
        uint32_t exploration_count;
+       uint32_t failure_count;
        uint32_t store_visible_count;
        uint32_t total_checking_count;  /* The number of times the store visibility is checked */