FuncNode::FuncNode() :
predicate_tree_initialized(false),
predicate_tree_entry(new Predicate(NULL, true)),
+ exit_count(0),
func_inst_map(),
inst_list(),
entry_insts(),
if (!branch_found && unset_predicates->size() != 0) {
ASSERT(unset_predicates->size() == 1);
Predicate * one_branch = (*unset_predicates)[0];
-
- if (!next_inst->is_single_location()) {
- Predicate * another_branch = new Predicate(next_inst);
- // another_branch->copy_predicate_expr(one_branch);
-
- uint64_t next_read = next_act->get_reads_from_value();
- bool isnull = ((void*)next_read == NULL);
- if (isnull) {
- one_branch->add_predicate_expr(NULLITY, NULL, 1);
- another_branch->add_predicate_expr(NULLITY, NULL, 0);
- } else {
- another_branch->add_predicate_expr(NULLITY, NULL, 1);
- one_branch->add_predicate_expr(NULLITY, NULL, 0);
- }
-
- curr_pred->add_child(another_branch);
- another_branch->set_parent(curr_pred);
- }
-
curr_pred = one_branch;
branch_found = true;
}
curr_pred = new_pred1;
else
curr_pred = new_pred2;
+ } else if (!next_inst->is_single_location()) {
+ Predicate * new_pred1 = new Predicate(next_inst);
+ new_pred1->add_predicate_expr(NULLITY, NULL, true);
+
+ Predicate * new_pred2 = new Predicate(next_inst);
+ new_pred2->add_predicate_expr(NULLITY, NULL, 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);
+
+ uint64_t next_read = next_act->get_reads_from_value();
+ bool isnull = ((void*)next_read == NULL);
+ if (isnull)
+ curr_pred = new_pred1;
+ else
+ curr_pred = new_pred2;
} else {
Predicate * new_pred = new Predicate(next_inst);
curr_pred->add_child(new_pred);
Predicate * parent = curr_pred->get_parent();
parent->add_child(another_branch);
-// another_branch.add_children(i);
}
}
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 print_predicate_tree();
+ void incr_exit_count() { exit_count++; }
+ uint32_t get_exit_count() { return exit_count; }
+
+ ModelList<action_list_t *> * get_action_list_buffer() { return &action_list_buffer; }
+
+ void print_predicate_tree();
void print_last_read(uint32_t tid);
MEMALLOC
bool predicate_tree_initialized;
Predicate * predicate_tree_entry; // a dummy node whose children are the real entries
+ uint32_t exit_count;
+
/* Use source line number as the key of hashtable, to check if
* atomic operation with this line number has been added or not
*/
/* Store the values read by atomic read actions per memory location for each thread */
ModelVector<read_map_t *> thrd_read_map;
+
+ ModelList<action_list_t *> action_list_buffer;
};
#endif /* __FUNCNODE_H__ */
FuncNode * func_node = func_nodes[func_id];
func_node->clear_read_map(tid);
- // model_print("hello function %s and thread %d\n", func_node->get_func_name(), tid);
action_list_t * curr_act_list = func_act_lists->back();
- func_node->update_tree(curr_act_list);
+ func_node->incr_exit_count();
+
+ /* defer the processing of curr_act_list until the function has exits a few times
+ * (currently 2 times) so that more information can be gathered to infer nullity predicates.
+ */
+ if (func_node->get_exit_count() >= 2) {
+ ModelList<action_list_t *> * action_list_buffer = func_node->get_action_list_buffer();
+ while (action_list_buffer->size() > 0) {
+ action_list_t * act_list = action_list_buffer->back();
+ action_list_buffer->pop_back();
+ func_node->update_tree(act_list);
+ }
+
+ func_node->update_tree(curr_act_list);
+ } else
+ func_node->get_action_list_buffer()->push_front(curr_act_list);
(*thrd_func_list)[id].pop_back();
func_act_lists->pop_back();