Write tests to test `libkleeRuntest`. The `replay_posix_runtime.c`

test is marked XFAIL because there is a bug in the implementation
of `libkleeRuntest`.

Quite a few changes had to be made to the lit configuration in
order to support these tests.

To run the tests I had to fix #480 for the autoconf/Makefile build
system otherwise the `libkleeRuntest` library would not be found
by the system linker at runtime.

7 files changed, 136 insertions, 3 deletions

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