lib.rs

#![no_std]
#![feature(compiler_builtins_lib)]
#![feature(lang_items)]
#![feature(core_intrinsics)]

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;

#[doc(hidden)]
pub use cstr_core::CStr;

/// Aborts the path in KLEE mode, does nothing otherwise
#[macro_export]
macro_rules! kabort {
    () => {
        #[cfg(feature = "klee-analysis")]
        unsafe { $crate::ll::abort() };
    };
}

#[cfg(feature = "klee-analysis")]
pub fn kassume(cond: bool) {
    unsafe {
        ll::klee_assume(cond);
    }
}

#[cfg(not(feature = "klee-analysis"))]
pub fn kassume(_cond: bool) {}

#[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(),
        )
    }
}

#[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!();
            }
        }
    };
}