nodestack: bugfix - reset backtracking points on diverging paths

Any time we diverge to a new execution path, we should reset the
backtracking information (i.e., which threads have executed and which
still must be backtracked) for the last node in the stack. We cannot
retain the "explored children" state after we have performed different
read-from or future-value divergence in the same node.

diff --git a/nodestack.cc b/nodestack.cc
index 59e9b5dcad8f9630b2e9dd7ad25a97728ea25458..9c0df20b5de89bd2876cde69ca281502506f4709 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -348,6 +348,14 @@ thread_id_t Node::get_next_backtrack()
        return int_to_id(i);
 }
 
+void Node::clear_backtracking()
+{
+       for (unsigned int i = 0; i < backtrack.size(); i++)
+               backtrack[i] = false;
+       for (unsigned int i = 0; i < explored_children.size(); i++)
+               explored_children[i] = false;
+}
+
 bool Node::is_enabled(Thread *t) const
 {
        int thread_id = id_to_int(t->get_id());
@@ -581,6 +589,7 @@ void NodeStack::pop_restofstack(int numAhead)
        for (unsigned int i = it; i < node_list.size(); i++)
                delete node_list[i];
        node_list.resize(it);
+       node_list.back()->clear_backtracking();
 }
 
 Node * NodeStack::get_head() const

diff --git a/nodestack.h b/nodestack.h
index cd34ba42189977d25ed52e0a57b60c3ca25839ed..941178d7be453267b7556a1226c4883a11128d9e 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -56,6 +56,7 @@ public:
        /* return true = backtrack set is empty */
        bool backtrack_empty() const;
 
+       void clear_backtracking();
        void explore_child(ModelAction *act, enabled_type_t *is_enabled);
        /* return false = thread was already in backtrack */
        bool set_backtrack(thread_id_t id);