model: correct plural ("bug" or "bugs")

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 3b83b569baf5c12f356aaf596023ca4fe3b3cde2..05e767981554a0c301169905a95ea5081d3cb8c0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -28,6 +28,8 @@ struct bug_message {
 
        char *msg;
        void print() { printf("%s", msg); }
+
+       SNAPSHOTALLOC
 };
 
 /**
@@ -40,6 +42,7 @@ struct model_snapshot_members {
        Thread *nextThread;
        ModelAction *next_backtrack;
        std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
+       struct execution_stats stats;
 };
 
 /** @brief Constructor */
@@ -47,8 +50,6 @@ ModelChecker::ModelChecker(struct model_params params) :
        /* Initialize default scheduler */
        params(params),
        scheduler(new Scheduler()),
-       num_executions(0),
-       num_feasible_executions(0),
        diverge(NULL),
        earliest_diverge(NULL),
        action_trace(new action_list_t()),
@@ -336,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 */
@@ -387,12 +373,41 @@ bool ModelChecker::have_bug_reports() const
 void ModelChecker::print_bugs() const
 {
        if (have_bug_reports()) {
-               printf("Bug report: %zu bugs detected\n", priv->bugs.size());
+               printf("Bug report: %zu bug%s detected\n",
+                               priv->bugs.size(),
+                               priv->bugs.size() > 1 ? "s" : "");
                for (unsigned int i = 0; i < priv->bugs.size(); i++)
                        priv->bugs[i]->print();
        }
 }
 
+/**
+ * @brief Record end-of-execution stats
+ *
+ * Must be run when exiting an execution. Records various stats.
+ * @see struct execution_stats
+ */
+void ModelChecker::record_stats()
+{
+       stats.num_total++;
+       if (!isfinalfeasible())
+               stats.num_infeasible++;
+       else if (have_bug_reports())
+               stats.num_buggy_executions++;
+       else if (is_complete_execution())
+               stats.num_complete++;
+}
+
+/** @brief Print execution stats */
+void ModelChecker::print_stats() const
+{
+       printf("Number of complete, bug-free executions: %d\n", stats.num_complete);
+       printf("Number of buggy executions: %d\n", stats.num_buggy_executions);
+       printf("Number of infeasible executions: %d\n", stats.num_infeasible);
+       printf("Total executions: %d\n", stats.num_total);
+       printf("Total nodes created: %d\n", node_stack->get_total_nodes());
+}
+
 /**
  * Queries the model-checker for more executions to explore and, if one
  * exists, resets the model-checker state to execute a new execution.
@@ -404,7 +419,7 @@ bool ModelChecker::next_execution()
 {
        DBG();
 
-       num_executions++;
+       record_stats();
 
        if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
                printf("Earliest divergence point since last feasible execution:\n");
@@ -414,15 +429,17 @@ bool ModelChecker::next_execution()
                        printf("(Not set)\n");
 
                earliest_diverge = NULL;
-               num_feasible_executions++;
 
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
-               print_bugs();
                checkDataRaces();
+               print_bugs();
+               printf("\n");
+               print_stats();
                print_summary();
        } else if (DBG_ENABLED()) {
+               printf("\n");
                print_summary();
        }
 
@@ -887,8 +904,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("Datarace");
+       checkDataRaces();
 }
 
 /**
@@ -1819,8 +1835,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("Datarace");
+       checkDataRaces();
 
        return updated;
 }
@@ -2253,17 +2268,12 @@ void ModelChecker::dumpGraph(char *filename) {
 
 void ModelChecker::print_summary()
 {
-       printf("\n");
-       printf("Number of executions: %d\n", num_executions);
-       printf("Number of feasible executions: %d\n", num_feasible_executions);
-       printf("Total nodes created: %d\n", node_stack->get_total_nodes());
-
 #if SUPPORT_MOD_ORDER_DUMP
        scheduler->print();
        char buffername[100];
-       sprintf(buffername, "exec%04u", num_executions);
+       sprintf(buffername, "exec%04u", stats.num_total);
        mo_graph->dumpGraphToFile(buffername);
-       sprintf(buffername, "graph%04u", num_executions);
+       sprintf(buffername, "graph%04u", stats.num_total);
        dumpGraph(buffername);
 #endif