assert bugs through common interface

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index de3b3259d79c1b47c78c75ed7fd41e3352fa764a..417252c3f92ceb3a4bb7948612ca3592f1be49de 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -18,6 +18,18 @@
 
 ModelChecker *model;
 
+struct bug_message {
+       bug_message(const char *str) {
+               const char *fmt = "  [BUG] %s\n";
+               msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
+               sprintf(msg, fmt, str);
+       }
+       ~bug_message() { if (msg) snapshot_free(msg); }
+
+       char *msg;
+       void print() { printf("%s", msg); }
+};
+
 /**
  * Structure for holding small ModelChecker members that should be snapshotted
  */
@@ -27,6 +39,7 @@ struct model_snapshot_members {
        modelclock_t used_sequence_numbers;
        Thread *nextThread;
        ModelAction *next_backtrack;
+       std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
 };
 
 /** @brief Constructor */
@@ -89,6 +102,9 @@ ModelChecker::~ModelChecker()
        delete scheduler;
        delete mo_graph;
 
+       for (unsigned int i = 0; i < priv->bugs.size(); i++)
+               delete priv->bugs[i];
+       priv->bugs.clear();
        snapshot_free(priv);
 }
 
@@ -311,6 +327,72 @@ bool ModelChecker::is_complete_execution() const
        return true;
 }
 
+/**
+ * @brief Assert a bug in the executing program.
+ *
+ * Use this function to assert any sort of bug in the user program. If the
+ * current trace is feasible (actually, a prefix of some feasible execution),
+ * then this execution will be aborted, printing the appropriate message. If
+ * 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?
+ */
+void ModelChecker::assert_bug(const char *msg, bool user_thread, bool immediate)
+{
+       priv->bugs.push_back(new bug_message(msg));
+
+       if (immediate || isfeasibleprefix()) {
+               set_assert();
+               if (user_thread)
+                       switch_to_master(NULL);
+       }
+}
+
+/**
+ * @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
+ * @see ModelChecker::assert_bug
+ * @param msg Descriptive message for the bug (do not include newline char)
+ */
+void ModelChecker::assert_bug_immediate(const char *msg)
+{
+       printf("Feasible: %s\n", isfeasibleprefix() ? "yes" : "no");
+       assert_bug(msg, false, true);
+}
+
+/** @return True, if any bugs have been reported for this execution */
+bool ModelChecker::have_bug_reports() const
+{
+       return priv->bugs.size() != 0;
+}
+
+/** @brief Print bug report listing for this execution (if any bugs exist) */
+void ModelChecker::print_bugs() const
+{
+       if (have_bug_reports()) {
+               printf("Bug report: %zu bugs detected\n", priv->bugs.size());
+               for (unsigned int i = 0; i < priv->bugs.size(); i++)
+                       priv->bugs[i]->print();
+       }
+}
+
 /**
  * Queries the model-checker for more executions to explore and, if one
  * exists, resets the model-checker state to execute a new execution.
@@ -324,9 +406,7 @@ bool ModelChecker::next_execution()
 
        num_executions++;
 
-       if (is_deadlocked())
-               printf("ERROR: DEADLOCK\n");
-       if (isfinalfeasible()) {
+       if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
                printf("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
                        earliest_diverge->print();
@@ -335,15 +415,15 @@ bool ModelChecker::next_execution()
 
                earliest_diverge = NULL;
                num_feasible_executions++;
-       }
 
-       DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
-                       pending_rel_seqs->size());
+               if (is_deadlocked())
+                       assert_bug("Deadlock detected");
 
-
-       if (isfinalfeasible() || DBG_ENABLED()) {
+               print_bugs();
                checkDataRaces();
                print_summary();
+       } else if (DBG_ENABLED()) {
+               print_summary();
        }
 
        if ((diverge = get_next_backtrack()) == NULL)
@@ -597,10 +677,8 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
        }
                //otherwise fall into the lock case
        case ATOMIC_LOCK: {
-               if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
-                       printf("Lock access before initialization\n");
-                       set_assert();
-               }
+               if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+                       assert_bug("Lock access before initialization");
                state->islocked = true;
                ModelAction *unlock = get_last_unlock(curr);
                //synchronize with the previous unlock statement
@@ -810,7 +888,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 
        /* See if we have realized a data race */
        if (checkDataRaces())
-               set_assert();
+               assert_bug("Datarace");
 }
 
 /**
@@ -1741,9 +1819,8 @@ 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()) {
-               set_assert();
-       }
+       if (checkDataRaces())
+               assert_bug("Datarace");
 
        return updated;
 }
@@ -2306,6 +2383,10 @@ bool ModelChecker::take_step() {
        /* Infeasible -> don't take any more steps */
        if (!isfeasible())
                return false;
+       else if (isfeasibleprefix() && have_bug_reports()) {
+               set_assert();
+               return false;
+       }
 
        if (params.bound != 0) {
                if (priv->used_sequence_numbers > params.bound) {