From d6aa3d792529d617999cf63ae68463c9c6be0fa1 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Fri, 16 Nov 2012 20:23:15 -0800
Subject: [PATCH] model/main: disable most printing by default, add verbosity

Adds a '-v' parameter for printing verbose info on a non-DEBUG build.
This effectively creates 3 classes of runs:

 - Default build, no -v: only prints info when discovering a buggy
   execution
 - Default build, -v: prints more verbose information, on all feasible
   executions (buggy or non-buggy)
 - Debug build: Built with 'make debug'. Most verbose; prints everything
   for every execution, including infeasible executions. Also prints
   DEBUG() prints (as usual).
---
 main.cc  |  7 ++++++-
 model.cc | 37 ++++++++++++++++++++++++++-----------
 model.h  |  3 +++
 3 files changed, 35 insertions(+), 12 deletions(-)

diff --git a/main.cc b/main.cc
index f79366f..f6ab259 100644
--- a/main.cc
+++ b/main.cc
@@ -23,6 +23,7 @@ static void param_defaults(struct model_params * params) {
 	params->bound = 0;
 	params->maxfuturevalues = 0;
 	params->expireslop = 10;
+	params->verbose = 0;
 }
 
 static void print_usage(struct model_params *params) {
@@ -47,13 +48,14 @@ static void print_usage(struct model_params *params) {
 "                      priority for execution. Default: %d\n"
 "-e                    Enabled count. Default: %d\n"
 "-b                    Upper length bound. Default: %d\n"
+"-v                    Print verbose execution information.\n"
 "--                    Program arguments follow.\n\n",
 params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->enabledcount, params->bound);
 	exit(EXIT_SUCCESS);
 }
 
 static void parse_options(struct model_params *params, int *argc, char ***argv) {
-	const char *shortopts = "hm:M:s:S:f:e:b:";
+	const char *shortopts = "hm:M:s:S:f:e:b:v";
 	int opt;
 	bool error = false;
 	while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {
@@ -82,6 +84,9 @@ static void parse_options(struct model_params *params, int *argc, char ***argv)
 		case 'M':
 			params->maxfuturevalues = atoi(optarg);
 			break;
+		case 'v':
+			params->verbose = 1;
+			break;
 		default: /* '?' */
 			error = true;
 			break;
diff --git a/model.cc b/model.cc
index 9ed6d42..199a8fc 100644
--- a/model.cc
+++ b/model.cc
@@ -425,24 +425,39 @@ bool ModelChecker::next_execution()
 	DBG();
 
 	if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
-		model_print("Earliest divergence point since last feasible execution:\n");
-		if (earliest_diverge)
-			earliest_diverge->print();
-		else
-			model_print("(Not set)\n");
-
-		earliest_diverge = NULL;
-
 		if (is_deadlocked())
 			assert_bug("Deadlock detected");
 
 		checkDataRaces();
-		print_bugs();
-		model_print("\n");
-		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()) {
+		print_program_output();
 		model_print("\n");
+		print_stats();
 		print_summary();
+	} else {
+		clear_program_output();
 	}
 
 	record_stats();
diff --git a/model.h b/model.h
index 86fa3e6..bbad36e 100644
--- a/model.h
+++ b/model.h
@@ -47,6 +47,9 @@ struct model_params {
 	 *  expiration time exceeds the existing one by more than the slop
 	 *  value */
 	unsigned int expireslop;
+
+	/** @brief Verbosity (0 = quiet; 1 = noisy) */
+	int verbose;
 };
 
 /** @brief Model checker execution stats */
-- 
2.34.1