Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
Loading items

Target

Select target project
  • pln/cargo-klee
  • markhakansson/cargo-klee
2 results
Select Git revision
Loading items
Show changes
Commits on Source (6)
Showing
with 196 additions and 808 deletions
{
"cSpell.ignoreWords": [
"Runtest",
"deps",
"is",
"istats",
"ktest",
"libc",
"llvm",
"muloti",
"rtlib",
"rustc"
]
}
\ No newline at end of file
# Changelog
## 2021-11-04
- added `KLEE` option `--disable-verify` to suppress [937](https://github.com/klee/klee/issues/937)
- added `clang` option `--rtlib=compiler-rt` to link `__muloti4`, see e.g., [295](https://github.com/android/ndk/issues/295)
\ No newline at end of file
[package]
name = "klee"
version = "0.2.0"
authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>"]
edition = "2018"
[dependencies]
cstr_core = "0.1.2"
[features]
klee-analysis = []
# Cargo subcommand `cargo klee` to compile Rust crates for KLEE analysis
# Cargo sub-command `cargo klee` to compile Rust crates for KLEE analysis
KLEE is a symbolic execution engine, based on the LLVM compiler infrastructure. KLEE generetes test cases aiming to cover (all) reachable paths of the input program. KLEE infers further checks for common program errors, e.g., out of bounds indexing and division by zero.
KLEE is a symbolic execution engine, based on the LLVM compiler infrastructure. KLEE generates test cases aiming to cover (all) reachable paths of the input program. KLEE infers further checks for common program errors, e.g., out of bounds indexing and division by zero.
Rust as being designed for safety, catches such errors and panics in precence of such faults. For analysis, a Rust `panic` implies an `abort`, which is detected as an error by KLEE, thus our `klee` tool spots potential panicing behavior of the application at hand.
Rust as being designed for safety, catches such errors and panics in presence of such faults. For analysis, a Rust `panic` implies an `abort`, which is detected as an error by KLEE, thus our `klee` tool spots potential `panic`ing behavior of the application at hand.
In effect, a Rust program passing KLEE analysis is thus ensured to be panic free at run-time, and thus the programmer may safely guide the Rust compiler to use unchecked operations (and thus improve the efficiency of the generated code), without jeopordizing memory safety and robustnes for programs. This holds in general for programs passing KLEE without panics, and in particular for operations checked by the KLEE run-time. In the latter case, unchecked operations can be fearlessly adopted, as it is sufficent to re-run KLEE if the source program is changed. In the general case of adopting unchecked operations safety can be
ensured by adding assertions to the source. If those assertions are condititonally compiled (e.g. under a `klee-analysis` feature) the assertions (and their implied overhead) will be omitted in a production build.
In effect, a Rust program passing KLEE analysis is thus ensured to be panic free at run-time. That granted, the programmer may safely guide the Rust compiler to use unchecked operations (and thus improve the efficiency of the generated code) without jeopardizing memory safety and robustness for the application at hand. This holds in general for programs passing KLEE without panics, and in particular for operations checked by the KLEE run-time. In the latter case, unchecked operations can be fearlessly adopted, as it is sufficient to re-run KLEE if the source program is changed. In the general case of adopting unchecked operations safety can be ensured by adding corresponding assertions to the source code. If those assertions are conditionally compiled (e.g. under a `klee-analysis` feature) the assertions (and their implied overhead) will be omitted in a production build.
## Requirements
- LLVM KLEE installed from recent package
- LLVM llc and clang for building replay binaries
- LLVM KLEE installed, (version 2.3pre, currently based on LLVM-v12).
- LLVM llc and clang for building replay binaries (currently based on LLVM-v12).
- GNU gdb for executing replay binaries
- nightly toolchain (edition-2018), tested with nightly-2019-01-25-x86_64-unknown-linux-gnu
- Rust tool-chain (edition-2018), tested with stable `rustc 1.56.1 (59eed8a2a 2021-11-01)`.
The `klee` tools (executables) needs to be installed and accessible in path, the KLEE libraries are assumed to be accessible under `/usr/lib`. The tool has been tested on the master branch of [KLEE](https://github.com/klee/klee) 2.3pre as of 2021-11-04, built under arch linux with the system LLVM (v12). You may use a custom install of KLEE, set the `LD_LIBRARY_PATH` to include the location of `kleeRuntest.so.1.0` (used by cargo-klee to dynamically link the library for replay of tests in gdb).
The `klee` tool needs to installed and accissible in path. The tool has been tested on the master branch of KLEE (https://github.com/klee/klee) as of Sun Nov 25 14:57:29 CET 2018, built under arch linux with the system LLVM (v7) using a modified aur recepie (https://aur.archlinux.org/packages/klee/), altered to refer `source` to the KLEE master branch.
## Limitations
## TODO
If the code under analysis is targeting another architecture (e.g., with other byte order or pointer size) the KLEE run-time system should be compiled for the target architecture to ensure compliance in between analysis and production code behavior. An ergonomic way of re-targeting KLEE has yet not been investigated. (This is not a Rust `klee` issue per-se, but rather a possible feature for further KLEE development.)
Currently only native KLEE is supported, we need to build a new docker with recent KLEE first in order to re-enable docker usage.
A Rust `no_std` application under linux will use the target triple `x86_64-unknown-linux-gnu` while KLEE uses the target triple `x86_64-pc-linux-gnu`, which renders a KLEE warning. To the best of our understanding both refers to the same (ABI) and thus the warning can be safely ignored.
If the code under analysis is targeting another architecture (e.g., with other byte order or pointer size) the KLEE run-time system should be compiled for the target architecture to ensure complience in between analysis and production code behavior. An ergonomic way of re-targeting KLEE has yet not been investigated. (This is not a Rust `klee` issue per-se, but rather a possible feature for further KLEE development.)
## usage
## Usage
``` console
$ cargo install --path cargo-klee # add -f, if already installed
> cargo install --path cargo-klee # add -f, if already installed
$ cd klee-examples
> cd klee-examples
$ cargo klee --help
cargo-klee 0.2.0
Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>
> cargo klee --help
cargo-klee 0.4.0
Lulea University of Technology (LTU)
KLEE analysis of Rust application
USAGE:
......@@ -45,7 +39,7 @@ FLAGS:
-g, --gdb Run the generated replay binary in `gdb`. The environment variable `GDB_CWD` determines the
`gdb` working directory, if unset `gdb` will execute in the current working directory
-h, --help Prints help information
-k, --klee Run KLEE test generatation [default enabled unless --replay]
-k, --klee Run KLEE test generation [default enabled unless --replay]
--release Build artifacts in release mode, with optimizations
-r, --replay Generate replay binary in target directory
-V, --version Prints version information
......@@ -56,19 +50,25 @@ OPTIONS:
--example <NAME> Build only the specified example
--features <FEATURES> Space-separated list of features to activate
> cargo klee --example get_sign
$ cargo klee --bin foo --release
....
KLEE: output directory is "/home/pln/rust/cargo-klee/klee-examples/target/release/deps/klee-out-5"
...
KLEE: Using Z3 solver backend
KLEE: ERROR: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 10
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
KLEE: done: total instructions = 89
KLEE: done: completed paths = 3
KLEE: done: partially completed paths = 0
KLEE: done: generated tests = 3
```
You may analyse code using either `--bin` and `--examples`. See `src/foo.rs` for a complete example for analysis and replay functionality.
\ No newline at end of file
You may analyse code using either `--bin` or `--examples`.
## Caveats
LLVM and `rustc` are both moving targets, and incompatibilities between versions of KLEE, LLVM and `rustc` may occur, and thus the tooling is somewhat fragile. The current release (0.4) has been tested on arch linux as of 2021-11-02 with the latest packages of `clang` and `llvm`. KLEE has been built from source to match the LLVM-12.
Cargo-klee compiles binaries without dependency to the Rust std library with the focus to verification of embedded applications.
## License
All rights reserved, use restricted for non-commercial purpose
[package]
authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.io>"]
authors = ["Lulea University of Technology (LTU)"]
name = "cargo-klee"
version = "0.2.0"
version = "0.4.0"
edition = "2018"
[dependencies]
libc = "0.2.33"
failure = "0.1.3"
cargo-project = "0.2.1"
either = "1.5.0"
clap = "2.32.0"
rustc_version = "0.2.3"
libc = "0.2.81"
failure = "0.1.8"
cargo-project = "0.2.4"
either = "1.6.1"
clap = "2.33.3"
rustc_version = "0.3.0"
......@@ -22,10 +22,10 @@ fn main() -> Result<(), failure::Error> {
fn run() -> Result<i32, failure::Error> {
let matches = App::new("cargo-klee")
.version("0.2.0")
.author("Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>")
.version("0.4.0")
.author("Lulea University of Technology (LTU)")
.about("KLEE analysis of Rust application")
// as this is used as a Cargo subcommand the first argument will be the name of the binary
// as this is used as a Cargo sub-command the first argument will be the name of the binary
// we ignore this argument
.arg(Arg::with_name("binary-name").hidden(true))
// TODO: custom target support (for now only target host is supported)
......@@ -83,7 +83,7 @@ fn run() -> Result<i32, failure::Error> {
Arg::with_name("klee")
.long("klee")
.short("k")
.help("Run KLEE test generatation [default enabled unless --replay]"),
.help("Run KLEE test generation [default enabled unless --replay]"),
)
.arg(
Arg::with_name("replay")
......@@ -124,7 +124,7 @@ fn run() -> Result<i32, failure::Error> {
// verbose output for debugging purposes
.arg("-v");
// set features, always inclidung `klee-analysis`
// set features, always including `klee-analysis`
if matches.is_present("all-features") {
cargo.arg("--all-features");
} else {
......@@ -207,6 +207,7 @@ fn run() -> Result<i32, failure::Error> {
}
// lookup the latest .ll file
// TODO: stable support for `metadata` from Cargo.
for e in fs::read_dir(path)? {
let e = e?;
let p = e.path();
......@@ -259,6 +260,7 @@ fn run() -> Result<i32, failure::Error> {
clang
.arg(obj)
.arg("--rtlib=compiler-rt")
.arg("-lkleeRuntest")
.args(&["-o", replay_name.to_str().unwrap()]);
......@@ -277,7 +279,8 @@ fn run() -> Result<i32, failure::Error> {
// klee analysis
if is_ktest || !is_replay {
let mut klee = Command::new("klee");
klee
// --disable-very to suppress know issue in klee https://github.com/klee/klee/issues/937
klee.arg("--disable-verify")
// ll file to analyse
.arg(ll.unwrap());
......
{
"cSpell.ignoreWords": [
"istats",
"ktest"
]
}
\ No newline at end of file
[package]
name = "klee-examples"
edition = "2018"
version = "0.2.0"
authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.io>"]
[dependencies]
klee = {git ="https://gitlab.henriktjader.com/pln/cargo-klee"}
#klee = {path =".."}
panic-abort = "0.3.1"
[dependencies.cortex-m]
version = "0.6.0"
# #features = ["inline-asm", "klee-analysis"]
[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"
[dependencies.stm32f413]
name = "cargo_klee_examples"
version = "0.3.0"
git = "https://gitlab.henriktjader.com/pln/stm32f413.git"
branch = "klee-analysis"
optional = true
[[examples]]
name = "gpioa"
path = "examples/gpioa.rs"
#required-features = ["klee-device"] # seem to work only in [[bin]]
[[bin]]
name = "foo"
path = "src/foo.rs"
[[bin]]
name = "register"
path = "src/register.rs"
authors = ["pln <Per Lindgren>"]
edition = "2018"
[[bin]]
name = "peripheral"
path = "src/peripheral.rs"
[dependencies.klee-sys]
git = "https://gitlab.henriktjader.com/pln/klee-sys.git"
version = "0.2.0"
[[bin]]
name = "clk"
path = "src/clk.rs"
[dependencies.panic-klee]
git = "https://gitlab.henriktjader.com/pln/panic-klee.git"
version = "0.1.0"
[[bin]]
name = "clk_simple"
path = "src/clk_simple.rs"
[features]
klee-analysis = ["klee-sys/klee-analysis"]
[profile.dev]
incremental = false
# lto = true
panic = "abort"
incremental = false # better optimization
lto = true # better optimization
codegen-units = 1 # better optimization
[profile.release]
debug = true
panic = "abort"
incremental = false
lto = true
debug = true # better debugging
incremental = false # better optimization
lto = true # better optimization
codegen-units = 1 # better optimization
[features]
klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis", "cortex-m/klee-analysis"]
klee-device = ["stm32f413/klee-analysis"]
// Testing a small Rust function.
// Inspired by `get_sign` https://klee.github.io/tutorials/testing-function/
// Here, we do not want to analyse the Rust run-time, thus `no_std`.
#![no_std]
#![no_main]
// Low level binding(s) to the KLEE API.
use klee_sys::klee_make_symbolic;
// Binding of Rust `panic` to KLEE `abort`.
use panic_klee as _;
fn get_sign(x: i32) -> i32 {
if x == 0 {
return 0;
}
if x < 0 {
return -1;
} else {
return 1;
}
}
// KLEE needs the non mangled `main` symbol.
#[no_mangle]
fn main() {
let mut a: i32 = 0;
klee_make_symbolic!(&mut a, "a");
get_sign(a);
}
// Compile a Rust program for KLEE test case generation.
//
// > cargo klee --examples get_sign
// ...
//
// KLEE: Using Z3 solver backend
//
// KLEE: done: total instructions = 89
// KLEE: done: completed paths = 3
// KLEE: done: generated tests = 3
//
// To view the generated tests:
//
// > ls target/debug/examples/klee-last/
// assembly.ll messages.txt run.stats test000002.ktest warnings.txt
// info run.istats test000001.ktest test000003.ktest
//
// > ktest-tool target/debug/examples/klee-last/test000001.ktest
// ktest file : 'target/debug/examples/klee-last/test000001.ktest'
// args : ['.../target/debug/examples/get_sign-<SOME_HASH>.ll']
// num objects: 1
// object 0: name: 'a'
// object 0: size: 4
// object 0: data: b'\x00\x00\x00\x80'
// object 0: hex : 0x00000080
// object 0: int : -2147483648
// object 0: uint: 2147483648
// object 0: text: ....
//
// (The order of test cases is non-deterministic, so your output might be different.)
//
// To replay test cases in `gdb`.
//
// > cargo klee --replay --gdb --example get_sign
// ...
// Reading symbols from get_sign.replay...
// (gdb) set environment KTEST_FILE=klee-last/test000001.ktest
// (gdb) break get_sign
// Breakpoint 1 at 0x555555555165: file examples/get_sign.rs, line 15.
// (gdb) run
// Breakpoint 1, get_sign::get_sign (x=-2147483648) at examples/get_sign.rs:15
// 15 if x == 0 {
// (gdb) next
// 18 if x < 0 {
// (gdb) next
// 19 return -1;
//
// The environment variable `GDB_CWD` determines the `gdb` working directory,
// if unset `gdb` will execute in the current working directory.
//
// For convenience the current working directory is set by default to coincide
// with the generated binary and KLEE tests.
//
// Problem shooting!!!
//
// For replay, the `kleeRuntest.so.1.0` library is dynamically linked.
// If not present in the default path you need to set `LD_LIBRARY_PATH` to include
// the location of this library.
//
// An error might look like this:
//
// (gdb) r
// Starting program: ...cargo-klee/klee-examples/target/debug/examples/get_sign.replay:
// error while loading shared libraries: libkleeRuntest.so.1.0:
// cannot open shared object file: No such file or directory
//
//! $ cargo klee --example gpioa --features klee-device
//!
#![no_std]
#![no_main]
extern crate cortex_m;
extern crate klee;
extern crate panic_abort;
extern crate stm32f413;
use cortex_m::peripheral::Peripherals;
#[no_mangle]
fn main() {
// accesss to core peripherals
let peripherals = Peripherals::take().unwrap();
let syst = peripherals.SYST;
// access to device peripherals
let p = stm32f413::Peripherals::take().unwrap();
let gpioa = p.GPIOA;
if gpioa.moder.read().bits() == 0 && syst.rvr.read() == 0 {
let _p = Peripherals::take().unwrap();
}
}
#![no_std]
#![no_main]
#[macro_use]
extern crate klee;
extern crate panic_abort;
extern crate volatile_register;
use volatile_register::RW;
#[no_mangle]
fn main() {
let rw: RW<u32> = unsafe { core::mem::uninitialized() };
unsafe {
rw.modify(|r| {
if r == 0 {
panic!(); // rust compiler calls panic abort
}
0
});
}
if rw.read() == 0 {
klee::kabort!(); // we directly call the intrinsic abort
}
}
#![no_std]
#![no_main]
extern crate klee;
extern crate panic_abort;
extern crate volatile_register;
use volatile_register::{RO, RW, WO};
#[no_mangle]
fn main() {
let rw: RW<u32> = unsafe { core::mem::uninitialized() };
let ro: RO<u32> = unsafe { core::mem::uninitialized() };
let wo: WO<u32> = unsafe { core::mem::uninitialized() };
unsafe { wo.write(2) };
if rw.read() == 0 {
unsafe {
rw.write(0);
}
if rw.read() == 0 {
panic!();
}
}
if ro.read() == 0 {
if ro.read() == 0 {
panic!();
}
}
}
#![no_std]
#![no_main]
extern crate cortex_m;
extern crate klee;
extern crate panic_abort;
use cortex_m::peripheral::Peripherals;
#[no_mangle]
fn main() {
// access to core peripherals
let peripherals = Peripherals::take().unwrap();
let syst = peripherals.SYST;
if syst.rvr.read() == 0 {
if syst.cvr.read() == 0x21 {
panic!();
}
}
}
#![no_std]
#![no_main]
#[macro_use]
extern crate klee;
extern crate panic_abort;
use klee::{kassert, kassume, ksymbol};
#[derive(Clone, Copy, Debug)]
pub struct CFGR {
hse: Option<u32>,
hclk: Option<u32>,
pclk1: Option<u32>,
pclk2: Option<u32>,
sysclk: Option<u32>,
usbclk: bool,
}
pub struct Requirements {
pllsrcclk: u32,
sysclk: u32,
usbclk: bool,
}
pub struct Unknowns {
pllp: u32,
pllm: u32,
plln: u32,
pllq: u32,
}
fn pll_derive(req: Requirements) -> Unknowns {
// assertions on requirements
kassert!(req.pllsrcclk % 1_000_000 == 0); // Multiple of 1MHz
kassert!(4_000_000 <= req.pllsrcclk && req.pllsrcclk <= 26_000_000); // Multiple of 1MHz
kassert!(req.sysclk % 1_000_000 == 0); // Multiple of 1MHz
// Sysclk output divisor must be one of 2, 4, 6 or 8
// (&!1 implies even numbers)
let pllp = core::cmp::min(8, (432_000_000 / req.sysclk) & !1);
let mut pllm: u32 = 0;
ksymbol!(&mut pllm, "pllm");
kassume(1 < pllm && pllm < 64); // field constraint
// Oscillator input constraint in the range from 1 to 2 MHz
kassume(1_000_000 <= req.pllsrcclk / pllm && req.pllsrcclk / pllm <= 2_000_000);
// Main scaler,
let plln = req.sysclk * pllp / (req.pllsrcclk / pllm);
assert!(50 <= plln && plln <= 432); // field constraint
// Oscillator output constraint
let osc = (req.pllsrcclk / pllm) * plln;
// 100MHz <= OSC <= 432MHz
kassume(100_000_000 <= osc && osc <= 432_000_000);
// 192MHz <= OSC <= 432MHz // for F401
// kassume(192_000_000 <= osc && osc <= 432_000_000);
// compute USB clock
// OSC / pllq = 48Mhz
let pllq = if req.usbclk {
let pllq = osc / 48_000_000;
kassume(osc / pllq == 48_000_000); // soundness
kassume(1 < pllq && pllq < 16); // field constraint
pllq
} else {
2 // set a valid value
};
// Calculate real system clock
let sysclk_real = osc / pllp;
kassume(sysclk_real == req.sysclk);
Unknowns {
pllp,
pllm,
plln,
pllq,
}
}
#[no_mangle]
fn main() {
let mut pllp: u32 = 0;
// let mut pll_in: u32 = 0;
let mut pllm: u32 = 0;
let mut plln: u32 = 0;
let mut pllq: u32 = 0;
ksymbol!(&mut pllp, "pllp");
// ksymbol!(&mut pll_in, "pll_in");
ksymbol!(&mut pllm, "pllm");
ksymbol!(&mut plln, "plln");
ksymbol!(&mut pllq, "pllq");
let req = Requirements {
pllsrcclk: 8_000_000,
sysclk: 96_000_000,
usbclk: true,
};
let u = pll_derive(req);
kassume(pllp == u.pllp);
// kassume(pll_in == u.pll_in);
kassume(pllm == u.pllm);
kassume(plln == u.plln);
kassume(pllq == u.pllq);
}
//! `cargo klee` will find several paths to aborts, but only one non-abort path.
//! This path contains a clock configuration that fulfills the requirements.
#![no_std]
#![no_main]
extern crate panic_abort;
use klee::{kassert, ksymbol};
#[derive(Clone, Copy, Debug)]
pub struct CFGR {
hse: Option<u32>,
hclk: Option<u32>,
pclk1: Option<u32>,
pclk2: Option<u32>,
sysclk: Option<u32>,
usbclk: bool,
}
pub struct Requirements {
pllsrcclk: u32,
sysclk: u32,
usbclk: bool,
}
pub struct Config {
pllp: u32,
pllm: u32,
plln: u32,
pllq: u32,
}
fn pll_check(c: Config, req: Requirements) {
// assertions on requirements
kassert!(req.pllsrcclk % 1_000_000 == 0); // Multiple of 1MHz
kassert!(4_000_000 <= req.pllsrcclk && req.pllsrcclk <= 26_000_000); // Multiple of 1MHz
kassert!(req.sysclk % 1_000_000 == 0); // Multiple of 1MHz
// Sysclk output divisor must be one of 2, 4, 6 or 8
// (&!1 implies even numbers)
kassert!(c.pllp == core::cmp::min(8, (432_000_000 / req.sysclk) & !1));
kassert!(1 < c.pllm && c.pllm < 64); // field constraint
// Oscillator input constraint in the range from 1 to 2 MHz
kassert!(1_000_000 <= req.pllsrcclk / c.pllm && req.pllsrcclk / c.pllm <= 2_000_000);
// Main scaler,
assert!(c.plln == req.sysclk * c.pllp / (req.pllsrcclk / c.pllm));
assert!(50 <= c.plln && c.plln <= 432); // field constraint
// Oscillator output constraint
let osc = (req.pllsrcclk / c.pllm) * c.plln;
// 100MHz <= OSC <= 432MHz
kassert!(100_000_000 <= osc && osc <= 432_000_000);
// compute USB clock
// OSC / pllq = 48Mhz
if req.usbclk {
kassert!(c.pllq == osc / 48_000_000);
kassert!(osc / c.pllq == 48_000_000); // soundness
kassert!(1 < c.pllq && c.pllq < 16); // field constraint
} else {
kassert!(c.pllq == 2); // set a valid value
};
// Calculate real system clock
let sysclk_real = osc / c.pllp;
kassert!(sysclk_real == req.sysclk);
}
#[no_mangle]
fn main() {
let mut pllp: u32 = 0;
let mut pllm: u32 = 0;
let mut plln: u32 = 0;
let mut pllq: u32 = 0;
ksymbol!(&mut pllp, "pllp");
ksymbol!(&mut pllm, "pllm");
ksymbol!(&mut plln, "plln");
ksymbol!(&mut pllq, "pllq");
let conf = Config {
pllp,
pllm,
plln,
pllq,
};
let req = Requirements {
pllsrcclk: 8_000_000,
sysclk: 96_000_000,
usbclk: true,
};
pll_check(conf, req);
}
//! Showcase how individual fields can be made symbolic
//! $ cargo klee --bin foo -r -k -g -v
//! ...
//! Reading symbols from register.replay...done.
//!
//! (gdb) set env KTEST_FILE=klee-last/test000001.ktest
//! (gdb) run # for the generated test the program will run to end
//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/debug/deps/foo.replay
//! [Inferior 1 (process 25074) exited with code 01]
//!
//! (gdb) set env KTEST_FILE=klee-last/test000002.ktest
//! (gdb) run # for the generated test the program will panic du to a division by zero, line 60
//! Starting program: /home/pln/rust/cargo-klee/klee-examples/target/debug/deps/foo.replay
//!
//! Program received signal SIGILL, Illegal instruction.
//! rust_begin_unwind (_info=0x7fffffffd9b8) at /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31
//! 31 unsafe { intrinsics::abort() }
//!
//! (gdb) backtrace
//! #0 rust_begin_unwind (_info=0x7fffffffd9b8) at /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/panic-abort-0.3.1/src/lib.rs:31
//! #1 0x000055555555530c in core::panicking::panic_fmt () at src/libcore/panicking.rs:85
//! #2 0x000055555555538b in core::panicking::panic () at src/libcore/panicking.rs:49
//! #3 0x0000555555555281 in foo::f2 (u=0) at src/foo.rs:60
//! #4 0x0000555555555234 in main () at src/foo.rs:51
//!
//! (gdb) frame 4
//! #4 0x0000555555555234 in main () at src/foo.rs:51
//! 51 let _ = f2(f1(u.a));
//!
//! //! (gdb) print u
//! $1 = foo::A {a: 255, b: 7}
#![no_std]
#![no_main]
#[macro_use]
extern crate klee;
extern crate panic_abort;
struct A {
a: u8,
b: u32,
}
#[no_mangle]
fn main() {
let mut a = 0;
ksymbol!(&mut a, "a");
let mut u = A { a: a, b: 0 };
u.b = 7;
let _ = f2(f1(u.a));
}
// add 1 wrapping instead of panic
fn f1(u: u8) -> u8 {
u.wrapping_add(1)
}
fn f2(u: u8) -> u8 {
100 / u
}
// > cargo klee --bin peripheral -r -k -g -v --release
// ...
// KLEE: done: total instructions = 33
// KLEE: done: completed paths = 1
// KLEE: done: generated tests = 1
//
// The example, has just one path, leading up to an abort.
// The reason is that the progam unconditionally will panic, as
// taking the peripheral is only only allowed once (for soundness).
// (Internally this in tracked by a state variable.)
//
// This is very good news, that KLEE will detect the error at compile time.
//
// Let's remove the error to see if the example code is correct.
// (comment out the second `take`)
//
// > cargo klee --bin peripheral -r -k -g -v --release
//
// KLEE: ERROR: src/peripheral.rs:104: divide by zero
// KLEE: NOTE: now ignoring this error at this location
//
// KLEE: done: total instructions = 85
// KLEE: done: completed paths = 2
// KLEE: done: generated tests = 2
//
//(gdb) shell ls klee-last
// assembly.ll info messages.txt run.istats run.stats test000001.div.err test000001.kquery test000001.ktest test000002.ktest warnings.txt
//
// So we see that test000001.ktest was causing a division error,
// the other test case passed
//
// (gdb) set env KTEST_FILE=klee-last/test000001.ktest
// (gdb) run
// ...
// Program received signal SIGFPE, Arithmetic exception.
// 0x00005555555551b0 in main () at src/peripheral.rs:104
// 104 let some_time_quota = unchecked_div(a, c - b);
//
// Let's look at the actual test
// (gdb) shell ktest-tool klee-last/test000001.ktest
// ktest file : 'klee-last/test000001.ktest'
// args : ['/home/pln/rust/cargo-klee/klee-examples/target/release/deps/peripheral-d1d6043ca4c81fef.ll']
// num objects: 5
// object 0: name: 'PRIMASK'
// 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: ....
// 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: ....
// object 2: name: 'vcell'
// object 2: size: 4
// object 2: data: b'\x00\x00\x00\x00'
// object 2: hex : 0x00000000
// object 2: int : 0
// object 2: uint: 0
// object 2: text: ....
// object 3: name: 'vcell'
// object 3: size: 4
// object 3: data: b'\x00\x00\x00\x00'
// object 3: hex : 0x00000000
// object 3: int : 0
// object 3: uint: 0
// object 3: text: ....
// object 4: name: 'vcell'
// object 4: size: 4
// object 4: data: b'\x00\x00\x00\x00'
// object 4: hex : 0x00000000
// object 4: int : 0
// object 4: uint: 0
// object 4: text: ....
//
// In order to analyze hardware dependent code, hardware access are treated
// as a new symbolic value. In `cortex-m` we give symbolic names to core peripherals.
// The svd2rust generated PAC is currently given the symbolic name `vcell`. This
// might in the future change to giving the address to the register instead.
//
// A breakdown of the example:
// Behind the scenes the PRIMASK register is accessed, and given concrete value.
// This access is along the happy path towards the error, so any value would
// suffice (in this case 0x00000000 was selected by KLEE).
//
// The first `vcell` access: was done when enabling the cycle counter.
// The rest of accesses stem from reading `a`, `b`, and `c`.
// Critical here is that KLEE spots that `(c - b) = 0`, leading up to a division
// by zero error (satisfied by `c` and `b` set to 0x00000000)
//
// Notice here, that this error is spotted EVEN while we are telling
// Rust to use the primitive (intrinsic) division for performance.
//
#![feature(core_intrinsics)] // we use intrinsic division
#![no_std]
#![no_main]
extern crate klee;
extern crate panic_abort;
extern crate cortex_m;
use cortex_m::peripheral::Peripherals;
use core::{intrinsics::unchecked_div, ptr::read_volatile};
#[no_mangle]
fn main() {
let peripherals = Peripherals::take().unwrap();
let mut dwt = peripherals.DWT;
dwt.enable_cycle_counter();
let a = dwt.cyccnt.read();
let b = dwt.cyccnt.read();
let c = dwt.cyccnt.read();
unsafe {
let some_time_quota = unchecked_div(a, c - b);
read_volatile(&some_time_quota); // prevent optization
}
}
// 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]
extern crate klee;
extern crate panic_abort;
extern crate volatile_register;
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!();
}
}
}
use core::intrinsics;
use core::panic::PanicInfo;
#[panic_handler]
fn panic(_info: &PanicInfo) -> ! {
unsafe { intrinsics::abort() }
}
#[lang = "eh_personality"]
extern "C" fn eh_personality() {}
#![no_std]
#![feature(compiler_builtins_lib)]
#![feature(lang_items)]
#![feature(core_intrinsics)]
extern crate cstr_core;
// #[cfg(feature = "klee-analysis")]
// mod lang_items;
#[cfg(feature = "klee-analysis")]
pub mod ll;
#[cfg(feature = "klee-analysis")]
use core::ffi::c_void;
#[doc(hidden)]
pub use cstr_core::CStr;
/// Aborts the path in KLEE mode, does nothing otherwise
#[macro_export]
macro_rules! kabort {
() => {
#[cfg(feature = "klee-analysis")]
unsafe { $crate::ll::abort() };
};
}
#[cfg(feature = "klee-analysis")]
pub fn kassume(cond: bool) {
unsafe {
ll::klee_assume(cond);
}
}
#[cfg(not(feature = "klee-analysis"))]
pub fn kassume(_cond: bool) {}
#[cfg(feature = "klee-analysis")]
pub fn kmksymbol<T>(t: &mut T, name: &'static CStr) {
unsafe {
ll::klee_make_symbolic(
t as *mut T as *mut c_void,
core::mem::size_of::<T>(),
name.as_ptr(),
)
}
}
#[cfg(not(feature = "klee-analysis"))]
pub fn kmksymbol<T>(_t: &mut T, _name: &'static CStr) {}
#[macro_export]
macro_rules! ksymbol {
(&mut $id:expr, $name:expr) => {
$crate::kmksymbol(unsafe { &mut $id }, unsafe {
$crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
})
};
}
/// If in KLEE mode, the assertion is made.
/// Otherwise, this is does nothing.
#[macro_export]
macro_rules! kassert {
($e:expr) => {
#[cfg(feature = "klee-analysis")]
{
if !$e {
$crate::kabort!();
}
}
};
}