diff --git a/README.md b/README.md index 7c735b8c97513291da882eb1b9dd234e62babff9..e479a867c730f4924e734bbdb5ad13749170aa41 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,38 @@ # 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!()`, any failing assertion will generate a concrete test. + +Variables (or rather memory locations) can be made symbolic, through the C API. + +``` 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 +); +``` + +The internal Rust abstraction: + +``` Rust +fn klee_make_symbolic<T>( + t: &mut T, // reference to generic type + name: &'static CStr // pointer to CString +) {...} +``` + +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 + +``` Rust + ... + let mut a = 0; + klee_make_symbolic(&mut a, "a"); +``` diff --git a/src/lib.rs b/src/lib.rs index ae04d93f1fa259b3ff4ef694f1d2dbbfc96b7352..cdbb617cde7ea097ebea62b819b6d0409112ac2d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,88 +1,49 @@ #![no_std] -// use core::intrinsics; -// use core::panic::PanicInfo; - -// #[panic_handler] -// fn panic(_info: &PanicInfo) -> ! { -// unsafe { intrinsics::abort() } -// } - -// #[lang = "eh_personality"] -// extern "C" fn eh_personality() {} -// extern crate cstr_core; - -// // #[cfg(feature = "klee-analysis")] -// // mod lang_items; -// #[cfg(feature = "klee-analysis")] -// pub mod ll; - -// #[cfg(feature = "klee-analysis")] -// use core::ffi::c_void; +use core::ffi::c_void; +#[doc(hidden)] +pub use cstr_core::CStr; -// #[doc(hidden)] -// pub use cstr_core::CStr; +pub mod ll; -// /// Aborts the path in KLEE mode, does nothing otherwise -// #[macro_export] -// macro_rules! kabort { -// () => { -// #[cfg(feature = "klee-analysis")] -// unsafe { $crate::ll::abort() }; -// }; -// } +pub mod panic; -// #[cfg(feature = "klee-analysis")] -// pub fn kassume(cond: bool) { -// unsafe { -// ll::klee_assume(cond); -// } -// } +//#[inline(always)] +#[inline(never)] +pub fn klee_abort() -> ! { + unsafe { ll::abort() }; +} -// #[cfg(not(feature = "klee-analysis"))] -// pub fn kassume(_cond: bool) {} +#[inline(always)] +pub fn klee_assume(cond: bool) { + unsafe { + ll::klee_assume(cond); + } +} -// #[cfg(feature = "klee-analysis")] -// pub fn kmksymbol<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(), -// ) +// #[inline(always)] +// pub fn klee_assert(cond: bool) { +// if !cond { +// klee_abort(); // } // } -// #[cfg(not(feature = "klee-analysis"))] -// pub fn kmksymbol<T>(_t: &mut T, _name: &'static CStr) {} - -// #[macro_export] -// macro_rules! ksymbol { -// (&mut $id:expr, $name:expr) => { -// $crate::kmksymbol(unsafe { &mut $id }, unsafe { -// $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) -// }) -// }; -// } - -// /// If in KLEE mode, the assertion is made. -// /// Otherwise, this is does nothing. -// #[macro_export] -// macro_rules! kassert { -// ($e:expr) => { -// #[cfg(feature = "klee-analysis")] -// { -// if !$e { -// $crate::kabort!(); -// } -// } -// }; -// } - -use core::ffi::c_void; +#[inline(always)] +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, + ) + } +} -extern "C" { - pub fn abort() -> !; - pub fn klee_assume(cond: bool); - pub fn klee_make_symbolic(ptr: *mut c_void, size: usize, name: *const i8); +#[macro_export] +macro_rules! klee_make_symbolic { + (&mut $id:expr, $name:expr) => { + $crate::klee_make_symbolic(unsafe { &mut $id }, unsafe { + $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) + }) + }; } diff --git a/src/ll.rs b/src/ll.rs new file mode 100644 index 0000000000000000000000000000000000000000..98cadac3449006cbbb7fccdff1eef709360d0dc6 --- /dev/null +++ b/src/ll.rs @@ -0,0 +1,8 @@ +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); +} diff --git a/src/panic.rs b/src/panic.rs new file mode 100644 index 0000000000000000000000000000000000000000..a910203ce8a66911b73cd40a91cdc2acf4c2b578 --- /dev/null +++ b/src/panic.rs @@ -0,0 +1,7 @@ +#[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() } +}