consistency check wip

examples/assume.rs

@@ -8,19 +8,23 @@ extern crate panic_abort;
 
 #[no_mangle]
 fn main() {
-    let mut a: u32 = unsafe { core::mem::uninitialized() };
-    let mut b: u32 = unsafe { core::mem::uninitialized() };
+    let mut a: u32 = 0;
+    let mut b: u32 = 0;
 
     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 );
+    let mut c = 0;
+    if a > 10 {
+        c+= 1;
+    }
+    // klee::kassume(b > 0);
+    let v = a + b;
 
     unsafe {
         core::ptr::read_volatile(&a);
         core::ptr::read_volatile(&b);
+        core::ptr::read_volatile(&v);
+        core::ptr::read_volatile(&c);
     }
-    // klee::kassume(a - b > 0);
-    // klee::kassert!(a> b);
 }

examples/model4.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, cannot be symbolic (awaiting const eval)
+impl RegC {
+    pub fn read(&self) -> u32 {
+        let v = self.0.read(); // to get a symbolic value
+        klee::kassume(v > 0); // to ensure that the value is positive
+        unsafe {
+            OLD_STATE += v;
+            OLD_STATE
+        }
+    }
+
+    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");
+    unsafe {
+        reg_c.write(init); // to ensure that the initial value is symbolic
+    }
+
+    let t1 = reg_c.read();
+    let t2 = reg_c.read();
+    klee::kassert!(t2 > t1);
+}