/* 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<Predicate *> * branches = (*curr_pred)->get_children();
for (uint i = 0;i < branches->size();i++) {
FuncInst * to_be_compared;
to_be_compared = pred_expression->func_inst;
- last_read = to_be_compared->get_associated_read(tid, recursion_depth, this_marker);
+ last_read = get_associated_read(tid, to_be_compared);
ASSERT(last_read != VALUE_NONE);
next_read = next_act->get_reads_from_value();
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 */
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();
}
FuncInst * create_new_inst(ModelAction *act);
FuncInst * get_inst(ModelAction *act);
- HashTable<const char *, FuncInst *, uintptr_t, 4, model_malloc, model_calloc, model_free> * getFuncInstMap() { return &func_inst_map; }
func_inst_list_mt * get_inst_list() { return &inst_list; }
func_inst_list_mt * get_entry_insts() { return &entry_insts; }
void add_entry_inst(FuncInst * inst);
void function_exit_handler(thread_id_t tid);
void update_tree(ModelAction * act);
- void update_inst_tree(func_inst_list_t * inst_list);
- void update_predicate_tree(ModelAction * act);
- bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, Predicate ** unset_predicate);
void add_to_val_loc_map(uint64_t val, void * loc);
void add_to_val_loc_map(value_set_t * values, void * loc);
void update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations);
- void set_predicate_tree_position(thread_id_t tid, Predicate * pred);
Predicate * get_predicate_tree_position(thread_id_t tid);
void add_predicate_to_trace(thread_id_t tid, Predicate *pred);
uint32_t get_marker(thread_id_t tid);
int get_recursion_depth(thread_id_t tid);
+ uint64_t get_associated_read(thread_id_t tid, FuncInst * inst);
void add_out_edge(FuncNode * other);
ModelList<FuncNode *> * get_out_edges() { return &out_edges; }
void init_local_maps(thread_id_t tid);
void reset_local_maps(thread_id_t tid);
+ void update_inst_tree(func_inst_list_t * inst_list);
+ void update_predicate_tree(ModelAction * act);
+ bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, Predicate ** unset_predicate);
+
void infer_predicates(FuncInst * next_inst, ModelAction * next_act, SnapVector<struct half_pred_expr *> * half_pred_expressions);
void generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
bool amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act);
ModelVector< ModelVector<predicate_trace_t *> * > thrd_predicate_trace;
+ void set_predicate_tree_position(thread_id_t tid, Predicate * pred);
+
void init_predicate_tree_data_structure(thread_id_t tid);
void reset_predicate_tree_data_structure(thread_id_t tid);
Predicate * curr_pred = func_node->get_predicate_tree_position(tid);
FuncInst * read_inst = func_node->get_inst(read);
- int index = func_node->get_recursion_depth(tid);
- uint32_t marker = func_node->get_marker(tid);
-
if (curr_pred != NULL) {
Predicate * selected_branch = NULL;
}
thrd_selected_child_branch[thread_id] = selected_branch;
- prune_writes(tid, index, marker, selected_branch, rf_set);
+ prune_writes(tid, selected_branch, rf_set);
}
thrd_last_read_act[thread_id] = read;
Predicate * selected_branch = get_selected_child_branch(tid);
FuncNode * func_node = history->get_curr_func_node(tid);
- int index = func_node->get_recursion_depth(tid);
- uint32_t marker = func_node->get_marker(tid);
-
// Increment failure count
selected_branch->incr_fail_count();
func_node->add_predicate_to_trace(tid, selected_branch); // For updating predicate weight
selected_branch = selectBranch(tid, curr_pred, read_inst);
thrd_selected_child_branch[thread_id] = selected_branch;
- prune_writes(tid, index, marker, selected_branch, rf_set);
+ prune_writes(tid, selected_branch, rf_set);
ASSERT(selected_branch);
}
*
* @return true if rf_set is pruned
*/
-bool NewFuzzer::prune_writes(thread_id_t tid, int index, uint32_t marker,
- Predicate * pred, SnapVector<ModelAction *> * rf_set)
+bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set)
{
if (pred == NULL)
return false;
break;
case EQUALITY:
FuncInst * to_be_compared;
+ FuncNode * func_node;
uint64_t last_read;
to_be_compared = expression->func_inst;
- last_read = to_be_compared->get_associated_read(tid, index, marker);
+ func_node = history->get_curr_func_node(tid);
+ last_read = func_node->get_associated_read(tid, to_be_compared);
ASSERT(last_read != VALUE_NONE);
equality = (write_val == last_read);
bool check_branch_inst(Predicate * curr_pred, FuncInst * read_inst, SnapVector<ModelAction *> * rf_set);
Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst);
- bool prune_writes(thread_id_t tid, int index, uint32_t marker, Predicate * pred, SnapVector<ModelAction *> * rf_set);
+ bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set);
int choose_branch_index(SnapVector<Predicate *> * branches);
/* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite.