add a data structrue to keep track of the run-time position in the predicate tree...

[c11tester.git] / history.cc

diff --git a/history.cc b/history.cc
index 68e8575fa25dadd204958dbbf5d61be239a58e67..b546cd0abd1bc65e48ec631b6cd47eb3eb832951 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -48,6 +48,9 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
 
        if ( func_nodes.size() <= func_id )
                resize_func_nodes( func_id + 1 );
+
+       FuncNode * func_node = func_nodes[func_id];
+       func_node->init_predicate_tree_position(tid);
 }
 
 /* @param func_id a non-zero value */
@@ -63,12 +66,13 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
 
        if (last_func_id == func_id) {
                FuncNode * func_node = func_nodes[func_id];
+               func_node->unset_predicate_tree_position(tid);
                //func_node->clear_read_map(tid);
 
                action_list_t * curr_act_list = func_act_lists->back();
 
                /* 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.
+                * (currently twice) so that more information can be gathered to infer nullity predicates.
                 */
                func_node->incr_exit_count();
                if (func_node->get_exit_count() >= 2) {
@@ -99,7 +103,7 @@ void ModelHistory::resize_func_nodes(uint32_t new_size)
        if ( old_size < new_size )
                func_nodes.resize(new_size);
 
-       for (uint32_t id = old_size;id < new_size;id++) {
+       for (uint32_t id = old_size; id < new_size; id++) {
                const char * func_name = func_map_rev[id];
                FuncNode * func_node = new FuncNode(this);
                func_node->set_func_id(id);
@@ -125,8 +129,20 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
        SnapList<action_list_t *> * func_act_lists = (*thrd_func_act_lists)[id];
 
        if (act->is_write()) {
-               add_to_write_history(act->get_location(), act->get_write_value());
-               
+               void * location = act->get_location();
+               uint64_t value = act->get_write_value();
+               add_to_write_history(location, value);
+
+               /* update FuncNodes */
+               SnapList<FuncNode *> * func_nodes = loc_func_nodes_map.get(location);
+               sllnode<FuncNode *> * it = NULL;
+               if (func_nodes != NULL)
+                       it = func_nodes->begin();
+
+               for (; it != NULL; it = it->getNext()) {
+                       FuncNode * func_node = it->getVal();
+                       func_node->add_to_val_loc_map(value, location);
+               }
        }
 
        /* the following does not care about actions without a position */
@@ -211,6 +227,7 @@ void ModelHistory::add_to_loc_func_nodes_map(void * location, FuncNode * node)
        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++) {