Skip to content
Snippets Groups Projects
Select Git revision
  • c0796c44abdc65427aae09177c01485a7800a7c5
  • master default protected
2 results

lib.rs

Blame
  • lib.rs 1.49 KiB
    #![no_std]
    #![feature(compiler_builtins_lib)]
    #![feature(lang_items)]
    #![feature(core_intrinsics)]
    
    extern crate cstr_core;
    
    mod lang_items;
    pub mod ll;
    pub mod mutex;
    
    use core::mem;
    
    use core::ffi::c_void;
    
    #[doc(hidden)]
    pub use cstr_core::CStr;
    
    #[inline(always)]
    pub fn abort() -> ! {
        unsafe { ll::abort() }
    }
    
    #[inline(always)]
    pub fn kassume(cond: bool) {
        unsafe {
            ll::klee_assume(cond);
        }
    }
    
    #[doc(hidden)]
    #[inline]
    pub fn ksymbol<T>(name: &CStr) -> T {
        let mut t: T = unsafe { mem::uninitialized() };
        unsafe {
            ll::klee_make_symbolic(
                &mut t as *mut T as *mut c_void,
                mem::size_of::<T>(),
                name.as_ptr(),
            )
        }
        t
    }
    
    pub fn kmksymbol<T>(t: &mut T, name: &CStr) {
        unsafe {
            ll::klee_make_symbolic(
                t as *mut T as *mut c_void,
                mem::size_of::<T>(),
                name.as_ptr(),
            )
        }
    }
    
    #[macro_export]
    macro_rules! ksymbol {
        ($name:expr) => {
            $crate::ksymbol(unsafe {
                $crate::CStr::from_bytes_with_nul_unchecked(
                    concat!($name, "\0").as_bytes(),
                )
            })
        };
        (&mut $id:expr, $name:expr) => {
            $crate::kmksymbol(unsafe { &mut $id }, unsafe {
                $crate::CStr::from_bytes_with_nul_unchecked(
                    concat!($name, "\0").as_bytes(),
                )
            })
        };
    }
    
    #[macro_export]
    macro_rules! kassert {
        ($e:expr) => {
            if !$e {
                unsafe { $crate::ll::abort() }
            }
        };
    }