From 41757c6c33945d547c0afa3b9456009e941540f3 Mon Sep 17 00:00:00 2001 From: weiyu Date: Thu, 22 Aug 2019 18:19:06 -0700 Subject: [PATCH] restructure code and working on deconstructors --- funcnode.cc | 165 ++++++++++++++++++++++++--------------------------- funcnode.h | 1 + predicate.cc | 11 ++++ predicate.h | 2 +- 4 files changed, 91 insertions(+), 88 deletions(-) diff --git a/funcnode.cc b/funcnode.cc index 26dfe5c9..aa99e972 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -317,95 +317,27 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) } if (!branch_found) { - if ( loc_act_map.contains(next_act->get_location()) ) { - ModelAction * last_act = loc_act_map.get(next_act->get_location()); - FuncInst * last_inst = get_inst(last_act); - - Predicate * new_pred1 = new Predicate(next_inst); - new_pred1->add_predicate_expr(EQUALITY, last_inst, true); - - Predicate * new_pred2 = new Predicate(next_inst); - new_pred2->add_predicate_expr(EQUALITY, last_inst, false); - - curr_pred->add_child(new_pred1); - curr_pred->add_child(new_pred2); - new_pred1->set_parent(curr_pred); - new_pred2->set_parent(curr_pred); - - uint64_t last_read = last_act->get_reads_from_value(); - uint64_t next_read = next_act->get_reads_from_value(); - - if ( last_read == next_read ) - curr_pred = new_pred1; - else - curr_pred = new_pred2; - } else if (!next_inst->is_single_location()) { - Predicate * new_pred1 = new Predicate(next_inst); - new_pred1->add_predicate_expr(NULLITY, NULL, true); - - Predicate * new_pred2 = new Predicate(next_inst); - new_pred2->add_predicate_expr(NULLITY, NULL, false); - - curr_pred->add_child(new_pred1); - curr_pred->add_child(new_pred2); - new_pred1->set_parent(curr_pred); - new_pred2->set_parent(curr_pred); - - uint64_t next_read = next_act->get_reads_from_value(); - bool isnull = ((void*)next_read == NULL); - if (isnull) - curr_pred = new_pred1; - else - curr_pred = new_pred2; - } else { - bool test = false; - void * loc = next_act->get_location(); - loc_set_t * loc_may_equal = loc_may_equal_map->get(loc); - if (loc_may_equal != NULL) { - loc_set_iter * loc_it = loc_may_equal->iterator(); - while (loc_it->hasNext()) { - void * neighbor = loc_it->next(); - if (loc_act_map.contains(neighbor)) { - model_print("loc %p may eqaul to loc %p\n", loc, neighbor); - ModelAction * last_act = loc_act_map.get(neighbor); - - FuncInst * last_inst = get_inst(last_act); - - Predicate * new_pred1 = new Predicate(next_inst); - new_pred1->add_predicate_expr(EQUALITY, last_inst, true); - - Predicate * new_pred2 = new Predicate(next_inst); - new_pred2->add_predicate_expr(EQUALITY, last_inst, false); - - curr_pred->add_child(new_pred1); - curr_pred->add_child(new_pred2); - new_pred1->set_parent(curr_pred); - new_pred2->set_parent(curr_pred); - - uint64_t last_read = last_act->get_reads_from_value(); - uint64_t next_read = next_act->get_reads_from_value(); - - if ( last_read == next_read ) - curr_pred = new_pred1; - else - curr_pred = new_pred2; - - test = true; - break; - } + bool may_equal = false; + void * loc = next_act->get_location(); + loc_set_t * loc_may_equal = loc_may_equal_map->get(loc); + if (loc_may_equal != NULL) { + loc_set_iter * loc_it = loc_may_equal->iterator(); + while (loc_it->hasNext()) { + void * neighbor = loc_it->next(); + if (loc_act_map.contains(neighbor)) { + model_print("loc %p may eqaul to loc %p\n", loc, neighbor); + gen_predicate_and_follow(&curr_pred, next_inst, next_act, &loc_act_map, EQUALITY, neighbor); + may_equal = true; + break; } - } - - if (!test) { - Predicate * new_pred = new Predicate(next_inst); - curr_pred->add_child(new_pred); - new_pred->set_parent(curr_pred); - - if (curr_pred->is_entry_predicate()) - new_pred->add_predicate_expr(NOPREDICATE, NULL, true); - - curr_pred = new_pred; } + } + + if (!may_equal) { + if (!next_inst->is_single_location()) + gen_predicate_and_follow(&curr_pred, next_inst, next_act, &loc_act_map, NULLITY, NULL); + else + gen_predicate_and_follow(&curr_pred, next_inst, next_act, &loc_act_map, UNSET, NULL); } } @@ -525,6 +457,65 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model return branch_found; } +void FuncNode::gen_predicate_and_follow(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, + HashTable * loc_act_map, token_t token, void * loc) +{ + Predicate * new_pred1 = new Predicate(next_inst); + Predicate * new_pred2 = new Predicate(next_inst); + new_pred1->set_parent(*curr_pred); + new_pred2->set_parent(*curr_pred); + + uint64_t next_read = next_act->get_reads_from_value(); + + switch (token) { + case UNSET: + if ( (*curr_pred)->is_entry_predicate() ) + new_pred1->add_predicate_expr(NOPREDICATE, NULL, true); + + (*curr_pred)->add_child(new_pred1); + *curr_pred = new_pred1; + delete new_pred2; + + break; + case EQUALITY: + ModelAction * last_act; + FuncInst * last_inst; + uint64_t last_read; + + last_act = loc_act_map->get(loc); + last_inst = get_inst(last_act); + last_read = last_act->get_reads_from_value(); + + new_pred1->add_predicate_expr(EQUALITY, last_inst, true); + new_pred2->add_predicate_expr(EQUALITY, last_inst, false); + (*curr_pred)->add_child(new_pred1); + (*curr_pred)->add_child(new_pred2); + + if ( last_read == next_read ) + *curr_pred = new_pred1; + else + *curr_pred = new_pred2; + break; + case NULLITY: + new_pred1->add_predicate_expr(NULLITY, NULL, true); + new_pred2->add_predicate_expr(NULLITY, NULL, false); + (*curr_pred)->add_child(new_pred1); + (*curr_pred)->add_child(new_pred2); + + if ( (void*)next_read == NULL ) + *curr_pred = new_pred1; + else + *curr_pred = new_pred2; + break; + default: + model_print("unknown predicate token\n"); + delete new_pred1; + delete new_pred2; + + break; + } +} + void FuncNode::add_to_val_loc_map(uint64_t val, void * loc) { loc_set_t * locations = val_loc_map->get(val); diff --git a/funcnode.h b/funcnode.h index 277e5256..2a5781bb 100644 --- a/funcnode.h +++ b/funcnode.h @@ -41,6 +41,7 @@ public: void update_predicate_tree(action_list_t * act_list); void deep_update(Predicate * pred); bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable* inst_act_map, SnapVector * unset_predicates); + void gen_predicate_and_follow(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable * loc_act_map, token_t token, void * loc); void incr_exit_count() { exit_count++; } uint32_t get_exit_count() { return exit_count; } diff --git a/predicate.cc b/predicate.cc index c8e39891..56954528 100644 --- a/predicate.cc +++ b/predicate.cc @@ -9,6 +9,17 @@ Predicate::Predicate(FuncInst * func_inst, bool is_entry) : backedges(16) {} +Predicate::~Predicate() +{ +// if (func_inst) +// delete func_inst; + + // parent should not be deleted + pred_expressions.reset(); + backedges.reset(); + children.clear(); +} + unsigned int pred_expr_hash(struct pred_expr * expr) { return (unsigned int)((uintptr_t)expr); diff --git a/predicate.h b/predicate.h index 732e39ab..f787983f 100644 --- a/predicate.h +++ b/predicate.h @@ -10,7 +10,7 @@ typedef HashSet PredExprSetIter; typedef enum predicate_token { - NOPREDICATE, EQUALITY, NULLITY + NOPREDICATE, UNSET, EQUALITY, NULLITY } token_t; /* If token is EQUALITY, then the predicate asserts whether -- 2.34.1