From 02835397656fb497b5f607ceabdf0831dc710b7e Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Tue, 8 Dec 2020 14:55:16 +0100
Subject: [PATCH] fixed cstr_core dependency
---
.vscode/settings.json | 7 +++++++
Cargo.toml | 7 ++++---
README.md | 18 ++++++++++++------
src/lib.rs | 6 +++---
src/lib_klee_replay.rs | 13 +------------
src/ll.rs | 2 +-
6 files changed, 28 insertions(+), 25 deletions(-)
create mode 100644 .vscode/settings.json
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000..c2ff717
--- /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 087dec5..994ee9f 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 889ab9a..f9a5bea 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 ddf1d7b..fcdcfce 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 be3b3e2..71ee5e3 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 ee2565a..6926b02 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
);
}
--
GitLab