From e52837077816345a2afa94b42195992a5871824c Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 4 Apr 2013 12:46:13 -0700 Subject: [PATCH] common: make model_print() use OS file descriptor, not C library FILE* A C library FILE does buffering (and possibly other opaque operations) that can conflict with the model-checker's methods of snapshotting memory. Particularly, it seems like we could corrupt and drop data that was written to model_out, if the data was large enough and buffered in just the right way. Really, with the presence of dprintf(), there is no reason to print to a FILE stream; we can just use the file descriptor (either STDOUT_FILENO or the descriptor received from dup2()). This fixes bugs seen in verbose mode, with a lot of extra debug printing. Some of the output was being dropped. --- common.cc | 20 ++++++++++---------- common.h | 4 ++-- model.cc | 3 --- 3 files changed, 12 insertions(+), 15 deletions(-) diff --git a/common.cc b/common.cc index b71c00a..a43064d 100644 --- a/common.cc +++ b/common.cc @@ -14,15 +14,17 @@ #define MAX_TRACE_LEN 100 -/** @brief Model-checker output stream; default to stdout until redirected */ -FILE *model_out = stdout; +/** @brief Model-checker output file descriptor; default to stdout until redirected */ +int model_out = STDOUT_FILENO; #define CONFIG_STACKTRACE /** Print a backtrace of the current program state. */ void print_trace(void) { #ifdef CONFIG_STACKTRACE - print_stacktrace(model_out); + FILE *file = fdopen(model_out, "w"); + print_stacktrace(file); + fclose(file); #else void *array[MAX_TRACE_LEN]; char **strings; @@ -69,7 +71,7 @@ static int fd_user_out; /**< @brief File descriptor from which to read user prog * * Redirects user program's stdout to a pipe so that we can dump it * selectively, when displaying bugs, etc. - * Also connects a special file 'model_out' directly to stdout, for printing + * Also connects a file descriptor 'model_out' directly to stdout, for printing * data when needed. * * The model-checker can selectively choose to print/hide the user program @@ -89,8 +91,7 @@ void redirect_output() int fd; /* Save stdout for later use */ - fd = dup(fileno(stdout)); - model_out = fdopen(fd, "w"); + model_out = dup(fileno(stdout)); /* Redirect program output to a pipe */ int pipefd[2]; @@ -149,16 +150,15 @@ void print_program_output() fflush(stdout); /* Read program output pipe and write to (real) stdout */ - int ret; + ssize_t ret; while (1) { ret = read_to_buf(fd_user_out, buf, sizeof(buf)); if (!ret) break; while (ret > 0) { - int res = fwrite(buf, 1, ret, model_out); + ssize_t res = write(model_out, buf, ret); if (res < 0) { - errno = ferror(model_out); - perror("fwrite"); + perror("write"); exit(EXIT_FAILURE); } ret -= res; diff --git a/common.h b/common.h index c861285..1071135 100644 --- a/common.h +++ b/common.h @@ -8,9 +8,9 @@ #include #include "config.h" -extern FILE *model_out; +extern int model_out; -#define model_print(fmt, ...) do { fprintf(model_out, 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/model.cc b/model.cc index b93653b..f385e56 100644 --- a/model.cc +++ b/model.cc @@ -154,9 +154,6 @@ void ModelChecker::reset_to_initial_state() DEBUG("+++ Resetting to initial state +++\n"); node_stack->reset_execution(); - /* Print all model-checker output before rollback */ - fflush(model_out); - /** * FIXME: if we utilize partial rollback, we will need to free only * those pending actions which were NOT pending before the rollback -- 2.34.1