Skip to content
Snippets Groups Projects
Commit 13126a20 authored by Per's avatar Per
Browse files

examples updated

parent ef1c8a79
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Cargo.lock
+ 288
− 1
View file @ 13126a20
# This file is automatically @generated by Cargo.
# It is not intended for manual editing.
[[package]]
name = "aligned"
version = "0.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "as-slice"
version = "0.1.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)",
"generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)",
"stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "autocfg"
version = "0.1.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "bare-metal"
version = "0.2.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"rustc_version 0.2.3 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "byteorder"
version = "1.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "cortex-m"
version = "0.6.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
"bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
"volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-rt"
version = "0.6.11"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"cortex-m-rt-macros 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)",
"r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-rt-macros"
version = "0.1.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
"quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
"syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-rtfm"
version = "0.5.1"
dependencies = [
"cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m-rt 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m-rtfm-macros 0.5.0",
"heapless 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)",
"rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-rtfm-macros"
version = "0.5.0"
dependencies = [
"proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
"quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
"rtfm-syntax 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
"syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cortex-m-semihosting"
version = "0.3.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cstr_core"
version = "0.1.2"
......@@ -14,21 +108,80 @@ name = "cty"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "generic-array"
version = "0.12.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "generic-array"
version = "0.13.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "hash32"
version = "0.1.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "heapless"
version = "0.5.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
"generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)",
"hash32 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "indexmap"
version = "1.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "klee-examples"
version = "0.1.0"
dependencies = [
"klee-sys 0.1.0",
"cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m-rtfm 0.5.1",
"cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)",
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
"lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)",
"panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
"panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)",
"vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
"volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "klee-sys"
version = "0.1.0"
source = "git+https://gitlab.henriktjader.com/pln/klee-sys.git#e3a296be9ce3376aa501dd60eefb3d0699506aef"
dependencies = [
"cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "lm3s6965"
version = "0.1.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)",
"cortex-m-rt 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "memchr"
version = "2.2.1"
......@@ -39,8 +192,142 @@ name = "panic-halt"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "panic-klee"
version = "0.1.0"
source = "git+https://gitlab.henriktjader.com/pln/panic-klee.git#3b0c897f49d7fff017424364e280bcb9dbaffa5d"
[[package]]
name = "proc-macro2"
version = "1.0.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "quote"
version = "1.0.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "r0"
version = "0.2.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "rtfm-core"
version = "0.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "rtfm-syntax"
version = "0.4.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"indexmap 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)",
"proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
"syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "rustc_version"
version = "0.2.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"semver 0.9.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "semver"
version = "0.9.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"semver-parser 0.7.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "semver-parser"
version = "0.7.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "stable_deref_trait"
version = "1.1.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "syn"
version = "1.0.11"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)",
"quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)",
"unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "typenum"
version = "1.11.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "unicode-xid"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "vcell"
version = "0.1.2"
source = "git+https://github.com/perlindgren/vcell.git?branch=trustit#29304497be5cf16aec53447473ff5a3f41783ba3"
dependencies = [
"klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)",
]
[[package]]
name = "volatile-register"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)",
]
[metadata]
"checksum aligned 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "eb1ce8b3382016136ab1d31a1b5ce807144f8b7eb2d5f16b2108f0f07edceb94"
"checksum as-slice 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "be6b7e95ac49d753f19cab5a825dea99a1149a04e4e3230b33ae16e120954c04"
"checksum autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "1d49d90015b3c36167a20fe2810c5cd875ad504b39cff3d4eae7977e6b7c1cb2"
"checksum bare-metal 0.2.5 (registry+https://github.com/rust-lang/crates.io-index)" = "5deb64efa5bd81e31fcd1938615a6d98c82eafcbcd787162b6f63b91d6bac5b3"
"checksum byteorder 1.3.2 (registry+https://github.com/rust-lang/crates.io-index)" = "a7c3dd8985a7111efc5c80b44e23ecdd8c007de8ade3b96595387e812b957cf5"
"checksum cortex-m 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)" = "145da2fc379bbd378ed425e75e1748214add9bbd800d4d5b77abb54ca423dbca"
"checksum cortex-m-rt 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)" = "33a716cd7d8627fae3892c2eede9249e50d2d79aedfb43ca28dad9a2b23876d9"
"checksum cortex-m-rt-macros 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "72b1073338d1e691b3b7aaf6bd61993e589ececce9242a02dfa5453e1b98918d"
"checksum cortex-m-semihosting 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)" = "113ef0ecffee2b62b58f9380f4469099b30e9f9cbee2804771b4203ba1762cfa"
"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 generic-array 0.12.3 (registry+https://github.com/rust-lang/crates.io-index)" = "c68f0274ae0e023facc3c97b2e00f076be70e254bc851d972503b328db79b2ec"
"checksum generic-array 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)" = "0ed1e761351b56f54eb9dcd0cfaca9fd0daecf93918e1cfc01c8a3d26ee7adcd"
"checksum hash32 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "d4041af86e63ac4298ce40e5cca669066e75b6f1aa3390fe2561ffa5e1d9f4cc"
"checksum heapless 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)" = "f339aa7d51777fc0af6aa7cbeb277dfc6e6c029cbdeda48d0fbb92c2337f0e69"
"checksum indexmap 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "712d7b3ea5827fcb9d4fda14bf4da5f136f0db2ae9c8f4bd4e2d1c6fde4e6db2"
"checksum klee-sys 0.1.0 (git+https://gitlab.henriktjader.com/pln/klee-sys.git)" = "<none>"
"checksum lm3s6965 0.1.3 (registry+https://github.com/rust-lang/crates.io-index)" = "8698042a7495160eac9f7298a32cd1ddbb6ad2780f766f5a99b4f0a6b915e0ad"
"checksum memchr 2.2.1 (registry+https://github.com/rust-lang/crates.io-index)" = "88579771288728879b57485cc7d6b07d648c9f0141eb955f8ab7f9d45394468e"
"checksum panic-halt 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "de96540e0ebde571dc55c73d60ef407c653844e6f9a1e2fdbd40c07b9252d812"
"checksum panic-klee 0.1.0 (git+https://gitlab.henriktjader.com/pln/panic-klee.git)" = "<none>"
"checksum proc-macro2 1.0.6 (registry+https://github.com/rust-lang/crates.io-index)" = "9c9e470a8dc4aeae2dee2f335e8f533e2d4b347e1434e5671afc49b054592f27"
"checksum quote 1.0.2 (registry+https://github.com/rust-lang/crates.io-index)" = "053a8c8bcc71fcce321828dc897a98ab9760bef03a4fc36693c231e5b3216cfe"
"checksum r0 0.2.2 (registry+https://github.com/rust-lang/crates.io-index)" = "e2a38df5b15c8d5c7e8654189744d8e396bddc18ad48041a500ce52d6948941f"
"checksum rtfm-core 0.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "9ec893edb2aa5b70320b94896ffea22a7ebb1cf3f942bb67cd5b60a865a63493"
"checksum rtfm-syntax 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)" = "4455e23c34df3d66454e7e218a4d76a7f83321d04a806be614463341cec4116e"
"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 stable_deref_trait 1.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "dba1a27d3efae4351c8051072d619e3ade2820635c3958d826bfea39d59b54c8"
"checksum syn 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)" = "dff0acdb207ae2fe6d5976617f887eb1e35a2ba52c13c7234c790960cdad9238"
"checksum typenum 1.11.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6d2783fe2d6b8c1101136184eb41be8b1ad379e4657050b8aaff0c79ee7575f9"
"checksum unicode-xid 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "826e7639553986605ec5979c7dd957c7895e93eabed50ab2ffa7f6128a75097c"
"checksum vcell 0.1.2 (git+https://github.com/perlindgren/vcell.git?branch=trustit)" = "<none>"
"checksum volatile-register 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)" = "0d67cb4616d99b940db1d6bd28844ff97108b498a6ca850e5b6191a532063286"
Cargo.toml
+ 1
− 0
View file @ 13126a20
......@@ -9,6 +9,7 @@ panic-halt = "0.2.0"
cortex-m-semihosting = "0.3.5"
lm3s6965 = "0.1.3"
vcell = "0.1.2"
volatile-register = "0.2.0"
[dependencies.panic-klee]
git = "https://gitlab.henriktjader.com/pln/panic-klee.git"
......
examples/klee_test.rs → examples/klee_hybrid_test.rs
+ 3
− 0
View file @ 13126a20
// example to show conditional compilation of hybrid applications
// compiling both for klee analysis and just as bare metal
//
#![no_std]
#![no_main]
......
examples/klee_only_test.rs 0 → 100644
+ 24
− 0
View file @ 13126a20
// example that shows different types of path termination
// and their effect to KLEE test case generation
#![no_std]
#![no_main]
use klee_sys::{klee_abort, klee_assert, klee_assert_eq, klee_make_symbolic};
use panic_klee as _;
#[no_mangle]
fn main() {
let mut a = 0;
klee_make_symbolic!(&mut a, "a");
match a {
0 => klee_abort!(),
1 => klee_abort!(),
2 => panic!(),
3 => panic!("3"), // just one instance of panic! will be spotted
4 => klee_assert!(false),
5 => klee_assert_eq!(false, true),
6 => klee_assert_eq!(false, true),
_ => (),
};
panic!("at end"); // just one instane of panic! will be spotted
}
examples/register_test.rs 0 → 100644
+ 105
− 0
View file @ 13126a20
// showcase volatile register
// This is the underlying abstraction to all register accesses using the
// embedded Rust ecosystem.
//
// When analyzed by KLEE, we make the return value symbolic, thus each access
// givs a new unique symbol. Even if we write a value to it, the next read
// will still be treated as a new symbol. That might be overly pessimistic
// but is a safe approximation for the worst case behavior of the hardware.
//
// > cargo klee --bin register --release
// ...
// KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.2/src/lib.rs:49: abort failure
// KLEE: NOTE: now ignoring this error at this location
// KLEE: done: total instructions = 33
// KLEE: done: completed paths = 3
// KLEE: done: generated tests = 3
//
// > ls target/release/deps/klee-last/
// assembly.ll info messages.txt run.istats run.stats test000001.ktest test000002.ktest test000003.abort.err test000003.kquery test000003.ktest warnings.txt
//
// We see that KLEE spoted the test3 hits unreachable (and thus panics)
//
// Let's look at the test cases separately:
//
// test1 passed:
// ktest-tool target/release/deps/klee-last/test000001.ktest
// ktest file : 'target/release/deps/klee-last/test000001.ktest'
// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
// num objects: 1
// object 0: name: 'vcell'
// object 0: size: 4
// object 0: data: b'\x00\x00\x00\x00'
// object 0: hex : 0x00000000
// object 0: int : 0
// object 0: uint: 0
// object 0: text: ....
// If the first read of the register is not 1 then we are ok.
//
// The second test also passed.
// ktest-tool target/release/deps/klee-last/test000002.ktest
// ktest file : 'target/release/deps/klee-last/test000002.ktest'
// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
// num objects: 2
// object 0: name: 'vcell'
// object 0: size: 4
// object 0: data: b'\x01\x00\x00\x00'
// object 0: hex : 0x01000000
// object 0: int : 1
// object 0: uint: 1
// object 0: text: ....
// object 1: name: 'vcell'
// object 1: size: 4
// object 1: data: b'\x00\x00\x00\x00'
// object 1: hex : 0x00000000
// object 1: int : 0
// object 1: uint: 0
// object 1: text: ....
// Here we are saved by the second reading of the register NOT giving
// returning 2.
//
// The third test gives the error.
// ktest-tool target/release/deps/klee-last/test000003.ktest
// ktest file : 'target/release/deps/klee-last/test000003.ktest'
// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/register-16afa0ec4812d3e4.ll']
// num objects: 2
// object 0: name: 'vcell'
// object 0: size: 4
// object 0: data: b'\x01\x00\x00\x00'
// object 0: hex : 0x01000000
// object 0: int : 1
// object 0: uint: 1
// object 0: text: ....
// object 1: name: 'vcell'
// object 1: size: 4
// object 1: data: b'\x02\x00\x00\x00'
// object 1: hex : 0x02000000
// object 1: int : 2
// object 1: uint: 2
// object 1: text: ....
//
// The first read gives 1, the second 2, and we hit unreacable.
#![no_std]
#![no_main]
use panic_klee as _;
use volatile_register::RW;
#[no_mangle]
fn main() {
// we emulate a read/write hardware register (rw)
let rw: RW<u32> = unsafe { core::mem::MaybeUninit::uninit().assume_init() };
// reading will render a symbolic value of type u32
if rw.read() == 1 {
// we emulate a write to the hardware register
unsafe { rw.write(0) };
// this read is still treated as a new symbolic value of type u32
if rw.read() == 2 {
unreachable!();
}
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment