model: rework assert_bug() and assert_user_bug() interfaces

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index ab16bf82528ea5ebf30766970b37faca5a6ada1f..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 */
@@ -446,8 +431,8 @@ bool ModelChecker::next_execution()
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
-               print_bugs();
                checkDataRaces();
+               print_bugs();
                printf("\n");
                print_stats();
                print_summary();
@@ -917,8 +902,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
        }
 
        /* See if we have realized a data race */
-       if (checkDataRaces())
-               assert_bug("Data race");
+       checkDataRaces();
 }
 
 /**
@@ -1849,8 +1833,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
        }
 
        // If we resolved promises or data races, see if we have realized a data race.
-       if (checkDataRaces())
-               assert_bug("Data race");
+       checkDataRaces();
 
        return updated;
 }