From 80f5924fb6c148ecb703dfeae5a751948062588b Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 16 Nov 2012 20:07:57 -0800 Subject: [PATCH] output redirection --- common.cc | 107 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ common.h | 4 +- main.cc | 4 ++ model.cc | 5 +++ output.h | 12 ++++++ 5 files changed, 131 insertions(+), 1 deletion(-) create mode 100644 output.h diff --git a/common.cc b/common.cc index d991599..bbb3053 100644 --- a/common.cc +++ b/common.cc @@ -1,15 +1,22 @@ #include #include #include +#include +#include +#include #include #include "common.h" #include "model.h" #include "stacktrace.h" +#include "output.h" #define MAX_TRACE_LEN 100 +FILE *model_out; +int fd_user_out; /**< @brief File descriptor from which to read user program output */ + #define CONFIG_STACKTRACE /** Print a backtrace of the current program state. */ void print_trace(void) @@ -52,3 +59,103 @@ void model_assert(bool expr, const char *file, int line) model->assert_user_bug(msg); } } + +/** + * @brief Setup output redirecting + * + * 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 + * data when needed. + * + * The model-checker can selectively choose to print/hide the user program + * output. + * @see clear_program_output + * @see print_program_output + * + * Note that the user program's pipe has limited memory, so if a program will + * output much data, we will need to buffer it in user-space during execution. + * This also means that if ModelChecker decides not to print an execution, it + * should promptly clear the pipe. + */ +void redirect_output() +{ + int fd; + + /* Save stdout for later use */ + fd = dup(fileno(stdout)); + model_out = fdopen(fd, "w"); + + /* Redirect program output to a pipe */ + int pipefd[2]; + if (pipe(pipefd) < 0) { + perror("pipe"); + exit(EXIT_FAILURE); + } + fd = dup2(pipefd[1], fileno(stdout)); // STDOUT_FILENO + close(pipefd[1]); + + /* Save the "read" side of the pipe for use later */ + fcntl(pipefd[0], F_SETFL, O_NONBLOCK); + fd_user_out = pipefd[0]; +} + +/** + * @brief Wrapper for reading data to buffer + * + * Besides a simple read, this handles the subtleties of EOF and nonblocking + * input (if fd is O_NONBLOCK). + * + * @param fd The file descriptor to read. + * @param buf Buffer to read to. + * @param maxlen Maximum data to read to buffer + * @return The length of data read. If zero, then we hit EOF or ran out of data + * (non-blocking) + */ +static ssize_t read_to_buf(int fd, char *buf, size_t maxlen) +{ + ssize_t ret = read(fd, buf, maxlen); + if (ret < 0) { + if (errno == EAGAIN || errno == EWOULDBLOCK) { + return 0; + } else { + perror("read"); + exit(EXIT_FAILURE); + } + } + return ret; +} + +/** @brief Dump any pending program output without printing */ +void clear_program_output() +{ + fflush(stdout); + char buf[200]; + while (read_to_buf(fd_user_out, buf, sizeof(buf))); +} + +/** @brief Print out any pending program output */ +void print_program_output() +{ + char buf[200]; + + /* Gather all program output */ + fflush(stdout); + + /* Read program output pipe and write to (real) stdout */ + int 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); + if (res < 0) { + errno = ferror(model_out); + perror("fwrite"); + exit(EXIT_FAILURE); + } + ret -= res; + } + } +} diff --git a/common.h b/common.h index b1d6b31..9c1e1ed 100644 --- a/common.h +++ b/common.h @@ -8,7 +8,9 @@ #include #include "config.h" -#define model_print(fmt, ...) do { printf(fmt, ##__VA_ARGS__); } while (0) +extern FILE *model_out; + +#define model_print(fmt, ...) do { fprintf(model_out, fmt, ##__VA_ARGS__); } while (0) #ifdef CONFIG_DEBUG #define DEBUG(fmt, ...) do { model_print("*** %25s(): line %-4d *** " fmt, __func__, __LINE__, ##__VA_ARGS__); } while (0) diff --git a/main.cc b/main.cc index f55b98d..f79366f 100644 --- a/main.cc +++ b/main.cc @@ -7,6 +7,7 @@ #include #include "common.h" #include "threads-model.h" +#include "output.h" #include "datarace.h" @@ -145,6 +146,9 @@ int main(int argc, char ** argv) { main_argc = argc; main_argv = argv; + /* Configure output redirection for the model-checker */ + redirect_output(); + /* Let's jump in quickly and start running stuff */ initSnapshotLibrary(10000, 1024, 1024, 4000, &model_main); } diff --git a/model.cc b/model.cc index bf54ecc..9ed6d42 100644 --- a/model.cc +++ b/model.cc @@ -13,6 +13,7 @@ #include "promise.h" #include "datarace.h" #include "threads-model.h" +#include "output.h" #define INITIAL_THREAD_ID 0 @@ -139,6 +140,10 @@ void ModelChecker::reset_to_initial_state() too_many_reads = false; bad_synchronization = false; reset_asserted(); + + /* Print all model-checker output before rollback */ + fflush(model_out); + snapshotObject->backTrackBeforeStep(0); } diff --git a/output.h b/output.h new file mode 100644 index 0000000..ca55b7a --- /dev/null +++ b/output.h @@ -0,0 +1,12 @@ +/** @file output.h + * @brief Functions for redirecting program output + */ + +#ifndef __OUTPUT_H__ +#define __OUTPUT_H__ + +void redirect_output(); +void clear_program_output(); +void print_program_output(); + +#endif /* __OUTPUT_H__ */ -- 2.34.1