From: weiyu Date: Thu, 15 Aug 2019 02:16:47 +0000 (-0700) Subject: change the structure of predicate expressions, and modify the way nullity predicates... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f8a45d8d10f16533c926096c7538b4d9be73240b;p=c11tester.git change the structure of predicate expressions, and modify the way nullity predicates are added --- diff --git a/funcnode.cc b/funcnode.cc index 5b6fb355..2bdd946d 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -225,6 +225,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) /* map a FuncInst to the parent of 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; @@ -234,7 +235,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) FuncInst * next_inst = get_inst(next_act); Predicate * old_pred = curr_pred; - bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &loc_act_map); + bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map); // check back edges if (!branch_found) { @@ -257,18 +258,20 @@ 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(EQUALITY, next_act->get_location(), true); + new_pred1->add_predicate_expr(EQUALITY, last_inst, true); Predicate * new_pred2 = new Predicate(next_inst); - new_pred2->add_predicate(EQUALITY, next_act->get_location(), false); + 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); - ModelAction * last_act = loc_act_map.get(next_act->get_location()); uint64_t last_read = last_act->get_reads_from_value(); uint64_t next_read = next_act->get_reads_from_value(); @@ -286,6 +289,7 @@ void FuncNode::update_predicate_tree(action_list_t * act_list) } loc_act_map.put(next_act->get_location(), next_act); + inst_act_map.put(next_inst, next_act); it = it->getNext(); } } @@ -307,11 +311,12 @@ void FuncNode::deep_update(Predicate * curr_pred) if (!has_null_pred) { // func_inst->print(); - Predicate * parent = curr_pred->get_parent(); - curr_pred->add_predicate(NULLITY, NULL, 0); - Predicate * another_branch = new Predicate(func_inst); - another_branch->add_predicate(NULLITY, NULL, 1); + another_branch->copy_predicate_expr(curr_pred); + another_branch->add_predicate_expr(NULLITY, NULL, 1); + curr_pred->add_predicate_expr(NULLITY, NULL, 0); + + Predicate * parent = curr_pred->get_parent(); parent->add_child(another_branch); // another_branch.add_children(i); } @@ -324,11 +329,12 @@ void FuncNode::deep_update(Predicate * curr_pred) } } -/* Given curr_pred and next_inst, find the branch following curr_pred that contains next_inst and the correct predicate +/* Given curr_pred and next_inst, find the branch following curr_pred that + * contains next_inst and the correct predicate. * @return true if branch found, false otherwise. */ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, - HashTable * loc_act_map) + HashTable * inst_act_map) { /* check if a branch with func_inst and corresponding predicate exists */ bool branch_found = false; @@ -351,12 +357,16 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model while (pred_expr_it->hasNext()) { pred_expr * pred_expression = pred_expr_it->next(); uint64_t last_read, next_read; - ModelAction * last_act; bool equality; switch(pred_expression->token) { case EQUALITY: - last_act = loc_act_map->get(next_act->get_location()); + FuncInst * to_be_compared; + ModelAction * last_act; + + to_be_compared = pred_expression->func_inst; + last_act = inst_act_map->get(to_be_compared); + last_read = last_act->get_reads_from_value(); next_read = next_act->get_reads_from_value(); diff --git a/funcnode.h b/funcnode.h index 730a7b7c..4e1f98d3 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* loc_act_map); + bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable* inst_act_map); void print_predicate_tree(); void print_last_read(uint32_t tid); diff --git a/predicate.cc b/predicate.cc index 128ac3dc..9ba69d38 100644 --- a/predicate.cc +++ b/predicate.cc @@ -18,16 +18,16 @@ bool pred_expr_equal(struct pred_expr * p1, struct pred_expr * p2) { if (p1->token != p2->token) return false; - if (p1->token == EQUALITY && p1->location != p2->location) + if (p1->token == EQUALITY && p1->func_inst != p2->func_inst) return false; if (p1->value != p2->value) return false; return true; } -void Predicate::add_predicate(token_t token, void * location, bool value) +void Predicate::add_predicate_expr(token_t token, FuncInst * func_inst, bool value) { - struct pred_expr *ptr = new pred_expr(token, location, value); + struct pred_expr *ptr = new pred_expr(token, func_inst, value); pred_expressions.add(ptr); } @@ -37,6 +37,18 @@ void Predicate::add_child(Predicate * child) children.push_back(child); } +void Predicate::copy_predicate_expr(Predicate * other) +{ + PredExprSet * other_pred_expressions = other->get_pred_expressions(); + PredExprSetIter * it = other_pred_expressions->iterator(); + + while (it->hasNext()) { + struct pred_expr * ptr = it->next(); + struct pred_expr * copy = new pred_expr(ptr->token, ptr->func_inst, ptr->value); + pred_expressions.add(copy); + } +} + void Predicate::print_predicate() { model_print("\"%p\" [shape=box, label=\"\n", this); @@ -54,7 +66,18 @@ void Predicate::print_predicate() while (it->hasNext()) { struct pred_expr * expr = it->next(); - model_print("predicate: token: %d, location: %p, value: %d\n", expr->token, expr->location, expr->value); + FuncInst * inst = expr->func_inst; + switch (expr->token) { + case EQUALITY: + model_print("predicate token: equality, position: %s, value: %d\n", inst->get_position(), expr->value); + break; + case NULLITY: + model_print("predicate token: nullity, value: %d\n", expr->value); + break; + default: + model_print("unknown predicate token\n"); + break; + } } model_print("\"];\n"); } diff --git a/predicate.h b/predicate.h index dbb959ea..3efd8905 100644 --- a/predicate.h +++ b/predicate.h @@ -18,14 +18,14 @@ typedef enum predicate_token { * read at memory location specified in predicate_expr. */ struct pred_expr { - pred_expr(token_t token, void * location, bool value) : + pred_expr(token_t token, FuncInst * inst, bool value) : token(token), - location(location), + func_inst(inst), value(value) {} token_t token; - void * location; + FuncInst * func_inst; bool value; MEMALLOC @@ -39,10 +39,12 @@ public: FuncInst * get_func_inst() { return func_inst; } PredExprSet * get_pred_expressions() { return &pred_expressions; } - void add_predicate(token_t token, void * location, bool value); + + void add_predicate_expr(token_t token, FuncInst * func_inst, bool value); void add_child(Predicate * child); void set_parent(Predicate * parent_pred) { parent = parent_pred; } void set_backedge(Predicate * back_pred) { backedge = back_pred; } + void copy_predicate_expr(Predicate * other); ModelVector * get_children() { return &children; } Predicate * get_parent() { return parent; }