Add default memory allocation and free functions for HSIterator and some other tiny...

[c11tester.git] / funcnode.cc

diff --git a/funcnode.cc b/funcnode.cc
index af268aad0d0cf95c3fbca6d8b32f134dc6f2af1a..18d7771bfba63ff6460a29039a564be1cd4e4000 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -5,6 +5,8 @@
 #include "predicate.h"
 #include "concretepredicate.h"
 
+#include "model.h"
+
 FuncNode::FuncNode(ModelHistory * history) :
        history(history),
        exit_count(0),
@@ -24,7 +26,6 @@ FuncNode::FuncNode(ModelHistory * history) :
        write_locations = new loc_set_t();
        val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
        loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
-       thrd_inst_act_map = new SnapVector<inst_act_map_t *>();
 
        //values_may_read_from = new value_set_t();
 }
@@ -32,17 +33,11 @@ FuncNode::FuncNode(ModelHistory * history) :
 /* 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();
        val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
        loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
-       thrd_inst_act_map = new SnapVector<inst_act_map_t *>();
 
        //values_may_read_from = new value_set_t();
 }
@@ -68,10 +63,13 @@ void FuncNode::add_inst(ModelAction *act)
                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();
@@ -183,7 +181,7 @@ void FuncNode::update_tree(action_list_t * act_list)
                                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);
                        }
                }
        }
@@ -365,6 +363,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model
                                        break;
                        }
                }
+               delete concrete_pred;
 
                if (predicate_correct) {
                        *curr_pred = branch;
@@ -585,6 +584,7 @@ Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid)
 void FuncNode::init_inst_act_map(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
+       SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
        uint old_size = thrd_inst_act_map->size();
 
        if (thrd_inst_act_map->size() <= (uint) thread_id) {
@@ -600,6 +600,8 @@ void FuncNode::init_inst_act_map(thread_id_t tid)
 void FuncNode::reset_inst_act_map(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
+       SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
+
        inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
        map->reset();
 }
@@ -607,6 +609,8 @@ void FuncNode::reset_inst_act_map(thread_id_t tid)
 void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act)
 {
        int thread_id = id_to_int(tid);
+       SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
+
        inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
        FuncInst * read_inst = get_inst(read_act);
        map->put(read_inst, read_act);
@@ -615,6 +619,8 @@ void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act)
 inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
+       SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
+
        return (*thrd_inst_act_map)[thread_id];
 }
 
@@ -634,6 +640,44 @@ void FuncNode::add_out_edge(FuncNode * other)
        }
 }
 
+/* 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);