diff options
| -rw-r--r-- | runtime/Runtest/Makefile | 11 | ||||
| -rw-r--r-- | runtime/Runtest/intrinsics.c | 69 | ||||
| -rw-r--r-- | test/CMakeLists.txt | 18 | ||||
| -rw-r--r-- | test/Makefile | 3 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_invalid_klee_assume.c | 44 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_invalid_klee_choose.c | 45 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_invalid_klee_range.c | 45 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_invalid_num_objects.c | 39 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_invalid_object_names.c | 45 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_invalid_object_size.c | 43 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_posix_runtime.c | 35 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_simple.c | 28 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_two_objects.c | 33 | ||||
| -rw-r--r-- | test/lit.cfg | 15 | ||||
| -rw-r--r-- | test/lit.site.cfg.in | 6 |
15 files changed, 458 insertions, 21 deletions
diff --git a/runtime/Runtest/Makefile b/runtime/Runtest/Makefile index 666fe06d..82e21345 100644 --- a/runtime/Runtest/Makefile +++ b/runtime/Runtest/Makefile @@ -59,3 +59,14 @@ ifeq ($(HOST_OS), $(filter $(HOST_OS), Linux GNU GNU/kFreeBSD)) # Don't allow unresolved symbols. LLVMLibsOptions += -Wl,--no-undefined endif + +ifeq ($(HOST_OS), Linux) + # HACK: Setup symlinks that `ldconfig` would set up + # so that libkleeRuntest can be used from the build directory. + # This is needed to run tests. + sym_link_name := $(SharedLibDir)/$(SharedPrefix)$(LIBRARYNAME)$(SHLIBEXT).$(SHARED_VERSION) + +all:: $(LibName.SO) + $(Verb) [ ! -e "$(sym_link_name)" ] && ln -s $(LibName.SO) "$(sym_link_name)" || echo "" + +endif diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c index 2302e278..4d785ee2 100644 --- a/runtime/Runtest/intrinsics.c +++ b/runtime/Runtest/intrinsics.c @@ -10,8 +10,9 @@ /* Straight C for linking simplicity */ #include <assert.h> -#include <stdlib.h> +#include <stdarg.h> #include <stdio.h> +#include <stdlib.h> #include <string.h> #include <sys/mman.h> #include <sys/time.h> @@ -31,6 +32,23 @@ static unsigned char rand_byte(void) { return x & 0xFF; } +static void report_internal_error(const char *msg, ...) + __attribute__((format(printf, 1, 2))); +static void report_internal_error(const char *msg, ...) { + fprintf(stderr, "KLEE_RUN_TEST_ERROR: "); + va_list ap; + va_start(ap, msg); + vfprintf(stderr, msg, ap); + va_end(ap); + fprintf(stderr, "\n"); + char *testErrorsNonFatal = getenv("KLEE_RUN_TEST_ERRORS_NON_FATAL"); + if (testErrorsNonFatal) { + fprintf(stderr, "KLEE_RUN_TEST_ERROR: Forcing execution to continue\n"); + } else { + exit(1); + } +} + void klee_make_symbolic(void *array, size_t nbytes, const char *name) { static int rand_init = -1; @@ -80,16 +98,34 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) { } } - if (testPosition >= testData->numObjects) { - fprintf(stderr, "ERROR: out of inputs, using zero\n"); - memset(array, 0, nbytes); - } else { - KTestObject *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); + for (;; ++testPosition) { + if (testPosition >= testData->numObjects) { + report_internal_error("out of inputs. Will use zero if continuing."); + memset(array, 0, nbytes); + break; + } else { + KTestObject *o = &testData->objects[testPosition]; + if (strcmp("model_version", o->name) == 0 && + strcmp("model_version", name) != 0) { + // Skip over this KTestObject because we've hit + // `model_version` which is from the POSIX runtime + // and the caller didn't ask for it. + continue; + } + if (strcmp(name, o->name) != 0) { + report_internal_error( + "object name mismatch. Requesting \"%s\" but returning \"%s\"", + name, o->name); + } + memcpy(array, o->bytes, nbytes < o->numBytes ? nbytes : o->numBytes); + if (nbytes != o->numBytes) { + report_internal_error("object sizes differ. Expected %zu but got %u", + nbytes, o->numBytes); + if (o->numBytes < nbytes) + memset((char *)array + o->numBytes, 0, nbytes - o->numBytes); + } + ++testPosition; + break; } } } @@ -102,14 +138,13 @@ uintptr_t klee_choose(uintptr_t n) { uintptr_t x; klee_make_symbolic(&x, sizeof x, "klee_choose"); if(x >= n) - fprintf(stderr, "ERROR: max = %ld, got = %ld\n", n, x); - assert(x < n); + report_internal_error("klee_choose failure. max = %ld, got = %ld\n", n, x); return x; } void klee_assume(uintptr_t x) { if (!x) { - fprintf(stderr, "ERROR: invalid klee_assume\n"); + report_internal_error("invalid klee_assume"); } } @@ -131,10 +166,8 @@ int klee_range(int begin, int end, const char* name) { int x; klee_make_symbolic(&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(); + report_internal_error("invalid klee_range(%u,%u,%s) value, got: %u\n", + begin, end, name, x); } return x; } diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 6d3ec926..0ae78faf 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -13,6 +13,8 @@ set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}") # is shared by both build systems. set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include") set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include") +set(NATIVE_CC "${CMAKE_C_COMPILER} -I ${CMAKE_SOURCE_DIR}/include") +set(NATIVE_CXX "${CMAKE_CXX_COMPILER} -I ${CMAKE_SOURCE_DIR}/include") set(TARGET_TRIPLE "${TARGET_TRIPLE}") if (ENABLE_KLEE_UCLIBC) set(ENABLE_UCLIBC 1) @@ -105,6 +107,20 @@ add_subdirectory(Concrete) ############################################################################### # Configure lit test suite ############################################################################### + +# Find path to libkleeRuntest target for `lit.site.cfg`. +# FIXME: This is not the right way to get the location of the target we have to +# set CMP0026 to old. +# This will likely break if using a multi-configuration generator. +if (POLICY CMP0026) + # HACK: Allow reading `LOCATION` property. + cmake_policy(SET CMP0026 OLD) +endif() +get_property(LIB_KLEE_RUN_TEST_PATH + TARGET kleeRuntest + PROPERTY LOCATION +) + configure_file(lit.site.cfg.in ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg @ONLY @@ -112,7 +128,7 @@ configure_file(lit.site.cfg.in add_custom_target(integrationtests COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}" - DEPENDS klee kleaver + DEPENDS klee kleaver kleeRuntest COMMENT "Running integration tests" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) diff --git a/test/Makefile b/test/Makefile index 0b176769..ed7ba197 100644 --- a/test/Makefile +++ b/test/Makefile @@ -84,4 +84,7 @@ lit.site.cfg: lit.site.cfg.in -e "s#@HAVE_SELINUX@#$(HAVE_SELINUX)#g" \ -e "s#@ENABLE_STP@#$(ENABLE_STP)#g" \ -e "s#@ENABLE_Z3@#$(ENABLE_Z3)#g" \ + -e "s#@NATIVE_CC@#$(CC) -I$(PROJ_SRC_ROOT)/include#g" \ + -e "s#@NATIVE_CXX@#$(CXX) -I$(PROJ_SRC_ROOT)/include#g" \ + -e "s#@LIB_KLEE_RUN_TEST_PATH@#$(SharedLibDir)/$(SharedPrefix)kleeRuntest$(SHLIBEXT)#g" \ $(PROJ_SRC_DIR)/lit.site.cfg.in > $@ diff --git a/test/Replay/libkleeruntest/replay_invalid_klee_assume.c b/test/Replay/libkleeruntest/replay_invalid_klee_assume.c new file mode 100644 index 00000000..12ac006e --- /dev/null +++ b/test/Replay/libkleeruntest/replay_invalid_klee_assume.c @@ -0,0 +1,44 @@ +// RUN: %llvmgcc -DASSUME_VALUE=1 %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: test ! -f %t.klee-out/test000002.ktest + +// Now try to replay with libkleeRuntest but build the binary to use a different +// value for the `klee_assume()` call. +// RUN: %cc -DASSUME_VALUE=32 -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner + +// Check that the default is to exit with an error +// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s + +// Check that setting `KLEE_RUN_TEST_ERRORS_NON_FATAL` will not exit with an error +// and will continue executing. +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest KLEE_RUN_TEST_ERRORS_NON_FATAL=1 %t_runner 2>&1 | FileCheck %s + +#include "klee/klee.h" +#include <stdint.h> +#include <stdio.h> + +#ifndef ASSUME_VALUE +#error ASSUME_VALUE must be defined +#endif + + +int main(int argc, char** argv) { + int x = 54; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x == ASSUME_VALUE); + +#ifdef PRINT_VALUE + printf("x=%d\n", x); +#endif + + return 0; +} +// CHECK: KLEE_RUN_TEST_ERROR: invalid klee_assume +// CHECK: KLEE_RUN_TEST_ERROR: Forcing execution to continue +// CHECK: x=1 + +// CHECK_FATAL: KLEE_RUN_TEST_ERROR: invalid klee_assume +// CHECK_FATAL-NOT: x=1 + diff --git a/test/Replay/libkleeruntest/replay_invalid_klee_choose.c b/test/Replay/libkleeruntest/replay_invalid_klee_choose.c new file mode 100644 index 00000000..62f514bf --- /dev/null +++ b/test/Replay/libkleeruntest/replay_invalid_klee_choose.c @@ -0,0 +1,45 @@ +// RUN: %llvmgcc -DBOUND_VALUE=32 -DFORCE_VALUE=20 %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=klee --search=dfs %t.bc +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: test ! -f %t.klee-out/test000002.ktest + +// Now try to replay with libkleeRuntest but build the binary to use a different +// bound for `klee_choose()`. +// RUN: %cc -DBOUND_VALUE=2 -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner + +// Check that the default is to exit with an error +// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s + +// Check that setting `KLEE_RUN_TEST_ERRORS_NON_FATAL` will not exit with an error +// and will continue executing. +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest KLEE_RUN_TEST_ERRORS_NON_FATAL=1 %t_runner 2>&1 | FileCheck %s + +#include "klee/klee.h" +#include <stdint.h> +#include <stdio.h> + +#ifndef BOUND_VALUE +#error BOUND_VALUE must be defined +#endif + + +int main(int argc, char** argv) { + int x = klee_choose(BOUND_VALUE); +#ifdef FORCE_VALUE + klee_assume(x == FORCE_VALUE); +#endif + +#ifdef PRINT_VALUE + printf("x=%d\n", x); +#endif + + return 0; +} +// CHECK: KLEE_RUN_TEST_ERROR: klee_choose failure. max = 2, got = 20 +// CHECK: KLEE_RUN_TEST_ERROR: Forcing execution to continue +// CHECK: x=20 + +// CHECK_FATAL: KLEE_RUN_TEST_ERROR: klee_choose failure. max = 2, got = 20 +// CHECK_FATAL-NOT: x=20 + diff --git a/test/Replay/libkleeruntest/replay_invalid_klee_range.c b/test/Replay/libkleeruntest/replay_invalid_klee_range.c new file mode 100644 index 00000000..c7d62027 --- /dev/null +++ b/test/Replay/libkleeruntest/replay_invalid_klee_range.c @@ -0,0 +1,45 @@ +// RUN: %llvmgcc -DBOUND_VALUE=32 -DFORCE_VALUE=20 %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --libc=klee --search=dfs %t.bc +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: test ! -f %t.klee-out/test000002.ktest + +// Now try to replay with libkleeRuntest but build the binary to use a different +// bound for `klee_range()`. +// RUN: %cc -DBOUND_VALUE=2 -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner + +// Check that the default is to exit with an error +// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s + +// Check that setting `KLEE_RUN_TEST_ERRORS_NON_FATAL` will not exit with an error +// and will continue executing. +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest KLEE_RUN_TEST_ERRORS_NON_FATAL=1 %t_runner 2>&1 | FileCheck %s + +#include "klee/klee.h" +#include <stdint.h> +#include <stdio.h> + +#ifndef BOUND_VALUE +#error BOUND_VALUE must be defined +#endif + + +int main(int argc, char** argv) { + int x = klee_range(0, BOUND_VALUE, "x"); +#ifdef FORCE_VALUE + klee_assume(x == FORCE_VALUE); +#endif + +#ifdef PRINT_VALUE + printf("x=%d\n", x); +#endif + + return 0; +} +// CHECK: KLEE_RUN_TEST_ERROR: invalid klee_range(0,2,x) value, got: 20 +// CHECK: KLEE_RUN_TEST_ERROR: Forcing execution to continue +// CHECK: x=20 + +// CHECK_FATAL: KLEE_RUN_TEST_ERROR: invalid klee_range(0,2,x) value, got: 20 +// CHECK_FATAL-NOT: x=20 + diff --git a/test/Replay/libkleeruntest/replay_invalid_num_objects.c b/test/Replay/libkleeruntest/replay_invalid_num_objects.c new file mode 100644 index 00000000..43bc4867 --- /dev/null +++ b/test/Replay/libkleeruntest/replay_invalid_num_objects.c @@ -0,0 +1,39 @@ +// Compile program that only makes one klee_make_symbolic() call +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc +// RUN: test -f %t.klee-out/test000001.ktest + +// Now try to replay with libkleeRuntest but build the binary so it +// makes two calls to klee_make_symbolic. +// RUN: %cc -DEXTRA_MAKE_SYMBOLIC %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner + +// Check that the default is to exit with an error +// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s + +// Check that setting `KLEE_RUN_TEST_ERRORS_NON_FATAL` will not exit with an error +// and will continue executing. +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest KLEE_RUN_TEST_ERRORS_NON_FATAL=1 %t_runner 2>&1 | FileCheck %s + +#include "klee/klee.h" +#include <stdio.h> + +int main(int argc, char** argv) { + int x = 0; + klee_make_symbolic(&x, sizeof(x), "x"); + +#ifdef EXTRA_MAKE_SYMBOLIC + int y = 1; + klee_make_symbolic(&y, sizeof(y), "x"); + klee_assume(y == 0); + fprintf(stderr, "y is \"%d\"\n", y); +#endif + return 0; +} +// CHECK: KLEE_RUN_TEST_ERROR: out of inputs +// CHECK: KLEE_RUN_TEST_ERROR: Forcing execution to continue +// CHECK: y is "0" + +// CHECK_FATAL: KLEE_RUN_TEST_ERROR: out of inputs +// CHECK_FATAL-NOT: y is "0" + diff --git a/test/Replay/libkleeruntest/replay_invalid_object_names.c b/test/Replay/libkleeruntest/replay_invalid_object_names.c new file mode 100644 index 00000000..9c75bebc --- /dev/null +++ b/test/Replay/libkleeruntest/replay_invalid_object_names.c @@ -0,0 +1,45 @@ +// RUN: %llvmgcc -DOBJ_NAME=simple_name %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc +// RUN: test -f %t.klee-out/test000001.ktest + +// Now try to replay with libkleeRuntest but build the binary to use a different +// object name +// RUN: %cc -DOBJ_NAME=wrong_name -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner + +// Check that the default is to exit with an error +// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s + +// Check that setting `KLEE_RUN_TEST_ERRORS_NON_FATAL` will not exit with an error +// and will continue executing. +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest KLEE_RUN_TEST_ERRORS_NON_FATAL=1 %t_runner 2>&1 | FileCheck %s + +#include "klee/klee.h" +#include <stdio.h> + +#ifndef OBJ_NAME +#error OBJ_NAME must be defined +#endif + +#define STRINGIFY(X) #X +#define XSTRINGIFY(X) STRINGIFY(X) + + +int main(int argc, char** argv) { + int x = 1; + klee_make_symbolic(&x, sizeof(x), XSTRINGIFY(OBJ_NAME)); + klee_assume(x == 0); + +#ifdef PRINT_VALUE + printf("x=%d\n", x); +#endif + + return 0; +} +// CHECK: KLEE_RUN_TEST_ERROR: object name mismatch. Requesting "wrong_name" but returning "simple_name" +// CHECK: KLEE_RUN_TEST_ERROR: Forcing execution to continue +// CHECK: x=0 + +// CHECK_FATAL: KLEE_RUN_TEST_ERROR: object name mismatch. Requesting "wrong_name" but returning "simple_name" +// CHECK_FATAL-NOT: x=0 + diff --git a/test/Replay/libkleeruntest/replay_invalid_object_size.c b/test/Replay/libkleeruntest/replay_invalid_object_size.c new file mode 100644 index 00000000..a1513ef9 --- /dev/null +++ b/test/Replay/libkleeruntest/replay_invalid_object_size.c @@ -0,0 +1,43 @@ +// RUN: %llvmgcc -DINT_TYPE=uint8_t %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: test ! -f %t.klee-out/test000002.ktest + +// Now try to replay with libkleeRuntest but build the binary to use a different +// size for variable `x`. +// RUN: %cc -DINT_TYPE=uint32_t -DPRINT_VALUE %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner + +// Check that the default is to exit with an error +// RUN: not env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner 2>&1 | FileCheck -check-prefix=CHECK_FATAL %s + +// Check that setting `KLEE_RUN_TEST_ERRORS_NON_FATAL` will not exit with an error +// and will continue executing. +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest KLEE_RUN_TEST_ERRORS_NON_FATAL=1 %t_runner 2>&1 | FileCheck %s +#include "klee/klee.h" +#include <stdint.h> +#include <stdio.h> + +#ifndef INT_TYPE +#error INT_TYPE must be defined +#endif + + +int main(int argc, char** argv) { + INT_TYPE x = 1; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x == 0); + +#ifdef PRINT_VALUE + printf("x=%d\n", x); +#endif + + return 0; +} +// CHECK: KLEE_RUN_TEST_ERROR: object sizes differ. Expected 4 but got 1 +// CHECK: KLEE_RUN_TEST_ERROR: Forcing execution to continue +// CHECK: x=0 + +// CHECK_FATAL: KLEE_RUN_TEST_ERROR: object sizes differ. Expected 4 but got 1 +// CHECK_FATAL-NOT: x=0 + diff --git a/test/Replay/libkleeruntest/replay_posix_runtime.c b/test/Replay/libkleeruntest/replay_posix_runtime.c new file mode 100644 index 00000000..70d8a1d9 --- /dev/null +++ b/test/Replay/libkleeruntest/replay_posix_runtime.c @@ -0,0 +1,35 @@ +// REQUIRES: posix-runtime +// FIXME: We need to fix a bug in libkleeRuntest +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --posix-runtime --search=dfs %t.bc +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: test -f %t.klee-out/test000002.ktest + +// Now try to replay with libkleeRuntest +// RUN: %cc %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: %ktest-tool %t.klee-out/test000001.ktest | FileCheck -check-prefix=CHECKMODEL %s +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner | FileCheck -check-prefix=TESTONE %s +// RUN: env KTEST_FILE=%t.klee-out/test000002.ktest %t_runner | FileCheck -check-prefix=TESTTWO %s + +#include "klee/klee.h" +#include <stdio.h> + +int main(int argc, char** argv) { + int x = 0; + klee_make_symbolic(&x, sizeof(x), "x"); + + if (x == 0) { + printf("x is 0\n"); + } else { + printf("x is not 0\n"); + } + return 0; +} + +// CHECKMODEL: num objects: 2 +// CHECKMODEL: object 0: name: {{b*}}'model_version' +// CHECKMODEL: object 1: name: {{b*}}'x' + +// TESTONE: x is not 0 +// TESTTWO: x is 0 diff --git a/test/Replay/libkleeruntest/replay_simple.c b/test/Replay/libkleeruntest/replay_simple.c new file mode 100644 index 00000000..cb9dfb85 --- /dev/null +++ b/test/Replay/libkleeruntest/replay_simple.c @@ -0,0 +1,28 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: test -f %t.klee-out/test000002.ktest + +// Now try to replay with libkleeRuntest +// RUN: %cc %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner | FileCheck -check-prefix=TESTONE %s +// RUN: env KTEST_FILE=%t.klee-out/test000002.ktest %t_runner | FileCheck -check-prefix=TESTTWO %s + +#include "klee/klee.h" +#include <stdio.h> + +int main(int argc, char** argv) { + int x = 0; + klee_make_symbolic(&x, sizeof(x), "x"); + + if (x == 0) { + printf("x is 0\n"); + } else { + printf("x is not 0\n"); + } + return 0; +} + +// TESTONE: x is not 0 +// TESTTWO: x is 0 diff --git a/test/Replay/libkleeruntest/replay_two_objects.c b/test/Replay/libkleeruntest/replay_two_objects.c new file mode 100644 index 00000000..f5be657c --- /dev/null +++ b/test/Replay/libkleeruntest/replay_two_objects.c @@ -0,0 +1,33 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc 2>&1 | FileCheck %s +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: test ! -f %t.klee-out/test000002.ktest + +// Now try to replay with libkleeRuntest +// RUN: %cc -DPRINT_VALUES %s %libkleeruntest -Wl,-rpath=%libkleeruntestdir -o %t_runner +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner | FileCheck -check-prefix=TESTONE %s + +#include "klee/klee.h" +#include <stdio.h> + +int main(int argc, char** argv) { + int x = 0; + int y = 0; + klee_make_symbolic(&x, sizeof(x), "x"); + klee_make_symbolic(&y, sizeof(x), "y"); + + klee_assume(x == 1); + klee_assume(y == 128); + +#ifdef PRINT_VALUES + printf("x=%d\n", x); + printf("y=%d\n", y); +#endif + + return 0; +} +// CHECK: KLEE: done: completed paths = 1 + +// TESTONE: x=1 +// TESTONE: y=128 diff --git a/test/lit.cfg b/test/lit.cfg index 39d23fc5..31552882 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -76,7 +76,7 @@ if config.test_exec_root is None: # Add substitutions from lit.site.cfg -subs = [ 'llvmgcc', 'llvmgxx'] +subs = [ 'llvmgcc', 'llvmgxx', 'cc', 'cxx'] for name in subs: value = getattr(config, name, None) if value == None: @@ -90,6 +90,10 @@ config.substitutions.append( ('%llvmas', os.path.join(llvm_tools_dir, 'llvm-as') # Add a substitution for llvm-ar config.substitutions.append( ('%llvmar', os.path.join(llvm_tools_dir, 'llvm-ar')) ) +# Add a substition for libkleeruntest +config.substitutions.append( ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest)) ) +config.substitutions.append( ('%libkleeruntest', config.libkleeruntest) ) + # Get KLEE and Kleaver specific parameters passed on llvm-lit cmd line # e.g. llvm-lit --param klee_opts=--help try: @@ -107,7 +111,10 @@ if len(kleaver_extra_params) != 0: print("Passing extra Kleaver command line args: {0}".format(kleaver_extra_params)) # Set absolute paths and extra cmdline args for KLEE's tools -subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), ('%klee','klee', klee_extra_params) ] +subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), + ('%klee','klee', klee_extra_params), + ('%ktest-tool', 'ktest-tool', '') +] for s,basename,extra_args in subs: config.substitutions.append( ( s, "{0} {1}".format( os.path.join(klee_tools_dir, basename), extra_args ).strip() @@ -140,3 +147,7 @@ if config.enable_z3: config.available_features.add('z3') else: config.available_features.add('not-z3') + +# POSIX runtime feature +if config.enable_posix_runtime: + config.available_features.add('posix-runtime') diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in index 5aff44ab..e53b1327 100644 --- a/test/lit.site.cfg.in +++ b/test/lit.site.cfg.in @@ -14,6 +14,9 @@ config.llvm_version_minor = "@LLVM_VERSION_MINOR@" config.llvmgcc = "@LLVMCC@" config.llvmgxx = "@LLVMCXX@" +config.cc = "@NATIVE_CC@" +config.cxx = "@NATIVE_CXX@" + # Features config.enable_uclibc = True if @ENABLE_UCLIBC@ == 1 else False config.enable_posix_runtime = True if @ENABLE_POSIX_RUNTIME@ == 1 else False @@ -24,6 +27,9 @@ config.enable_z3 = True if @ENABLE_Z3@ == 1 else False # Current target config.target_triple = "@TARGET_TRIPLE@" +# Path to libkleeRuntest +config.libkleeruntest = "@LIB_KLEE_RUN_TEST_PATH@" + # Let the main config do the real work. try: lit |