#include "predicate.h"
#include "concretepredicate.h"
+#include "model.h"
+
FuncNode::FuncNode(ModelHistory * history) :
history(history),
exit_count(0),
/* Reallocate snapshotted memories when new executions start */
void FuncNode::set_new_exec_flag()
{
- for (mllnode<FuncInst *> * it = inst_list.begin(); it != NULL; it = it->getNext()) {
- FuncInst * inst = it->getVal();
- inst->unset_location();
- }
-
action_list_buffer = new SnapList<action_list_t *>();
read_locations = new loc_set_t();
write_locations = new loc_set_t();
FuncInst * inst = func_inst_map.get(position);
ASSERT(inst->get_type() == act->get_type());
+ int curr_execution_number = model->get_execution_number();
- // locations are set to NULL when new executions start
- if (inst->get_location() == NULL)
+ /* Reset locations when new executions start */
+ if (inst->get_execution_number() != curr_execution_number) {
inst->set_location(act->get_location());
+ inst->set_execution_number(curr_execution_number);
+ }
if (inst->get_location() != act->get_location())
inst->not_single_location();
read_locations->add(loc);
value_set_t * write_values = write_history->get(loc);
add_to_val_loc_map(write_values, loc);
- history->update_loc_func_nodes_map(loc, this);
+ history->update_loc_rd_func_nodes_map(loc, this);
}
}
}
}
}
+/* Compute the distance between this FuncNode and the target node.
+ * Return -1 if the target node is unreachable or the actual distance
+ * is greater than max_step.
+ */
+int FuncNode::compute_distance(FuncNode * target, int max_step)
+{
+ SnapList<FuncNode *> queue;
+ HashTable<FuncNode *, int, uintptr_t, 0> distances;
+
+ int dist = 0;
+ queue.push_back(this);
+ distances.put(this, dist);
+
+ while (!queue.empty()) {
+ FuncNode * curr = queue.front();
+ queue.pop_front();
+
+ if (curr == target)
+ return dist;
+ else if (max_step < dist)
+ return -1;
+
+ dist++;
+ ModelList<FuncNode *> * outEdges = curr->get_out_edges();
+ mllnode<FuncNode *> * it;
+ for (it = outEdges->begin(); it != NULL; it = it->getNext()) {
+ FuncNode * out_node = it->getVal();
+ if ( !distances.contains(out_node) ) {
+ queue.push_back(out_node);
+ distances.put(out_node, dist);
+ }
+ }
+ }
+
+ /* Target node is unreachable */
+ return -1;
+}
+
void FuncNode::print_predicate_tree()
{
model_print("digraph function_%s {\n", func_name);