about summary refs log tree commit diff homepage
path: root/runtime/Runtest
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2009-05-21 04:36:41 +0000
committerDaniel Dunbar <daniel@zuster.org>2009-05-21 04:36:41 +0000
commit6f290d8f9e9d7faac295cb51fc96884a18f4ded4 (patch)
tree46e7d426abc0c9f06ac472ac6f7f9e661b5d78cb /runtime/Runtest
parenta55960edd4dcd7535526de8d2277642522aa0209 (diff)
downloadklee-6f290d8f9e9d7faac295cb51fc96884a18f4ded4.tar.gz
Initial KLEE checkin.
 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'runtime/Runtest')
-rw-r--r--runtime/Runtest/Makefile19
-rw-r--r--runtime/Runtest/intrinsics.c154
2 files changed, 173 insertions, 0 deletions
diff --git a/runtime/Runtest/Makefile b/runtime/Runtest/Makefile
new file mode 100644
index 00000000..dd21c4a9
--- /dev/null
+++ b/runtime/Runtest/Makefile
@@ -0,0 +1,19 @@
+#===-- runtime/Runtest/Makefile ----------------------------*- Makefile -*--===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+LEVEL=../..
+
+USEDLIBS=kleeBasic.a
+LIBRARYNAME=kleeRuntest
+SHARED_LIBRARY=1
+LINK_LIBS_IN_SHARED = 1
+DONT_BUILD_RELINKED = 1
+NO_PEDANTIC=1
+
+include $(LEVEL)/Makefile.common
diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c
new file mode 100644
index 00000000..1a2fd030
--- /dev/null
+++ b/runtime/Runtest/intrinsics.c
@@ -0,0 +1,154 @@
+//===-- intrinsics.c ------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+/* Straight C for linking simplicity */
+
+#include <assert.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <sys/mman.h>
+#include <sys/time.h>
+#include <time.h>
+
+#include "klee/klee.h"
+
+#include "klee/Internal/ADT/BOut.h"
+
+static BOut *testData = 0;
+static unsigned testPosition = 0;
+
+static unsigned char rand_byte(void) {
+  unsigned x = rand();
+  x ^= x>>16;
+  x ^= x>>8;
+  return x & 0xFF;
+}
+
+void klee_make_symbolic_name(void *array, unsigned nbytes, const char *name) {
+  static int rand_init = -1;
+
+  if (rand_init == -1) {
+    if (getenv("KLEE_RANDOM")) {
+      struct timeval tv;
+      gettimeofday(&tv, 0);
+      rand_init = 1;
+      srand(tv.tv_sec ^ tv.tv_usec);
+    } else {
+      rand_init = 0;
+    }
+  }
+
+  if (rand_init) {
+    if (!strcmp(name,"syscall_a0")) {
+      unsigned long long *v = array;
+      assert(nbytes == 8);
+      *v = rand() % 69;
+    } else {
+      char *c = array;
+      unsigned i;
+      for (i=0; i<nbytes; i++)
+        c[i] = rand_byte();
+    }
+    return;
+  }
+
+  if (!testData) {
+    char tmp[256];
+    char *name = getenv("KLEE_RUNTEST");
+
+    if (!name) {
+      fprintf(stdout, "KLEE-RUNTIME: KLEE_RUNTEST not set, please enter .bout path: ");
+      fflush(stdout);
+      name = tmp;
+      if (!fgets(tmp, sizeof tmp, stdin) || !strlen(tmp)) {
+        fprintf(stderr, "KLEE-RUNTIME: cannot replay, no KLEE_RUNTEST or user input\n");
+        exit(1);
+      }
+      tmp[strlen(tmp)-1] = '\0'; /* kill newline */
+    }
+    testData = bOut_fromFile(name);
+    if (!testData) {
+      fprintf(stderr, "KLEE-RUNTIME: unable to open .bout file\n");
+      exit(1);
+    }
+  }
+
+  if (testPosition >= testData->numObjects) {
+    fprintf(stderr, "ERROR: out of inputs, using zero\n");
+    memset(array, 0, nbytes);
+  } else {
+    BOutObject *o = &testData->objects[testPosition++];
+    memcpy(array, o->bytes, nbytes<o->numBytes ? nbytes : o->numBytes);
+    if (nbytes != o->numBytes) {
+      fprintf(stderr, "ERROR: object sizes differ\n");
+      if (o->numBytes < nbytes) 
+        memset((char*) array + o->numBytes, 0, nbytes - o->numBytes);
+    }
+  }
+}
+
+void klee_make_symbolic(void *array, unsigned nbytes) {
+  klee_make_symbolic_name(array, nbytes, "unnamed");
+}
+
+void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment) {
+#if 1
+  return mmap((void*) 0x90000000, nelems*size, PROT_READ|PROT_WRITE, 
+              MAP_PRIVATE
+#ifdef MAP_ANONYMOUS
+              |MAP_ANONYMOUS
+#endif
+              , 0, 0);
+#else
+  char *buffer = malloc(nelems*size + alignment - 1);
+  buffer += (alignment - (long)buffer % alignment);
+  return buffer;
+#endif
+}
+
+void klee_silent_exit(int x) {
+  exit(x);
+}
+
+unsigned klee_choose(unsigned n) {
+  unsigned x;
+  klee_make_symbolic(&x, sizeof x);
+  if(x >= n)
+    fprintf(stderr, "ERROR: max = %d, got = %d\n", n, x);
+  assert(x < n);
+  return x;
+}
+
+void klee_assume(unsigned x) {
+  if (!x) {
+    fprintf(stderr, "ERROR: invalid klee_assume\n");
+  }
+}
+
+unsigned klee_get_value(unsigned x) {
+  return x;
+}
+
+int klee_range_name(int begin, int end, const char* name) {
+  int x;
+  klee_make_symbolic_name(&x, sizeof x, name);
+  if (x<begin || x>=end) {
+    fprintf(stderr, 
+            "KLEE: ERROR: invalid klee_range(%u,%u,%s) value, got: %u\n", 
+            begin, end, name, x);
+    abort();
+  }
+  return x;
+}
+
+/* not sure we should even define.  is for debugging. */
+void klee_print_expr(const char *msg, ...) { }
+
+void klee_set_forking(unsigned enable) { }