Commit d282cfbb authored by Per's avatar Per

works

parent af44f383
......@@ -8,31 +8,42 @@ LLVM KLEE performs symbolic execution of LLVM-IR programs. For each path KLEE wi
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!()`, any failing assertion will generate a concrete test.
As `assert!()`/`assert_eq!()` etc. expands to conditional `panic!()`, thus a failing assertion will be caught.
Variables (or rather memory locations) can be made symbolic, through the C API.
Variables (or rather `memory objects`) can be made symbolic, through the KLEE C API. We bind the KLEE API in the `ll` module.
``` Rust
pub fn klee_make_symbolic(
ptr: *mut core::ffi::c_void, // pointer do the data
size: usize, // size (in bytes)
name: *const i8 // pointer to zero-teriminted C string
);
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:
The internal Rust abstraction, calls into the FFI binding.
``` Rust
fn klee_make_symbolic<T>(
t: &mut T, // reference to generic type
name: &'static CStr // pointer to CString
name: &'static CStr // reference to static CStr
) {...}
```
However dealing with CStr is cumbersome in user code so we provide a macro, `klee_mk_symbol!(&mut T, &str)`, that zero-termintes the `&str`. You can use
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:
``` Rust
...
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.
#![no_std]
use core::ffi::c_void;
use cstr_core::c_char;
#[doc(hidden)]
pub use cstr_core::CStr;
......@@ -8,8 +10,7 @@ pub mod ll;
pub mod panic;
//#[inline(always)]
#[inline(never)]
#[inline(always)]
pub fn klee_abort() -> ! {
unsafe { ll::abort() };
}
......@@ -21,24 +22,42 @@ pub fn klee_assume(cond: bool) {
}
}
// #[inline(always)]
// pub fn klee_assert(cond: bool) {
// if !cond {
// klee_abort();
// }
// }
#[inline(always)]
fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) {
pub fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) {
unsafe {
ll::klee_make_symbolic(
t as *mut T as *mut c_void,
core::mem::size_of::<T>(),
name.as_ptr() as *const u8,
name.as_ptr() as *const c_char,
)
}
}
#[macro_export]
macro_rules! klee_abort {
() => {
unsafe { $crate::ll::abort() };
};
}
#[macro_export]
macro_rules! klee_assert {
($e:expr) => {{
if !$e {
unsafe { $crate::ll::abort() };
}
}};
}
#[macro_export]
macro_rules! klee_assert_eq {
($e1:expr, $e2:expr ) => {{
if !($e1 == $e2) {
unsafe { $crate::ll::abort() };
}
}};
}
#[macro_export]
macro_rules! klee_make_symbolic {
(&mut $id:expr, $name:expr) => {
......
extern "C" {
#[inline(always)]
pub fn abort() -> !;
#[inline(always)]
pub fn klee_assume(cond: bool);
#[inline(always)]
pub fn klee_make_symbolic(ptr: *mut core::ffi::c_void, size: usize, name: *const u8);
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
);
}
#[cfg(not(test))] // avoid warning duplicate lang-item
#[panic_handler]
#[inline(never)]
fn panic(_info: &core::panic::PanicInfo) -> ! {
// abort symbol caught by LLVM-KLEE
unsafe { crate::ll::abort() }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment