X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=funcnode.cc;h=b28fbd5bb5c8b925af9cc0573be8cecec1cd16b6;hp=d328a4c5d24f6753fe0faf9338e153bc7284072a;hb=c0c4fcf47d8209da26e686b308d8c20ffc8220d3;hpb=70acabc306bc3014b3698e394908faf23a66a0b8 diff --git a/funcnode.cc b/funcnode.cc index d328a4c5..b28fbd5b 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -1,4 +1,11 @@ +#include "action.h" +#include "history.h" #include "funcnode.h" +#include "funcinst.h" +#include "predicate.h" +#include "concretepredicate.h" + +#include "model.h" FuncNode::FuncNode(ModelHistory * history) : history(history), @@ -19,7 +26,6 @@ FuncNode::FuncNode(ModelHistory * history) : write_locations = new loc_set_t(); val_loc_map = new HashTable(); loc_may_equal_map = new HashTable(); - thrd_inst_act_map = new SnapVector(); //values_may_read_from = new value_set_t(); } @@ -27,17 +33,11 @@ FuncNode::FuncNode(ModelHistory * history) : /* Reallocate snapshotted memories when new executions start */ void FuncNode::set_new_exec_flag() { - for (mllnode * it = inst_list.begin(); it != NULL; it = it->getNext()) { - FuncInst * inst = it->getVal(); - inst->unset_location(); - } - action_list_buffer = new SnapList(); read_locations = new loc_set_t(); write_locations = new loc_set_t(); val_loc_map = new HashTable(); loc_may_equal_map = new HashTable(); - thrd_inst_act_map = new SnapVector(); //values_may_read_from = new value_set_t(); } @@ -63,10 +63,13 @@ void FuncNode::add_inst(ModelAction *act) FuncInst * inst = func_inst_map.get(position); ASSERT(inst->get_type() == act->get_type()); + int curr_execution_number = model->get_execution_number(); - // locations are set to NULL when new executions start - if (inst->get_location() == NULL) + /* Reset locations when new executions start */ + if (inst->get_execution_number() != curr_execution_number) { inst->set_location(act->get_location()); + inst->set_execution_number(curr_execution_number); + } if (inst->get_location() != act->get_location()) inst->not_single_location(); @@ -136,7 +139,7 @@ void FuncNode::update_tree(action_list_t * act_list) if (act_list == NULL || act_list->size() == 0) return; - HashTable * write_history = history->getWriteHistory(); + HashTable * write_history = history->getWriteHistory(); /* build inst_list from act_list for later processing */ func_inst_list_t inst_list; @@ -178,7 +181,7 @@ void FuncNode::update_tree(action_list_t * act_list) read_locations->add(loc); value_set_t * write_values = write_history->get(loc); add_to_val_loc_map(write_values, loc); - history->update_loc_func_nodes_map(loc, this); + history->update_loc_rd_func_nodes_map(loc, this); } } } @@ -331,9 +334,10 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model unset_predicates->push_back(branch); } - SnapVector concrete_exprs = branch->evaluate(inst_act_map); - for (uint i = 0; i < concrete_exprs.size(); i++) { - struct concrete_pred_expr concrete = concrete_exprs[i]; + ConcretePredicate * concrete_pred = branch->evaluate(inst_act_map, next_act->get_tid()); + SnapVector * concrete_exprs = concrete_pred->getExpressions(); + for (uint i = 0; i < concrete_exprs->size(); i++) { + struct concrete_pred_expr concrete = (*concrete_exprs)[i]; uint64_t next_read; bool equality; @@ -359,6 +363,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model break; } } + delete concrete_pred; if (predicate_correct) { *curr_pred = branch; @@ -579,6 +584,7 @@ Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid) void FuncNode::init_inst_act_map(thread_id_t tid) { int thread_id = id_to_int(tid); + SnapVector * thrd_inst_act_map = history->getThrdInstActMap(func_id); uint old_size = thrd_inst_act_map->size(); if (thrd_inst_act_map->size() <= (uint) thread_id) { @@ -594,6 +600,8 @@ void FuncNode::init_inst_act_map(thread_id_t tid) void FuncNode::reset_inst_act_map(thread_id_t tid) { int thread_id = id_to_int(tid); + SnapVector * thrd_inst_act_map = history->getThrdInstActMap(func_id); + inst_act_map_t * map = (*thrd_inst_act_map)[thread_id]; map->reset(); } @@ -601,6 +609,8 @@ void FuncNode::reset_inst_act_map(thread_id_t tid) void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act) { int thread_id = id_to_int(tid); + SnapVector * thrd_inst_act_map = history->getThrdInstActMap(func_id); + inst_act_map_t * map = (*thrd_inst_act_map)[thread_id]; FuncInst * read_inst = get_inst(read_act); map->put(read_inst, read_act); @@ -609,6 +619,8 @@ void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act) inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid) { int thread_id = id_to_int(tid); + SnapVector * thrd_inst_act_map = history->getThrdInstActMap(func_id); + return (*thrd_inst_act_map)[thread_id]; } @@ -628,6 +640,51 @@ void FuncNode::add_out_edge(FuncNode * other) } } +/* Compute the distance between this FuncNode and the target node. + * Return -1 if the target node is unreachable or the actual distance + * is greater than max_step. + */ +int FuncNode::compute_distance(FuncNode * target, int max_step) +{ + if (target == NULL) + return -1; + else if (target == this) + return 0; + + SnapList queue; + HashTable distances(128); + + queue.push_back(this); + distances.put(this, 0); + + while (!queue.empty()) { + FuncNode * curr = queue.front(); + queue.pop_front(); + int dist = distances.get(curr); + + if (max_step <= dist) + return -1; + + ModelList * outEdges = curr->get_out_edges(); + mllnode * it; + for (it = outEdges->begin(); it != NULL; it = it->getNext()) { + FuncNode * out_node = it->getVal(); + + /* This node has not been visited before */ + if ( !distances.contains(out_node) ) { + if (out_node == target) + return dist + 1; + + queue.push_back(out_node); + distances.put(out_node, dist + 1); + } + } + } + + /* Target node is unreachable */ + return -1; +} + void FuncNode::print_predicate_tree() { model_print("digraph function_%s {\n", func_name);