From a201c66fd1c0a7fdae3408572ae0befc37616259 Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Mon, 13 Jan 2020 23:01:05 +0100
Subject: [PATCH] ktest
---
examples/f401_ktest.rs | 58 ++++++++++++++++++++++++------------------
1 file changed, 33 insertions(+), 25 deletions(-)
diff --git a/examples/f401_ktest.rs b/examples/f401_ktest.rs
index 54d5aad..9ea2d19 100644
--- a/examples/f401_ktest.rs
+++ b/examples/f401_ktest.rs
@@ -8,43 +8,51 @@ extern crate panic_halt;
use stm32f4::stm32f401 as stm32;
-use cortex_m::{asm, bkpt, iprintln};
+use cortex_m::{asm, bkpt};
use cortex_m_rt::entry;
-
+// // use klee_sys::klee_make_symbolic2;
+// // Mimic RTFM resources
+// static mut X: u32 = 54;
#[entry]
+#[inline(never)]
fn main() -> ! {
- let mut x: u32 = 54;
- // klee_make_symbolic(&mut x);
- // while x == 0 {}
- // // asm::bkpt();
- //
- //
- bkpt!(1);
- asm::nop();
- asm::nop();
-
- bkpt!(2);
- asm::nop();
-
- bkpt!();
+ let mut x = 54;
+
+ klee_make_symbolic(&mut x);
+
+ if x == 0 {
+ bkpt!();
+ }
+
loop {
asm::nop();
}
}
-#[inline(always)]
-fn klee_make_symbolic<T>(data: &mut T) {
- asm::bkpt();
- // unsafe { klee_bkpt(data as *mut T as *mut core::ffi::c_void) };
+#[inline(never)]
+pub fn klee_make_symbolic<T>(data: &mut T) {
+ // force llvm to consider data to be mutaded
+ unsafe {
+ asm!("bkpt #0" : /* output */: /* input */ "r"(data): /* clobber */ : "volatile")
+ }
}
-#[no_mangle]
-pub extern "C" fn klee_bkpt(data: *mut core::ffi::c_void) {
- //*data = 0;
- asm::bkpt();
-}
+// pub fn taint() {
+// unsafe {
+// X = 73;
+// }
+// }
+
+// #[no_mangle]
+// pub extern "C" fn klee_bkpt(data: *mut core::ffi::c_void) {
+// bkpt!();
+// }
// extern "C" {
// pub fn klee_bkpt(ptr: *mut core::ffi::c_void, // pointer to the data
// );
// }
+// cargo objdump --bin app --release -- -disassemble -no-show-raw-insn
+
+// unsafe { asm!("mov $0,R15" : "=r"(r) ::: "volatile") }
+// cargo objdump --example f401_ktest --release --features f4,inline-asm --target thumbv7em-none-eabihf -- -d
--
GitLab