From 41c6591c9cf171d2b5ce6f2f3122aa1ae947de30 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Sat, 11 Nov 2017 18:07:26 +0100
Subject: [PATCH] lab4
---
klee-examples/examples/cc_codegen_eq.rs | 79 ++++++
klee-examples/examples/cc_lab4_contract.rs | 276 +++++++++++++++++++++
2 files changed, 355 insertions(+)
create mode 100644 klee-examples/examples/cc_codegen_eq.rs
create mode 100644 klee-examples/examples/cc_lab4_contract.rs
diff --git a/klee-examples/examples/cc_codegen_eq.rs b/klee-examples/examples/cc_codegen_eq.rs
new file mode 100644
index 0000000..3bfb13f
--- /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_lab4_contract.rs b/klee-examples/examples/cc_lab4_contract.rs
new file mode 100644
index 0000000..4b72936
--- /dev/null
+++ b/klee-examples/examples/cc_lab4_contract.rs
@@ -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);
+}
--
GitLab