more examples

Cargo.toml

 [package]
-name = "plcopen"
-version = "0.1.0"
-authors = ["Per Lindgren <per.lindgren@ltu.se>"]
-edition = "2018"
+name = "klee-examples"
+version = "0.2.0"
+authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.io>"]
 
 [dependencies]
 klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
+panic-abort = "0.3.1"
 
-[[bin]]
-name = "main"
-path = "src/main.rs"
+[dependencies.cortex-m]
+version = "0.6.0"
 
-[features]
-klee-analysis = ["klee/klee-analysis"]
+[patch.crates-io]
+vcell = { git = "https://github.com/perlindgren/vcell.git" }
+volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
+cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
+
+[dependencies.volatile-register]
+version = "0.3.0"
+
+[dependencies.stm32f413]
+version = "0.3.0"
+git = "https://gitlab.henriktjader.com/pln/stm32f413.git"
+branch = "klee-analysis" 
+optional = true
+
+[[examples]]
+name = "gpioa"
+path = "examples/gpioa.rs"
+#required-features = ["klee-device"] # seem to work only in [[bin]]
 
 [profile.dev]
 incremental = false
@@ -22,3 +37,7 @@ incremental = false
 debug = true
 panic = "abort"
 lto = true
+
+[features]
+klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis", "cortex-m/klee-analysis"]
+klee-device = ["stm32f413/klee-analysis"]

examples/assume.rs

+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+#[no_mangle]
+fn main() {
+    let mut a: u32 = unsafe { core::mem::uninitialized() };
+    let mut b: u32 = unsafe { core::mem::uninitialized() };
+
+    klee::ksymbol!(&mut a, "a");
+    klee::ksymbol!(&mut b, "b");
+
+    // klee::kassume(a > b && a - b > 0);
+    klee::kassume( ((a - b > 0) as u32 & (a - b > 0) as u32 ) == 1 );
+
+    unsafe {
+        core::ptr::read_volatile(&a);
+        core::ptr::read_volatile(&b);
+    }
+    // klee::kassume(a - b > 0);
+    // klee::kassert!(a> b);
+}

examples/concurrent.rs

+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+extern crate volatile_register;
+use volatile_register::{RO, RW, WO};
+
+#[no_mangle]
+fn main() {
+    let rw: RW<u32> = unsafe { core::mem::uninitialized() };
+    let ro: RO<u32> = unsafe { core::mem::uninitialized() };
+    let wo: WO<u32> = unsafe { core::mem::uninitialized() };
+
+    unsafe { wo.write(2) };
+
+    if rw.read() == 0 {
+        unsafe {
+            rw.write(0);
+        }
+        if rw.read() == 0 {
+            panic!();
+        }
+    }
+
+    if ro.read() == 0 {
+        if ro.read() == 0 {
+            panic!();
+        }
+    }
+}

examples/model.rs

+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+extern crate volatile_register;
+use volatile_register::RW;
+
+struct Device<'a> {
+    ptr: &'a RW<u32>,
+}
+
+// HW model.
+// The register holds values 0..31
+impl<'a> Device<'a> {
+    pub fn read(&self) -> u32 {
+        let v = self.ptr.read();
+        klee::kassume(v < 32);
+        v
+    }
+    pub unsafe fn write(&self, v: u32) {
+        klee::kassert!(v < 32);
+        let v = self.ptr.write(v);
+    }
+}
+
+#[no_mangle]
+fn main() {
+    let reg = unsafe { core::mem::uninitialized() };
+    let device = Device { ptr: &reg };
+
+    let v = device.read();
+    if v > 5 {
+        unsafe {
+            device.write(v - 1);
+        }
+        if device.read() == v - 1 {
+            panic!();
+        }
+    }
+}

examples/model2.rs

+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+extern crate volatile_register;
+use volatile_register::RW;
+
+// model RegA
+// values always in the range 0..31
+struct RegA(RW<u32>);
+
+impl RegA {
+    pub fn read(&self) -> u32 {
+        let v = self.0.read();
+        klee::kassume(v < 32);
+        v
+    }
+    pub unsafe fn write(&self, v: u32) {
+        klee::kassert!(v < 32);
+        let v = self.0.write(v);
+    }
+}
+
+// model RegB
+// values always increases
+struct RegB(RW<u32>);
+
+static mut STATE: u32 = 0; // reset value
+impl RegB {
+    pub fn read(&self) -> u32 {
+        unsafe {
+            STATE += 1;
+            STATE
+        }
+    }
+    pub unsafe fn write(&self, v: u32) {
+        STATE = v;
+    }
+}
+
+#[no_mangle]
+fn main() {
+    let reg_a: RegA = unsafe { core::mem::uninitialized() };
+    let reg_b: RegB = unsafe { core::mem::uninitialized() };
+
+    unsafe {
+        reg_b.write(0);
+    }
+
+    let t1 = reg_b.read();
+    let t2 = reg_b.read();
+
+    let diff = 100 / (t2 - t1);
+
+    klee::kassert!(t2 > t1);
+
+    let v = reg_a.read();
+    if v > 5 {
+        unsafe {
+            reg_a.write(v - 1);
+        }
+        if reg_a.read() == v - 1 {
+            panic!();
+        }
+    }
+}

examples/model3.rs

+// cargo klee --example registers --release
+
+#![no_std]
+#![no_main]
+
+extern crate klee;
+extern crate panic_abort;
+
+extern crate volatile_register;
+use volatile_register::RW;
+
+// model RegC
+// values always increases
+// but are non-deterministic
+struct RegC(RW<u32>);
+
+static mut OLD_STATE: u32 = 0; // reset value
+impl RegC {
+    pub fn read(&self) -> u32 {
+        let v = self.0.read();
+        unsafe {
+            // klee::kassume(v - 0xFFFF_FFFC > 0);
+            // klee::kassume(v - OLD_STATE > 0);
+            // klee::kassert!(v > OLD_STATE);
+            klee::kassume(v > OLD_STATE);
+
+            OLD_STATE = v;
+        }
+        v
+    }
+    pub unsafe fn write(&self, v: u32) {
+        OLD_STATE = v;
+    }
+}
+
+#[no_mangle]
+fn main() {
+    let reg_c: RegC = unsafe { core::mem::uninitialized() };
+    let mut init: u32 = unsafe { core::mem::uninitialized() };
+    klee::ksymbol!(&mut init, "init");
+    //klee::kassume(init < 0xFFFF_FFFC);
+    //init = 0xFFFF_FFFD;
+    unsafe {
+        reg_c.write(init);
+    }
+
+    let t1 = reg_c.read();
+    let t2 = reg_c.read();
+    // let t3 = reg_c.read();
+
+    // let diff = 100 / (t2 - t1);
+
+    klee::kassert!(t2 > t1);
+    //klee::kassert!(t3 > t2);
+    //klee::kassert!(t3 > t1);
+}