From 799276ea12cde3248704457458b69cc1d25b0d6d Mon Sep 17 00:00:00 2001
From: Nils Fitinghoff <nils.fitinghoff@grepit.se>
Date: Fri, 29 Mar 2019 16:19:12 +0100
Subject: [PATCH] match the code from the paper exactly
---
examples/eq_paper.rs | 105 ++++++++++++++-----------------------------
1 file changed, 33 insertions(+), 72 deletions(-)
diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs
index a881738..9eeeb2a 100644
--- a/examples/eq_paper.rs
+++ b/examples/eq_paper.rs
@@ -1,6 +1,9 @@
#![allow(non_snake_case)]
#![no_main]
+#![no_std]
+
+extern crate panic_abort;
extern crate klee;
use klee::{kassert, kassume, ksymbol};
@@ -34,109 +37,67 @@ fn main() {
let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
ksymbol!(&mut DATA, "DATA");
- let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() };
-
- let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
-
- let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
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
+ // TIMEOUT_CNTR_HISTORY
+ let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
for i in 0..HORIZON {
- periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
- STATE_H[i] = STATE;
- CNTR_H[i] = TIMEOUT_CNTR;
+ eq(&mut STATE, &mut CNTR, &mut DATA[i]);
- // invariants
- // 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);
- }
+ STATE_H[i] = STATE; // update STATE history
+ CNTR_H[i] = CNTR; // update CNTR history
- // !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)
+ // (1) !a | !b -> !S8000
if !DATA[i].a | !DATA[i].b {
kassert!(!(STATE == S8000));
}
-
- // 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);
+
+ // (2) S8000 -> a & b
+ if STATE == S8000 {
+ kassert!(DATA[i].a & DATA[i].b);
}
-
- // transition invariants
+
if i > 0 {
match STATE_H[i - 1] {
+ // (3)
C001 | C002 | C003 => {
- // transitions from error
- kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
+ kassert!(
+ (STATE == S8001)
+ | (STATE == STATE_H[i - 1])
+ );
}
+ // (4)
S8005 => {
- kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
+ kassert!(
+ (STATE == S8001)
+ | (STATE == C003)
+ | (STATE == STATE_H[i - 1])
+ );
}
_ => (),
}
}
- // // DISCREPANCY related invariants
match STATE {
- // Error -> timeout
- C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
+ // (5)
+ C001 | C002 | C003 => kassert!(CNTR == 0),
S8004 | S8005 | S8014 => {
- // // remaining in a waiting state decreases the counter
+ // (6)
if i > 0 {
- if STATE_H[i - 1] == STATE_H[i] {
- kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
+ if STATE_H[i - 1] == STATE {
+ kassert!(CNTR_H[i] < CNTR_H[i - 1]);
}
}
- // // Waiting states -> !timeout
- // // Waiting states implies that TIMEOUT_CNTR has not yet expired
- // // and that the time remaining is not longer than the DISCREPANCY
- // kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
- // kassert!(TIMEOUT_CNTR <= DISCREPANCY);
}
_ => {}
}
-
- // // liveness?
- // if i == HORIZON - 1 {
- // let mut ok = false;
- // for j in 0..=i {
- // if STATE_H[j] == S8001 {
- // ok = true;
- // }
- // }
- // kassert!(ok);
- // }
-
- // if i > 0 {
- // match STATE_H[i - 1] {
- // C001 | C002 | C003 | S8005 => {
- // // no (immediate) transition from error / recover to Enable state
- // kassert!(!(STATE == S8000));
- // }
- // _ => {
- // // liveness from Init and Wait states, Enable is ensured
- // if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
- // kassert!(STATE == S8000);
- // }
- // }
- // }
- // }
-
- unsafe { core::ptr::read_volatile(&STATE_H[i]) };
}
}
-fn periodic(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