+void NewFuzzer::check_store_visibility(Predicate * curr_pred, FuncInst * read_inst,
+ inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set)
+{
+ ASSERT(!rf_set->empty());
+ if (curr_pred == NULL || read_inst == NULL)
+ return;
+
+ ModelVector<Predicate *> * children = curr_pred->get_children();
+ SnapVector<Predicate *> branches;
+
+ /* The children predicates may have different FuncInsts */
+ for (uint i = 0; i < children->size(); i++) {
+ Predicate * child = (*children)[i];
+ if (child->get_func_inst() == read_inst) {
+ branches.push_back(child);
+ }
+ }
+
+ /* Predicate children have not been generated */
+ if (branches.empty())
+ return;
+
+ /* 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;
+ }
+ }
+ }
+}
+
+