about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorAndrew Santosa <santosa_1999@yahoo.com>2018-06-21 14:14:08 +0800
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-10-26 18:33:00 +0300
commitbe340780e6261416320dd099753e17080de69534 (patch)
tree5b0c252c821117e70d0520211a0eaf53cf4eddce
parent0525bd791318fe0ce2b68a7b4596f34c2770ef53 (diff)
downloadklee-be340780e6261416320dd099753e17080de69534.tar.gz
Added gen-bout tool to generate ktest file (file.bout) using specified concrete arguments and files.
* Sample use cases:
  * Using an interesting input as a seed, such as a crashing input.
  * Analyzing the path condition of a crashing input.
* Also added the test: test/Runtime/POSIX/GenBout.c
-rw-r--r--test/Runtime/POSIX/GenBout.c72
-rw-r--r--test/lit.cfg3
-rw-r--r--tools/CMakeLists.txt1
-rw-r--r--tools/gen-bout/CMakeLists.txt17
-rw-r--r--tools/gen-bout/gen-bout.cpp278
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;
+}