From: weiyu Date: Fri, 16 Aug 2019 02:05:01 +0000 (-0700) Subject: try to infer nullity predicate inside update_predicate_tree. Maybe rethink about... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8eee53a1677bf0aa8a3c4769dff56d2fad1886fc;p=c11tester.git try to infer nullity predicate inside update_predicate_tree. Maybe rethink about the way to check back edges --- diff --git a/funcnode.cc b/funcnode.cc index 2bdd946d..940a8f78 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -7,7 +7,9 @@ FuncNode::FuncNode() : inst_list(), entry_insts(), thrd_read_map() -{} +{ + predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true); +} /* Check whether FuncInst with the same type, position, and location * as act has been added to func_inst_map or not. If not, add it. @@ -113,9 +115,6 @@ void FuncNode::update_tree(action_list_t * act_list) inst_list.push_back(func_inst); -// model_print("position: %s ", act->get_position()); -// act->print(); - if (func_inst->is_read()) read_act_list.push_back(act); } @@ -123,7 +122,7 @@ void FuncNode::update_tree(action_list_t * act_list) model_print("function %s\n", func_name); update_inst_tree(&inst_list); update_predicate_tree(&read_act_list); - deep_update(predicate_tree_entry); +// deep_update(predicate_tree_entry); print_predicate_tree(); } @@ -222,39 +221,69 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) } predicate_tree_initialized = true; */ - /* map a FuncInst to the parent of its predicate */ + /* map a FuncInst to the its predicate */ HashTable inst_pred_map(128); HashTable loc_act_map(128); HashTable inst_act_map(128); sllnode *it = act_list->begin(); Predicate * curr_pred = predicate_tree_entry; - while (it != NULL) { ModelAction * next_act = it->getVal(); FuncInst * next_inst = get_inst(next_act); - Predicate * old_pred = curr_pred; + SnapVector * unset_predicates = new SnapVector(); + + bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map, unset_predicates); - bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map); + /* no predicate, follow the only branch */ + if (!branch_found && unset_predicates->size() != 0) { + ASSERT(unset_predicates->size() == 1); + Predicate * one_branch = (*unset_predicates)[0]; + + if (!next_inst->is_single_location()) { + Predicate * another_branch = new Predicate(next_inst); + // another_branch->copy_predicate_expr(one_branch); + + uint64_t next_read = next_act->get_reads_from_value(); + bool isnull = ((void*)next_read == NULL); + if (isnull) { + one_branch->add_predicate_expr(NULLITY, NULL, 1); + another_branch->add_predicate_expr(NULLITY, NULL, 0); + } else { + another_branch->add_predicate_expr(NULLITY, NULL, 1); + one_branch->add_predicate_expr(NULLITY, NULL, 0); + } + + curr_pred->add_child(another_branch); + another_branch->set_parent(curr_pred); + } + + curr_pred = one_branch; + branch_found = true; + } + + delete unset_predicates; // check back edges if (!branch_found) { + bool backedge_found = false; Predicate * back_pred = curr_pred->get_backedge(); if (back_pred != NULL) { curr_pred = back_pred; - continue; - } + backedge_found = true; + } else if (inst_pred_map.contains(next_inst)) { + inst_pred_map.remove(curr_pred->get_func_inst()); + Predicate * old_pred = inst_pred_map.get(next_inst); + back_pred = old_pred->get_parent(); - if (inst_pred_map.contains(next_inst)) { - back_pred = inst_pred_map.get(next_inst); curr_pred->set_backedge(back_pred); curr_pred = back_pred; - continue; + backedge_found = true; } - } - if (!inst_pred_map.contains(next_inst)) - inst_pred_map.put(next_inst, old_pred); + if (backedge_found) + continue; + } if (!branch_found) { if ( loc_act_map.contains(next_act->get_location()) ) { @@ -284,10 +313,16 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) 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 (!inst_pred_map.contains(next_inst)) + inst_pred_map.put(next_inst, curr_pred); + loc_act_map.put(next_act->get_location(), next_act); inst_act_map.put(next_inst, next_act); it = it->getNext(); @@ -334,7 +369,8 @@ void FuncNode::deep_update(Predicate * curr_pred) * @return true if branch found, false otherwise. */ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, - HashTable * inst_act_map) + HashTable * inst_act_map, + SnapVector * unset_predicates) { /* check if a branch with func_inst and corresponding predicate exists */ bool branch_found = false; @@ -344,22 +380,25 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model if (branch->get_func_inst() != next_inst) continue; + /* check against predicate expressions */ + bool predicate_correct = true; PredExprSet * pred_expressions = branch->get_pred_expressions(); + PredExprSetIter * pred_expr_it = pred_expressions->iterator(); - /* no predicate, follow the only branch */ if (pred_expressions->getSize() == 0) { - *curr_pred = branch; - branch_found = true; - break; + predicate_correct = false; + unset_predicates->push_back(branch); } - PredExprSetIter * pred_expr_it = pred_expressions->iterator(); while (pred_expr_it->hasNext()) { pred_expr * pred_expression = pred_expr_it->next(); uint64_t last_read, next_read; bool equality; switch(pred_expression->token) { + case NOPREDICATE: + predicate_correct = true; + break; case EQUALITY: FuncInst * to_be_compared; ModelAction * last_act; @@ -369,29 +408,29 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model last_read = last_act->get_reads_from_value(); next_read = next_act->get_reads_from_value(); - equality = (last_read == next_read); - if (equality == pred_expression->value) { - *curr_pred = branch; -// model_print("predicate: token: %d, location: %p, value: %d - ", pred_expression->token, pred_expression->location, pred_expression->value); next_inst->print(); - branch_found = true; - } + if (equality != pred_expression->value) + predicate_correct = false; + break; case NULLITY: next_read = next_act->get_reads_from_value(); equality = ((void*)next_read == NULL); - //model_print("%s ", next_act->get_position()); next_act->print(); - if (equality == pred_expression->value) { - *curr_pred = branch; - branch_found = true; - } + if (equality != pred_expression->value) + predicate_correct = false; break; default: + predicate_correct = false; model_print("unkown predicate token\n"); break; } } + if (predicate_correct) { + *curr_pred = branch; + branch_found = true; + break; + } } return branch_found; diff --git a/funcnode.h b/funcnode.h index 4e1f98d3..c4bf9fed 100644 --- a/funcnode.h +++ b/funcnode.h @@ -38,7 +38,7 @@ public: /* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */ 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); + bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable* inst_act_map, SnapVector * unset_predicates); void print_predicate_tree(); void print_last_read(uint32_t tid); diff --git a/predicate.cc b/predicate.cc index 9ba69d38..5bc23098 100644 --- a/predicate.cc +++ b/predicate.cc @@ -62,12 +62,14 @@ void Predicate::print_predicate() PredExprSetIter * it = pred_expressions.iterator(); if (pred_expressions.getSize() == 0) - model_print("no predicate\n"); + model_print("predicate unset\n"); while (it->hasNext()) { struct pred_expr * expr = it->next(); FuncInst * inst = expr->func_inst; switch (expr->token) { + case NOPREDICATE: + break; case EQUALITY: model_print("predicate token: equality, position: %s, value: %d\n", inst->get_position(), expr->value); break; diff --git a/predicate.h b/predicate.h index 3efd8905..dd101149 100644 --- a/predicate.h +++ b/predicate.h @@ -10,7 +10,7 @@ typedef HashSet PredExprSetIter; typedef enum predicate_token { - EQUALITY, NULLITY + NOPREDICATE, EQUALITY, NULLITY } token_t; /* If token is EQUALITY, then the predicate asserts whether