diff options
| -rw-r--r-- | runtime/Runtest/Makefile | 11 | ||||
| -rw-r--r-- | test/CMakeLists.txt | 18 | ||||
| -rw-r--r-- | test/Makefile | 3 | ||||
| -rw-r--r-- | test/Replay/libkleeruntest/replay_posix_runtime.c | 36 | ||||
| -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 |
8 files changed, 147 insertions, 3 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/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_posix_runtime.c b/test/Replay/libkleeruntest/replay_posix_runtime.c new file mode 100644 index 00000000..57f97dd0 --- /dev/null +++ b/test/Replay/libkleeruntest/replay_posix_runtime.c @@ -0,0 +1,36 @@ +// REQUIRES: posix-runtime +// FIXME: We need to fix a bug in libkleeRuntest +// XFAIL: * +// 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 |