From 296a8323773485ce19039bd4bd5d273d879c8bef Mon Sep 17 00:00:00 2001
From: Nils Fitinghoff <nils.fitinghoff@grepit.se>
Date: Fri, 29 Mar 2019 17:19:17 +0100
Subject: [PATCH] revert to a fixed version of the original
the version pulled in from the paper gave completely different results
---
examples/eq_paper.rs | 82 ++++++++++++++++++++++++--------------------
1 file changed, 44 insertions(+), 38 deletions(-)
diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs
index 8449c50..c381369 100644
--- a/examples/eq_paper.rs
+++ b/examples/eq_paper.rs
@@ -2,8 +2,8 @@
#![no_main]
#![no_std]
-extern crate klee;
extern crate panic_abort;
+extern crate klee;
use klee::{kassert, kassume, ksymbol};
#[derive(Debug, Copy, Clone)]
@@ -33,79 +33,85 @@ const F: bool = false;
#[no_mangle]
fn main() {
- let mut DATA: [Data; HORIZON] =
- unsafe { core::mem::uninitialized() };
+ let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
ksymbol!(&mut DATA, "DATA");
- let mut STATE = S8001;
- let mut STATE_H: [State; HORIZON] =
- unsafe { core::mem::uninitialized() }; // STATE_HISTORY
- let mut CNTR: u32 =
- unsafe { core::mem::uninitialized() }; // TIMEOUT_CNTR
+ let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() };
- // TIMEOUT_CNTR_HISTORY
- let mut CNTR_H: [u32; HORIZON] =
- unsafe { core::mem::uninitialized() };
+ let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
- for i in 0..HORIZON {
- eq(&mut STATE, &mut CNTR, &mut DATA[i]);
+ let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
+ let mut STATE = S8001;
- STATE_H[i] = STATE; // update STATE history
- CNTR_H[i] = CNTR; // update CNTR history
+ for i in 0..HORIZON {
+ eq(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
+ STATE_H[i] = STATE;
+ CNTR_H[i] = TIMEOUT_CNTR;
+
+ // invariants
+ // (1) S8000 -> a & b
+ // ensures that Enable implies that both a and b are true
+ // this is the main safety condition
+ if STATE == S8000 {
+ kassert!(DATA[i].a & DATA[i].b);
+ }
- // (1) !a | !b -> !S8000
+ // (2) !a | !b -> !S8000
+ // ensures that if any input is false we cannot enter the Enable state
+ // this can also be seen as a safty condition
+ // (can it be derived from the first condition, but we keep is as
+ // an indication that the verification works as expected)
+ // Indeed the number of spanned paths remains the same
+ // (with or without the below assertion, so its proven redundant by KLEE)
if !DATA[i].a | !DATA[i].b {
kassert!(!(STATE == S8000));
}
- // (2) S8000 -> a & b
- if STATE == S8000 {
- kassert!(DATA[i].a & DATA[i].b);
+ // S8001 -> !a & !b
+ // we can only stay or enter the Init state unless either (or both) inputs are false
+ if STATE == S8001 {
+ kassert!(!DATA[i].a | !DATA[i].b);
}
+ // transition invariants
if i > 0 {
match STATE_H[i - 1] {
- // (3)
C001 | C002 | C003 => {
- kassert!(
- (STATE == S8001)
- | (STATE == STATE_H[i - 1])
- );
+ // (3)
+ // transitions from error
+ kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
}
- // (4)
S8005 => {
- kassert!(
- (STATE == S8001)
- | (STATE == C003)
- | (STATE == STATE_H[i - 1])
- );
+ // (4)
+ kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
}
_ => (),
}
}
+ // // DISCREPANCY related invariants
match STATE {
+ // Error -> timeout
// (5)
- C001 | C002 | C003 => kassert!(CNTR == 0),
+ C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
S8004 | S8005 | S8014 => {
// (6)
+ // remaining in a waiting state decreases the counter
if i > 0 {
- if STATE_H[i - 1] == STATE {
- kassert!(CNTR_H[i] < CNTR_H[i - 1]);
+ if STATE_H[i - 1] == STATE_H[i] {
+ kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
}
}
}
_ => {}
}
+
+ unsafe { core::ptr::read_volatile(&STATE_H[i]) };
}
}
-fn eq(
- STATE: &mut State,
- TIMEOUT_CNTR: &mut u32,
- data: &Data,
-) {
+fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
*STATE = match STATE {
S8000 => match (data.a, data.b) {
(F, F) => S8001,
--
GitLab