klee-sys
Low-level bindings to LLVM-KLEE.
Design
LLVM KLEE performs symbolic execution of LLVM-IR programs. For each path KLEE will generate a concrete test.
A path is termintated either by executing to end or hitting the abort symbol. We bind the Rust panic_handler to the abort symbol, thus any panic!() will result in path termination (and consequitively a concrete test).
As assert!()/assert_eq!() etc. expands to conditional panic!(), thus a failing assertion will be caught.
Variables (or rather memory objects) can be made symbolic, through the KLEE C API. We bind the KLEE API in the ll module.
pub fn klee_make_symbolic(
ptr: *mut core::ffi::c_void, // pointer to the data
size: usize, // size (in bytes)
name: *const cstr_core::c_char, // pointer to zero-terminted C string
);
}The internal Rust abstraction, calls into the FFI binding.
fn klee_make_symbolic<T>(
t: &mut T, // reference to generic type
name: &'static CStr // reference to static CStr
) {...}However dealing with CStr is cumbersome in Rust user code so we provide a macro, klee_make_symbolic!(&mut T, &str), that zero-termintes the &str and cast it to the appropriate type.
Example usage:
...
let mut a = 0;
klee_make_symbolic(&mut a, "a");KLEE test case generation
LLVM KLEE strives to cover all feasible paths. When generating tests for errors encountered (paths to abort), KLEE will generate one test for each unique position in the source code that lead up to the abort. Code that emits a Rust panic!(), will all reach the same panic_handler (which calls into abort), and KLEE will detect the panic_handler as the source of the error, and consequently generate one such test. (Perhaps there is a way to force KLEE to generate one test per unique path leading up to the panic_handler, but we have not yet found it. Tech note: The panic implementation can unfortunately not be inlined as far as we have seen.)
As a consequence, you have to eleminate sources of panic!() one by one, which may be time consuming.
We provide a set of macros klee_abort, klee_assert and klee_assert_eq, that gets fully inlined, allowing KLEE to generate specific tests for each failing assertion.