From: Brian Norris <banorris@uci.edu>
Date: Fri, 16 Nov 2012 22:58:32 +0000 (-0800)
Subject: model: rework assert_bug() and assert_user_bug() interfaces
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=dc0339b4449ed07afa7c69936108146d72676a68

model: rework assert_bug() and assert_user_bug() interfaces

We don't need assert_bug_immediate(), and we don't need some of the
optional parameters in assert_bug(). Just simplify down to two
interfaces:

    assert_bug()
    assert_user_bug()

The former is useful for all bugs triggered from model-checker threads,
and the latter is useful from a user-thread context, so that you can
immediately switch to the model-checking context and exit the program -
but *only if* the trace is currently-feasible.
---

diff --git a/common.cc b/common.cc
index 8b5c9971..f37f92f1 100644
--- a/common.cc
+++ b/common.cc
@@ -49,6 +49,6 @@ void model_assert(bool expr, const char *file, int line)
 		char msg[100];
 		sprintf(msg, "Program has hit assertion in file %s at line %d\n",
 				file, line);
-		model->assert_bug(msg, true);
+		model->assert_user_bug(msg);
 	}
 }
diff --git a/model.cc b/model.cc
index 33e88050..97e112f4 100644
--- a/model.cc
+++ b/model.cc
@@ -337,45 +337,30 @@ bool ModelChecker::is_complete_execution() const
  * the current trace is not yet feasible, the error message will be stashed and
  * printed if the execution ever becomes feasible.
  *
- * This function can also be used to immediately trigger the bug; that is, we
- * don't wait for a feasible execution before aborting. Only use the
- * "immediate" option when you know that the infeasibility is justified (e.g.,
- * pending release sequences are not a problem)
- *
  * @param msg Descriptive message for the bug (do not include newline char)
- * @param user_thread Was this assertion triggered from a user thread?
- * @param immediate Should this bug be triggered immediately?
+ * @return True if bug is immediately-feasible
  */
-void ModelChecker::assert_bug(const char *msg, bool user_thread, bool immediate)
+bool ModelChecker::assert_bug(const char *msg)
 {
 	priv->bugs.push_back(new bug_message(msg));
 
-	if (immediate || isfeasibleprefix()) {
+	if (isfeasibleprefix()) {
 		set_assert();
-		if (user_thread)
-			switch_to_master(NULL);
+		return true;
 	}
+	return false;
 }
 
 /**
- * @brief Assert a bug in the executing program, with a default message
- * @see ModelChecker::assert_bug
- * @param user_thread Was this assertion triggered from a user thread?
- */
-void ModelChecker::assert_bug(bool user_thread)
-{
-	assert_bug("bug detected", user_thread);
-}
-
-/**
- * @brief Assert a bug in the executing program immediately
+ * @brief Assert a bug in the executing program, asserted by a user thread
  * @see ModelChecker::assert_bug
  * @param msg Descriptive message for the bug (do not include newline char)
  */
-void ModelChecker::assert_bug_immediate(const char *msg)
+void ModelChecker::assert_user_bug(const char *msg)
 {
-	printf("Feasible: %s\n", isfeasibleprefix() ? "yes" : "no");
-	assert_bug(msg, false, true);
+	/* If feasible bug, bail out now */
+	if (assert_bug(msg))
+		switch_to_master(NULL);
 }
 
 /** @return True, if any bugs have been reported for this execution */
diff --git a/model.h b/model.h
index 58ee152a..85deb05e 100644
--- a/model.h
+++ b/model.h
@@ -116,9 +116,8 @@ public:
 	void finish_execution();
 	bool isfeasibleprefix() const;
 
-	void assert_bug(const char *msg, bool user_thread = false, bool immediate = false);
-	void assert_bug(bool user_thread = true);
-	void assert_bug_immediate(const char *msg);
+	bool assert_bug(const char *msg);
+	void assert_user_bug(const char *msg);
 
 	void set_assert() {asserted=true;}
 	bool is_deadlocked() const;