From b5cdd7ee16b73bbfe53040d23994351f85f83785 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 1 Nov 2012 21:43:07 -0700
Subject: [PATCH] model: totally destroy 'curr' within initialize_curr_action()

We don't really want 'curr' and 'newcurr' to hang around together. So
convert initialize_curr_action() to have two "return" parameters; it
overwrites the 'curr' pointer as a return value and it returns a status
boolean to show that it overwrote it. This may help prevent some future
bugs.
---
 model.cc | 48 ++++++++++++++++++++++++++----------------------
 model.h  |  2 +-
 2 files changed, 27 insertions(+), 23 deletions(-)

diff --git a/model.cc b/model.cc
index 775b796f..7181f869 100644
--- a/model.cc
+++ b/model.cc
@@ -744,41 +744,46 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
  * initializing clock vectors, and computing the promises to fulfill.
  *
  * @param curr The current action, as passed from the user context; may be
- * freed/invalidated after the execution of this function
- * @return The current action, as processed by the ModelChecker. Is only the
- * same as the parameter @a curr if this is a newly-explored action.
+ * freed/invalidated after the execution of this function, with a different
+ * action "returned" its place (pass-by-reference)
+ * @return True if curr is a newly-explored action; false otherwise
  */
-ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
+bool ModelChecker::initialize_curr_action(ModelAction **curr)
 {
 	ModelAction *newcurr;
 
-	if (curr->is_rmwc() || curr->is_rmw()) {
-		newcurr = process_rmw(curr);
-		delete curr;
+	if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
+		newcurr = process_rmw(*curr);
+		delete *curr;
 
 		if (newcurr->is_rmw())
 			compute_promises(newcurr);
-		return newcurr;
+
+		*curr = newcurr;
+		return false;
 	}
 
-	curr->set_seq_number(get_next_seq_num());
+	(*curr)->set_seq_number(get_next_seq_num());
 
-	newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
+	newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
 	if (newcurr) {
 		/* First restore type and order in case of RMW operation */
-		if (curr->is_rmwr())
-			newcurr->copy_typeandorder(curr);
+		if ((*curr)->is_rmwr())
+			newcurr->copy_typeandorder(*curr);
 
-		ASSERT(curr->get_location() == newcurr->get_location());
-		newcurr->copy_from_new(curr);
+		ASSERT((*curr)->get_location() == newcurr->get_location());
+		newcurr->copy_from_new(*curr);
 
 		/* Discard duplicate ModelAction; use action from NodeStack */
-		delete curr;
+		delete *curr;
 
 		/* Always compute new clock vector */
 		newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+		*curr = newcurr;
+		return false; /* Action was explored previously */
 	} else {
-		newcurr = curr;
+		newcurr = *curr;
 
 		/* Always compute new clock vector */
 		newcurr->create_cv(get_parent_action(newcurr->get_tid()));
@@ -795,8 +800,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 		else if (newcurr->is_notify_one()) {
 			newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
 		}
+		return true; /* This was a new ModelAction */
 	}
-	return newcurr;
 }
 
 /**
@@ -854,18 +859,17 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		return get_next_thread(NULL);
 	}
 
-	ModelAction *newcurr = initialize_curr_action(curr);
+	bool newly_explored = initialize_curr_action(&curr);
 
-	wake_up_sleeping_actions(newcurr);
+	wake_up_sleeping_actions(curr);
 
 	/* Add the action to lists before any other model-checking tasks */
 	if (!second_part_of_rmw)
-		add_action_to_lists(newcurr);
+		add_action_to_lists(curr);
 
 	/* Build may_read_from set for newly-created actions */
-	if (curr == newcurr && curr->is_read())
+	if (newly_explored && curr->is_read())
 		build_reads_from_past(curr);
-	curr = newcurr;
 
 	/* Initialize work_queue with the "current action" work */
 	work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
diff --git a/model.h b/model.h
index d0043a1f..8ff9d375 100644
--- a/model.h
+++ b/model.h
@@ -139,7 +139,7 @@ private:
 	 */
 	void set_current_action(ModelAction *act) { priv->current_action = act; }
 	Thread * check_current_action(ModelAction *curr);
-	ModelAction * initialize_curr_action(ModelAction *curr);
+	bool initialize_curr_action(ModelAction **curr);
 	bool process_read(ModelAction *curr, bool second_part_of_rmw);
 	bool process_write(ModelAction *curr);
 	bool process_mutex(ModelAction *curr);
-- 
2.34.1