From: Brian Norris <banorris@uci.edu>
Date: Sat, 23 Feb 2013 03:01:13 +0000 (-0800)
Subject: nodestack: bugfix - reset backtracking points on diverging paths
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6df4a86031c4831b581e39b093c5fad128bda582;p=c11tester.git

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 59e9b5dc..9c0df20b 100644
--- 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 cd34ba42..941178d7 100644
--- 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);