model: rework assert_bug() and assert_user_bug() interfaces
authorBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 22:58:32 +0000 (14:58 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 22:58:32 +0000 (14:58 -0800)
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.

common.cc
model.cc
model.h

index 8b5c997..f37f92f 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);
                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);
        }
 }
        }
 }
index 33e8805..97e112f 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.
  *
  * 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 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));
 
 {
        priv->bugs.push_back(new bug_message(msg));
 
-       if (immediate || isfeasibleprefix()) {
+       if (isfeasibleprefix()) {
                set_assert();
                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)
  */
  * @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 */
 }
 
 /** @return True, if any bugs have been reported for this execution */
diff --git a/model.h b/model.h
index 58ee152..85deb05 100644 (file)
--- a/model.h
+++ b/model.h
@@ -116,9 +116,8 @@ public:
        void finish_execution();
        bool isfeasibleprefix() const;
 
        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;
 
        void set_assert() {asserted=true;}
        bool is_deadlocked() const;