X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=funcnode.cc;h=55785fa89ca6060caab68d8a3d50710f43c073b2;hp=952824ce5db2df7c5a00a9616dd81a954a776c4a;hb=251ac4b4bf3a9f2d3cfacc1e6618200ca1c431ac;hpb=7da037811c33ae78db573226a1c5a4907a967962 diff --git a/funcnode.cc b/funcnode.cc index 952824ce..55785fa8 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -11,9 +11,12 @@ #include FuncNode::FuncNode(ModelHistory * history) : + func_id(0), + func_name(NULL), history(history), inst_counter(1), marker(1), + exit_count(0), thrd_markers(), thrd_recursion_depth(), func_inst_map(), @@ -22,6 +25,7 @@ FuncNode::FuncNode(ModelHistory * history) : thrd_inst_pred_maps(), thrd_inst_id_maps(), thrd_loc_inst_maps(), + likely_null_set(), thrd_predicate_tree_position(), thrd_predicate_trace(), edge_table(32), @@ -189,6 +193,11 @@ void FuncNode::function_exit_handler(thread_id_t tid) update_predicate_tree_weight(tid); reset_predicate_tree_data_structure(tid); + + exit_count++; + //model_print("exit count: %d\n", exit_count); + +// print_predicate_tree(); } /** @@ -219,13 +228,9 @@ void FuncNode::update_tree(ModelAction * act) write_locations->add(loc); history->update_loc_wr_func_nodes_map(loc, this); } - - // Do not process writes for now - return; } if (act->is_read()) { - /* If func_inst may only read_from a single location, then: * * The first time an action reads from some location, @@ -239,12 +244,15 @@ void FuncNode::update_tree(ModelAction * act) add_to_val_loc_map(write_values, loc); history->update_loc_rd_func_nodes_map(loc, this); } + + // Keep a has-been-zero-set record + if ( likely_reads_from_null(act) ) + likely_null_set.put(func_inst, true); } // update_inst_tree(&inst_list); TODO - update_predicate_tree(act); -// print_predicate_tree(); + update_predicate_tree(act); } /** @@ -298,7 +306,6 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) bool amended; while (true) { FuncInst * next_inst = get_inst(next_act); - next_inst->set_associated_read(tid, recursion_depth, this_marker, next_act->get_reads_from_value()); Predicate * unset_predicate = NULL; bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicate); @@ -340,12 +347,13 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) continue; } - if (next_act->is_write()) + if (next_act->is_write()) { curr_pred->set_write(true); + } if (next_act->is_read()) { /* Only need to store the locations of read actions */ - loc_inst_map->put(next_inst->get_location(), next_inst); + loc_inst_map->put(next_act->get_location(), next_inst); } inst_pred_map->put(next_inst, curr_pred); @@ -356,12 +364,17 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) curr_pred->incr_expl_count(); add_predicate_to_trace(tid, curr_pred); + if (next_act->is_read()) + next_inst->set_associated_read(tid, recursion_depth, this_marker, next_act->get_reads_from_value()); + break; } // A check - if (selected_branch != NULL && !amended) - ASSERT(selected_branch == curr_pred); + if (next_act->is_read()) { +// if (selected_branch != NULL && !amended) +// ASSERT(selected_branch == curr_pred); + } } /* Given curr_pred and next_inst, find the branch following curr_pred that @@ -374,9 +387,6 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, /* Check if a branch with func_inst and corresponding predicate exists */ bool branch_found = false; thread_id_t tid = next_act->get_tid(); - int thread_id = id_to_int(tid); - uint32_t this_marker = thrd_markers[thread_id]->back(); - int recursion_depth = thrd_recursion_depth[thread_id]; ModelVector * branches = (*curr_pred)->get_children(); for (uint i = 0;i < branches->size();i++) { @@ -413,10 +423,11 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, case EQUALITY: FuncInst * to_be_compared; to_be_compared = pred_expression->func_inst; - ASSERT(to_be_compared != next_inst); - last_read = to_be_compared->get_associated_read(tid, recursion_depth, this_marker); - ASSERT(last_read != VALUE_NONE); + last_read = get_associated_read(tid, to_be_compared); + if (last_read == VALUE_NONE) + predicate_correct = false; + // ASSERT(last_read != VALUE_NONE); next_read = next_act->get_reads_from_value(); equality = (last_read == next_read); @@ -425,9 +436,8 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, break; case NULLITY: - next_read = next_act->get_reads_from_value(); // TODO: implement likely to be null - equality = ( (void*) (next_read & 0xffffffff) == NULL); + equality = likely_reads_from_null(next_act); if (equality != pred_expression->value) predicate_correct = false; break; @@ -481,15 +491,13 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act, delete loc_it; } - } else { - // next_inst is not single location - uint64_t read_val = next_act->get_reads_from_value(); + } - // only infer NULLITY predicate when it is actually NULL. - if ( (void*)read_val == NULL) { - struct half_pred_expr * expression = new half_pred_expr(NULLITY, NULL); - half_pred_expressions->push_back(expression); - } + // next_inst is not single location and has been null + bool likely_null = likely_null_set.contains(next_inst); + if ( !next_inst->is_single_location() && likely_null ) { + struct half_pred_expr * expression = new half_pred_expr(NULLITY, NULL); + half_pred_expressions->push_back(expression); } } else { /* Pure writes */ @@ -570,10 +578,10 @@ bool FuncNode::amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, } } - uint64_t read_val = next_act->get_reads_from_value(); + bool likely_null = likely_null_set.contains(next_inst); // only generate NULLITY predicate when it is actually NULL. - if ( !next_inst->is_single_location() && (void*)read_val == NULL ) { + if ( !next_inst->is_single_location() && likely_null ) { Predicate * new_pred = new Predicate(next_inst); curr_pred->add_child(new_pred); @@ -646,6 +654,15 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location delete loc_it; } +bool FuncNode::likely_reads_from_null(ModelAction * read) +{ + uint64_t read_val = read->get_reads_from_value(); + if ( (void *)(read_val && 0xffffffff) == NULL ) + return true; + + return false; +} + void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred) { int thread_id = id_to_int(tid); @@ -676,7 +693,7 @@ void FuncNode::init_marker(thread_id_t tid) if (old_size < thread_id + 1) { thrd_markers.resize(thread_id + 1); - for (int i = old_size; i < thread_id + 1; i++) { + for (int i = old_size;i < thread_id + 1;i++) { thrd_markers[i] = new ModelVector(); thrd_recursion_depth.push_back(-1); } @@ -686,15 +703,13 @@ void FuncNode::init_marker(thread_id_t tid) thrd_recursion_depth[thread_id]++; } -uint32_t FuncNode::get_marker(thread_id_t tid) +uint64_t FuncNode::get_associated_read(thread_id_t tid, FuncInst * inst) { int thread_id = id_to_int(tid); - return thrd_markers[thread_id]->back(); -} + int recursion_depth = thrd_recursion_depth[thread_id]; + uint marker = thrd_markers[thread_id]->back(); -int FuncNode::get_recursion_depth(thread_id_t tid) -{ - return thrd_recursion_depth[id_to_int(tid)]; + return inst->get_associated_read(tid, recursion_depth, marker); } /* Make sure elements of maps are initialized properly when threads enter functions */ @@ -710,7 +725,7 @@ void FuncNode::init_local_maps(thread_id_t tid) thrd_inst_id_maps.resize(new_size); thrd_inst_pred_maps.resize(new_size); - for (int i = old_size; i < new_size; i++) { + for (int i = old_size;i < new_size;i++) { thrd_loc_inst_maps[i] = new ModelVector; thrd_inst_id_maps[i] = new ModelVector; thrd_inst_pred_maps[i] = new ModelVector; @@ -761,7 +776,7 @@ void FuncNode::init_predicate_tree_data_structure(thread_id_t tid) thrd_predicate_tree_position.resize(thread_id + 1); thrd_predicate_trace.resize(thread_id + 1); - for (int i = old_size; i < thread_id + 1; i++) { + for (int i = old_size;i < thread_id + 1;i++) { thrd_predicate_tree_position[i] = new ModelVector(); thrd_predicate_trace[i] = new ModelVector(); } @@ -777,8 +792,7 @@ void FuncNode::reset_predicate_tree_data_structure(thread_id_t tid) thrd_predicate_tree_position[thread_id]->pop_back(); // Free memories allocated in init_predicate_tree_data_structure - predicate_trace_t * trace = thrd_predicate_trace[thread_id]->back(); - delete trace; + delete thrd_predicate_trace[thread_id]->back(); thrd_predicate_trace[thread_id]->pop_back(); } @@ -809,6 +823,7 @@ int FuncNode::compute_distance(FuncNode * target, int max_step) else if (target == this) return 0; + // Be careful with memory SnapList queue; HashTable distances(128); @@ -848,8 +863,8 @@ void FuncNode::update_predicate_tree_weight(thread_id_t tid) predicate_trace_t * trace = thrd_predicate_trace[id_to_int(tid)]->back(); // Update predicate weights based on prediate trace - for (mllnode * rit = trace->end(); rit != NULL; rit = rit->getPrev()) { - Predicate * node = rit->getVal(); + for (int i = trace->size() - 1;i >= 0;i--) { + Predicate * node = (*trace)[i]; ModelVector * children = node->get_children(); if (children->size() == 0) {