diff options
| -rw-r--r-- | test/Runtime/POSIX/GenBout.c | 72 | ||||
| -rw-r--r-- | test/lit.cfg | 3 | ||||
| -rw-r--r-- | tools/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | tools/gen-bout/CMakeLists.txt | 17 | ||||
| -rw-r--r-- | tools/gen-bout/gen-bout.cpp | 278 |
5 files changed, 370 insertions, 1 deletions
diff --git a/test/Runtime/POSIX/GenBout.c b/test/Runtime/POSIX/GenBout.c new file mode 100644 index 00000000..44979735 --- /dev/null +++ b/test/Runtime/POSIX/GenBout.c @@ -0,0 +1,72 @@ +// RUN: rm -rf file.bout +// RUN: echo -n aaaa > %t.aaaa.txt +// RUN: echo -n bbbb > %t.bbbb.txt +// RUN: echo -n cccc > %t.cccc.txt +// RUN: %gen-bout -o -p -q file1 --sym-stdin %t.aaaa.txt --sym-file %t.bbbb.txt --sym-stdout %t.cccc.txt +// RUN: %cc %s -O0 -o %t +// RUN: %klee-replay %t file.bout 2>&1 | grep "klee-replay: EXIT STATUS: NORMAL" + +#include <sys/types.h> +#include <sys/stat.h> +#include <fcntl.h> +#include <stdio.h> +#include <string.h> +#include <unistd.h> + +int check_fd(int fd, const int file_size) { + struct stat fs; + + if (fstat(fd, &fs) < 0) + return -1; + + if (fs.st_size != file_size) + return -1; + + return 0; +} + +int check_file(const char *file_name, const int file_size) { + int fd; + + if ((fd = open(file_name, O_RDONLY)) < 0) + return -1; + + if (check_fd(fd, file_size) < 0) + return -1; + + close(fd); + return 0; +} + +int main(int argc, char **argv) { + int i = 0; + + if (argc != 5) + return 1; + + if (strcmp(argv[1], "-o")) + return 1; + + if (strcmp(argv[2], "-p")) + return 1; + + if (strcmp(argv[3], "-q")) + return 1; + + if (strcmp(argv[4], "file1")) + return 1; + + if (check_file("A", 4)) + return 1; + + if (check_fd(0, 4)) + return 1; + + if (check_fd(1, 1024)) + return 1; + + printf("tests passed\n"); + + return 0; +} + diff --git a/test/lit.cfg b/test/lit.cfg index a9982150..4913fa5f 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -138,7 +138,8 @@ if len(kleaver_extra_params) != 0: subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), ('%klee-replay', 'klee-replay', ''), ('%klee','klee', klee_extra_params), - ('%ktest-tool', 'ktest-tool', '') + ('%ktest-tool', 'ktest-tool', ''), + ('%gen-bout', 'gen-bout', '') ] for s,basename,extra_args in subs: config.substitutions.append( diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index 9bf2acf8..6fe153d7 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -6,6 +6,7 @@ # License. See LICENSE.TXT for details. # #===------------------------------------------------------------------------===# +add_subdirectory(gen-bout) add_subdirectory(gen-random-bout) add_subdirectory(kleaver) add_subdirectory(klee) diff --git a/tools/gen-bout/CMakeLists.txt b/tools/gen-bout/CMakeLists.txt new file mode 100644 index 00000000..07cfb3c7 --- /dev/null +++ b/tools/gen-bout/CMakeLists.txt @@ -0,0 +1,17 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# +add_executable(gen-bout + gen-bout.cpp +) + +set(KLEE_LIBS kleeBasic) + +target_link_libraries(gen-bout ${KLEE_LIBS}) + +install(TARGETS gen-bout RUNTIME DESTINATION bin) diff --git a/tools/gen-bout/gen-bout.cpp b/tools/gen-bout/gen-bout.cpp new file mode 100644 index 00000000..d8754251 --- /dev/null +++ b/tools/gen-bout/gen-bout.cpp @@ -0,0 +1,278 @@ +//===-- gen-bout.cpp --------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include <assert.h> +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <sys/types.h> +#include <sys/stat.h> +#include <time.h> +#include <unistd.h> + +#include "klee/Internal/ADT/KTest.h" + +#if defined(__FreeBSD__) || defined(__minix) +#define stat64 stat +#endif + + +#define MAX 64 +static void push_obj(KTest *b, const char *name, unsigned total_bytes, + unsigned char *bytes) { + KTestObject *o = &b->objects[b->numObjects++]; + assert(b->numObjects < MAX); + + o->name = strdup(name); + o->numBytes = total_bytes; + o->bytes = (unsigned char *)malloc(o->numBytes); + + memcpy(o->bytes, bytes, total_bytes); +} + +static void push_range(KTest *b, const char *name, unsigned value) { + KTestObject *o = &b->objects[b->numObjects++]; + assert(b->numObjects < MAX); + + o->name = strdup(name); + o->numBytes = 4; + o->bytes = (unsigned char *)malloc(o->numBytes); + + *(unsigned *)o->bytes = value; +} + +void print_usage_and_exit(char *program_name) { + fprintf(stderr, + "%s: Tool for generating ktest file with concrete input, " + "e.g., for using a concrete crashing input as a ktest seed.\n", + program_name); + fprintf(stderr, "Usage: %s <arguments>\n", program_name); + fprintf(stderr, " <arguments> are the command-line arguments of the " + "programs, with the following treated as special:\n"); + fprintf(stderr, " --sym-stdin <filename> - Specifying a file that " + "is the content of the stdin (only once).\n"); + fprintf(stderr, " --sym-stdout <filename> - Specifying a file that " + "is the content of the stdout (only once).\n"); + fprintf(stderr, " --sym-file <filename> - Specifying a file that " + "is the content of a file named A provided for the program " + "(only once).\n"); + fprintf(stderr, " Ex: %s -o -p -q file1 --sym-stdin file2 --sym-file file3 " + "--sym-stdout file4\n", + program_name); + exit(1); +} + +int main(int argc, char *argv[]) { + unsigned i, argv_copy_idx; + unsigned file_counter = 0; + char *stdout_content_filename = NULL; + char *stdin_content_filename = NULL; + char *content_filenames_list[1024]; + char **argv_copy; + + if (argc < 2) + print_usage_and_exit(argv[0]); + + KTest b; + b.symArgvs = 0; + b.symArgvLen = 0; + + b.numObjects = 0; + b.objects = (KTestObject *)malloc(MAX * sizeof *b.objects); + + if ((argv_copy = (char **)malloc(sizeof(char *) * argc * 2)) == NULL) { + fprintf(stderr, "Could not allocate more memory\n"); + return 1; + } + + argv_copy[0] = (char *)malloc(strlen(argv[0]) + 1); + strcpy(argv_copy[0], argv[0]); + argv_copy_idx = 1; + + for (i = 1; i < (unsigned)argc; i++) { + if (strcmp(argv[i], "--sym-stdout") == 0 || + strcmp(argv[i], "-sym-stdout") == 0) { + if (++i == (unsigned)argc || argv[i][0] == '-') + print_usage_and_exit(argv[0]); + + if (stdout_content_filename) + print_usage_and_exit(argv[0]); + + stdout_content_filename = argv[i]; + + } else if (strcmp(argv[i], "--sym-stdin") == 0 || + strcmp(argv[i], "-sym-stdin") == 0) { + if (++i == (unsigned)argc || argv[i][0] == '-') + print_usage_and_exit(argv[0]); + + if (stdin_content_filename) + print_usage_and_exit(argv[0]); + + stdin_content_filename = argv[i]; + } else if (strcmp(argv[i], "--sym-file") == 0 || + strcmp(argv[i], "-sym-file") == 0) { + if (++i == (unsigned)argc || argv[i][0] == '-') + print_usage_and_exit(argv[0]); + + content_filenames_list[file_counter++] = argv[i]; + } else { + long nbytes = strlen(argv[i]) + 1; + static int total_args = 0; + + char arg[1024]; + sprintf(arg, "arg%d", total_args++); + push_obj(&b, (const char *)arg, nbytes, (unsigned char *)argv[i]); + + char *buf1 = (char *)malloc(1024); + char *buf2 = (char *)malloc(1024); + strcpy(buf1, "-sym-arg"); + sprintf(buf2, "%ld", nbytes - 1); + argv_copy[argv_copy_idx++] = buf1; + argv_copy[argv_copy_idx++] = buf2; + } + } + + if (file_counter > 0) { + FILE *fp; + struct stat64 file_stat; + char *content_filename = content_filenames_list[file_counter - 1]; + + if ((fp = fopen(content_filename, "r")) == NULL || + stat64(content_filename, &file_stat) < 0) { + fprintf(stderr, "Failure opening %s\n", content_filename); + print_usage_and_exit(argv[0]); + } + + long nbytes = file_stat.st_size; + char filename[7] = "A-data"; + char statname[12] = "A-data-stat"; + + unsigned char *file_content, *fptr; + if ((file_content = (unsigned char *)malloc(nbytes)) == NULL) { + fprintf(stderr, "Memory allocation failure\n"); + exit(1); + } + + int read_char; + fptr = file_content; + while ((read_char = fgetc(fp)) != EOF) { + *fptr = (unsigned char)read_char; + fptr++; + } + + push_obj(&b, filename, nbytes, file_content); + push_obj(&b, statname, sizeof(struct stat64), (unsigned char *)&file_stat); + + free(file_content); + + char *buf1 = (char *)malloc(1024); + char *buf2 = (char *)malloc(1024); + char *buf3 = (char *)malloc(1024); + sprintf(buf1, "-sym-files"); + sprintf(buf2, "1"); + sprintf(buf3, "%ld", nbytes); + argv_copy[argv_copy_idx++] = buf1; + argv_copy[argv_copy_idx++] = buf2; + argv_copy[argv_copy_idx++] = buf3; + } + + if (stdin_content_filename) { + FILE *fp; + struct stat64 file_stat; + char filename[6] = "stdin"; + char statname[11] = "stdin-stat"; + + if ((fp = fopen(stdin_content_filename, "r")) == NULL || + stat64(stdin_content_filename, &file_stat) < 0) { + fprintf(stderr, "Failure opening %s\n", stdin_content_filename); + print_usage_and_exit(argv[0]); + } + + unsigned char *file_content, *fptr; + if ((file_content = (unsigned char *)malloc(file_stat.st_size)) == NULL) { + fprintf(stderr, "Memory allocation failure\n"); + exit(1); + } + + int read_char; + fptr = file_content; + while ((read_char = fgetc(fp)) != EOF) { + *fptr = (unsigned char)read_char; + fptr++; + } + + push_obj(&b, filename, file_stat.st_size, file_content); + push_obj(&b, statname, sizeof(struct stat64), (unsigned char *)&file_stat); + + free(file_content); + + char *buf1 = (char *)malloc(1024); + char *buf2 = (char *)malloc(1024); + sprintf(buf1, "-sym-stdin"); + sprintf(buf2, "%ld", file_stat.st_size); + argv_copy[argv_copy_idx++] = buf1; + argv_copy[argv_copy_idx++] = buf2; + } + + if (stdout_content_filename) { + FILE *fp; + struct stat64 file_stat; + unsigned char file_content[1024]; + char filename[7] = "stdout"; + char statname[12] = "stdout-stat"; + + if ((fp = fopen(stdout_content_filename, "r")) == NULL || + stat64(stdout_content_filename, &file_stat) < 0) { + fprintf(stderr, "Failure opening %s\n", stdout_content_filename); + print_usage_and_exit(argv[0]); + } + + int read_char; + for (int i = 0; i < file_stat.st_size && i < 1024; ++i) { + read_char = fgetc(fp); + file_content[i] = (unsigned char)read_char; + } + + for (int i = file_stat.st_size; i < 1024; ++i) { + file_content[i] = 0; + } + + file_stat.st_size = 1024; + + push_obj(&b, filename, 1024, file_content); + push_obj(&b, statname, sizeof(struct stat64), (unsigned char *)&file_stat); + + char *buf = (char *)malloc(1024); + sprintf(buf, "-sym-stdout"); + argv_copy[argv_copy_idx++] = buf; + } + + argv_copy[argv_copy_idx] = 0; + + b.numArgs = argv_copy_idx; + b.args = argv_copy; + + push_range(&b, "model_version", 1); + + if (!kTest_toFile(&b, "file.bout")) + assert(0); + + for (int i = 0; i < (int)b.numObjects; ++i) { + free(b.objects[i].name); + free(b.objects[i].bytes); + } + free(b.objects); + + for (int i = 0; i < (int)argv_copy_idx; ++i) { + free(argv_copy[i]); + } + free(argv_copy); + + return 0; +} |