From 7d0c573d7715185dcda1bc15c3d54b62c5460e31 Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Tue, 26 Mar 2019 10:33:09 +0100
Subject: [PATCH] dfs
---
Cargo.toml | 14 +--
examples/eq_dfs.rs | 232 +++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 240 insertions(+), 6 deletions(-)
create mode 100644 examples/eq_dfs.rs
diff --git a/Cargo.toml b/Cargo.toml
index ef7258b..d471951 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -5,16 +5,13 @@ authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.
[dependencies]
klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
+enumset = "0.3.16"
+panic-abort = "0.3.1"
# panic-abort = "0.3.1"
[dependencies.cortex-m]
version = "0.6.0"
-[patch.crates-io]
-vcell = { git = "https://github.com/perlindgren/vcell.git" }
-volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
-cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
-
[dependencies.volatile-register]
version = "0.3.0"
@@ -24,6 +21,11 @@ git = "https://gitlab.henriktjader.com/pln/stm32f413.git"
branch = "klee-analysis"
optional = true
+[patch.crates-io]
+vcell = { git = "https://github.com/perlindgren/vcell.git" }
+volatile-register = { git = "https://github.com/perlindgren/volatile-register.git" }
+cortex-m = { git = "https://github.com/perlindgren/cortex-m.git", branch = "klee-analysis" }
+
[[examples]]
name = "gpioa"
path = "examples/gpioa.rs"
@@ -31,7 +33,7 @@ path = "examples/gpioa.rs"
[profile.dev]
incremental = false
-# lto = true
+lto = true
[profile.release]
debug = true
diff --git a/examples/eq_dfs.rs b/examples/eq_dfs.rs
new file mode 100644
index 0000000..c800ec2
--- /dev/null
+++ b/examples/eq_dfs.rs
@@ -0,0 +1,232 @@
+#![allow(non_snake_case)]
+#![no_main]
+#![no_std]
+
+extern crate panic_abort;
+extern crate klee;
+use klee::{kassert, kassume, ksymbol};
+
+#[derive(Debug, Copy, Clone)]
+pub struct Data {
+ a: bool,
+ b: bool,
+}
+
+#[derive(Debug, Copy, Clone, PartialEq)]
+pub enum State {
+ S8000,
+ S8001,
+ S8004,
+ S8014,
+ S8005,
+ C001,
+ C002,
+ C003,
+}
+
+use State::*;
+
+const DISCREPANCY: u32 = 2;
+// const HORIZON: usize = (2 * DISCREPANCY + 5) as usize;
+const HORIZON: usize = 100 as usize;
+
+const T: bool = true;
+const F: bool = false;
+
+#[no_mangle]
+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() };
+ // initial state, Init
+ let mut i = 0;
+ let mut TIMEOUT_CNTR: u32 = DISCREPANCY;
+ let mut STATE = S8001;
+ STATE_H[i] = STATE;
+ CNTR_H[i] = TIMEOUT_CNTR;
+ i += 1; // next state index
+
+ loop {
+ eq(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
+ STATE_H[i] = STATE;
+ CNTR_H[i] = TIMEOUT_CNTR;
+
+ // 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);
+ }
+
+ // !a | !b -> !S8000
+ // ensures that if any input is false we cannot enter the Enable state
+ // this can also be seen as a safety 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));
+ }
+
+ // 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] {
+ C001 | C002 | C003 => {
+ // transitions from error
+ kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
+ }
+ S8005 => {
+ kassert!(
+ (STATE_H[i] == S8001)
+ | (STATE == C003)
+ | (STATE == STATE_H[i - 1])
+ );
+ }
+ _ => (),
+ }
+ }
+
+ // // DISCREPANCY related invariants
+ match STATE {
+ // Error -> timeout
+ C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
+
+ S8004 | S8005 | S8014 => {
+ // // remaining in a waiting state decreases the counter
+ if i > 0 {
+ if STATE_H[i - 1] == STATE_H[i] {
+ kassert!(TIMEOUT_CNTR < 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]) };
+
+ let mut is_visited = false;
+ match STATE {
+ S8004 | S8005 | S8014 => {}
+ _ => {
+ for j in 0..i {
+ if (STATE_H[i] == STATE_H[j]) {
+ is_visited = true;
+ }
+ }
+ }
+ }
+
+ if is_visited {
+ break;
+ }
+ i += 1;
+ if i == HORIZON {
+ kassert!(false);
+ }
+ }
+}
+
+fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
+ *STATE = match STATE {
+ S8000 => match (data.a, data.b) {
+ (F, F) => S8001,
+ (F, T) | (T, F) => {
+ *TIMEOUT_CNTR = DISCREPANCY;
+ S8005
+ }
+ (T, T) => S8000,
+ },
+ S8001 => match (data.a, data.b) {
+ (F, F) => S8001,
+ (F, T) => {
+ *TIMEOUT_CNTR = DISCREPANCY;
+ S8014
+ }
+ (T, F) => {
+ *TIMEOUT_CNTR = DISCREPANCY;
+ S8004
+ }
+ (T, T) => S8000,
+ },
+ S8004 => match *TIMEOUT_CNTR {
+ 0 => C001,
+ _ => {
+ *TIMEOUT_CNTR -= 1;
+ match (data.a, data.b) {
+ (F, _) => S8001,
+ (_, T) => S8000,
+ _ => S8004,
+ }
+ }
+ },
+ S8014 => match *TIMEOUT_CNTR {
+ 0 => C002,
+ _ => {
+ *TIMEOUT_CNTR -= 1;
+ match (data.a, data.b) {
+ (_, F) => S8001,
+ (T, _) => S8000,
+ _ => S8014,
+ }
+ }
+ },
+ S8005 => match *TIMEOUT_CNTR {
+ 0 => C003,
+ _ => {
+ *TIMEOUT_CNTR -= 1;
+ match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => S8005,
+ }
+ }
+ },
+ C001 | C002 | C003 => match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => *STATE,
+ },
+ };
+}
--
GitLab