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++.

1 files changed, 6 insertions, 0 deletions

diff --git a/include/klee/klee.h b/include/klee/klee.h
index 99fe15c7..fafdd55f 100644
--- a/include/klee/klee.h
+++ b/include/klee/klee.h
@@ -103,6 +103,12 @@ extern "C" {
   unsigned klee_is_symbolic(uintptr_t n);
 
 
+  /* Return true if replaying a concrete test case using the libkleeRuntime library
+   * Return false if executing symbolically in KLEE.
+   */
+  unsigned klee_is_replay();
+
+
   /* The following intrinsics are primarily intended for internal use
      and may have peculiar semantics. */