From a6769d0ab79f6e4d8ae979a96efdd17f6fe7c1d3 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Tue, 8 Dec 2020 22:28:19 +0100
Subject: [PATCH] cargo klee 0.3.0
---
.vscode/settings.json | 10 +++
Cargo.toml | 12 ---
README.md | 57 ++++++-------
cargo-klee/Cargo.toml | 16 ++--
cargo-klee/src/main.rs | 9 +-
klee-examples/.vscode/settings.json | 6 ++
klee-examples/Cargo.toml | 76 +++++------------
klee-examples/examples/get_sign.rs | 82 +++++++++++++++++++
klee-examples/examples/gpioa.rs | 26 ------
klee-examples/examples/modify.rs | 27 ------
klee-examples/examples/registers.rs | 32 --------
klee-examples/examples/systick.rs | 21 -----
klee-examples/src/clk.rs | 111 -------------------------
klee-examples/src/clk_simple.rs | 99 ----------------------
klee-examples/src/foo.rs | 61 --------------
klee-examples/src/peripheral.rs | 123 ----------------------------
klee-examples/src/register.rs | 107 ------------------------
src/lang_items.rs | 10 ---
src/lib.rs | 73 -----------------
src/ll.rs | 7 --
20 files changed, 155 insertions(+), 810 deletions(-)
create mode 100644 .vscode/settings.json
delete mode 100644 Cargo.toml
create mode 100644 klee-examples/.vscode/settings.json
create mode 100644 klee-examples/examples/get_sign.rs
delete mode 100644 klee-examples/examples/gpioa.rs
delete mode 100644 klee-examples/examples/modify.rs
delete mode 100644 klee-examples/examples/registers.rs
delete mode 100644 klee-examples/examples/systick.rs
delete mode 100644 klee-examples/src/clk.rs
delete mode 100644 klee-examples/src/clk_simple.rs
delete mode 100644 klee-examples/src/foo.rs
delete mode 100644 klee-examples/src/peripheral.rs
delete mode 100644 klee-examples/src/register.rs
delete mode 100644 src/lang_items.rs
delete mode 100644 src/lib.rs
delete mode 100644 src/ll.rs
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000..a8a3442
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,10 @@
+{
+ "cSpell.ignoreWords": [
+ "deps",
+ "is",
+ "ktest",
+ "libc",
+ "llvm",
+ "rustc"
+ ]
+}
\ No newline at end of file
diff --git a/Cargo.toml b/Cargo.toml
deleted file mode 100644
index 9121070..0000000
--- a/Cargo.toml
+++ /dev/null
@@ -1,12 +0,0 @@
-[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 = []
-
diff --git a/README.md b/README.md
index 56fdc5b..48dc312 100644
--- a/README.md
+++ b/README.md
@@ -1,40 +1,34 @@
-# 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 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 `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, and thus 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 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 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 assertions to the source. 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
- 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 rustc 1.48.0 (7eac88abb 2020-11-16).
+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.2 as of 2020-12-08, built under arch linux with the system LLVM (v11).
-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.3.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,18 @@ 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 = 92
+KLEE: done: completed paths = 3
+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`.
+
+## License
+
+All rights reserved, use restricted for non-commercial purpose
diff --git a/cargo-klee/Cargo.toml b/cargo-klee/Cargo.toml
index 4341bf2..81d3da6 100644
--- a/cargo-klee/Cargo.toml
+++ b/cargo-klee/Cargo.toml
@@ -1,13 +1,13 @@
[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.3.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"
diff --git a/cargo-klee/src/main.rs b/cargo-klee/src/main.rs
index 92a81c7..c3b3c79 100644
--- a/cargo-klee/src/main.rs
+++ b/cargo-klee/src/main.rs
@@ -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.3.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")
@@ -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();
diff --git a/klee-examples/.vscode/settings.json b/klee-examples/.vscode/settings.json
new file mode 100644
index 0000000..1635b45
--- /dev/null
+++ b/klee-examples/.vscode/settings.json
@@ -0,0 +1,6 @@
+{
+ "cSpell.ignoreWords": [
+ "istats",
+ "ktest"
+ ]
+}
\ No newline at end of file
diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
index 47c4325..95801f2 100644
--- a/klee-examples/Cargo.toml
+++ b/klee-examples/Cargo.toml
@@ -1,68 +1,30 @@
[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/KLEE/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"]
diff --git a/klee-examples/examples/get_sign.rs b/klee-examples/examples/get_sign.rs
new file mode 100644
index 0000000..ede56f0
--- /dev/null
+++ b/klee-examples/examples/get_sign.rs
@@ -0,0 +1,82 @@
+// 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 = 92
+// 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 : ['/home/pln/courses/d7020e/cargo-klee/klee-examples/target/debug/examples/get_sign-672cfed85f9cca07.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: ....
+//
+// 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.
diff --git a/klee-examples/examples/gpioa.rs b/klee-examples/examples/gpioa.rs
deleted file mode 100644
index 39a9276..0000000
--- a/klee-examples/examples/gpioa.rs
+++ /dev/null
@@ -1,26 +0,0 @@
-//! $ 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();
- }
-}
diff --git a/klee-examples/examples/modify.rs b/klee-examples/examples/modify.rs
deleted file mode 100644
index eb22811..0000000
--- a/klee-examples/examples/modify.rs
+++ /dev/null
@@ -1,27 +0,0 @@
-#![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
- }
-}
diff --git a/klee-examples/examples/registers.rs b/klee-examples/examples/registers.rs
deleted file mode 100644
index 037ee4f..0000000
--- a/klee-examples/examples/registers.rs
+++ /dev/null
@@ -1,32 +0,0 @@
-#![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!();
- }
- }
-}
diff --git a/klee-examples/examples/systick.rs b/klee-examples/examples/systick.rs
deleted file mode 100644
index 2c77034..0000000
--- a/klee-examples/examples/systick.rs
+++ /dev/null
@@ -1,21 +0,0 @@
-#![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!();
- }
- }
-}
diff --git a/klee-examples/src/clk.rs b/klee-examples/src/clk.rs
deleted file mode 100644
index d8b689d..0000000
--- a/klee-examples/src/clk.rs
+++ /dev/null
@@ -1,111 +0,0 @@
-#![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);
-}
diff --git a/klee-examples/src/clk_simple.rs b/klee-examples/src/clk_simple.rs
deleted file mode 100644
index 5c5e5d3..0000000
--- a/klee-examples/src/clk_simple.rs
+++ /dev/null
@@ -1,99 +0,0 @@
-//! `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);
-}
diff --git a/klee-examples/src/foo.rs b/klee-examples/src/foo.rs
deleted file mode 100644
index 190c845..0000000
--- a/klee-examples/src/foo.rs
+++ /dev/null
@@ -1,61 +0,0 @@
-//! 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
-}
diff --git a/klee-examples/src/peripheral.rs b/klee-examples/src/peripheral.rs
deleted file mode 100644
index f451fb2..0000000
--- a/klee-examples/src/peripheral.rs
+++ /dev/null
@@ -1,123 +0,0 @@
-// > 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
- }
-}
diff --git a/klee-examples/src/register.rs b/klee-examples/src/register.rs
deleted file mode 100644
index f16ef61..0000000
--- a/klee-examples/src/register.rs
+++ /dev/null
@@ -1,107 +0,0 @@
-// 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!();
- }
- }
-}
diff --git a/src/lang_items.rs b/src/lang_items.rs
deleted file mode 100644
index 36ec0bd..0000000
--- a/src/lang_items.rs
+++ /dev/null
@@ -1,10 +0,0 @@
-use core::intrinsics;
-use core::panic::PanicInfo;
-
-#[panic_handler]
-fn panic(_info: &PanicInfo) -> ! {
- unsafe { intrinsics::abort() }
-}
-
-#[lang = "eh_personality"]
-extern "C" fn eh_personality() {}
diff --git a/src/lib.rs b/src/lib.rs
deleted file mode 100644
index 91976ba..0000000
--- a/src/lib.rs
+++ /dev/null
@@ -1,73 +0,0 @@
-#![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!();
- }
- }
- };
-}
diff --git a/src/ll.rs b/src/ll.rs
deleted file mode 100644
index e821d1f..0000000
--- a/src/ll.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-use core::ffi::c_void;
-
-extern "C" {
- pub fn abort() -> !;
- pub fn klee_assume(cond: bool);
- pub fn klee_make_symbolic(ptr: *mut c_void, size: usize, name: *const i8);
-}
--
GitLab