Commit af44f383 authored by Per's avatar Per

painc

parent 7772df35
# 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");
```
#![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())
})
};
}
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);
}
#[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