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 8b5c99717137d1d3f6a95b423fb6c8bf6fc2b08f..f37f92f1ba7434cdddd365564048b711ddc40816 100644 (file)
--- 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 33e8805078b546ac8d1b4f87dab3ea31e9be2651..97e112f4b16ce149109a41bc9349c32930ce998f 100644 (file)
--- 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 58ee152aa7ce94c6ae84f7d14bdec5d6894447ce..85deb05e911dc33ae7ea1b245625802dbf4c8708 100644 (file)
--- 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;