From: Brian Norris Date: Fri, 16 Nov 2012 23:23:40 +0000 (-0800) Subject: printf -> model_print X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=adf77053d498af32ab4c6764b50d4265bed5996c 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 1387ed15..486e89ee 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 e56c2ace..6cd943b8 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 f37f92f1..d9915993 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 81b26728..b1d6b31e 100644 --- a/common.h +++ b/common.h @@ -8,8 +8,10 @@ #include #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 4d3b7de8..d5c69ccb 100644 --- a/hashtable.h +++ b/hashtable.h @@ -9,6 +9,7 @@ #include #include #include "mymemory.h" +#include "common.h" /** * Hashtable linked node class, for chained storage of hash table conflicts. By @@ -161,7 +162,7 @@ template *) _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 fb4acbe7..10e2d3b9 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: [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n" "\n" "Options:\n" diff --git a/model.cc b/model.cc index 05e76798..8dcb6f3a 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 5922a32d..6ea6b929 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 b4f75e03..4da3cd60 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 fb00d151..e930a336 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; regionlastRegion;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; regionlastRegion;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 dc2db2d9..dd2a5983 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;