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-Tag: oopsla2013~226
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=6df4a86031c4831b581e39b093c5fad128bda582

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 59e9b5d..9c0df20 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 cd34ba4..941178d 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);