model: add "# redundant" stat

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 199a8fc3505f7273a8cab4dedcbb64db693d96cf..df06760893018d5bc1756cd89df263c6ed117cc6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -401,18 +401,48 @@ void ModelChecker::record_stats()
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;
+       else
+               stats.num_redundant++;
 }
 
 /** @brief Print execution stats */
 void ModelChecker::print_stats() const
 {
        model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+       model_print("Number of redundant executions: %d\n", stats.num_redundant);
        model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
        model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
        model_print("Total executions: %d\n", stats.num_total);
        model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
 }
 
+/**
+ * @brief End-of-exeuction print
+ * @param printbugs Should any existing bugs be printed?
+ */
+void ModelChecker::print_execution(bool printbugs) const
+{
+       print_program_output();
+
+       if (DBG_ENABLED() || params.verbose) {
+               model_print("Earliest divergence point since last feasible execution:\n");
+               if (earliest_diverge)
+                       earliest_diverge->print();
+               else
+                       model_print("(Not set)\n");
+
+               model_print("\n");
+               print_stats();
+       }
+
+       /* Don't print invalid bugs */
+       if (printbugs)
+               print_bugs();
+
+       model_print("\n");
+       print_summary();
+}
+
 /**
  * Queries the model-checker for more executions to explore and, if one
  * exists, resets the model-checker state to execute a new execution.
@@ -423,44 +453,28 @@ void ModelChecker::print_stats() const
 bool ModelChecker::next_execution()
 {
        DBG();
+       /* Is this execution a feasible execution that's worth bug-checking? */
+       bool complete = isfinalfeasible() && (is_complete_execution() ||
+                       have_bug_reports());
 
-       if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
+       /* End-of-execution bug checks */
+       if (complete) {
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
                checkDataRaces();
+       }
 
-               if (DBG_ENABLED() || params.verbose || have_bug_reports()) {
-                       print_program_output();
-
-                       if (DBG_ENABLED() || params.verbose) {
-                               model_print("Earliest divergence point since last feasible execution:\n");
-                               if (earliest_diverge)
-                                       earliest_diverge->print();
-                               else
-                                       model_print("(Not set)\n");
-
-                               model_print("\n");
-                               print_stats();
-                       }
-
-                       print_bugs();
-                       model_print("\n");
-                       print_summary();
-               } else
-                       clear_program_output();
+       record_stats();
 
-               earliest_diverge = NULL;
-       } else if (DBG_ENABLED()) {
-               print_program_output();
-               model_print("\n");
-               print_stats();
-               print_summary();
-       } else {
+       /* Output */
+       if (DBG_ENABLED() || params.verbose || have_bug_reports())
+               print_execution(complete);
+       else
                clear_program_output();
-       }
 
-       record_stats();
+       if (complete)
+               earliest_diverge = NULL;
 
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
@@ -2287,7 +2301,8 @@ void ModelChecker::dumpGraph(char *filename) {
 }
 #endif
 
-void ModelChecker::print_summary()
+/** @brief Prints an execution trace summary. */
+void ModelChecker::print_summary() const
 {
 #if SUPPORT_MOD_ORDER_DUMP
        scheduler->print();