+}
+
+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.
+ */
+bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act,
+ HashTable<FuncInst *, ModelAction *, uintptr_t, 0> * inst_act_map,
+ SnapVector<Predicate *> * unset_predicates)
+{
+ /* check if a branch with func_inst and corresponding predicate exists */
+ bool branch_found = false;
+ ModelVector<Predicate *> * branches = (*curr_pred)->get_children();
+ for (uint i = 0; i < branches->size(); i++) {
+ Predicate * branch = (*branches)[i];
+ if (branch->get_func_inst() != next_inst)
+ continue;
+
+ /* check against predicate expressions */
+ bool predicate_correct = true;
+ PredExprSet * pred_expressions = branch->get_pred_expressions();
+ PredExprSetIter * pred_expr_it = pred_expressions->iterator();
+
+ if (pred_expressions->getSize() == 0) {
+ predicate_correct = false;
+ unset_predicates->push_back(branch);
+ }
+
+ while (pred_expr_it->hasNext()) {
+ pred_expr * pred_expression = pred_expr_it->next();
+ uint64_t last_read, next_read;
+ bool equality;
+
+ switch(pred_expression->token) {
+ case NOPREDICATE:
+ predicate_correct = true;
+ break;
+ case EQUALITY:
+ FuncInst * to_be_compared;
+ ModelAction * last_act;
+
+ to_be_compared = pred_expression->func_inst;
+ last_act = inst_act_map->get(to_be_compared);
+
+ last_read = last_act->get_reads_from_value();
+ next_read = next_act->get_reads_from_value();
+ equality = (last_read == next_read);
+ if (equality != pred_expression->value)
+ predicate_correct = false;
+
+ break;
+ case NULLITY:
+ next_read = next_act->get_reads_from_value();
+ equality = ((void*)next_read == NULL);
+ if (equality != pred_expression->value)
+ predicate_correct = false;
+ break;
+ default:
+ predicate_correct = false;
+ model_print("unkown predicate token\n");
+ break;
+ }
+ }
+
+ if (predicate_correct) {
+ *curr_pred = branch;
+ branch_found = true;