Edits

[c11tester.git] / funcnode.cc

diff --git a/funcnode.cc b/funcnode.cc
index 92e37955dd97f673fc2bf1abc714cba2731c8f5e..2a8d7c1b21b6a096c091be86425473e24c65eac0 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -6,6 +6,8 @@
 #include "concretepredicate.h"
 
 #include "model.h"
+#include "execution.h"
+#include "newfuzzer.h"
 #include <cmath>
 
 FuncNode::FuncNode(ModelHistory * history) :
@@ -217,9 +219,6 @@ void FuncNode::update_tree(ModelAction * act)
                        write_locations->add(loc);
                        history->update_loc_wr_func_nodes_map(loc, this);
                }
-
-               // Do not process writes for now
-               return;
        }
 
        if (act->is_read()) {
@@ -240,6 +239,7 @@ void FuncNode::update_tree(ModelAction * act)
        }
 
 //     update_inst_tree(&inst_list); TODO
+
        update_predicate_tree(act);
 
 //     print_predicate_tree();
@@ -290,16 +290,19 @@ void FuncNode::update_predicate_tree(ModelAction * next_act)
        inst_id_map_t * inst_id_map = thrd_inst_id_maps[thread_id]->back();
 
        Predicate * curr_pred = get_predicate_tree_position(tid);
+       NewFuzzer * fuzzer = (NewFuzzer *)model->get_execution()->getFuzzer();
+       Predicate * selected_branch = fuzzer->get_selected_child_branch(tid);
+
+       bool amended;
        while (true) {
                FuncInst * next_inst = get_inst(next_act);
-               next_inst->set_associated_read(tid, recursion_depth, this_marker, next_act->get_reads_from_value());
 
                Predicate * unset_predicate = NULL;
                bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicate);
 
                // A branch with unset predicate expression is detected
                if (!branch_found && unset_predicate != NULL) {
-                       bool amended = amend_predicate_expr(curr_pred, next_inst, next_act);
+                       amended = amend_predicate_expr(curr_pred, next_inst, next_act);
                        if (amended)
                                continue;
                        else {
@@ -334,12 +337,13 @@ void FuncNode::update_predicate_tree(ModelAction * next_act)
                        continue;
                }
 
-               if (next_act->is_write())
+               if (next_act->is_write()) {
                        curr_pred->set_write(true);
+               }
 
                if (next_act->is_read()) {
                        /* Only need to store the locations of read actions */
-                       loc_inst_map->put(next_inst->get_location(), next_inst);
+                       loc_inst_map->put(next_act->get_location(), next_inst);
                }
 
                inst_pred_map->put(next_inst, curr_pred);
@@ -350,8 +354,17 @@ void FuncNode::update_predicate_tree(ModelAction * next_act)
 
                curr_pred->incr_expl_count();
                add_predicate_to_trace(tid, curr_pred);
+               if (next_act->is_read())
+                       next_inst->set_associated_read(tid, recursion_depth, this_marker, next_act->get_reads_from_value());
+
                break;
        }
+
+       // A check
+       if (next_act->is_read()) {
+               if (selected_branch != NULL && !amended)
+                       ASSERT(selected_branch == curr_pred);
+       }
 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that
@@ -364,9 +377,6 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst,
        /* Check if a branch with func_inst and corresponding predicate exists */
        bool branch_found = false;
        thread_id_t tid = next_act->get_tid();
-       int thread_id = id_to_int(tid);
-       uint32_t this_marker = thrd_markers[thread_id]->back();
-       int recursion_depth = thrd_recursion_depth[thread_id];
 
        ModelVector<Predicate *> * branches = (*curr_pred)->get_children();
        for (uint i = 0;i < branches->size();i++) {
@@ -403,9 +413,8 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst,
                        case EQUALITY:
                                FuncInst * to_be_compared;
                                to_be_compared = pred_expression->func_inst;
-                               ASSERT(to_be_compared != next_inst);
 
-                               last_read = to_be_compared->get_associated_read(tid, recursion_depth, this_marker);
+                               last_read = get_associated_read(tid, to_be_compared);
                                ASSERT(last_read != VALUE_NONE);
 
                                next_read = next_act->get_reads_from_value();
@@ -676,15 +685,13 @@ void FuncNode::init_marker(thread_id_t tid)
        thrd_recursion_depth[thread_id]++;
 }
 
-uint32_t FuncNode::get_marker(thread_id_t tid)
+uint64_t FuncNode::get_associated_read(thread_id_t tid, FuncInst * inst)
 {
        int thread_id = id_to_int(tid);
-       return thrd_markers[thread_id]->back();
-}
+       int recursion_depth = thrd_recursion_depth[thread_id];
+       uint marker = thrd_markers[thread_id]->back();
 
-int FuncNode::get_recursion_depth(thread_id_t tid)
-{
-       return thrd_recursion_depth[id_to_int(tid)];
+       return inst->get_associated_read(tid, recursion_depth, marker);
 }
 
 /* Make sure elements of maps are initialized properly when threads enter functions */
@@ -767,8 +774,7 @@ void FuncNode::reset_predicate_tree_data_structure(thread_id_t tid)
        thrd_predicate_tree_position[thread_id]->pop_back();
 
        // Free memories allocated in init_predicate_tree_data_structure
-       predicate_trace_t * trace = thrd_predicate_trace[thread_id]->back();
-       delete trace;
+       delete thrd_predicate_trace[thread_id]->back();
        thrd_predicate_trace[thread_id]->pop_back();
 }