Work around changes in newer versions of glibc

diff --git a/common.cc b/common.cc
index b57e93c7e3db3fb10bbb4564a9ecac65dd66feb9..b445ce359596cbbaed1e539dfed25ee353d5a566 100644 (file)
--- a/common.cc
+++ b/common.cc
@@ -25,6 +25,7 @@
 
 /** @brief Model-checker output file descriptor; default to stdout until redirected */
 int model_out = STDOUT_FILENO;
+int model_err = STDERR_FILENO;
 
 #define CONFIG_STACKTRACE
 /** Print a backtrace of the current program state. */

diff --git a/common.h b/common.h
index 720637153067b7e03d56b24a02d0d480fe85c257..89b59b42177094a12f362ca4fe321587d058b9f3 100644 (file)
--- a/common.h
+++ b/common.h
@@ -18,8 +18,16 @@
 #include "config.h"
 
 extern int model_out;
+extern int model_err;
+extern int switch_alloc;
+
+#define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ##__VA_ARGS__); switch_alloc = 0; } while (0)
+
+#define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
+
+#define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ##__VA_ARGS__); } while (0)
+
 
-#define model_print(fmt, ...) do { dprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
 
 #ifdef CONFIG_DEBUG
 #define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ##__VA_ARGS__); } while (0)

diff --git a/constgen.cc b/constgen.cc
index 6e452ac747eac71bfb68fee065faef6c4d8daca7..2f3375b23070d0cd9ccde22677440b042b0ca6ac 100644 (file)
--- a/constgen.cc
+++ b/constgen.cc
@@ -308,7 +308,7 @@ void ConstGen::printEventGraph() {
        sprintf(buffer, "eventgraph%u.dot",schedule_graph);
        schedule_graph++;
        int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
-       dprintf(file, "digraph eventgraph {\n");
+       model_dprintf(file, "digraph eventgraph {\n");
        
        EPRecord *first=execution->getEPRecord(MCID_FIRST);
        printRecord(first, file);
@@ -318,19 +318,19 @@ void ConstGen::printEventGraph() {
                printRecord(record, file);
        }
 
-       dprintf(file, "}\n");
+       model_dprintf(file, "}\n");
        close(file);
 }
 
 void ConstGen::doPrint(EPRecord *record, int file) {
-       dprintf(file, "%lu[label=\"",(uintptr_t)record);
+       model_dprintf(file, "%lu[label=\"",(uintptr_t)record);
        record->print(file);
-       dprintf(file, "\"];\n");
+       model_dprintf(file, "\"];\n");
        if (record->getNextRecord()!=NULL)
-               dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
+               model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
        
        if (record->getChildRecord()!=NULL)
-               dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
+               model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
 }
 
 void ConstGen::printRecord(EPRecord *record, int file) {
@@ -362,7 +362,7 @@ void ConstGen::printRecord(EPRecord *record, int file) {
                                //runs code
                                if (branchdir->getFirstRecord()!=NULL) {
                                        workstack->push_back(branchdir->getFirstRecord());
-                                       dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord());
+                                       model_dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord());
                                }
                        }
                        return;
@@ -878,7 +878,7 @@ bool * ConstGen::runSolver() {
        } else {
                delete solver;
                solver=NULL;
-               dprintf(2, "INDETER\n");
+               model_print_err("INDETER\n");
                model_print("INDETER\n");
                exit(-1);
                return NULL;

diff --git a/eprecord.cc b/eprecord.cc
index 10b4537980e28b9173fddd07bc22ce9ca7fa0366..a11d2d6d11e0b2b5c1f6bfdb6f3a2c73d515ad83 100644 (file)
--- a/eprecord.cc
+++ b/eprecord.cc
@@ -132,13 +132,13 @@ IntHashSet * EPRecord::getReturnValueSet() {
 void EPRecord::print(int f) {
        if (event==RMW) {
                if (op==ADD)
-                       dprintf(f, "add");
+                       model_dprintf(f, "add");
                else if (op==EXC)
-                       dprintf(f, "exc");
+                       model_dprintf(f, "exc");
                else
-                       dprintf(f, "cas");
+                       model_dprintf(f, "cas");
        } else
-               dprintf(f, "%s",eventToStr(event));
+               model_dprintf(f, "%s",eventToStr(event));
        IntHashSet *i=NULL;
        switch(event) {
        case LOAD:
@@ -153,14 +153,14 @@ void EPRecord::print(int f) {
        case FUNCTION: {
                if (!getPhi()) {
                        CGoalIterator *cit=completed->iterator();
-                       dprintf(f, "{");
+                       model_dprintf(f, "{");
                        while(cit->hasNext()) {
                                CGoal *goal=cit->next();
-                               dprintf(f,"(");
+                               model_dprintf(f,"(");
                                for(uint i=0;i<getNumFuncInputs();i++) {
-                                       dprintf(f,"%lu ", goal->getValue(i+VC_BASEINDEX));
+                                       model_dprintf(f,"%lu ", goal->getValue(i+VC_BASEINDEX));
                                }
-                               dprintf(f,"=> %lu)", goal->getOutput());
+                               model_dprintf(f,"=> %lu)", goal->getOutput());
                        }
                        delete cit;
                }
@@ -171,23 +171,23 @@ void EPRecord::print(int f) {
        }
        if (i!=NULL) {
                IntIterator *it=i->iterator();
-               dprintf(f, "{");
+               model_dprintf(f, "{");
 
                while(it->hasNext()) {
-                       dprintf(f, "%lu ", it->next());
+                       model_dprintf(f, "%lu ", it->next());
                }
-               dprintf(f, "}");
+               model_dprintf(f, "}");
                delete it;
        }
 
        for(uint i=0;i<numinputs;i++) {
                IntIterator *it=setarray[i]->iterator();
-               dprintf(f,"{");
+               model_dprintf(f,"{");
                while(it->hasNext()) {
                        uint64_t v=it->next();
-                       dprintf(f,"%lu ", v);
+                       model_dprintf(f,"%lu ", v);
                }
-               dprintf(f,"}");
+               model_dprintf(f,"}");
                delete it;
        }
 

diff --git a/execpoint.cc b/execpoint.cc
index d35bd8d09efb70d48ca3491e24ec91256447c591..7b632134b87093f0f3d3f2364005d75b4ce9768d 100644 (file)
--- a/execpoint.cc
+++ b/execpoint.cc
@@ -130,26 +130,26 @@ bool ExecPointEquals(ExecPoint *e1, ExecPoint * e2) {
 }
 
 void ExecPoint::print(int f) {
-       dprintf(f,"<tid=%u,",tid);
+       model_dprintf(f,"<tid=%u,",tid);
        for(unsigned int i=0;i<size;i+=2) {
                switch((ExecPointType)pairarray[i]) {
                case EP_BRANCH:
-                       dprintf(f,"br");
+                       model_dprintf(f,"br");
                        break;
                case EP_COUNTER:
-                       dprintf(f,"cnt");
+                       model_dprintf(f,"cnt");
                        break;
                case EP_LOOP:
-                       dprintf(f,"lp");
+                       model_dprintf(f,"lp");
                        break;
                default:
                        ASSERT(false);
                }
-               dprintf(f, "(%u)", pairarray[i+1]);
+               model_dprintf(f, "(%u)", pairarray[i+1]);
                if ((i+2)<size)
-                       dprintf(f, ", ");
+                       model_dprintf(f, ", ");
        }
-       dprintf(f, ">");
+       model_dprintf(f, ">");
 }
 
 void ExecPoint::print() {

diff --git a/main.cc b/main.cc
index d8d4193b1256b0d8cf767391246502dd4a877a85..9060af5f96124b38ce244a79100bfe8421f3b556 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -125,6 +125,18 @@ int main(int argc, char **argv)
        main_argc = argc;
        main_argv = argv;
 
+       /*
+        * If this printf statement is removed, CDSChecker will fail on an
+        * assert on some versions of glibc.  The first time printf is
+        * called, it allocated internal buffers.  We can't easily snapshot
+        * libc since we also use it.
+        */
+       
+       printf("SATCheck\n"
+                                "Copyright (c) 2016 Regents of the University of California. All rights reserved.\n"
+                                "Distributed under the GPLv2\n"
+                                "Written by Brian Demsky and Patrick Lam\n\n");
+       
        /* Configure output redirection for the model-checker */
        redirect_output();
 

diff --git a/mcexecution.cc b/mcexecution.cc
index 36afe0b81f030112102e0f7a07e2ae1c9e69c09f..9ea8af61aa5cde891a08a9ed4296ae2c4cb49704 100644 (file)
--- a/mcexecution.cc
+++ b/mcexecution.cc
@@ -111,21 +111,21 @@ void MCExecution::dumpExecution() {
        sprintf(buffer, "exec%u.dot",schedule_graph);
        schedule_graph++;
        int file=open(buffer,O_WRONLY|O_TRUNC|O_CREAT, S_IRWXU);
-       dprintf(file, "digraph execution {\n");
+       model_dprintf(file, "digraph execution {\n");
        EPRecord *last=NULL;
        for(uint i=0;i<EPList->size();i++) {
                EPValue *epv=(*EPList)[i];
                if (epv==NULL)
                        continue;
                EPRecord *record=epv->getRecord();
-               dprintf(file, "%lu[label=\"",(uintptr_t)record);
+               model_dprintf(file, "%lu[label=\"",(uintptr_t)record);
                record->print(file);
-               dprintf(file, "\"];\n");
+               model_dprintf(file, "\"];\n");
                if (last!=NULL)
-                       dprintf(file, "%lu->%lu;", (uintptr_t) last, (uintptr_t) record);
+                       model_dprintf(file, "%lu->%lu;", (uintptr_t) last, (uintptr_t) record);
                last=record;
        }
-       dprintf(file, "}\n");
+       model_dprintf(file, "}\n");
        close(file);
 }
 

diff --git a/model.cc b/model.cc
index 7da359bbd2b9e144bf778afcd8ffcd28025f63a0..2ac46b8313fba22a175dd27ac5d1664e36ad4288 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -44,7 +44,7 @@ void MC::check() {
                execution->reset();
                snapshot_backtrack_before(0);
        } while(!execution->get_planner()->is_finished());
-       dprintf(2, "Finished!\n");
+       model_print_err("Finished!\n");
 }
 
 

diff --git a/mymemory.cc b/mymemory.cc
index 8d95dfa68e2277f60f9cd4287ae62ec6499c780b..ea65c8967f471db37c601ca41a103e607f5d4e7d 100644 (file)
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -26,6 +26,7 @@
 size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
 int nextRequest = 0;
 int howManyFreed = 0;
+int switch_alloc = 0;
 #if !USE_MPROTECT_SNAPSHOT
 static mspace sStaticSpace = NULL;
 #endif
@@ -226,7 +227,11 @@ void *malloc(size_t size)
 {
        if (user_snapshot_space) {
                /* Only perform user allocations from user context */
-               return user_malloc(size);
+               if (switch_alloc) {
+                       return model_malloc(size);
+               } else {
+                       return user_malloc(size);
+               }
        } else
                return HandleEarlyAllocationRequest(size);
 }
@@ -235,7 +240,11 @@ void *malloc(size_t size)
 void free(void * ptr)
 {
        if (!DontFree(ptr))
-               mspace_free(user_snapshot_space, ptr);
+               if (switch_alloc) {
+                       model_free(ptr);
+               } else {
+                       mspace_free(user_snapshot_space, ptr);
+               }
 }
 
 /** @brief Snapshotting realloc implementation for user programs */

diff --git a/stacktrace.h b/stacktrace.h
index 7a3ac505764db65bdc9760a7aff4d89da0e3284a..f7c451c8cfcde9fcfb2351f55fc6076a9362cef5 100644 (file)
--- a/stacktrace.h
+++ b/stacktrace.h
@@ -15,7 +15,7 @@
  */
 static inline void print_stacktrace(int fd = STDERR_FILENO, unsigned int max_frames = 63)
 {
-       dprintf(fd, "stack trace:\n");
+       model_dprintf(fd, "stack trace:\n");
 
        // storage array for stack trace address data
        void* addrlist[max_frames+1];
@@ -24,7 +24,7 @@ static inline void print_stacktrace(int fd = STDERR_FILENO, unsigned int max_fra
        int addrlen = backtrace(addrlist, sizeof(addrlist) / sizeof(void*));
 
        if (addrlen == 0) {
-               dprintf(fd, "  <empty, possibly corrupt>\n");
+               model_dprintf(fd, "  <empty, possibly corrupt>\n");
                return;
        }
 
@@ -68,17 +68,17 @@ static inline void print_stacktrace(int fd = STDERR_FILENO, unsigned int max_fra
                                                                                                                                                        funcname, &funcnamesize, &status);
                        if (status == 0) {
                                funcname = ret; // use possibly realloc()-ed string
-                               dprintf(fd, "  %s : %s+%s\n",
+                               model_dprintf(fd, "  %s : %s+%s\n",
                                                                symbollist[i], funcname, begin_offset);
                        } else {
                                // demangling failed. Output function name as a C function with
                                // no arguments.
-                               dprintf(fd, "  %s : %s()+%s\n",
+                               model_dprintf(fd, "  %s : %s()+%s\n",
                                                                symbollist[i], begin_name, begin_offset);
                        }
                } else {
                        // couldn't parse the line? print the whole line.
-                       dprintf(fd, "  %s\n", symbollist[i]);
+                       model_dprintf(fd, "  %s\n", symbollist[i]);
                }
        }