From 3cc10cd7ba94e6a8eeedd0904c75ee613700a8ff Mon Sep 17 00:00:00 2001 From: weiyu Date: Tue, 10 Sep 2019 17:21:35 -0700 Subject: [PATCH] Make sure that actions that do writes are labeled correctly in predicate trees --- funcnode.cc | 34 +++++++++++++++++++++++++++------- funcnode.h | 15 ++++++++------- predicate.cc | 5 +++++ predicate.h | 11 ++++++++--- 4 files changed, 48 insertions(+), 17 deletions(-) diff --git a/funcnode.cc b/funcnode.cc index 3f238fc1..64972b4d 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -147,16 +147,23 @@ void FuncNode::update_tree(action_list_t * act_list) inst_list.push_back(func_inst); - if (func_inst->is_write()) + /* NOTE: for rmw actions, func_inst and act may have different + * action types because of action type conversion in ModelExecution + * func_inst->is_write() <==> pure writes (excluding rmw) */ + if (func_inst->is_write()) { + // model_print("write detected\n"); rw_act_list.push_back(act); + } + /* func_inst->is_read() <==> read + rmw */ if (func_inst->is_read()) { rw_act_list.push_back(act); /* If func_inst may only read_from a single location, then: * - * The first time an action reads from some location, import all the values that have - * been written to this location from ModelHistory and notify ModelHistory that this - * FuncNode may read from this location. + * The first time an action reads from some location, + * import all the values that have been written to this + * location from ModelHistory and notify ModelHistory + * that this FuncNode may read from this location. */ void * loc = act->get_location(); if (!read_locations->contains(loc) && func_inst->is_single_location()) { @@ -273,6 +280,9 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) continue; } + if (next_act->is_write()) + curr_pred->set_write(true); + inst_pred_map.put(next_inst, curr_pred); if (!inst_id_map.contains(next_inst)) inst_id_map.put(next_inst, inst_counter++); @@ -304,6 +314,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model PredExprSet * pred_expressions = branch->get_pred_expressions(); PredExprSetIter * pred_expr_it = pred_expressions->iterator(); + /* Only read and rmw actions my have unset predicate expressions */ if (pred_expressions->getSize() == 0) { predicate_correct = false; unset_predicates->push_back(branch); @@ -355,6 +366,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model return branch_found; } +/* Infer predicate expressions, which are generated in FuncNode::generate_predicates */ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act, HashTable * loc_act_map, SnapVector * half_pred_expressions) @@ -362,6 +374,7 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act, void * loc = next_act->get_location(); if (next_inst->is_read()) { + /* read + rmw */ if ( loc_act_map->contains(loc) ) { ModelAction * last_act = loc_act_map->get(loc); FuncInst * last_inst = get_inst(last_act); @@ -394,7 +407,8 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act, } } } else { - // TODO: when next_act is a write action, do anything? + /* Pure writes */ + // TODO: do anything here? } } @@ -407,12 +421,14 @@ void FuncNode::generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, (*curr_pred)->add_child(new_pred); new_pred->set_parent(*curr_pred); - /* entry predicates and predicates containing write actions + /* entry predicates and predicates containing pure write actions * have no predicate expressions */ if ( (*curr_pred)->is_entry_predicate() ) new_pred->add_predicate_expr(NOPREDICATE, NULL, true); - else if (next_inst->is_write()) + else if (next_inst->is_write()) { + /* next_inst->is_write() <==> pure writes */ new_pred->add_predicate_expr(NOPREDICATE, NULL, true); + } return; } @@ -526,6 +542,7 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location } } +/* Every time a thread enters a function, set its position to the predicate tree entry */ void FuncNode::init_predicate_tree_position(thread_id_t tid) { int thread_id = id_to_int(tid); @@ -541,12 +558,14 @@ void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred) predicate_tree_position[thread_id] = pred; } +/* @return The position of a thread in a predicate tree */ Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid) { int thread_id = id_to_int(tid); return predicate_tree_position[thread_id]; } +/* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */ void FuncNode::init_inst_act_map(thread_id_t tid) { int thread_id = id_to_int(tid); @@ -561,6 +580,7 @@ void FuncNode::init_inst_act_map(thread_id_t tid) } } +/* Reset elements of thrd_inst_act_map when threads exit functions */ void FuncNode::reset_inst_act_map(thread_id_t tid) { int thread_id = id_to_int(tid); diff --git a/funcnode.h b/funcnode.h index 53f071f1..b022284a 100644 --- a/funcnode.h +++ b/funcnode.h @@ -32,12 +32,8 @@ public: void update_tree(action_list_t * act_list); void update_inst_tree(func_inst_list_t * inst_list); - void update_predicate_tree(action_list_t * act_list); bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable * inst_act_map, SnapVector * unset_predicates); - void infer_predicates(FuncInst * next_inst, ModelAction * next_act, HashTable * loc_act_map, SnapVector * half_pred_expressions); - void generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, SnapVector * half_pred_expressions); - bool amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act); void incr_exit_count() { exit_count++; } uint32_t get_exit_count() { return exit_count; } @@ -82,21 +78,26 @@ private: /* Possible entry atomic actions in this function */ func_inst_list_mt entry_insts; + void infer_predicates(FuncInst * next_inst, ModelAction * next_act, HashTable * loc_act_map, SnapVector * half_pred_expressions); + void generate_predicates(Predicate ** curr_pred, FuncInst * next_inst, SnapVector * half_pred_expressions); + bool amend_predicate_expr(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act); + /* Store action_lists when calls to update_tree are deferred */ ModelList action_list_buffer; /* read_locations: set of locations read by this FuncNode * val_loc_map: keep track of locations that have the same values written to; - * loc_may_equal_map: deduced from val_loc_map; - */ + * loc_may_equal_map: look up locations that may share the same value as key; + * deduced from val_loc_map; */ loc_set_t * read_locations; HashTable * val_loc_map; HashTable * loc_may_equal_map; // value_set_t * values_may_read_from; - /* run-time position in the predicate tree for each thread */ + /* Run-time position in the predicate tree for each thread */ ModelVector predicate_tree_position; + /* A run-time map from FuncInst to ModelAction for each thread; needed by NewFuzzer */ SnapVector * thrd_inst_act_map; }; diff --git a/predicate.cc b/predicate.cc index 2d777778..5cc0219c 100644 --- a/predicate.cc +++ b/predicate.cc @@ -3,6 +3,7 @@ Predicate::Predicate(FuncInst * func_inst, bool is_entry) : func_inst(func_inst), entry_predicate(is_entry), + does_write(false), pred_expressions(16), children(), parent(NULL), @@ -89,6 +90,10 @@ void Predicate::print_predicate() break; } } + + if (does_write) { + model_print("Does write\n"); + } model_print("\"];\n"); } diff --git a/predicate.h b/predicate.h index e901d91f..4243a0d8 100644 --- a/predicate.h +++ b/predicate.h @@ -66,6 +66,10 @@ public: bool is_entry_predicate() { return entry_predicate; } void set_entry_predicate() { entry_predicate = true; } + /* Whether func_inst does write or not */ + bool is_write() { return does_write; } + void set_write(bool is_write) { does_write = is_write; } + void print_predicate(); void print_pred_subtree(); @@ -73,15 +77,16 @@ public: private: FuncInst * func_inst; bool entry_predicate; + bool does_write; - /* may have multiple predicate expressions */ + /* May have multiple predicate expressions */ PredExprSet pred_expressions; ModelVector children; - /* only a single parent may exist */ + /* Only a single parent may exist */ Predicate * parent; - /* may have multiple back edges, e.g. nested loops */ + /* May have multiple back edges, e.g. nested loops */ PredSet backedges; }; -- 2.34.1