diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000000000000000000000000000000000000..c2ff7179673f152f3b22c834cb91e8a54799e9c2 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,7 @@ +{ + "cSpell.ignoreWords": [ + "concat", + "core", + "cstr" + ] +} \ No newline at end of file diff --git a/Cargo.toml b/Cargo.toml index 087dec5234898c30d46b45ea60204d0fbeff3a19..994ee9fc33a6aba88f00f137a4c4ed842ea778d2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,11 +1,12 @@ [package] name = "klee-sys" -version = "0.1.0" +version = "0.2.0" authors = ["pln <Per Lindgren>"] edition = "2018" -[dependencies] -cstr_core = "0.1.2" +[dependencies.cstr_core] +version = "0.2.2" +default-features = false [features] inline-asm = [] diff --git a/README.md b/README.md index 889ab9a512314f6eee1f6963553f3c65cebef410..f9a5beaddfb408d8759df2f0e3aef9e922d29bb7 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,7 @@ Variables (or rather `memory objects`) can be made symbolic, through the KLEE C pub fn klee_make_symbolic( ptr: *mut core::ffi::c_void, // pointer to the data size: usize, // size (in bytes) - name: *const cstr_core::c_char, // pointer to zero-terminted C string + name: *const cstr_core::c_char, // pointer to zero-terminated C string ); } ``` @@ -24,13 +24,19 @@ pub fn klee_make_symbolic( The internal Rust abstraction, calls into the FFI binding. ``` Rust -fn klee_make_symbolic<T>( - t: &mut T, // reference to generic type - name: &'static CStr // reference to static CStr -) {...} +#[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, + ) + } +} ``` -However dealing with CStr is cumbersome in Rust user code so we provide a macro, `klee_make_symbolic!(&mut T, &str)`, that zero-termintes the `&str` and cast it to the appropriate type. +However dealing with CStr is cumbersome in Rust user code so we provide a macro, `klee_make_symbolic!(&mut T, &str)`, that zero-terminates the `&str` and cast it to the appropriate type. Example usage: diff --git a/src/lib.rs b/src/lib.rs index ddf1d7bce9e56a9e53d806620c0779d1f649e1ce..fcdcfce2097bb5b1468aae0dba39340ea3b5679c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -14,7 +14,7 @@ //! TODO: better documentation (as always) #![no_std] -#![cfg_attr(feature = "inline-asm", feature(asm))] +#![cfg_attr(feature = "inline-asm", feature(llvm_asm))] // re-exports for klee-analysis #[cfg(feature = "klee-analysis")] @@ -22,13 +22,13 @@ mod lib_klee_analysis; #[cfg(feature = "klee-analysis")] pub mod ll; // low level bindings #[cfg(feature = "klee-analysis")] -pub use lib_klee_analysis::*; // functions and macros +pub use lib_klee_analysis::*; // re-export functions and macros // re-exports for klee-replay #[cfg(feature = "klee-replay")] mod lib_klee_replay; #[cfg(feature = "klee-replay")] -pub use lib_klee_replay::*; // functions and macros +pub use lib_klee_replay::*; // re-export functions and macros #[cfg(all(not(feature = "klee-analysis"), not(feature = "klee-replay")))] compile_error!("feature required, either `klee-analysis` or `klee-replay`"); diff --git a/src/lib_klee_replay.rs b/src/lib_klee_replay.rs index be3b3e24d3de0d7f03629606fabcc99ae66393f5..71ee5e3821549ac36ad4ceaf95f196f33cab2b01 100644 --- a/src/lib_klee_replay.rs +++ b/src/lib_klee_replay.rs @@ -1,17 +1,6 @@ -use core::ffi::c_void; -use cstr_core::c_char; - -#[doc(hidden)] -pub use cstr_core::CStr; - #[cfg(not(feature = "inline-asm"))] compile_error!("klee-replay requires feature `inline-asm`"); -#[inline(always)] -fn klee_abort() -> ! { - panic!(); -} - /// suppress assumption #[inline(always)] pub fn klee_assume(_cond: bool) {} @@ -20,7 +9,7 @@ pub fn klee_assume(_cond: bool) {} pub fn klee_make_symbolic<T>(t: &mut T) { // force LLVM to consider data to be mutated unsafe { - asm!("bkpt #0" : /* output */: /* input */ "r"(t): /* clobber */ : "volatile") + llvm_asm!("bkpt #0" : /* output */: /* input */ "r"(t): /* clobber */ : "volatile") } } diff --git a/src/ll.rs b/src/ll.rs index ee2565a9ab12aad6768d35e5956a5604776b9e88..6926b02fc6d1ccf0d4a5f64fa354a179af61b70b 100644 --- a/src/ll.rs +++ b/src/ll.rs @@ -5,6 +5,6 @@ extern "C" { pub fn klee_make_symbolic( ptr: *mut core::ffi::c_void, // pointer to the data size: usize, // size (in bytes) - name: *const cstr_core::c_char, // pointer to zero-terminted C string + name: *const cstr_core::c_char, // pointer to zero-terminated C string ); }