update_inst_tree(&inst_list);
update_predicate_tree(&read_act_list);
-// deep_update(predicate_tree_entry);
print_predicate_tree();
}
}
}
-void FuncNode::deep_update(Predicate * curr_pred)
-{
- FuncInst * func_inst = curr_pred->get_func_inst();
- if (func_inst != NULL && !func_inst->is_single_location()) {
- bool has_null_pred = false;
- PredExprSet * pred_expressions = curr_pred->get_pred_expressions();
- PredExprSetIter * pred_expr_it = pred_expressions->iterator();
- while (pred_expr_it->hasNext()) {
- pred_expr * pred_expression = pred_expr_it->next();
- if (pred_expression->token == NULLITY) {
- has_null_pred = true;
- break;
- }
- }
-
- if (!has_null_pred) {
-// func_inst->print();
- Predicate * another_branch = new Predicate(func_inst);
- 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);
- }
- }
-
- ModelVector<Predicate *> * branches = curr_pred->get_children();
- for (uint i = 0; i < branches->size(); i++) {
- Predicate * branch = (*branches)[i];
- deep_update(branch);
- }
-}
-
/* 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.
/* 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<FuncInst *, ModelAction *, uintptr_t, 0>* inst_act_map, SnapVector<Predicate *> * unset_predicates);
void generate_predicate(Predicate ** curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
-
void incr_exit_count() { exit_count++; }
uint32_t get_exit_count() { return exit_count; }
func_node_list->push_back(node);
}
+/* Reallocate some snapshotted memories when new executions start */
void ModelHistory::set_new_exec_flag()
{
for (uint i = 1; i < func_nodes.size(); i++) {
private:
uint32_t func_counter;
- /* map function names to integer ids */
+ /* Map function names to integer ids */
HashTable<const char *, uint32_t, uintptr_t, 4, model_malloc, model_calloc, model_free> func_map;
- /* map integer ids to function names */
+ /* Map integer ids to function names */
ModelVector<const char *> func_map_rev;
ModelVector<FuncNode *> func_nodes;
HashTable<void *, value_set_t *, uintptr_t, 4> write_history;
+
+ /* Map a location to FuncNodes that may read from it */
HashTable<void *, SnapList<FuncNode *> *, uintptr_t, 4> loc_func_nodes_map;
};