printf -> model_print
authorBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 23:23:40 +0000 (15:23 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 23:23:40 +0000 (15:23 -0800)
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.

action.cc
clockvector.cc
common.cc
common.h
hashtable.h
main.cc
model.cc
mymemory.cc
nodestack.cc
snapshot.cc
threads.cc

index 1387ed1..486e89e 100644 (file)
--- 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 */
index e56c2ac..6cd943b 100644 (file)
@@ -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" : ", ");
 }
index f37f92f..d991599 100644 (file)
--- 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)
index 81b2672..b1d6b31 100644 (file)
--- 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
index 4d3b7de..d5c69cc 100644 (file)
@@ -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 (file)
--- 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"
index 05e7679..8dcb6f3 100644 (file)
--- 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,
index 5922a32..6ea6b92 100644 (file)
@@ -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);
        }
 
index b4f75e0..4da3cd6 100644 (file)
@@ -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
index fb00d15..e930a33 100644 (file)
 
 #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);
                }
        }
index dc2db2d..dd2a598 100644 (file)
@@ -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;