From 9b118168e566572b39ea187ee7fff3c5693c4a3d Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Fri, 10 Nov 2017 04:02:34 +0100
Subject: [PATCH] cc updates
---
klee-examples/examples/cc_add.rs | 32 +++++++++++
klee-examples/examples/cc_contract.rs | 64 ++++++++++++++++++++++
klee-examples/examples/cc_contract_err.rs | 64 ++++++++++++++++++++++
klee-examples/examples/cc_equivalence.rs | 25 +++++++++
klee-examples/examples/cc_loop.rs | 16 ++++--
klee-examples/examples/cc_native_add.rs | 3 +-
klee-examples/examples/cc_saturating.rs | 5 +-
klee-examples/examples/cc_unchecked_div.rs | 24 ++++++++
klee-examples/examples/cc_wrapping.rs | 7 +--
klee/src/lib.rs | 8 +--
rls1509755957780.log | 6 ++
11 files changed, 237 insertions(+), 17 deletions(-)
create mode 100644 klee-examples/examples/cc_add.rs
create mode 100644 klee-examples/examples/cc_contract.rs
create mode 100644 klee-examples/examples/cc_contract_err.rs
create mode 100644 klee-examples/examples/cc_equivalence.rs
create mode 100644 klee-examples/examples/cc_unchecked_div.rs
create mode 100644 rls1509755957780.log
diff --git a/klee-examples/examples/cc_add.rs b/klee-examples/examples/cc_add.rs
new file mode 100644
index 0000000..d0e3e84
--- /dev/null
+++ b/klee-examples/examples/cc_add.rs
@@ -0,0 +1,32 @@
+#![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
+}
diff --git a/klee-examples/examples/cc_contract.rs b/klee-examples/examples/cc_contract.rs
new file mode 100644
index 0000000..99c7be9
--- /dev/null
+++ b/klee-examples/examples/cc_contract.rs
@@ -0,0 +1,64 @@
+#![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));
+}
diff --git a/klee-examples/examples/cc_contract_err.rs b/klee-examples/examples/cc_contract_err.rs
new file mode 100644
index 0000000..d1d27aa
--- /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::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));
+}
diff --git a/klee-examples/examples/cc_equivalence.rs b/klee-examples/examples/cc_equivalence.rs
new file mode 100644
index 0000000..683b045
--- /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_loop.rs b/klee-examples/examples/cc_loop.rs
index b3dcaaa..87eea38 100644
--- a/klee-examples/examples/cc_loop.rs
+++ b/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) }
}
diff --git a/klee-examples/examples/cc_native_add.rs b/klee-examples/examples/cc_native_add.rs
index 6f272c7..75ccba3 100644
--- a/klee-examples/examples/cc_native_add.rs
+++ b/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
}
diff --git a/klee-examples/examples/cc_saturating.rs b/klee-examples/examples/cc_saturating.rs
index 2ee2f41..db43512 100644
--- a/klee-examples/examples/cc_saturating.rs
+++ b/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)
}
diff --git a/klee-examples/examples/cc_unchecked_div.rs b/klee-examples/examples/cc_unchecked_div.rs
new file mode 100644
index 0000000..9193598
--- /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::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) }
+}
diff --git a/klee-examples/examples/cc_wrapping.rs b/klee-examples/examples/cc_wrapping.rs
index 2689548..b8ad048 100644
--- a/klee-examples/examples/cc_wrapping.rs
+++ b/klee-examples/examples/cc_wrapping.rs
@@ -5,21 +5,20 @@
extern crate klee;
use core::ptr;
- use core::intrinsics::unchecked_div;
+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
}
diff --git a/klee/src/lib.rs b/klee/src/lib.rs
index f2b035b..48b0dbf 100644
--- a/klee/src/lib.rs
+++ b/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())
})
}
diff --git a/rls1509755957780.log b/rls1509755957780.log
new file mode 100644
index 0000000..a29dede
--- /dev/null
+++ b/rls1509755957780.log
@@ -0,0 +1,6 @@
+error: expected expression, found `+`
+ --> stdin:22:11
+ |
+22 | j++;
+ | ^
+
--
GitLab