Skip to content
Snippets Groups Projects
Commit 58e3a2f0 authored by Nils Fitinghoff's avatar Nils Fitinghoff
Browse files

dfs without the extra edges (for the comparison in the paper)

parent 1f3199bd
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Cargo.lock
+ 70
− 0
View file @ 58e3a2f0
......@@ -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>"
examples/eq_dfs_paper.rs 0 → 100644
+ 254
− 0
View file @ 58e3a2f0
#![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,
},
};
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment