From: Brian Norris <banorris@uci.edu>
Date: Fri, 16 Nov 2012 23:23:40 +0000 (-0800)
Subject: printf -> model_print
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=adf77053d498af32ab4c6764b50d4265bed5996c;p=cdsspec-compiler.git

printf -> model_print

As we move toward redirecting program output, we will need a special
printf function for model-checking prints. Just define a simple
model_print() for now.
---

diff --git a/action.cc b/action.cc
index 1387ed1..486e89e 100644
--- a/action.cc
+++ b/action.cc
@@ -468,22 +468,22 @@ void ModelAction::print() const
 		break;
 	}
 
-	printf("(%4d) Thread: %-2d   Action: %-13s   MO: %7s  Loc: %14p   Value: %-#18" PRIx64,
+	model_print("(%4d) Thread: %-2d   Action: %-13s   MO: %7s  Loc: %14p   Value: %-#18" PRIx64,
 			seq_number, id_to_int(tid), type_str, mo_str, location, valuetoprint);
 	if (is_read()) {
 		if (reads_from)
-			printf("  Rf: %-3d", reads_from->get_seq_number());
+			model_print("  Rf: %-3d", reads_from->get_seq_number());
 		else
-			printf("  Rf: ?  ");
+			model_print("  Rf: ?  ");
 	}
 	if (cv) {
 		if (is_read())
-			printf(" ");
+			model_print(" ");
 		else
-			printf("          ");
+			model_print("          ");
 		cv->print();
 	} else
-		printf("\n");
+		model_print("\n");
 }
 
 /** @brief Print nicely-formatted info about this ModelAction */
diff --git a/clockvector.cc b/clockvector.cc
index e56c2ac..6cd943b 100644
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -89,7 +89,7 @@ modelclock_t ClockVector::getClock(thread_id_t thread) {
 void ClockVector::print() const
 {
 	int i;
-	printf("CV: (");
+	model_print("CV: (");
 	for (i = 0; i < num_threads; i++)
-		printf("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
+		model_print("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
 }
diff --git a/common.cc b/common.cc
index f37f92f..d991599 100644
--- a/common.cc
+++ b/common.cc
@@ -24,10 +24,10 @@ void print_trace(void)
 	size = backtrace(array, MAX_TRACE_LEN);
 	strings = backtrace_symbols(array, size);
 
-	printf("\nDumping stack trace (%d frames):\n", size);
+	model_print("\nDumping stack trace (%d frames):\n", size);
 
 	for (i = 0; i < size; i++)
-		printf("\t%s\n", strings[i]);
+		model_print("\t%s\n", strings[i]);
 
 	free(strings);
 #endif /* CONFIG_STACKTRACE */
@@ -40,7 +40,7 @@ void model_print_summary(void)
 
 void assert_hook(void)
 {
-	printf("Add breakpoint to line %u in file %s.\n",__LINE__,__FILE__);
+	model_print("Add breakpoint to line %u in file %s.\n",__LINE__,__FILE__);
 }
 
 void model_assert(bool expr, const char *file, int line)
diff --git a/common.h b/common.h
index 81b2672..b1d6b31 100644
--- a/common.h
+++ b/common.h
@@ -8,8 +8,10 @@
 #include <stdio.h>
 #include "config.h"
 
+#define model_print(fmt, ...) do { printf(fmt, ##__VA_ARGS__); } while (0)
+
 #ifdef CONFIG_DEBUG
-#define DEBUG(fmt, ...) do { printf("*** %25s(): line %-4d *** " fmt, __func__, __LINE__, ##__VA_ARGS__); } while (0)
+#define DEBUG(fmt, ...) do { model_print("*** %25s(): line %-4d *** " fmt, __func__, __LINE__, ##__VA_ARGS__); } while (0)
 #define DBG() DEBUG("\n")
 #define DBG_ENABLED() (1)
 #else
diff --git a/hashtable.h b/hashtable.h
index 4d3b7de..d5c69cc 100644
--- a/hashtable.h
+++ b/hashtable.h
@@ -9,6 +9,7 @@
 #include <stdio.h>
 #include <string.h>
 #include "mymemory.h"
+#include "common.h"
 
 /**
  * Hashtable linked node class, for chained storage of hash table conflicts. By
@@ -161,7 +162,7 @@ template<typename _Key, typename _Val, typename _KeyInt, int _Shift=0, void * (*
 		unsigned int oldcapacity = capacity;
 
 		if((newtable = (struct hashlistnode<_Key,_Val> *) _calloc(newsize, sizeof(struct hashlistnode<_Key,_Val>))) == NULL) {
-			printf("Calloc error %s %d\n", __FILE__, __LINE__);
+			model_print("Calloc error %s %d\n", __FILE__, __LINE__);
 			exit(-1);
 		}
 		
diff --git a/main.cc b/main.cc
index fb4acbe..10e2d3b 100644
--- a/main.cc
+++ b/main.cc
@@ -28,7 +28,7 @@ static void print_usage(struct model_params *params) {
 	/* Reset defaults before printing */
 	param_defaults(params);
 
-	printf(
+	model_print(
 "Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
 "\n"
 "Options:\n"
diff --git a/model.cc b/model.cc
index 05e7679..8dcb6f3 100644
--- a/model.cc
+++ b/model.cc
@@ -27,7 +27,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
 };
@@ -373,7 +373,7 @@ bool ModelChecker::have_bug_reports() const
 void ModelChecker::print_bugs() const
 {
 	if (have_bug_reports()) {
-		printf("Bug report: %zu bug%s detected\n",
+		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++)
@@ -401,11 +401,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());
 }
 
 /**
@@ -422,11 +422,11 @@ bool ModelChecker::next_execution()
 	record_stats();
 
 	if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
-		printf("Earliest divergence point since last feasible execution:\n");
+		model_print("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
 			earliest_diverge->print();
 		else
-			printf("(Not set)\n");
+			model_print("(Not set)\n");
 
 		earliest_diverge = NULL;
 
@@ -435,11 +435,11 @@ bool ModelChecker::next_execution()
 
 		checkDataRaces();
 		print_bugs();
-		printf("\n");
+		model_print("\n");
 		print_stats();
 		print_summary();
 	} else if (DBG_ENABLED()) {
-		printf("\n");
+		model_print("\n");
 		print_summary();
 	}
 
@@ -447,7 +447,7 @@ bool ModelChecker::next_execution()
 		return false;
 
 	if (DBG_ENABLED()) {
-		printf("Next execution will diverge at:\n");
+		model_print("Next execution will diverge at:\n");
 		diverge->print();
 	}
 
@@ -2198,11 +2198,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");
 	}
 }
 
@@ -2226,16 +2226,16 @@ static void print_list(action_list_t *list)
 {
 	action_list_t::iterator it;
 
-	printf("---------------------------------------------------------------------\n");
-	printf("Trace:\n");
+	model_print("---------------------------------------------------------------------\n");
+	model_print("Trace:\n");
 	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
@@ -2278,9 +2278,9 @@ void ModelChecker::print_summary()
 #endif
 
 	if (!isfinalfeasible())
-		printf("INFEASIBLE EXECUTION!\n");
+		model_print("INFEASIBLE EXECUTION!\n");
 	print_list(action_trace);
-	printf("\n");
+	model_print("\n");
 }
 
 /**
@@ -2415,7 +2415,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,
diff --git a/mymemory.cc b/mymemory.cc
index 5922a32..6ea6b92 100644
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -135,7 +135,7 @@ void * HandleEarlyAllocationRequest(size_t sz)
 	sz = (sz + 7) & ~7;
 
 	if (sz > (BOOTSTRAPBYTES-offset)) {
-		printf("OUT OF BOOTSTRAP MEMORY\n");
+		model_print("OUT OF BOOTSTRAP MEMORY\n");
 		exit(EXIT_FAILURE);
 	}
 
diff --git a/nodestack.cc b/nodestack.cc
index b4f75e0..4da3cd6 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -91,7 +91,7 @@ void Node::print()
 	if (action)
 		action->print();
 	else
-		printf("******** empty action ********\n");
+		model_print("******** empty action ********\n");
 }
 
 /** @brief Prints info about may_read_from set */
@@ -495,14 +495,14 @@ NodeStack::~NodeStack()
 
 void NodeStack::print()
 {
-	printf("............................................\n");
-	printf("NodeStack printing node_list:\n");
+	model_print("............................................\n");
+	model_print("NodeStack printing node_list:\n");
 	for (unsigned int it = 0; it < node_list.size(); it++) {
 		if (it == this->iter)
-			printf("vvv following action is the current iterator vvv\n");
+			model_print("vvv following action is the current iterator vvv\n");
 		node_list[it]->print();
 	}
-	printf("............................................\n");
+	model_print("............................................\n");
 }
 
 /** Note: The is_enabled set contains what actions were enabled when
diff --git a/snapshot.cc b/snapshot.cc
index fb00d15..e930a33 100644
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -19,10 +19,10 @@
 
 #include "common.h"
 
-#define FAILURE(mesg) { printf("failed in the API: %s with errno relative message: %s\n", mesg, strerror( errno ) ); exit(EXIT_FAILURE); }
+#define FAILURE(mesg) { model_print("failed in the API: %s with errno relative message: %s\n", mesg, strerror( errno ) ); exit(EXIT_FAILURE); }
 
 #ifdef CONFIG_SSDEBUG
-#define SSDEBUG		printf
+#define SSDEBUG		model_print
 #else
 #define SSDEBUG(...)	do { } while (0)
 #endif
@@ -86,9 +86,9 @@ static void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsna
  */
 static void HandlePF( int sig, siginfo_t *si, void * unused){
 	if( si->si_code == SEGV_MAPERR ){
-		printf("Real Fault at %p\n", si->si_addr);
+		model_print("Real Fault at %p\n", si->si_addr);
 		print_trace();
-		printf("For debugging, place breakpoint at: %s:%d\n",
+		model_print("For debugging, place breakpoint at: %s:%d\n",
 				__FILE__, __LINE__);
 		exit( EXIT_FAILURE );
 	}
@@ -96,7 +96,7 @@ static void HandlePF( int sig, siginfo_t *si, void * unused){
 
 	unsigned int backingpage=snapshotrecord->lastBackingPage++; //Could run out of pages...
 	if (backingpage==snapshotrecord->maxBackingPages) {
-		printf("Out of backing pages at %p\n", si->si_addr);
+		model_print("Out of backing pages at %p\n", si->si_addr);
 		exit( EXIT_FAILURE );
 	}
 
@@ -151,12 +151,12 @@ void initSnapshotLibrary(unsigned int numbackingpages,
 	sa.sa_sigaction = HandlePF;
 #ifdef MAC
 	if( sigaction( SIGBUS, &sa, NULL ) == -1 ){
-		printf("SIGACTION CANNOT BE INSTALLED\n");
+		model_print("SIGACTION CANNOT BE INSTALLED\n");
 		exit(EXIT_FAILURE);
 	}
 #endif
 	if( sigaction( SIGSEGV, &sa, NULL ) == -1 ){
-		printf("SIGACTION CANNOT BE INSTALLED\n");
+		model_print("SIGACTION CANNOT BE INSTALLED\n");
 		exit(EXIT_FAILURE);
 	}
 
@@ -251,7 +251,7 @@ void addMemoryRegionToSnapShot( void * addr, unsigned int numPages) {
 #if USE_MPROTECT_SNAPSHOT
 	unsigned int memoryregion=snapshotrecord->lastRegion++;
 	if (memoryregion==snapshotrecord->maxRegions) {
-		printf("Exceeded supported number of memory regions!\n");
+		model_print("Exceeded supported number of memory regions!\n");
 		exit(EXIT_FAILURE);
 	}
 
@@ -268,13 +268,13 @@ snapshot_id takeSnapshot( ){
 	for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
 		if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ ) == -1 ){
 			perror("mprotect");
-			printf("Failed to mprotect inside of takeSnapShot\n");
+			model_print("Failed to mprotect inside of takeSnapShot\n");
 			exit(EXIT_FAILURE);
 		}
 	}
 	unsigned int snapshot=snapshotrecord->lastSnapShot++;
 	if (snapshot==snapshotrecord->maxSnapShots) {
-		printf("Out of snapshots\n");
+		model_print("Out of snapshots\n");
 		exit(EXIT_FAILURE);
 	}
 	snapshotrecord->snapShots[snapshot].firstBackingPage=snapshotrecord->lastBackingPage;
@@ -305,7 +305,7 @@ void rollBack( snapshot_id theID ){
 	for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
 		if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ | PROT_WRITE ) == -1 ){
 			perror("mprotect");
-			printf("Failed to mprotect inside of takeSnapShot\n");
+			model_print("Failed to mprotect inside of takeSnapShot\n");
 			exit(EXIT_FAILURE);
 		}
 	}
diff --git a/threads.cc b/threads.cc
index dc2db2d..dd2a598 100644
--- a/threads.cc
+++ b/threads.cc
@@ -161,7 +161,7 @@ Thread::Thread(thrd_t *t, void (*func)(void *), void *a) :
 	/* Initialize state */
 	ret = create_context();
 	if (ret)
-		printf("Error in create_context\n");
+		model_print("Error in create_context\n");
 
 	id = model->get_next_id();
 	*user_thread = id;