From: weiyu Date: Thu, 13 Feb 2020 01:07:22 +0000 (-0800) Subject: Handle predicate weight updates X-Git-Url: http://demsky.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=f9cdc3f4a12363409956eb957252e6107aff8d45 Handle predicate weight updates --- diff --git a/funcnode.cc b/funcnode.cc index 896c60eb..c01173ae 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -20,10 +20,10 @@ FuncNode::FuncNode(ModelHistory * history) : thrd_inst_pred_map(), thrd_inst_id_map(), thrd_loc_inst_map(), - predicate_tree_position(), + thrd_predicate_tree_position(), + thrd_predicate_trace(), predicate_leaves(), leaves_tmp_storage(), - weight_debug_vec(), failed_predicates(), edge_table(32), out_edges() @@ -169,9 +169,9 @@ void FuncNode::add_entry_inst(FuncInst * inst) void FuncNode::function_entry_handler(thread_id_t tid) { set_marker(tid); - init_predicate_tree_position(tid); init_inst_act_map(tid); - init_maps(tid); + init_local_maps(tid); + init_predicate_tree_data_structure(tid); } void FuncNode::function_exit_handler(thread_id_t tid) @@ -179,7 +179,7 @@ void FuncNode::function_exit_handler(thread_id_t tid) exit_count++; reset_inst_act_map(tid); - reset_maps(tid); + reset_local_maps(tid); Predicate * exit_pred = get_predicate_tree_position(tid); if (exit_pred->get_exit() == NULL) { @@ -187,8 +187,8 @@ void FuncNode::function_exit_handler(thread_id_t tid) exit_pred->set_exit(predicate_tree_exit); } - int thread_id = id_to_int(tid); - predicate_tree_position[thread_id]->pop_back(); + update_predicate_tree_weight(tid); + reset_predicate_tree_data_structure(tid); } /** @@ -290,9 +290,6 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) inst_pred_map_t * inst_pred_map = thrd_inst_pred_map[thread_id]; inst_id_map_t * inst_id_map = thrd_inst_id_map[thread_id]; - // Clear the set of leaves encountered in this path - // leaves_tmp_storage.clear(); - Predicate * curr_pred = get_predicate_tree_position(tid); while (true) { FuncInst * next_inst = get_inst(next_act); @@ -322,9 +319,6 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) Predicate * old_pred = inst_pred_map->get(next_inst); Predicate * back_pred = old_pred->get_parent(); - // For updating weights - leaves_tmp_storage.push_back(curr_pred); - // Add to the set of backedges curr_pred->add_backedge(back_pred); curr_pred = back_pred; @@ -356,11 +350,11 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) inst_id_map->put(next_inst, inst_counter++); curr_pred->incr_expl_count(); + add_predicate_to_trace(tid, curr_pred); break; } // leaves_tmp_storage.push_back(curr_pred); -// update_predicate_tree_weight(); } /* Given curr_pred and next_inst, find the branch following curr_pred that @@ -652,25 +646,10 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location delete loc_it; } -void FuncNode::init_predicate_tree_position(thread_id_t tid) -{ - int thread_id = id_to_int(tid); - int old_size = predicate_tree_position.size(); - - if (old_size <= thread_id + 1) { - predicate_tree_position.resize(thread_id + 1); - - for (int i = old_size; i < thread_id + 1; i++) - predicate_tree_position[i] = new ModelVector(); - } - - predicate_tree_position[thread_id]->push_back(predicate_tree_entry); -} - void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred) { int thread_id = id_to_int(tid); - ModelVector * stack = predicate_tree_position[thread_id]; + ModelVector * stack = thrd_predicate_tree_position[thread_id]; (*stack)[stack->size() - 1] = pred; } @@ -678,7 +657,13 @@ void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred) Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid) { int thread_id = id_to_int(tid); - return predicate_tree_position[thread_id]->back(); + return thrd_predicate_tree_position[thread_id]->back(); +} + +void FuncNode::add_predicate_to_trace(thread_id_t tid, Predicate * pred) +{ + int thread_id = id_to_int(tid); + thrd_predicate_trace[thread_id]->back()->push_back(pred); } /* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */ @@ -737,13 +722,14 @@ void FuncNode::set_marker(thread_id_t tid) } /* Make sure elements of maps are initialized properly when threads enter functions */ -void FuncNode::init_maps(thread_id_t tid) +void FuncNode::init_local_maps(thread_id_t tid) { int thread_id = id_to_int(tid); uint old_size = thrd_loc_inst_map.size(); if (old_size <= (uint) thread_id) { uint new_size = thread_id + 1; + thrd_loc_inst_map.resize(new_size); thrd_inst_id_map.resize(new_size); thrd_inst_pred_map.resize(new_size); @@ -757,7 +743,7 @@ void FuncNode::init_maps(thread_id_t tid) } /* Reset elements of maps when threads exit functions */ -void FuncNode::reset_maps(thread_id_t tid) +void FuncNode::reset_local_maps(thread_id_t tid) { int thread_id = id_to_int(tid); thrd_loc_inst_map[thread_id]->reset(); @@ -765,6 +751,35 @@ void FuncNode::reset_maps(thread_id_t tid) thrd_inst_pred_map[thread_id]->reset(); } +void FuncNode::init_predicate_tree_data_structure(thread_id_t tid) +{ + int thread_id = id_to_int(tid); + int old_size = thrd_predicate_tree_position.size(); + + if (old_size <= thread_id + 1) { + thrd_predicate_tree_position.resize(thread_id + 1); + thrd_predicate_trace.resize(thread_id + 1); + + for (int i = old_size; i < thread_id + 1; i++) { + thrd_predicate_tree_position[i] = new ModelVector(); + thrd_predicate_trace[i] = new ModelVector(); + } + } + + thrd_predicate_tree_position[thread_id]->push_back(predicate_tree_entry); + thrd_predicate_trace[thread_id]->push_back(new predicate_trace_t()); +} + +void FuncNode::reset_predicate_tree_data_structure(thread_id_t tid) +{ + int thread_id = id_to_int(tid); + thrd_predicate_tree_position[thread_id]->pop_back(); + + predicate_trace_t * trace = thrd_predicate_trace[thread_id]->back(); + delete trace; + thrd_predicate_trace[thread_id]->pop_back(); +} + /* Add FuncNodes that this node may follow */ void FuncNode::add_out_edge(FuncNode * other) { @@ -866,130 +881,33 @@ static void quickSort(ModelVector<_Tp *> * arr, int low, int high) } } -void FuncNode::assign_initial_weight() -{ - PredSetIter * it = predicate_leaves.iterator(); - leaves_tmp_storage.clear(); - - while (it->hasNext()) { - Predicate * pred = it->next(); - double weight = 100.0 / sqrt(pred->get_expl_count() + pred->get_fail_count() + 1); - pred->set_weight(weight); - leaves_tmp_storage.push_back(pred); - } - delete it; - - quickSort(&leaves_tmp_storage, 0, leaves_tmp_storage.size() - 1); - - // assign scores for internal nodes; - while ( !leaves_tmp_storage.empty() ) { - Predicate * leaf = leaves_tmp_storage.back(); - leaves_tmp_storage.pop_back(); - - Predicate * curr = leaf->get_parent(); - while (curr != NULL) { - if (curr->get_weight() != 0) { - // Has been exlpored - break; - } - - ModelVector * children = curr->get_children(); - double weight_sum = 0; - bool has_unassigned_node = false; - - for (uint i = 0;i < children->size();i++) { - Predicate * child = (*children)[i]; - - // If a child has unassigned weight - double weight = child->get_weight(); - if (weight == 0) { - has_unassigned_node = true; - break; - } else - weight_sum += weight; - } - - if (!has_unassigned_node) { - double average_weight = (double) weight_sum / (double) children->size(); - double weight = average_weight * pow(0.9, curr->get_depth()); - curr->set_weight(weight); - } else - break; - - curr = curr->get_parent(); - } - } -} - -void FuncNode::update_predicate_tree_weight() +void FuncNode::update_predicate_tree_weight(thread_id_t tid) { - if (marker == 2) { - // Predicate tree is initially built - assign_initial_weight(); - return; - } - - 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() + pred->get_fail_count() + 1); - pred->set_weight(weight); - } - - // Update weights in internal nodes - while ( !leaves_tmp_storage.empty() ) { - Predicate * leaf = leaves_tmp_storage.back(); - leaves_tmp_storage.pop_back(); + predicate_trace_t * trace = thrd_predicate_trace[id_to_int(tid)]->back(); - Predicate * curr = leaf->get_parent(); - while (curr != NULL) { - ModelVector * children = curr->get_children(); - double weight_sum = 0; - bool has_unassigned_node = false; + // Update predicate weights based on prediate trace + for (mllnode * rit = trace->end(); rit != NULL; rit = rit->getPrev()) { + Predicate * node = rit->getVal(); + if (predicate_leaves.contains(node)) { + double weight = 100.0 / sqrt(node->get_expl_count() + node->get_fail_count() + 1); + node->set_weight(weight); + } else { + double weight_sum = 0.0; + ModelVector * children = node->get_children(); for (uint i = 0;i < children->size();i++) { Predicate * child = (*children)[i]; - double weight = child->get_weight(); - if (weight != 0) - weight_sum += weight; - else if ( predicate_leaves.contains(child) ) { - // If this child is a leaf - double weight = 100.0 / sqrt(child->get_expl_count() + 1); - child->set_weight(weight); - weight_sum += weight; - } else { - has_unassigned_node = true; - weight_debug_vec.push_back(child); // For debugging purpose - break; - } + weight_sum += weight; } - if (!has_unassigned_node) { - double average_weight = (double) weight_sum / (double) children->size(); - double weight = average_weight * pow(0.9, curr->get_depth()); - curr->set_weight(weight); - } else - break; - - curr = curr->get_parent(); + double average_weight = (double) weight_sum / (double) children->size(); + double weight = average_weight * pow(0.9, node->get_depth()); + node->set_weight(weight); } } - - for (uint i = 0;i < weight_debug_vec.size();i++) { - Predicate * tmp = weight_debug_vec[i]; - ASSERT( tmp->get_weight() != 0 ); - } } void FuncNode::print_predicate_tree() diff --git a/funcnode.h b/funcnode.h index ed2213a7..d8b0bc1a 100644 --- a/funcnode.h +++ b/funcnode.h @@ -13,6 +13,8 @@ typedef HashTable inst_id_map_t; typedef HashTable inst_pred_map_t; +typedef ModelList predicate_trace_t; + typedef enum edge_type { IN_EDGE, OUT_EDGE, BI_EDGE } edge_type_t; @@ -51,10 +53,11 @@ public: void add_to_val_loc_map(value_set_t * values, void * loc); void update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations); - void init_predicate_tree_position(thread_id_t tid); void set_predicate_tree_position(thread_id_t tid, Predicate * pred); Predicate * get_predicate_tree_position(thread_id_t tid); + void add_predicate_to_trace(thread_id_t tid, Predicate *pred); + void init_inst_act_map(thread_id_t tid); void reset_inst_act_map(thread_id_t tid); void update_inst_act_map(thread_id_t tid, ModelAction * read_act); @@ -103,8 +106,8 @@ private: /* Delect read actions at the same locations when updating predicate trees */ ModelVector thrd_loc_inst_map; - void init_maps(thread_id_t tid); - void reset_maps(thread_id_t tid); + void init_local_maps(thread_id_t tid); + void reset_local_maps(thread_id_t tid); void infer_predicates(FuncInst * next_inst, ModelAction * next_act, SnapVector * half_pred_expressions); void generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector * half_pred_expressions); @@ -126,11 +129,15 @@ private: /* Run-time position in the predicate tree for each thread * The inner vector is used to deal with recursive functions. */ - ModelVector< ModelVector * > predicate_tree_position; + ModelVector< ModelVector * > thrd_predicate_tree_position; + + ModelVector< ModelVector * > thrd_predicate_trace; + + void init_predicate_tree_data_structure(thread_id_t tid); + void reset_predicate_tree_data_structure(thread_id_t tid); PredSet predicate_leaves; ModelVector leaves_tmp_storage; - ModelVector weight_debug_vec; PredSet failed_predicates; /* Store the relation between this FuncNode and other FuncNodes */ @@ -139,8 +146,7 @@ private: /* FuncNodes that follow this node */ ModelList out_edges; - void assign_initial_weight(); - void update_predicate_tree_weight(); + void update_predicate_tree_weight(thread_id_t tid); }; #endif /* __FUNCNODE_H__ */ diff --git a/newfuzzer.cc b/newfuzzer.cc index 027b7d4f..299156b8 100644 --- a/newfuzzer.cc +++ b/newfuzzer.cc @@ -34,7 +34,7 @@ void NewFuzzer::register_engine(ModelChecker *_model, ModelExecution *execution) int NewFuzzer::selectWrite(ModelAction *read, SnapVector * 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); @@ -54,7 +54,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector * rf_set if (curr_pred != NULL) { Predicate * selected_branch = NULL; - if (check_branch_inst(curr_pred, read_inst, inst_act_map, rf_set)) + if (check_branch_inst(curr_pred, read_inst, 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 * rf_set while (it->hasNext()) { curr_pred = it->next(); - if (check_branch_inst(curr_pred, read_inst, inst_act_map, rf_set)) { + if (check_branch_inst(curr_pred, read_inst, rf_set)) { selected_branch = selectBranch(tid, curr_pred, read_inst); break; } @@ -119,7 +119,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector * rf_set * @return False if no child matches read_inst */ bool NewFuzzer::check_branch_inst(Predicate * curr_pred, FuncInst * read_inst, - inst_act_map_t * inst_act_map, SnapVector * rf_set) + SnapVector * rf_set) { available_branches_tmp_storage.clear(); diff --git a/newfuzzer.h b/newfuzzer.h index 02c3fc01..129364c1 100644 --- a/newfuzzer.h +++ b/newfuzzer.h @@ -49,7 +49,7 @@ private: SnapVector thrd_selected_child_branch; SnapVector< SnapVector *> thrd_pruned_writes; - bool check_branch_inst(Predicate * curr_pred, FuncInst * read_inst, inst_act_map_t * inst_act_map, SnapVector * rf_set); + bool check_branch_inst(Predicate * curr_pred, FuncInst * read_inst, SnapVector * rf_set); Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst); bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector * rf_set, inst_act_map_t * inst_act_map); int choose_branch_index(SnapVector * branches);