diff --git a/klee-examples/examples/array.rs b/klee-examples/examples/array.rs
new file mode 100644
index 0000000000000000000000000000000000000000..4dbb026385d80a6155206bae4db276ded8da1282
--- /dev/null
+++ b/klee-examples/examples/array.rs
@@ -0,0 +1,23 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+#[no_mangle]
+fn main() -> u32 {
+ let mut u: [u32; 32] = unsafe { core::mem::uninitialized() };
+ ksymbol!(&mut u, "u");
+
+ let mut z = 0;
+ unsafe {
+ for (i, x) in u.iter().enumerate() {
+ if ptr::read_volatile(x) == 0 {
+ z = i;
+ }
+ }
+ }
+ return z as u32;
+}
diff --git a/klee-examples/examples/cc_add.rs b/klee-examples/examples/cc_add.rs
new file mode 100644
index 0000000000000000000000000000000000000000..b1a0b30c89bc9b84193dc0ea399fb700a5298a94
--- /dev/null
+++ b/klee-examples/examples/cc_add.rs
@@ -0,0 +1,34 @@
+#![no_std]
+#![no_main]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::intrinsics::unchecked_div;
+use core::ptr;
+
+#[no_mangle]
+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
+}
diff --git a/klee-examples/examples/cc_codegen.rs b/klee-examples/examples/cc_codegen.rs
new file mode 100644
index 0000000000000000000000000000000000000000..00ee4d9bd34657ac3c8fd313f1bfe29776edc970
--- /dev/null
+++ b/klee-examples/examples/cc_codegen.rs
@@ -0,0 +1,60 @@
+#![no_std]
+#![no_main]
+#![allow(dead_code)]
+
+#[macro_use]
+extern crate klee;
+use core::ptr;
+
+//# FUNCTION codgen(): UNSIGNED INTEGER;
+// # LOCAL SIGNED INTEGER n;
+// # LOCAL UNSIGNED INTEGER x, y;
+// # BEGIN
+// # n := [count the number of 0's in word "seed"];
+// # x := [rotate "seed" left by 30 bits];
+// # y := [shift "seed" right-ARITHMETIC by 6 bits];
+// # seed := x XOR y XOR n;
+// # RETURN( seed XOR 0x464b713e );
+// # END;
+// #
+// # hint: if "seed" is initialized to 0x3e944b9f,
+// # the first five calls will generate these values:
+// # 0x891432f9, 0x4aa1dccc, 0xc54270fa, 0x9885155f, 0xce83d1b8, ...
+// # your code is to be written farther down (see comment below).
+
+fn codgen(seed: &mut u32) -> u32 {
+ let mut n: i32 = 32;
+ let lseed: u32 = seed.clone(); // copy value of seed
+ let mut s: u32 = lseed;
+ let x: u32;
+ let y: u32;
+
+ //n = [count the number of 0's in word "seed"];
+ while s != 0 {
+ if s & 1u32 == 1u32 {
+ n -= 1;
+ }
+ s >>= 1; // >> is logic shift
+ }
+
+ // x := [rotate "seed" left by 30 bits];
+ x = lseed << 30 | ((lseed >> 2) & ((1 << (30 + 1)) - 1));
+
+ // y := [shift "seed" right-ARITHMETIC by 6 bits];
+ y = ((lseed as i32) >> 6) as u32;
+
+ // seed := x XOR y XOR n;
+ *seed = x ^ y ^ (n as u32);
+
+ // RETURN( seed XOR 0x464b713e );
+ (*seed) ^ 0x464b713e
+}
+
+#[no_mangle]
+fn main() {
+ // test that codgen works
+ let mut seed = ksymbol!("seed");
+ unsafe {
+ ptr::read_volatile(&codgen(&mut seed));
+ }
+}
diff --git a/klee-examples/examples/cc_codegen_eq.rs b/klee-examples/examples/cc_codegen_eq.rs
new file mode 100644
index 0000000000000000000000000000000000000000..3bfb13fcdf686385ec6fe2d1c7e1fa0460be3061
--- /dev/null
+++ b/klee-examples/examples/cc_codegen_eq.rs
@@ -0,0 +1,79 @@
+#![no_std]
+#![allow(dead_code)]
+
+#[macro_use]
+extern crate klee;
+use core::ptr;
+
+//# FUNCTION codgen(): UNSIGNED INTEGER;
+// # LOCAL SIGNED INTEGER n;
+// # LOCAL UNSIGNED INTEGER x, y;
+// # BEGIN
+// # n := [count the number of 0's in word "seed"];
+// # x := [rotate "seed" left by 30 bits];
+// # y := [shift "seed" right-ARITHMETIC by 6 bits];
+// # seed := x XOR y XOR n;
+// # RETURN( seed XOR 0x464b713e );
+// # END;
+// #
+// # hint: if "seed" is initialized to 0x3e944b9f,
+// # the first five calls will generate these values:
+// # 0x891432f9, 0x4aa1dccc, 0xc54270fa, 0x9885155f, 0xce83d1b8, ...
+// # your code is to be written farther down (see comment below).
+
+fn codgen(seed: &mut u32) -> u32 {
+ let mut n: i32 = 32;
+ let lseed: u32 = seed.clone(); // copy value of seed
+ let mut s: u32 = lseed;
+ let x: u32;
+ let y: u32;
+
+ //n = [count the number of 0's in word "seed"];
+ while s != 0 {
+ if s & 1u32 == 1u32 {
+ n -= 1;
+ }
+ s >>= 1; // >> is logic shift
+ }
+
+ // x := [rotate "seed" left by 30 bits];
+ x = lseed << 30 | ((lseed >> 2) & ((1 << (30 + 1)) - 1));
+
+ // y := [shift "seed" right-ARITHMETIC by 6 bits];
+ y = ((lseed as i32) >> 6) as u32;
+
+ // seed := x XOR y XOR n;
+ *seed = x ^ y ^ (n as u32);
+
+ // RETURN( seed XOR 0x464b713e );
+ (*seed) ^ 0x464b713e
+}
+
+fn codgen2(seed: &mut u32) -> u32 {
+ let mut n: i32 = 32;
+ let mut s: u32 = *seed;
+ let x: u32;
+ let y: u32;
+
+ while s != 0 {
+ if s & 1u32 == 1u32 {
+ n -= 1;
+ }
+ s >>= 1;
+ }
+
+ x = *seed << 30 | ((*seed >> 2) & ((1 << (30 + 1)) - 1));
+ y = ((*seed as i32) >> 6) as u32;
+ *seed = x ^ y ^ (n as u32);
+ *seed ^ 0x464b713e
+}
+
+fn main() {
+ // test that codgen works
+ let mut seed = ksymbol!("seed");
+ let mut seed_copy = seed;
+ kassert!(codgen(&mut seed) == codgen2(&mut seed_copy));
+ // unsafe {
+ // ptr::read_volatile(&codgen(&mut seed));
+ // }
+}
diff --git a/klee-examples/examples/cc_contract.rs_no b/klee-examples/examples/cc_contract.rs_no
new file mode 100644
index 0000000000000000000000000000000000000000..8e1d816be107e41d8c168c529ea85732583ff70c
--- /dev/null
+++ b/klee-examples/examples/cc_contract.rs_no
@@ -0,0 +1,64 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+use klee::kassume;
+
+use core::intrinsics::unchecked_div;
+use core::ptr;
+
+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));
+}
diff --git a/klee-examples/examples/cc_contract_err.rs b/klee-examples/examples/cc_contract_err.rs
new file mode 100644
index 0000000000000000000000000000000000000000..35321844668a6e08d2bda214dc63b188a45cd4ed
--- /dev/null
+++ b/klee-examples/examples/cc_contract_err.rs
@@ -0,0 +1,64 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+use klee::kassume;
+
+use core::intrinsics::unchecked_div;
+use core::ptr;
+
+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));
+}
diff --git a/klee-examples/examples/cc_equivalence.rs b/klee-examples/examples/cc_equivalence.rs
new file mode 100644
index 0000000000000000000000000000000000000000..683b0451382d5e3b49eb92e98a587fe8246bcf33
--- /dev/null
+++ b/klee-examples/examples/cc_equivalence.rs
@@ -0,0 +1,25 @@
+#![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)
+}
diff --git a/klee-examples/examples/cc_lab4.rs_no b/klee-examples/examples/cc_lab4.rs_no
new file mode 100644
index 0000000000000000000000000000000000000000..c1d0ae022571b0d138ec41e8b500304f3075158a
--- /dev/null
+++ b/klee-examples/examples/cc_lab4.rs_no
@@ -0,0 +1,276 @@
+//! Prints "Hello, world!" on the OpenOCD console using semihosting
+//!
+//! ---
+
+#![no_std]
+#![allow(dead_code)]
+
+#[macro_use]
+extern crate klee;
+use core::cmp;
+
+static mut PLAIN: [u8; 132] = [0; 132];
+
+static ABC: [u32; 4] = [0x9fdd9158, 0x85715808, 0xac73323a, 0];
+static CODED: [u32; 132] = [
+ 0x015e7a47,
+ 0x2ef84ebb,
+ 0x177a8db4,
+ 0x1b722ff9,
+ 0x5dc7cff0,
+ 0x5dc9dea6,
+ 0x1da0c15a,
+ 0xe4c236a2,
+ 0x3d16b0d0,
+ 0x1f397842,
+ 0xaae0d2ba,
+ 0x11246674,
+ 0x0845317f,
+ 0xd5512dad,
+ 0xb6184977,
+ 0xd293a53e,
+ 0x7d9c2716,
+ 0xd917eae6,
+ 0xd8852384,
+ 0x286e46f9,
+ 0xce566029,
+ 0xcefe7daf,
+ 0x62d726d4,
+ 0x0dbaeb2d,
+ 0x95f57c60,
+ 0xed515141,
+ 0x29b77d0f,
+ 0x9f7b8d0c,
+ 0x45a8395a,
+ 0xfead2b72,
+ 0x883d434c,
+ 0xed8ddf60,
+ 0xe51e65e4,
+ 0x19bf6bb1,
+ 0xfeb505ec,
+ 0x662aa23c,
+ 0xf6827cf8,
+ 0xd1dc7a5c,
+ 0x4fa5b066,
+ 0x7ddd25a4,
+ 0xa8ba8e8a,
+ 0x72846227,
+ 0xf8f636fb,
+ 0x2b389a9c,
+ 0xe4038bf6,
+ 0x6e169877,
+ 0xad028132,
+ 0x84dbfe8c,
+ 0x243762ff,
+ 0x59c8f80c,
+ 0xb6e0db4b,
+ 0xedb8cab7,
+ 0xcd4b39f6,
+ 0xaf263741,
+ 0x18d9965f,
+ 0x1ab1f037,
+ 0x5b458792,
+ 0xc94d960d,
+ 0xd45cedea,
+ 0x2160aca3,
+ 0x93c77766,
+ 0x2d66e105,
+ 0x9ff74d4f,
+ 0x6dc22f21,
+ 0x6b03d689,
+ 0x5fc48de0,
+ 0x1138f000,
+ 0xccb58e57,
+ 0xf9c8e200,
+ 0x7ab26e3c,
+ 0xc61dcb3e,
+ 0x6aefccb0,
+ 0x7a452f05,
+ 0xa5cf0731,
+ 0xa249383f,
+ 0x628fe534,
+ 0xcad81710,
+ 0x7f616276,
+ 0x3ce18308,
+ 0xed4857ff,
+ 0xd1e5b1d1,
+ 0xc2e84dc2,
+ 0xaa003742,
+ 0xaf637488,
+ 0x831afc48,
+ 0x287a69a0,
+ 0x6e04546e,
+ 0x13dffa07,
+ 0x3232fb10,
+ 0xd69e2e09,
+ 0x355d8dc7,
+ 0xef902301,
+ 0x9a89ac15,
+ 0x967dc900,
+ 0x08dc2b1c,
+ 0x6b5be690,
+ 0x894b0e02,
+ 0xe26af9af,
+ 0xa6fd3b23,
+ 0xfcf213e5,
+ 0x85217608,
+ 0x7fd3be8b,
+ 0xa2e757fb,
+ 0x3717a341,
+ 0x85ee426d,
+ 0x394bb856,
+ 0x12ac98c3,
+ 0xec7d4ab5,
+ 0x721b6989,
+ 0x30e36360,
+ 0xaa018403,
+ 0x9ee61196,
+ 0xa8697adc,
+ 0x51e9d65a,
+ 0x11023594,
+ 0xc4c4b36b,
+ 0xda80bf7a,
+ 0xbd5a645e,
+ 0x18cea918,
+ 0xa723dda8,
+ 0x0126c05e,
+ 0x2962d48a,
+ 0xd5f7d312,
+ 0xb8947041,
+ 0x7c1e2e9a,
+ 0x945eeac3,
+ 0x7110fb1c,
+ 0xa7bc72cc,
+ 0xdf47dfbb,
+ 0x09a1c6c8,
+ 0xc2e41061,
+ 0,
+];
+
+//# FUNCTION codgen(): UNSIGNED INTEGER;
+// # LOCAL SIGNED INTEGER n;
+// # LOCAL UNSIGNED INTEGER x, y;
+// # BEGIN
+// # n := [count the number of 0's in word "seed"];
+// # x := [rotate "seed" left by 30 bits];
+// # y := [shift "seed" right-ARITHMETIC by 6 bits];
+// # seed := x XOR y XOR n;
+// # RETURN( seed XOR 0x464b713e );
+// # END;
+// #
+// # hint: if "seed" is initialized to 0x3e944b9f,
+// # the first five calls will generate these values:
+// # 0x891432f9, 0x4aa1dccc, 0xc54270fa, 0x9885155f, 0xce83d1b8, ...
+// # your code is to be written farther down (see comment below).
+//
+
+fn codgen(seed: &mut u32) -> u32 {
+ let mut n: i32 = 32;
+ let lseed: u32 = seed.clone(); // copy value of seed
+ let mut s: u32 = lseed;
+ let x: u32;
+ let y: u32;
+
+ //n = [count the number of 0's in word "seed"];
+ while s != 0 {
+ if s & 1u32 == 1u32 {
+ n -= 1;
+ }
+ s >>= 1; // >> is logic shift
+ }
+
+ // x := [rotate "seed" left by 30 bits];
+ x = lseed << 30 | ((lseed >> 2) & ((1 << (30 + 1)) - 1));
+
+ // y := [shift "seed" right-ARITHMETIC by 6 bits];
+ y = ((lseed as i32) >> 6) as u32;
+
+ // seed := x XOR y XOR n;
+ *seed = x ^ y ^ (n as u32);
+
+ // RETURN( seed XOR 0x464b713e );
+ (*seed) ^ 0x464b713e
+}
+
+//
+fn decode_org(wordarr: &[u32], bytearr: &mut [u8], seed: &mut u32) -> u32 {
+ let m: u32;
+ let mut r: u32;
+ let x: u32;
+ let y: u32;
+
+ x = !codgen(seed);
+ if wordarr[0] == 0 {
+ bytearr[0] = 0;
+ r = x;
+ } else {
+ y = decode(&wordarr[1..], &mut bytearr[1..], seed);
+ m = x.wrapping_sub(y).wrapping_sub(wordarr[0]);
+ bytearr[0] = (m >> 13) as u8;
+ r = (-(codgen(seed) as i32)) as u32;
+ r = x.wrapping_add(y)
+ .wrapping_add(m)
+ .wrapping_add(r)
+ .wrapping_add(5);
+ }
+ r
+}
+
+
+mod rnd {
+ use core::mem;
+ static mut I: usize = 0;
+ static RND: [u32; 132] = [0; 132]; // unsafe { mem::uninitialized() };
+ pub fn get() -> u32 {
+ unsafe {
+ let r = RND[I];
+ I += 1;
+ r
+ }
+ }
+ pub fn ksymbolic() {
+ unsafe {
+ make_symbolic(
+ &mut RND as *mut [u32; 132] as *mut c_void,
+ mem::size_of::<[u32; 132]>(),
+ "name".as_ptr(),
+ )
+ }
+ }
+}
+fn decode(wordarr: &[u32], bytearr: &mut [u8], seed: &mut u32) -> u32 {
+ let m: u32;
+ let mut r: u32;
+ let x: u32;
+ let y: u32;
+
+ //x = !codgen(seed);
+ //x = ksymbol!("x");
+ x = rnd::get();
+
+ if wordarr == [] {
+ bytearr[0] = 0;
+ r = x;
+ } else {
+ y = decode(&wordarr[1..], &mut bytearr[1..], seed);
+ m = x.wrapping_sub(y).wrapping_sub(wordarr[0]);
+ bytearr[0] = (m >> 13) as u8;
+ //let cg: u32 = ksymbol!("cg");
+ //let cg: u32 = codgen(seed);
+ let cg: u32 = rnd::get();
+ r = (-(cg as i32)) as u32;
+ r = x.wrapping_add(y)
+ .wrapping_add(m)
+ .wrapping_add(r)
+ .wrapping_add(5);
+ }
+ r
+}
+
+fn main() {
+ //let mut seed = 0x0e0657c1;
+ let mut seed = ksymbol!("seed");
+ rnd::ksymbolic();
+ let abc: [u32; 4] = ksymbol!("abc");
+ decode(&abc[..], unsafe { &mut PLAIN }, &mut seed);
+}
diff --git a/klee-examples/examples/cc_lab4_contract.rs b/klee-examples/examples/cc_lab4_contract.rs
new file mode 100644
index 0000000000000000000000000000000000000000..44da140ef4b306b7301e2014d82467bb70c33e91
--- /dev/null
+++ b/klee-examples/examples/cc_lab4_contract.rs
@@ -0,0 +1,160 @@
+#![no_std]
+#![no_main]
+#![allow(dead_code)]
+
+#[macro_use]
+extern crate klee;
+use core::cmp;
+
+static mut PLAIN: [u8; 132] = [0; 132];
+
+static ABC: [u32; 4] = [0x9fdd9158, 0x85715808, 0xac73323a, 0];
+static CODED: [u32; 132] = [
+ 0x015e7a47, 0x2ef84ebb, 0x177a8db4, 0x1b722ff9, 0x5dc7cff0, 0x5dc9dea6, 0x1da0c15a, 0xe4c236a2,
+ 0x3d16b0d0, 0x1f397842, 0xaae0d2ba, 0x11246674, 0x0845317f, 0xd5512dad, 0xb6184977, 0xd293a53e,
+ 0x7d9c2716, 0xd917eae6, 0xd8852384, 0x286e46f9, 0xce566029, 0xcefe7daf, 0x62d726d4, 0x0dbaeb2d,
+ 0x95f57c60, 0xed515141, 0x29b77d0f, 0x9f7b8d0c, 0x45a8395a, 0xfead2b72, 0x883d434c, 0xed8ddf60,
+ 0xe51e65e4, 0x19bf6bb1, 0xfeb505ec, 0x662aa23c, 0xf6827cf8, 0xd1dc7a5c, 0x4fa5b066, 0x7ddd25a4,
+ 0xa8ba8e8a, 0x72846227, 0xf8f636fb, 0x2b389a9c, 0xe4038bf6, 0x6e169877, 0xad028132, 0x84dbfe8c,
+ 0x243762ff, 0x59c8f80c, 0xb6e0db4b, 0xedb8cab7, 0xcd4b39f6, 0xaf263741, 0x18d9965f, 0x1ab1f037,
+ 0x5b458792, 0xc94d960d, 0xd45cedea, 0x2160aca3, 0x93c77766, 0x2d66e105, 0x9ff74d4f, 0x6dc22f21,
+ 0x6b03d689, 0x5fc48de0, 0x1138f000, 0xccb58e57, 0xf9c8e200, 0x7ab26e3c, 0xc61dcb3e, 0x6aefccb0,
+ 0x7a452f05, 0xa5cf0731, 0xa249383f, 0x628fe534, 0xcad81710, 0x7f616276, 0x3ce18308, 0xed4857ff,
+ 0xd1e5b1d1, 0xc2e84dc2, 0xaa003742, 0xaf637488, 0x831afc48, 0x287a69a0, 0x6e04546e, 0x13dffa07,
+ 0x3232fb10, 0xd69e2e09, 0x355d8dc7, 0xef902301, 0x9a89ac15, 0x967dc900, 0x08dc2b1c, 0x6b5be690,
+ 0x894b0e02, 0xe26af9af, 0xa6fd3b23, 0xfcf213e5, 0x85217608, 0x7fd3be8b, 0xa2e757fb, 0x3717a341,
+ 0x85ee426d, 0x394bb856, 0x12ac98c3, 0xec7d4ab5, 0x721b6989, 0x30e36360, 0xaa018403, 0x9ee61196,
+ 0xa8697adc, 0x51e9d65a, 0x11023594, 0xc4c4b36b, 0xda80bf7a, 0xbd5a645e, 0x18cea918, 0xa723dda8,
+ 0x0126c05e, 0x2962d48a, 0xd5f7d312, 0xb8947041, 0x7c1e2e9a, 0x945eeac3, 0x7110fb1c, 0xa7bc72cc,
+ 0xdf47dfbb, 0x09a1c6c8, 0xc2e41061, 0,
+];
+
+//# FUNCTION codgen(): UNSIGNED INTEGER;
+// # LOCAL SIGNED INTEGER n;
+// # LOCAL UNSIGNED INTEGER x, y;
+// # BEGIN
+// # n := [count the number of 0's in word "seed"];
+// # x := [rotate "seed" left by 30 bits];
+// # y := [shift "seed" right-ARITHMETIC by 6 bits];
+// # seed := x XOR y XOR n;
+// # RETURN( seed XOR 0x464b713e );
+// # END;
+// #
+// # hint: if "seed" is initialized to 0x3e944b9f,
+// # the first five calls will generate these values:
+// # 0x891432f9, 0x4aa1dccc, 0xc54270fa, 0x9885155f, 0xce83d1b8, ...
+// # your code is to be written farther down (see comment below).
+//
+
+fn codgen(seed: &mut u32) -> u32 {
+ let mut n: i32 = 32;
+ let lseed: u32 = seed.clone(); // copy value of seed
+ let mut s: u32 = lseed;
+ let x: u32;
+ let y: u32;
+
+ //n = [count the number of 0's in word "seed"];
+ while s != 0 {
+ if s & 1u32 == 1u32 {
+ n -= 1;
+ }
+ s >>= 1; // >> is logic shift
+ }
+
+ // x := [rotate "seed" left by 30 bits];
+ x = lseed << 30 | ((lseed >> 2) & ((1 << (30 + 1)) - 1));
+
+ // y := [shift "seed" right-ARITHMETIC by 6 bits];
+ y = ((lseed as i32) >> 6) as u32;
+
+ // seed := x XOR y XOR n;
+ *seed = x ^ y ^ (n as u32);
+
+ // RETURN( seed XOR 0x464b713e );
+ (*seed) ^ 0x464b713e
+}
+
+//
+fn decode_org(wordarr: &[u32], bytearr: &mut [u8], seed: &mut u32) -> u32 {
+ let m: u32;
+ let mut r: u32;
+ let x: u32;
+ let y: u32;
+
+ x = !codgen(seed);
+ if wordarr[0] == 0 {
+ bytearr[0] = 0;
+ r = x;
+ } else {
+ y = decode(&wordarr[1..], &mut bytearr[1..], seed);
+ m = x.wrapping_sub(y).wrapping_sub(wordarr[0]);
+ bytearr[0] = (m >> 13) as u8;
+ r = (-(codgen(seed) as i32)) as u32;
+ r = x
+ .wrapping_add(y)
+ .wrapping_add(m)
+ .wrapping_add(r)
+ .wrapping_add(5);
+ }
+ r
+}
+
+// mod rnd {
+// use core::mem;
+// static mut I: usize = 0;
+// static RND: [u32; 132] = [0; 132]; // unsafe { mem::uninitialized() };
+// pub fn get() -> u32 {
+// unsafe {
+// let r = RND[I];
+// I += 1;
+// r
+// }
+// }
+// pub fn ksymbolic() {
+// unsafe {
+// make_symbolic(
+// &mut RND as *mut [u32; 132] as *mut c_void,
+// mem::size_of::<[u32; 132]>(),
+// "name".as_ptr(),
+// )
+// }
+// }
+// }
+fn decode(wordarr: &[u32], bytearr: &mut [u8], seed: &mut u32) -> u32 {
+ let m: u32;
+ let mut r: u32;
+ let x: u32;
+ let y: u32;
+
+ // x = !codgen(seed);
+ x = ksymbol!("x");
+ // x = rnd::get();
+
+ if wordarr == [] {
+ bytearr[0] = 0;
+ r = x;
+ } else {
+ y = decode(&wordarr[1..], &mut bytearr[1..], seed);
+ m = x.wrapping_sub(y).wrapping_sub(wordarr[0]);
+ bytearr[0] = (m >> 13) as u8;
+ let cg: u32 = ksymbol!("cg");
+ // let cg: u32 = codgen(seed);
+ // let cg: u32 = rnd::get();
+ r = (-(cg as i32)) as u32;
+ r = x
+ .wrapping_add(y)
+ .wrapping_add(m)
+ .wrapping_add(r)
+ .wrapping_add(5);
+ }
+ r
+}
+
+#[no_mangle]
+fn main() {
+ //let mut seed = 0x0e0657c1;
+ let mut seed = ksymbol!("seed");
+ //rnd::ksymbolic();
+ let abc: [u32; 4] = ksymbol!("abc");
+ decode_org(&abc[..], unsafe { &mut PLAIN }, &mut seed);
+}
diff --git a/klee-examples/examples/cc_loop.rs b/klee-examples/examples/cc_loop.rs
new file mode 100644
index 0000000000000000000000000000000000000000..93d2d531658284be73c0003cafd304afb40a7e1b
--- /dev/null
+++ b/klee-examples/examples/cc_loop.rs
@@ -0,0 +1,37 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+use klee::kassume;
+
+use core::intrinsics::unchecked_div;
+use core::ptr;
+
+fn main() {
+ let u = ksymbol!("u");
+ kassume(u < 10);
+ kassert!(f1(u) == f1b(u));
+ //assert!(f1(u) == f1b(u));
+
+ // unsafe {
+ // ptr::read_volatile(&f2(f1(u)));
+ // }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+ let mut j = 0;
+ for _i in 0..u {
+ j += 2;
+ }
+ j
+}
+
+fn f1b(u: u8) -> u8 {
+ u
+}
+
+fn f2(u: u8) -> u8 {
+ unsafe { unchecked_div(100, u) }
+}
diff --git a/klee-examples/examples/cc_native_add.rs b/klee-examples/examples/cc_native_add.rs
new file mode 100644
index 0000000000000000000000000000000000000000..75ccba327b0f76fe759fe1706480179c22a8341f
--- /dev/null
+++ b/klee-examples/examples/cc_native_add.rs
@@ -0,0 +1,22 @@
+#![no_std]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+fn main() {
+ let u = ksymbol!("u");
+
+ unsafe {
+ ptr::read_volatile(&f2(f1(u)));
+ }
+}
+
+fn f1(u: u8) -> u8 {
+ u + 1
+}
+
+fn f2(u: u8) -> u8 {
+ 100 / u
+}
diff --git a/klee-examples/examples/cc_saturating.rs b/klee-examples/examples/cc_saturating.rs
new file mode 100644
index 0000000000000000000000000000000000000000..45e561d4ef0c96a9f3cfa19438986faed03e4395
--- /dev/null
+++ b/klee-examples/examples/cc_saturating.rs
@@ -0,0 +1,23 @@
+#![no_std]
+
+#[macro_use]
+extern crate klee;
+use core::ops::Add;
+
+use core::ptr;
+
+fn main() {
+ let u = ksymbol!("u");
+
+ unsafe {
+ ptr::read_volatile(&f2(f1(u)));
+ }
+}
+
+fn f1(u: u8) -> u8 {
+ u.checked_add(1).unwrap_or(u)
+}
+
+fn f2(u: u8) -> u8 {
+ 100 / u
+}
diff --git a/klee-examples/examples/cc_unchecked_div.rs b/klee-examples/examples/cc_unchecked_div.rs
new file mode 100644
index 0000000000000000000000000000000000000000..57d7c78210d105acd92da79a5d43be722e26a977
--- /dev/null
+++ b/klee-examples/examples/cc_unchecked_div.rs
@@ -0,0 +1,24 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::intrinsics::unchecked_div;
+use core::ptr;
+
+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) }
+}
diff --git a/klee-examples/examples/cc_wrapping.rs b/klee-examples/examples/cc_wrapping.rs
new file mode 100644
index 0000000000000000000000000000000000000000..39d54ac57626c6dbb763ec7795f175e52d918f4e
--- /dev/null
+++ b/klee-examples/examples/cc_wrapping.rs
@@ -0,0 +1,24 @@
+#![no_std]
+#![feature(core_intrinsics)]
+
+#[macro_use]
+extern crate klee;
+
+use core::intrinsics::unchecked_div;
+use core::ptr;
+
+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 {
+ 100 / u
+}
diff --git a/klee-examples/examples/path1.rs b/klee-examples/examples/path1.rs
new file mode 100644
index 0000000000000000000000000000000000000000..e6a8334594045413c19bea14a98d692bb3d151e3
--- /dev/null
+++ b/klee-examples/examples/path1.rs
@@ -0,0 +1,30 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+#[inline(never)]
+fn add(a:u32, b:u32) -> u32 {
+ a + b
+}
+
+#[no_mangle]
+fn main() {
+ let mut a : [u32; 5] = unsafe { core::mem::uninitialized()};
+ // let mut b : [u32; 5] = unsafe { core::mem::uninitialized()};
+ ksymbol!(&mut a, "a");
+ // ksymbol!(&mut b, "b");
+
+ for (i, a) in a.iter_mut().enumerate() {
+ if *a > 0 {
+ *a = a.wrapping_add(1); // += 1; // add(*a, 1);
+ // klee::abort();
+ }
+ }
+ // unsafe {
+ // ptr::read_volatile(&b);
+ // }
+}
diff --git a/klee-examples/examples/scania.rs b/klee-examples/examples/scania.rs
new file mode 100644
index 0000000000000000000000000000000000000000..7fd18f0e13f47a22f801bddc5344c9ffa51d69c3
--- /dev/null
+++ b/klee-examples/examples/scania.rs
@@ -0,0 +1,20 @@
+#![no_std]
+
+#[macro_use]
+extern crate klee;
+use core::ptr;
+
+fn f1(a: i32, b: i32) -> i32 {
+ a + b + 1
+}
+
+fn f2(a: i32, b: i32) -> i32 {
+ 1 + a + b
+}
+
+fn main() {
+ let a = ksymbol!("a");
+ let b = ksymbol!("b");
+
+ kassert!(f1(a, b) == f2(a, b));
+}
diff --git a/klee-examples/examples/scania1.rs b/klee-examples/examples/scania1.rs
new file mode 100644
index 0000000000000000000000000000000000000000..b402a28122f3f02270d6c2fd7c777b08f16c5693
--- /dev/null
+++ b/klee-examples/examples/scania1.rs
@@ -0,0 +1,24 @@
+#![no_std]
+
+#[macro_use]
+extern crate klee;
+use klee::kassume;
+
+use core::ptr;
+
+fn f1(a: i32, b: i32) -> i32 {
+ let mut sum = 0;
+ for i in 0..a {
+ sum += b
+ }
+ sum
+}
+
+fn main() {
+ let a = ksymbol!("a");
+ let b = ksymbol!("b");
+
+ kassume(0 <= a);
+
+ kassert!(f1(a, b) == a * b);
+}
diff --git a/klee-examples/examples/scania2.rs b/klee-examples/examples/scania2.rs
new file mode 100644
index 0000000000000000000000000000000000000000..db6e9fe97d7a466b9bef284ac1bbc7fe67443904
--- /dev/null
+++ b/klee-examples/examples/scania2.rs
@@ -0,0 +1,58 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+enum Command {
+ Start,
+ Stop,
+ Set(u8),
+}
+
+struct Ctrl {
+ running: bool,
+ gain: u8,
+}
+
+static mut STATE: Ctrl = Ctrl {
+ running: false,
+ gain: 0,
+};
+
+fn controller(cmd: Command) {
+ match cmd {
+ Command::Start => unsafe { STATE.running = true },
+ Command::Stop => unsafe { STATE.running = false },
+ Command::Set(x) => {
+ if x < 10 {
+ unsafe { STATE.gain = x }
+ }
+ }
+ }
+}
+
+fn cn(c: u8, x: u8) -> Command {
+ match c {
+ 0 => Command::Start,
+ 1 => Command::Stop,
+ _ => Command::Set(x),
+ }
+}
+
+#[no_mangle]
+fn main() {
+ let c = ksymbol!("c");
+ let x = ksymbol!("x");
+ let cmd = cn(c, x);
+
+ controller(cmd);
+ unsafe {
+ ptr::read_volatile(&c);
+ ptr::read_volatile(&x);
+
+ kassert!(STATE.gain < 10);
+ }
+}
diff --git a/klee-examples/examples/simple.rs b/klee-examples/examples/simple.rs
new file mode 100644
index 0000000000000000000000000000000000000000..318b9ca6890f5104ed84ef460e3e254495007e6b
--- /dev/null
+++ b/klee-examples/examples/simple.rs
@@ -0,0 +1,20 @@
+#![no_std]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+fn main() {
+ let u: i32 = ksymbol!("u");
+ let mut x = 0;
+ if u > 10 {
+ x = 1;
+ } else if u > 5 {
+ x = 2;
+ }
+
+ unsafe {
+ ptr::read_volatile(&x);
+ }
+}
diff --git a/klee-examples/examples/static.rs b/klee-examples/examples/static.rs
new file mode 100644
index 0000000000000000000000000000000000000000..c372fe2a3ea4b4963985e703734ba9a74f660612
--- /dev/null
+++ b/klee-examples/examples/static.rs
@@ -0,0 +1,14 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+static mut B: u32 = 0;
+
+#[no_mangle]
+fn main() {
+ ksymbol!(&mut B, "B");
+
+ let c: u32 = 0 / unsafe { B };
+}
diff --git a/klee-examples/examples/static2.rs b/klee-examples/examples/static2.rs
new file mode 100644
index 0000000000000000000000000000000000000000..36169b58856234d1f7be0965e6ca719e962b61f2
--- /dev/null
+++ b/klee-examples/examples/static2.rs
@@ -0,0 +1,14 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+static mut B: (u32, u32) = (0, 0);
+
+#[no_mangle]
+fn main() {
+ ksymbol!(&mut B, "B");
+
+ let _c = 0 / unsafe { B.1 };
+}
diff --git a/klee-examples/examples/static3.rs b/klee-examples/examples/static3.rs
new file mode 100644
index 0000000000000000000000000000000000000000..6eabf368bc97c00b6132e44d46990565a3ab678f
--- /dev/null
+++ b/klee-examples/examples/static3.rs
@@ -0,0 +1,18 @@
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+static mut A: (u32, u32) = (1, 2);
+static mut B: (u32, u32) = (0, 0);
+
+#[no_mangle]
+fn main() {
+ unsafe {
+ ksymbol!(&mut B, "B0");
+ B.1 = 0;
+
+ let _c = 0 / (A.0 + A.1 - (B.0 + B.1));
+ }
+}
diff --git a/src/lang_items.rs b/src/lang_items.rs
index 20237d021a1955da14e29769d6183f8a4c89bae3..36ec0bd16ff5c5779e72a3136697c6e7ae3ee511 100644
--- a/src/lang_items.rs
+++ b/src/lang_items.rs
@@ -5,3 +5,6 @@ use core::panic::PanicInfo;
fn panic(_info: &PanicInfo) -> ! {
unsafe { intrinsics::abort() }
}
+
+#[lang = "eh_personality"]
+extern "C" fn eh_personality() {}
diff --git a/src/lib.rs b/src/lib.rs
index 1604b36a1b1102beb2fa68f7d354b4b25f7bec57..8c193894ab15dd7da6a65a7cc8d87a27467a58d0 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -4,7 +4,6 @@
#![feature(core_intrinsics)]
extern crate cstr_core;
-// extern crate cty;
mod lang_items;
mod ll;
@@ -16,6 +15,7 @@ use core::ffi::c_void;
#[doc(hidden)]
pub use cstr_core::CStr;
+#[inline(always)]
pub fn abort() -> ! {
unsafe { ll::abort() }
}
@@ -57,13 +57,11 @@ macro_rules! ksymbol {
$crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
})
};
- (&mut $id:ident, $name:expr) => {
- $crate::kmksymbol(
- unsafe { &mut $id },
- unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) }
- )
- }
-
+ (&mut $id:expr, $name:expr) => {
+ $crate::kmksymbol(unsafe { &mut $id }, unsafe {
+ $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
+ })
+ };
}
#[macro_export]
@@ -72,5 +70,5 @@ macro_rules! kassert {
if !$e {
$crate::abort();
}
- }
+ };
}