Version that finds the bug of iris

[c11tester.git] / newfuzzer.cc

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 6a9f930506d95d16789e10ff2516aa0b1adc4afd..e76d8961e47d3357360be5ee09270e4b0d75f01e 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -33,7 +33,7 @@ void NewFuzzer::register_engine(ModelHistory * history, ModelExecution *executio
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {
-//     return random() % rf_set->size();
+       return random() % rf_set->size();
 
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);
@@ -67,35 +67,6 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
 
                //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());
 
-/*--
-               Thread * read_thread = execution->get_thread(tid);
-               bool should_reselect_predicate = true;
-               bool should_sleep = should_conditional_sleep(selected_branch);
-               dist_info_vec.clear();
-
-               if (!find_threads(read)) {
-                       update_predicate_score(selected_branch, SLEEP_FAIL_TYPE1);
-                       should_reselect_predicate = true;
-               } else if (!should_sleep) {
-                       update_predicate_score(selected_branch, SLEEP_FAIL_TYPE2);
-                       should_reselect_predicate = true;
-               } else {
-                       for (uint i = 0; i < dist_info_vec.size(); i++) {
-                               struct node_dist_info info = dist_info_vec[i];
-                               history->add_waiting_thread(tid, info.tid, info.target, info.dist);
-                       }
-
-                       // reset thread pending action and revert sequence numbers
-                       read_thread->set_pending(read);
-                       read->reset_seq_number();
-                       execution->restore_last_seq_num();
-
-                       conditional_sleep(read_thread);
-                       // Returning -1 stops the while loop of ModelExecution::process_read
-                       return -1;      
-               }
-*/
-
                SnapVector<ModelAction *> * pruned_writes = thrd_pruned_writes[thread_id];
                for (uint i = 0; i < pruned_writes->size(); i++) {
                        rf_set->push_back( (*pruned_writes)[i] );
@@ -127,44 +98,36 @@ void NewFuzzer::check_store_visibility(Predicate * curr_pred, FuncInst * read_in
                return;
 
        ModelVector<Predicate *> * children = curr_pred->get_children();
-       SnapVector<Predicate *> branches;
 
-       /* The children predicates may have different FuncInsts */
+       /* Iterate over all predicate children */
        for (uint i = 0; i < children->size(); i++) {
-               Predicate * child = (*children)[i];
-               if (child->get_func_inst() == read_inst) {
-                       branches.push_back(child);
-               }
-       }
+               Predicate * branch = (*children)[i];
 
-       /* Predicate children have not been generated */
-       if (branches.empty())
-               return;
+               /* The children predicates may have different FuncInsts */
+               if (branch->get_func_inst() == read_inst) {
+                       PredExprSet * pred_expressions = branch->get_pred_expressions();
 
-       /* Iterate over all predicate children */
-       for (uint i = 0; i < branches.size(); i++) {
-               Predicate * branch = branches[i];
-               PredExprSet * pred_expressions = branch->get_pred_expressions();
-
-               /* Do not check unset predicates */
-               if (pred_expressions->isEmpty())
-                       continue;
-
-               branch->incr_total_checking_count();
-
-               /* Iterate over all write actions */
-               for (uint j = 0; j < rf_set->size(); j++) {
-                       ModelAction * write_act = (*rf_set)[j];
-                       uint64_t write_val = write_act->get_write_value();
-                       bool dummy = true;
-                       bool satisfy_predicate = check_predicate_expressions(pred_expressions, inst_act_map, write_val, &dummy);
-
-                       /* If one write value satisfies the predicate, go to check the next predicate */
-                       if (satisfy_predicate) {
-                               branch->incr_store_visible_count();
-                               break;
+                       /* Do not check unset predicates */
+                       if (pred_expressions->isEmpty())
+                               continue;
+
+                       branch->incr_total_checking_count();
+
+                       /* Iterate over all write actions */
+                       for (uint j = 0; j < rf_set->size(); j++) {
+                               ModelAction * write_act = (*rf_set)[j];
+                               uint64_t write_val = write_act->get_write_value();
+                               bool dummy = true;
+                               bool satisfy_predicate = check_predicate_expressions(pred_expressions, inst_act_map, write_val, &dummy);
+
+                               /* If one write value satisfies the predicate, go to check the next predicate */
+                               if (satisfy_predicate) {
+                                       branch->incr_store_visible_count();
+                                       break;
+                               }
                        }
                }
+
        }
 }
 
@@ -190,11 +153,6 @@ Predicate * NewFuzzer::selectBranch(thread_id_t tid, Predicate * curr_pred, Func
                Predicate * child = (*children)[i];
                if (child->get_func_inst() == read_inst && !failed_predicates.contains(child)) {
                        branches.push_back(child);
-
-                       /*-- max of (exploration counts + 1)
-                       if (child->get_expl_count() + 1 > numerator)
-                               numerator = child->get_expl_count() + 1;
-                       */
                }
        }