Skip to content
Snippets Groups Projects
Commit 3e49ed21 authored by Per's avatar Per
Browse files

refactoring

parent c8275a34
No related branches found
No related tags found
No related merge requests found
...@@ -6,3 +6,8 @@ edition = "2018" ...@@ -6,3 +6,8 @@ edition = "2018"
[dependencies] [dependencies]
cstr_core = "0.1.2" cstr_core = "0.1.2"
[features]
inline-asm = []
klee-analysis = []
klee-replay = []
#![no_std] //! Documentation:
//!
use core::ffi::c_void; //! ```
use cstr_core::c_char; //! cargo doc --features klee-analysis --open
//!
#[doc(hidden)] //! cargo doc --features klee-replay --features inline-asm --open
pub use cstr_core::CStr; //! ```
//!
pub mod ll; //! Notice that replay requires the `inline asm` feature.
//!
#[inline(always)] //! TODO: unfortunately it seems that attributes only can apply to a single item
fn klee_abort() -> ! { //! so the conditionals have to be repeated
unsafe { ll::abort() }; //!
} //! TODO: better documentation (as always)
#[inline(always)]
pub fn klee_assume(cond: bool) {
unsafe {
ll::klee_assume(cond);
}
}
#[inline(always)] #![no_std]
pub fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) { #![cfg_attr(feature = "inline-asm", feature(asm))]
unsafe {
ll::klee_make_symbolic( // re-exports for klee-analysis
t as *mut T as *mut c_void, #[cfg(feature = "klee-analysis")]
core::mem::size_of::<T>(), mod lib_klee_analysis;
name.as_ptr() as *const c_char, #[cfg(feature = "klee-analysis")]
) pub mod ll; // low level bindings
} #[cfg(feature = "klee-analysis")]
} pub use lib_klee_analysis::*; // functions and macros
/// terminates path (and generates unique test) // re-exports for klee-replay
#[macro_export] #[cfg(feature = "klee-replay")]
macro_rules! klee_abort { mod lib_klee_replay;
() => { #[cfg(feature = "klee-replay")]
unsafe { $crate::ll::abort() }; pub use lib_klee_replay::*; // functions and macros
};
}
/// conditionally terminates path (and generates unique test)
#[macro_export]
macro_rules! klee_assert {
($e:expr) => {{
if !$e {
unsafe { $crate::ll::abort() };
}
}};
}
/// condititonally terminates path (and generates unique test)
#[macro_export]
macro_rules! klee_assert_eq {
($e1:expr, $e2:expr ) => {{
if !($e1 == $e2) {
unsafe { $crate::ll::abort() };
}
}};
}
/// makes mutable reference symbolic associated to static string
#[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())
})
};
}
use core::ffi::c_void;
use cstr_core::c_char;
#[doc(hidden)]
pub use cstr_core::CStr;
#[inline(always)]
fn klee_abort() -> ! {
unsafe { crate::ll::abort() };
}
/// introduces assumption
#[inline(always)]
pub fn klee_assume(cond: bool) {
unsafe {
crate::ll::klee_assume(cond);
}
}
/// makes refence symbolic
#[inline(always)]
pub fn klee_make_symbolic<T>(t: &mut T, name: &'static CStr) {
unsafe {
crate::ll::klee_make_symbolic(
t as *mut T as *mut c_void,
core::mem::size_of::<T>(),
name.as_ptr() as *const c_char,
)
}
}
/// terminates path (and generates unique test)
#[macro_export]
macro_rules! klee_abort {
() => {
unsafe { $crate::ll::abort() };
};
}
/// conditionally terminates path (and generates unique test)
#[macro_export]
macro_rules! klee_assert {
($e:expr) => {{
if !$e {
unsafe { $crate::ll::abort() };
}
}};
}
/// condititonally terminates path (and generates unique test)
#[macro_export]
macro_rules! klee_assert_eq {
($e1:expr, $e2:expr ) => {{
if !($e1 == $e2) {
unsafe { $crate::ll::abort() };
}
}};
}
/// makes mutable reference symbolic associated to static string
#[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())
})
};
}
use core::ffi::c_void;
use cstr_core::c_char;
#[doc(hidden)]
pub use cstr_core::CStr;
#[inline(always)]
fn klee_abort() -> ! {
panic!();
}
/// suppress assumption
#[inline(always)]
pub fn klee_assume(_cond: bool) {}
#[inline(always)]
pub fn klee_make_symbolic<T>(t: &mut T) {
// force llvm to consider data to be mutaded
unsafe {
asm!("bkpt #0" : /* output */: /* input */ "r"(t): /* clobber */ : "volatile")
}
}
/// terminates path
#[macro_export]
macro_rules! klee_abort {
() => {
panic!()
};
}
/// condititonally terminates path
#[macro_export]
macro_rules! klee_assert {
($e:expr) => {
assert!($e)
};
}
/// condititonally terminates path
#[macro_export]
macro_rules! klee_assert_eq {
($e1:expr, $e2:expr ) => {
assert_eq!($e1, $e2)
};
}
/// makes mutable reference symbolic associated to static string
#[macro_export]
macro_rules! klee_make_symbolic {
(&mut $id:expr, $name:expr) => {
$crate::klee_make_symbolic(unsafe { &mut $id })
};
}
//! Low level bindings
extern "C" { extern "C" {
pub fn abort() -> !; pub fn abort() -> !;
pub fn klee_assume(cond: bool); pub fn klee_assume(cond: bool);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment