diff --git a/Cargo.lock b/Cargo.lock
index 111a7acfd8601558193a07b131f0cb1f689bfc2f..5b9a9acedd042634116b225a148431a6a5b008c3 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -43,6 +43,25 @@ name = "cty"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
+[[package]]
+name = "enumset"
+version = "0.3.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "enumset_derive 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
+ "num-traits 0.2.6 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "enumset_derive"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "proc-macro2 0.4.27 (registry+https://github.com/rust-lang/crates.io-index)",
+ "quote 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)",
+ "syn 0.15.29 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
[[package]]
name = "klee"
version = "0.2.0"
@@ -56,7 +75,9 @@ name = "klee-examples"
version = "0.2.0"
dependencies = [
"cortex-m 0.6.0 (git+https://github.com/perlindgren/cortex-m.git?branch=klee-analysis)",
+ "enumset 0.3.17 (registry+https://github.com/rust-lang/crates.io-index)",
"klee 0.2.0 (git+https://gitlab.henriktjader.com/pln/cargo-klee)",
+ "panic-abort 0.3.1 (registry+https://github.com/rust-lang/crates.io-index)",
"stm32f413 0.3.0 (git+https://gitlab.henriktjader.com/pln/stm32f413.git?branch=klee-analysis)",
"volatile-register 0.3.0 (git+https://github.com/perlindgren/volatile-register.git)",
]
@@ -70,6 +91,32 @@ dependencies = [
"version_check 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
]
+[[package]]
+name = "num-traits"
+version = "0.2.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "panic-abort"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
+name = "proc-macro2"
+version = "0.4.27"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "unicode-xid 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "quote"
+version = "0.6.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "proc-macro2 0.4.27 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
[[package]]
name = "rustc_version"
version = "0.2.3"
@@ -101,6 +148,21 @@ dependencies = [
"vcell 0.2.0 (git+https://github.com/perlindgren/vcell.git)",
]
+[[package]]
+name = "syn"
+version = "0.15.29"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "proc-macro2 0.4.27 (registry+https://github.com/rust-lang/crates.io-index)",
+ "quote 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)",
+ "unicode-xid 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "unicode-xid"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
[[package]]
name = "vcell"
version = "0.2.0"
@@ -129,12 +191,20 @@ dependencies = [
"checksum cortex-m 0.6.0 (git+https://github.com/perlindgren/cortex-m.git?branch=klee-analysis)" = "<none>"
"checksum cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
"checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
+"checksum enumset 0.3.17 (registry+https://github.com/rust-lang/crates.io-index)" = "2d67547bfa69f4ca1c960f151d502f3b6db7cbb523ae2b20c6da7333c69fa24c"
+"checksum enumset_derive 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "f90b5cdb387bc97d281c59fffebe335cf0a01e1734e1fc0e92d731fdbb9ceb36"
"checksum klee 0.2.0 (git+https://gitlab.henriktjader.com/pln/cargo-klee)" = "<none>"
"checksum memchr 2.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "db4c41318937f6e76648f42826b1d9ade5c09cafb5aef7e351240a70f39206e9"
+"checksum num-traits 0.2.6 (registry+https://github.com/rust-lang/crates.io-index)" = "0b3a5d7cc97d6d30d8b9bc8fa19bf45349ffe46241e8816f50f62f6d6aaabee1"
+"checksum panic-abort 0.3.1 (registry+https://github.com/rust-lang/crates.io-index)" = "2c14a66511ed17b6a8b4256b868d7fd207836d891db15eea5195dbcaf87e630f"
+"checksum proc-macro2 0.4.27 (registry+https://github.com/rust-lang/crates.io-index)" = "4d317f9caece796be1980837fd5cb3dfec5613ebdb04ad0956deea83ce168915"
+"checksum quote 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)" = "cdd8e04bd9c52e0342b406469d494fcb033be4bdbe5c606016defbb1681411e1"
"checksum rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)" = "138e3e0acb6c9fb258b19b67cb8abd63c00679d2851805ea151465464fe9030a"
"checksum semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)" = "1d7eb9ef2c18661902cc47e535f9bc51b78acd254da71d375c2f6720d9a40403"
"checksum semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)" = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3"
"checksum stm32f413 0.3.0 (git+https://gitlab.henriktjader.com/pln/stm32f413.git?branch=klee-analysis)" = "<none>"
+"checksum syn 0.15.29 (registry+https://github.com/rust-lang/crates.io-index)" = "1825685f977249735d510a242a6727b46efe914bb67e38d30c071b1b72b1d5c2"
+"checksum unicode-xid 0.1.0 (registry+https://github.com/rust-lang/crates.io-index)" = "fc72304796d0818e357ead4e000d19c9c174ab23dc11093ac919054d20a6a7fc"
"checksum vcell 0.2.0 (git+https://github.com/perlindgren/vcell.git)" = "<none>"
"checksum version_check 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "914b1a6776c4c929a602fafd8bc742e06365d4bcbe48c30f9cca5824f70dc9dd"
"checksum volatile-register 0.3.0 (git+https://github.com/perlindgren/volatile-register.git)" = "<none>"
diff --git a/examples/eq_dfs_paper.rs b/examples/eq_dfs_paper.rs
new file mode 100644
index 0000000000000000000000000000000000000000..41da0120b5fb691a7d0ec9c83ac4432245be7773
--- /dev/null
+++ b/examples/eq_dfs_paper.rs
@@ -0,0 +1,254 @@
+#![allow(non_snake_case)]
+#![no_main]
+#![no_std]
+
+extern crate klee;
+extern crate panic_abort;
+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 = 1;
+const HORIZON: usize = (DISCREPANCY * 3 + 4) as usize;
+
+const T: bool = true;
+const F: bool = false;
+
+#[no_mangle]
+fn main() {
+ let mut DATA: [Data; HORIZON + 1] =
+ unsafe { core::mem::uninitialized() };
+ ksymbol!(&mut DATA, "DATA");
+
+ let mut STATE_H: [State; HORIZON + 1] =
+ unsafe { core::mem::uninitialized() };
+
+ let mut CNTR_H: [u32; HORIZON + 1] =
+ 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);
+ // }
+ // }
+ // }
+ // }
+
+ let mut is_visited = false;
+ match STATE {
+ S8004 | S8005 | S8014 => {
+ for j in 0..i {
+ if (STATE_H[i] == STATE_H[j]
+ && CNTR_H[i] == CNTR_H[j])
+ {
+ is_visited = true;
+ }
+ }
+ }
+ _ => {
+ for j in 0..i {
+ if (STATE_H[i] == STATE_H[j]) {
+ is_visited = true;
+ }
+ }
+ }
+ }
+
+ if is_visited {
+ break;
+ }
+
+ if i == HORIZON {
+ kassert!(false);
+ }
+
+ i += 1;
+ }
+}
+
+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 => match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => *STATE,
+ },
+ C003 => match (data.a, data.b) {
+ (F, F) => S8001,
+ _ => C003,
+ },
+ };
+}