From fdc038715881f395ddbac1625160236f8db2c1d7 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 14 Dec 2016 16:50:40 -0800 Subject: [PATCH 1/1] Work around changes in newer versions of glibc --- common.cc | 1 + common.h | 10 +++++++++- constgen.cc | 16 ++++++++-------- eprecord.cc | 28 ++++++++++++++-------------- execpoint.cc | 14 +++++++------- main.cc | 12 ++++++++++++ mcexecution.cc | 10 +++++----- model.cc | 2 +- mymemory.cc | 13 +++++++++++-- stacktrace.h | 10 +++++----- 10 files changed, 73 insertions(+), 43 deletions(-) diff --git a/common.cc b/common.cc index b57e93c..b445ce3 100644 --- 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 7206371..89b59b4 100644 --- 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 6e452ac..2f3375b 100644 --- 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 10b4537..a11d2d6 100644 --- 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;igetValue(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;iiterator(); - 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 d35bd8d..7b63213 100644 --- a/execpoint.cc +++ b/execpoint.cc @@ -130,26 +130,26 @@ bool ExecPointEquals(ExecPoint *e1, ExecPoint * e2) { } void ExecPoint::print(int f) { - dprintf(f,""); + model_dprintf(f, ">"); } void ExecPoint::print() { diff --git a/main.cc b/main.cc index d8d4193..9060af5 100644 --- 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 36afe0b..9ea8af6 100644 --- 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;isize();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 7da359b..2ac46b8 100644 --- 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 8d95dfa..ea65c89 100644 --- 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 7a3ac50..f7c451c 100644 --- 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, " \n"); + model_dprintf(fd, " \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]); } } -- 2.34.1