From 07148eeb5ea4d1c6c51e6aa5a666811ef9f50b90 Mon Sep 17 00:00:00 2001 From: Alastair Reid Date: Thu, 30 Jul 2020 17:02:20 +0000 Subject: New intrinsic: klee_is_replay This instrinsic detects whether the program is being executed symbolically or concretely (i.e., using the libkleeRuntest library). The intended usage (illustrated in the test program) is to allow the test program to display the input values by invoking any libraries it wants to. This is especially valuable if you are constructing complex, structured values and for languages like Rust (or C++) that have rich libraries and print libraries. For example, you might pick a symbolic value N with the assumption "0 <= N < 10" and then pick N symbolic values and write them to an array. The resulting ktest file is a bit hard to understand compared with the output of the standard print function in Rust/C++. --- test/Replay/libkleeruntest/replay_detection.c | 33 +++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 test/Replay/libkleeruntest/replay_detection.c (limited to 'test') diff --git a/test/Replay/libkleeruntest/replay_detection.c b/test/Replay/libkleeruntest/replay_detection.c new file mode 100644 index 00000000..7516ecd1 --- /dev/null +++ b/test/Replay/libkleeruntest/replay_detection.c @@ -0,0 +1,33 @@ +// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t.bc +// +// There should be a unique solution +// 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 %s + +#include "klee/klee.h" +#include + +int main(int argc, char** argv) { + int x = 0; + klee_make_symbolic(&x, sizeof(x), "x"); + + if (klee_is_replay()) { // only print x on replay runs + printf("x = %d\n", x); + } + + // For the sake of testing, these constraints have a single solution + klee_assume(40 < x); + klee_assume(x < 43); + klee_assume((x & 1) == 0); + + return 0; +} + +// When replaying, it should print the concrete value it is running with +// CHECK: x = 42 -- cgit 1.4.1