model: print_summary() should be const

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 97e112f4b16ce149109a41bc9349c32930ce998f..691cd72bbbbd5275473ddf0993f70138256a0f0b 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -13,6 +13,7 @@
 #include "promise.h"
 #include "datarace.h"
 #include "threads-model.h"
+#include "output.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -27,7 +28,7 @@ struct bug_message {
        ~bug_message() { if (msg) snapshot_free(msg); }
 
        char *msg;
-       void print() { printf("%s", msg); }
+       void print() { model_print("%s", msg); }
 
        SNAPSHOTALLOC
 };
@@ -139,6 +140,10 @@ void ModelChecker::reset_to_initial_state()
        too_many_reads = false;
        bad_synchronization = false;
        reset_asserted();
+
+       /* Print all model-checker output before rollback */
+       fflush(model_out);
+
        snapshotObject->backTrackBeforeStep(0);
 }
 
@@ -373,7 +378,9 @@ 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());
+               model_print("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();
        }
@@ -399,11 +406,11 @@ void ModelChecker::record_stats()
 /** @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());
+       model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+       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());
 }
 
 /**
@@ -417,35 +424,49 @@ bool ModelChecker::next_execution()
 {
        DBG();
 
-       record_stats();
-
        if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
-               printf("Earliest divergence point since last feasible execution:\n");
-               if (earliest_diverge)
-                       earliest_diverge->print();
-               else
-                       printf("(Not set)\n");
-
-               earliest_diverge = NULL;
-
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
                checkDataRaces();
-               print_bugs();
-               printf("\n");
-               print_stats();
-               print_summary();
+
+               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();
+
+               earliest_diverge = NULL;
        } else if (DBG_ENABLED()) {
-               printf("\n");
+               print_program_output();
+               model_print("\n");
+               print_stats();
                print_summary();
+       } else {
+               clear_program_output();
        }
 
+       record_stats();
+
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
        if (DBG_ENABLED()) {
-               printf("Next execution will diverge at:\n");
+               model_print("Next execution will diverge at:\n");
                diverge->print();
        }
 
@@ -2196,11 +2217,11 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                assert_bug("May read from uninitialized atomic");
 
        if (DBG_ENABLED() || !initialized) {
-               printf("Reached read action:\n");
+               model_print("Reached read action:\n");
                curr->print();
-               printf("Printing may_read_from\n");
+               model_print("Printing may_read_from\n");
                curr->get_node()->print_may_read_from();
-               printf("End printing may_read_from\n");
+               model_print("End printing may_read_from\n");
        }
 }
 
@@ -2220,20 +2241,22 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr
        }
 }
 
-static void print_list(action_list_t *list)
+static void print_list(action_list_t *list, int exec_num = -1)
 {
        action_list_t::iterator it;
 
-       printf("---------------------------------------------------------------------\n");
-       printf("Trace:\n");
+       model_print("---------------------------------------------------------------------\n");
+       if (exec_num >= 0)
+               model_print("Execution %d:\n", exec_num);
+
        unsigned int hash=0;
 
        for (it = list->begin(); it != list->end(); it++) {
                (*it)->print();
                hash=hash^(hash<<3)^((*it)->hash());
        }
-       printf("HASH %u\n", hash);
-       printf("---------------------------------------------------------------------\n");
+       model_print("HASH %u\n", hash);
+       model_print("---------------------------------------------------------------------\n");
 }
 
 #if SUPPORT_MOD_ORDER_DUMP
@@ -2264,7 +2287,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();
@@ -2276,9 +2300,9 @@ void ModelChecker::print_summary()
 #endif
 
        if (!isfinalfeasible())
-               printf("INFEASIBLE EXECUTION!\n");
-       print_list(action_trace);
-       printf("\n");
+               model_print("INFEASIBLE EXECUTION!\n");
+       print_list(action_trace, stats.num_total);
+       model_print("\n");
 }
 
 /**
@@ -2413,7 +2437,7 @@ bool ModelChecker::take_step() {
         */
        if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
                        isfinalfeasible() && !unrealizedraces.empty()) {
-               printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
+               model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
                                pending_rel_seqs->size());
                ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
                                std::memory_order_seq_cst, NULL, VALUE_NONE,