From: weiyu Date: Mon, 9 Dec 2019 20:49:14 +0000 (-0800) Subject: experiment with exponential decay model X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=57748ff26d916528ba0df0b1d2c699a901386d5f;p=c11tester.git experiment with exponential decay model --- diff --git a/execution.cc b/execution.cc index 3a73e353..e1c5e2dd 100644 --- a/execution.cc +++ b/execution.cc @@ -300,8 +300,6 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * while(true) { int index = fuzzer->selectWrite(curr, rf_set); - if (index == -1)// no feasible write exists - return false; ModelAction *rf = (*rf_set)[index]; @@ -723,12 +721,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (curr->is_read() && !second_part_of_rmw) { process_read(curr, rf_set); delete rf_set; - -/* bool success = process_read(curr, rf_set); - delete rf_set; - if (!success) - return curr; // Do not add action to lists - */ } else ASSERT(rf_set == NULL); diff --git a/funcnode.cc b/funcnode.cc index c1b277e8..663447bf 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -6,6 +6,7 @@ #include "concretepredicate.h" #include "model.h" +#include FuncNode::FuncNode(ModelHistory * history) : history(history), @@ -20,7 +21,9 @@ FuncNode::FuncNode(ModelHistory * history) : { predicate_tree_entry = new Predicate(NULL, true); predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true); + predicate_tree_exit = new Predicate(NULL, false, true); + predicate_tree_exit->alloc_pre_exit_predicates(); predicate_tree_exit->set_depth(MAX_DEPTH); /* Snapshot data structures below */ @@ -335,7 +338,10 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) curr_pred->incr_expl_count(); } - curr_pred->set_exit(predicate_tree_exit); + if (curr_pred->get_exit() == NULL) { + // Exit predicate is unset yet + curr_pred->set_exit(predicate_tree_exit); + } } /* Given curr_pred and next_inst, find the branch following curr_pred that @@ -721,6 +727,67 @@ int FuncNode::compute_distance(FuncNode * target, int max_step) return -1; } +void FuncNode::assign_base_score() +{ + SnapVector leaves; + SnapList queue; + queue.push_front(predicate_tree_entry); + + // assign leaf score + while ( !queue.empty() ) { + Predicate * node = queue.back(); + queue.pop_back(); + + ModelVector * children = node->get_children(); + if (children->empty()) { + node->set_weight(1); + leaves.push_back(node); + } + + for (uint i = 0; i < children->size(); i++) + queue.push_front( (*children)[i] ); + } + + // assign scores for internal nodes; + while ( !leaves.empty() ) { + Predicate * leaf = leaves.back(); + leaves.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::print_predicate_tree() { model_print("digraph function_%s {\n", func_name); @@ -728,22 +795,3 @@ void FuncNode::print_predicate_tree() predicate_tree_exit->print_predicate(); model_print("}\n"); // end of graph } - -void FuncNode::print_val_loc_map() -{ -/* - value_set_iter * val_it = values_may_read_from->iterator(); - while (val_it->hasNext()) { - uint64_t value = val_it->next(); - model_print("val %llx: ", value); - - loc_set_t * locations = val_loc_map->get(value); - loc_set_iter * loc_it = locations->iterator(); - while (loc_it->hasNext()) { - void * location = loc_it->next(); - model_print("%p ", location); - } - model_print("\n"); - } - */ -} diff --git a/funcnode.h b/funcnode.h index 47384733..ea0be029 100644 --- a/funcnode.h +++ b/funcnode.h @@ -60,9 +60,8 @@ public: ModelList * get_out_edges() { return &out_edges; } int compute_distance(FuncNode * target, int max_step = MAX_DIST); + void assign_base_score(); void print_predicate_tree(); - void print_val_loc_map(); - void print_last_read(thread_id_t tid); MEMALLOC private: diff --git a/history.cc b/history.cc index a5b437c5..67f873b6 100644 --- a/history.cc +++ b/history.cc @@ -579,7 +579,9 @@ void ModelHistory::print_func_node() for (uint32_t i = 1;i < func_nodes.size();i++) { FuncNode * func_node = func_nodes[i]; + func_node->assign_base_score(); func_node->print_predicate_tree(); + /* func_inst_list_mt * entry_insts = func_node->get_entry_insts(); model_print("function %s has entry actions\n", func_node->get_func_name()); diff --git a/predicate.cc b/predicate.cc index 77107051..eb979f88 100644 --- a/predicate.cc +++ b/predicate.cc @@ -8,6 +8,7 @@ Predicate::Predicate(FuncInst * func_inst, bool is_entry, bool is_exit) : exit_predicate(is_exit), does_write(false), depth(0), + weight(0), exploration_count(0), store_visible_count(0), total_checking_count(0), @@ -60,6 +61,22 @@ void Predicate::set_parent(Predicate * parent_pred) depth = parent_pred->get_depth() + 1; } +void Predicate::set_exit(Predicate * exit_pred) +{ + exit = exit_pred; + exit_pred->add_pre_exit_predicate(this); +} + +void Predicate::alloc_pre_exit_predicates() +{ + pre_exit_predicates = new ModelVector(); +} + +void Predicate::add_pre_exit_predicate(Predicate * pred) +{ + pre_exit_predicates->push_back(pred); +} + void Predicate::copy_predicate_expr(Predicate * other) { PredExprSet * other_pred_expressions = other->get_pred_expressions(); @@ -136,7 +153,7 @@ void Predicate::print_predicate() return; } - model_print("depth: %d\n", depth); + model_print("depth: %u; weight: %g\n", depth, weight); func_inst->print(); diff --git a/predicate.h b/predicate.h index 97e495de..0512835f 100644 --- a/predicate.h +++ b/predicate.h @@ -23,8 +23,9 @@ public: void add_predicate_expr(token_t token, FuncInst * func_inst, bool value); void add_child(Predicate * child); void set_parent(Predicate * parent_pred); - void set_exit(Predicate * exit_pred) { exit = exit_pred; } + void set_exit(Predicate * exit_pred); void add_backedge(Predicate * back_pred) { backedges.add(back_pred); } + void set_weight(double weight_) { weight = weight_; } void copy_predicate_expr(Predicate * other); Predicate * get_single_child(FuncInst * inst); @@ -32,10 +33,14 @@ public: Predicate * get_parent() { return parent; } Predicate * get_exit() { return exit; } PredSet * get_backedges() { return &backedges; } + double get_weight() { return weight; } bool is_entry_predicate() { return entry_predicate; } void set_entry_predicate() { entry_predicate = true; } + void alloc_pre_exit_predicates(); + void add_pre_exit_predicate(Predicate * pred); + /* Whether func_inst does write or not */ bool is_write() { return does_write; } void set_write(bool is_write) { does_write = is_write; } @@ -65,6 +70,7 @@ private: /* Height of this predicate node in the predicate tree */ uint32_t depth; + double weight; uint32_t exploration_count; uint32_t store_visible_count; @@ -78,6 +84,9 @@ private: Predicate * parent; Predicate * exit; + /* Predicates precede exit nodes. Only used by exit predicates */ + ModelVector * pre_exit_predicates; + /* May have multiple back edges, e.g. nested loops */ PredSet backedges; };