cc updates

klee-examples/examples/cc_add.rs

+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    let u = ksymbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    // if u > 254 {
+    //     u
+    // } else {
+    //     u.wrapping_add(1)
+    // }
+    // // u.checked_add(1).unwrap_or(u)
+    u + 1
+}
+
+fn f2(u: u8) -> u8 {
+    // unsafe { unchecked_div( 100, u) }
+    100 / u
+}

klee-examples/examples/cc_contract.rs

+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+use klee::kassume;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    f1_check();
+    f2_check();
+    f2_f1_check();
+}
+
+// contract f1
+fn f1_pre(u: u8) -> bool {
+    true
+}
+
+fn f1_post(u: u8) -> bool {
+    u > 0
+}
+
+// check pre-post f1
+fn f1_check() {
+    let u = ksymbol!("u");
+    kassume(f1_pre(u));
+    let r = f1(u);
+    kassert!(f1_post(r));
+}
+
+fn f1(u: u8) -> u8 {
+    u.checked_add(1).unwrap_or(u)
+}
+
+// contract f2
+fn f2_pre(u: u8) -> bool {
+    u != 0
+}
+
+fn f2_post(u: u8) -> bool {
+    true
+}
+
+// check pre-post f2
+fn f2_check() {
+    let u = ksymbol!("u");
+    kassume(f2_pre(u));
+    let r = f2(u);
+    kassert!(f2_post(r));
+}
+
+fn f2(u: u8) -> u8 {
+    unsafe { unchecked_div(100, u) }
+}
+
+// check f2_f1 composition
+fn f2_f1_check() {
+    let u = ksymbol!("u");
+    kassume(f1_post(u));
+    kassert!(f2_pre(u));
+}

klee-examples/examples/cc_contract_err.rs

+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+use klee::kassume;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    f1_check();
+    f2_check();
+    f2_f1_check();
+}
+
+// contract f1
+fn f1_pre(u: u8) -> bool {
+    true
+}
+
+fn f1_post(u: u8) -> bool {
+    u > 0
+}
+
+// check pre-post f1
+fn f1_check() {
+    let u = ksymbol!("u");
+    kassume(f1_pre(u));
+    let r = f1(u);
+    kassert!(f1_post(r));
+}
+
+fn f1(u: u8) -> u8 {
+    u.wrapping_add(1)
+}
+
+// contract f2
+fn f2_pre(u: u8) -> bool {
+    u != 0
+}
+
+fn f2_post(u: u8) -> bool {
+    true
+}
+
+// check pre-post f2
+fn f2_check() {
+    let u = ksymbol!("u");
+    kassume(f2_pre(u));
+    let r = f2(u);
+    kassert!(f2_post(r));
+}
+
+fn f2(u: u8) -> u8 {
+    unsafe { unchecked_div(100, u) }
+}
+
+// check f2_f1 composition
+fn f2_f1_check() {
+    let u = ksymbol!("u");
+    kassume(f1_post(u));
+    kassert!(f2_pre(u));
+}

klee-examples/examples/cc_equivalence.rs

+#![no_std]
+
+#[macro_use]
+extern crate klee;
+use core::ops::Add;
+
+use core::ptr;
+
+fn main() {
+    let u = ksymbol!("u");
+
+    kassert!(f1(u) == f1b(u));
+}
+
+fn f1(u: u8) -> u8 {
+    if u < 255 {
+        u + 1
+    } else {
+        u
+    }
+}
+
+fn f1b(u: u8) -> u8 {
+    u.checked_add(1).unwrap_or(u)
+}

klee-examples/examples/cc_loop.rs

@@ -3,16 +3,20 @@
 
 #[macro_use]
 extern crate klee;
+use klee::kassume;
 
 use core::ptr;
 use core::intrinsics::unchecked_div;
 
 fn main() {
-    let u = symbol!("u");
+    let u = ksymbol!("u");
+    kassume(u < 10);
+    //kassert!(f1(u) == f1b(u));
+    assert!(f1(u) == f1b(u));
 
-    unsafe {
-        ptr::read_volatile(&f2(f1(u)));
-    }
+    // unsafe {
+    //     ptr::read_volatile(&f2(f1(u)));
+    // }
 }
 
 // add 1 wrapping
@@ -24,6 +28,10 @@ fn f1(u: u8) -> u8 {
     j
 }
 
+fn f1b(u: u8) -> u8 {
+    u
+}
+
 fn f2(u: u8) -> u8 {
     unsafe { unchecked_div(100, u) }
 }

klee-examples/examples/cc_native_add.rs

@@ -6,14 +6,13 @@ extern crate klee;
 use core::ptr;
 
 fn main() {
-    let u = symbol!("u");
+    let u = ksymbol!("u");
 
     unsafe {
         ptr::read_volatile(&f2(f1(u)));
     }
 }
 
-// add 1 wrapping
 fn f1(u: u8) -> u8 {
     u + 1
 }

klee-examples/examples/cc_saturating.rs

@@ -7,16 +7,15 @@ use core::ops::Add;
 use core::ptr;
 
 fn main() {
-    let u = symbol!("u");
+    let u = ksymbol!("u");
 
     unsafe {
         ptr::read_volatile(&f2(f1(u)));
     }
 }
 
-// add 1 saturating
+
 fn f1(u: u8) -> u8 {
-    //if u < 255 { u + 1 } else { u } 
     u.checked_add(1).unwrap_or(u)
 }
 

klee-examples/examples/cc_unchecked_div.rs

+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+use core::intrinsics::unchecked_div;
+
+fn main() {
+    let u = ksymbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+fn f1(u: u8) -> u8 {
+    u.wrapping_add(1)
+}
+
+fn f2(u: u8) -> u8 {
+    unsafe { unchecked_div(100, u) }
+}

klee-examples/examples/cc_wrapping.rs

@@ -8,18 +8,17 @@ use core::ptr;
 use core::intrinsics::unchecked_div;
 
 fn main() {
-    let u = symbol!("u");
+    let u = ksymbol!("u");
 
     unsafe {
         ptr::read_volatile(&f2(f1(u)));
     }
 }
 
-// add 1 wrapping
 fn f1(u: u8) -> u8 {
     u.wrapping_add(1)
 }
 
 fn f2(u: u8) -> u8 {
-    unsafe { unchecked_div( 100, u) }
+    100 / u
 }

klee/src/lib.rs

@@ -24,7 +24,7 @@ pub fn abort() -> ! {
     unsafe { ll::abort() }
 }
 
-pub fn assume(cond: bool) {
+pub fn kassume(cond: bool) {
     unsafe {
         ll::klee_assume(cond);
     }
@@ -32,7 +32,7 @@ pub fn assume(cond: bool) {
 
 #[doc(hidden)]
 #[inline]
-pub fn symbol<T>(name: &CStr) -> T {
+pub fn ksymbol<T>(name: &CStr) -> T {
     let mut t: T = unsafe { mem::uninitialized() };
     unsafe {
         ll::klee_make_symbolic(
@@ -45,9 +45,9 @@ pub fn symbol<T>(name: &CStr) -> T {
 }
 
 #[macro_export]
-macro_rules! symbol {
+macro_rules! ksymbol {
     ($name:expr) => {
-        $crate::symbol(unsafe {
+        $crate::ksymbol(unsafe {
             $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
         })
     }

rls1509755957780.log

+error: expected expression, found `+`
+  --> stdin:22:11
+   |
+22 |         j++;
+   |           ^
+