initial commit, paths broken

.gitignore

+/target
+**/*.rs.bk

Cargo.toml

+[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 = []
+

README.md

+# Cargo subcommand `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. The KLEE run-time 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.
+
+In effect, 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.
+
+## 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)
+
+The `klee` tool needs to installed and accissible in path. The tool has been tested on a 
+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.
+
+## TODO
+
+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
+
+``` console
+$ systemctl start docker.service # if not already started/enabled, docker is optional
+
+$ cargo install --path cargo-klee # add -f, if already installed
+
+$ cd klee-examples
+
+$ cargo klee --example foo --release
+
+KLEE: output directory is "/home/pln/rust/klee/klee-examples/target/release/examples/klee-out-0"
+KLEE: Using Z3 solver backend
+warning: Linking two modules of different target triples: klee_div_zero_check.bc' is 'x86_64-pc-linux-gnu' whereas 'target/release/examples/foo-cda2f387c054965f.ll' is 'x86_64-unknown-linux-gnu'
+
+KLEE: ERROR: /home/pln/rust/klee/src/lang_items.rs:6: abort failure
+KLEE: NOTE: now ignoring this error at this location
+
+KLEE: done: total instructions = 22
+KLEE: done: completed paths = 2
+KLEE: done: generated tests = 2
+```
+
+KLEE generates two test cases, we can view them by:
+
+``` sh
+$ ktest-tool target/release/examples/klee-last/test000001.ktest
+ktest file : 'target/release/examples/klee-last/test000001.ktest'
+args       : ['target/release/examples/foo-cda2f387c054965f.ll']
+num objects: 1
+object    0: name: b'u'
+object    0: size: 1
+object    0: data: b'\xff'
+
+$ ktest-tool target/release/examples/klee-last/test000002.ktest
+ktest file : 'target/release/examples/klee-last/test000002.ktest'
+args       : ['target/release/examples/foo-cda2f387c054965f.ll']
+num objects: 1
+object    0: name: b'u'
+object    0: size: 1
+object    0: data: b'\x00'
+```
+
+The first test triggers an error, we can view details by:
+
+``` sh
+$ more target/release/examples/klee-last/test000001.abort.err
+Error: abort failure
+File: /home/pln/rust/klee/src/lang_items.rs
+Line: 6
+assembly.ll line: 49
+Stack: 
+        #000000049 in _ZN4core9panicking9panic_fmt17h8e7152a45a601b4bE () at /home/pln/rust/klee/src/lang_items.rs:6
+        #100000055 in _ZN4core9panicking5panic17h9a94013c5e0723bbE () at /rustc/edaac35d67bed09260dc0c318acc5212fb66246e/src/libcore/panicking.rs:52
+        #200000023 in main () at /home/pln/rust/klee/klee-examples/examples/foo.rs:24
+```
+
+In this case it is the Rust built in division by zero detection that causes a `panic!`.
+
+The error found is at line 24.
+
+``` rust
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+#[no_mangle]
+fn main() {
+    let u = ksymbol!("u");
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    u.wrapping_add(1)
+}
+
+fn f2(u: u8) -> u8 {
+    100 / u // <- Rust div 0 panic! 
+}
+```
+
+The application is compiled for `#[no_std]` (thus isolating the application to dependencies of the environment). `extern crate klee` gives us access to the `klee` bindings. `ksymbol` marks the variable `u` as symbolic (unknown). `read_volatile(&T)` ensures that `T` is computed (and thus prevents the corresesponding code from being optimized out by the compiler).
+
+## Examples
+
+Further examples is found in the `klee-examples` directory.
+
+- `foo`, shows the above example.
+- `foo2`, shows further use of `ksymbol!(&mut T, &str)` for making declared variables symbolic.
\ No newline at end of file

cargo-klee/Cargo.toml

+[package]
+authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.io>"]
+name = "cargo-klee"
+version = "0.2.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"

cargo-klee/src/main.rs

+extern crate libc;
+
+use std::{
+    env, fs,
+    path::PathBuf,
+    process::{self, Command},
+    time::SystemTime,
+};
+
+use cargo_project::{Artifact, Profile, Project};
+use clap::{App, Arg};
+
+fn main() -> Result<(), failure::Error> {
+    match run() {
+        Ok(ec) => process::exit(ec),
+        Err(e) => {
+            eprintln!("error: {}", e);
+            process::exit(1)
+        }
+    }
+}
+
+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>")
+        .about("KLEE analysis of Rust application")
+        // as this is used as a Cargo subcommand 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)
+        // .arg(
+        //     Arg::with_name("target")
+        //         .long("target")
+        //         .takes_value(true)
+        //         .value_name("TRIPLE")
+        //         .help("Target triple for which the code is compiled"),
+        // )
+        .arg(
+            Arg::with_name("verbose")
+                .long("verbose")
+                .short("v")
+                .help("Use verbose output"),
+        )
+        .arg(
+            Arg::with_name("example")
+                .long("example")
+                .takes_value(true)
+                .value_name("NAME")
+                .required_unless("bin")
+                .conflicts_with("bin")
+                .help("Build only the specified example"),
+        )
+        .arg(
+            Arg::with_name("bin")
+                .long("bin")
+                .takes_value(true)
+                .value_name("NAME")
+                .required_unless("example")
+                .conflicts_with("example")
+                .help("Build only the specified binary"),
+        )
+        .arg(
+            Arg::with_name("release")
+                .long("release")
+                .help("Build artifacts in release mode, with optimizations"),
+        )
+        .arg(
+            Arg::with_name("features")
+                .long("features")
+                .takes_value(true)
+                .value_name("FEATURES")
+                .help("Space-separated list of features to activate"),
+        )
+        .arg(
+            Arg::with_name("all-features")
+                .long("all-features")
+                .takes_value(false)
+                .help("Activate all available features"),
+        )
+        // TODO, support additional parameters to KLEE
+        .arg(
+            Arg::with_name("klee")
+                .long("klee")
+                .short("k")
+                .help("Run KLEE test generatation [default enabled unless --replay]"),
+        )
+        .arg(
+            Arg::with_name("replay")
+                .long("replay")
+                .short("r")
+                .help("Generate replay binary in target directory"),
+        )
+        .arg(
+            Arg::with_name("gdb")
+                .long("gdb")
+                .short("g")
+                .help("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"),
+        )
+        .get_matches();
+
+    let is_example = matches.is_present("example");
+    let is_binary = matches.is_present("bin");
+    let verbose = matches.is_present("verbose");
+    let is_release = matches.is_present("release");
+    let is_replay = matches.is_present("replay");
+    let is_ktest = matches.is_present("ktest");
+    let is_gdb = matches.is_present("gdb");
+
+    // let target_flag = matches.value_of("target"); // not currently supported
+
+    // we rely on `clap` for either `example` or `bin`
+    let file = if is_example {
+        matches.value_of("example").unwrap()
+    } else {
+        matches.value_of("bin").unwrap()
+    };
+
+    // turn `cargo klee --example foo` into `cargo rustc --example foo -- (..)`
+    let mut cargo = Command::new("cargo");
+    cargo
+        // compile using rustc
+        .arg("rustc")
+        // verbose output for debugging purposes
+        .arg("-v");
+
+    // set features, always inclidung `klee-analysis`
+    if matches.is_present("all-features") {
+        cargo.arg("--all-features");
+    } else {
+        if let Some(features) = matches.value_of("features") {
+            let mut vec: Vec<&str> = features.split(" ").collect::<Vec<&str>>();
+            vec.push("klee-analysis");
+            cargo.args(&["--features", &vec.join(" ")]);
+        } else {
+            cargo.args(&["--features", "klee-analysis"]);
+        }
+    }
+
+    // select (single) application to compile
+    // derive basic settings from `cargo`
+    if is_example {
+        cargo.args(&["--example", file]);
+    } else {
+        cargo.args(&["--bin", file]);
+    }
+
+    // default is debug mode
+    if is_release {
+        cargo.arg("--release");
+    }
+
+    cargo
+        // enable shell coloring of result
+        .arg("--color=always")
+        .arg("--")
+        // ignore linking
+        .args(&["-C", "linker=true"])
+        // force LTO, to get a single oject file
+        .args(&["-C", "lto"])
+        // output the LLVM-IR (.ll file) for KLEE analysis
+        .arg("--emit=llvm-ir")
+        // force panic=abort in all crates, override .cargo settings
+        .env("RUSTFLAGS", "-C panic=abort");
+    // TODO, force `incremental=false`, `codegen-units=1`?
+
+    if verbose {
+        eprintln!("\n{:?}\n", cargo);
+    }
+
+    // execute the command and unwrap the result into status
+    let status = cargo.status()?;
+
+    if !status.success() {
+        return Ok(status.code().unwrap_or(1));
+    }
+
+    let cwd = env::current_dir()?;
+
+    let meta = rustc_version::version_meta()?;
+    let host = meta.host;
+
+    let project = Project::query(cwd)?;
+
+    let profile = if is_release {
+        Profile::Release
+    } else {
+        Profile::Dev
+    };
+
+    let mut path: PathBuf = if is_example {
+        project.path(Artifact::Example(file), profile, None, &host)?
+    } else {
+        project.path(Artifact::Bin(file), profile, None, &host)?
+    };
+
+    // llvm-ir file
+    let mut ll = None;
+    // most recently modified
+    let mut mrm = SystemTime::UNIX_EPOCH;
+    let prefix = format!("{}-", file.replace('-', "_"));
+
+    path = path.parent().expect("unreachable").to_path_buf();
+
+    if is_binary {
+        path = path.join("deps"); // the .ll file is placed in ../deps
+    }
+
+    // lookup the latest .ll file
+    for e in fs::read_dir(path)? {
+        let e = e?;
+        let p = e.path();
+
+        if p.extension().map(|e| e == "ll").unwrap_or(false) {
+            if p.file_stem()
+                .expect("unreachable")
+                .to_str()
+                .expect("unreachable")
+                .starts_with(&prefix)
+            {
+                let modified = e.metadata()?.modified()?;
+                if ll.is_none() {
+                    ll = Some(p);
+                    mrm = modified;
+                } else {
+                    if modified > mrm {
+                        ll = Some(p);
+                        mrm = modified;
+                    }
+                }
+            }
+        }
+    }
+
+    let mut obj = ll.clone().unwrap();
+    let replay_name = obj.with_file_name(file).with_extension("replay");
+
+    // replay compilation
+    if is_replay {
+        // compile to object code for replay using `llc`
+        let mut llc = Command::new("llc");
+        llc.arg("-filetype=obj")
+            .arg("-relocation-model=pic")
+            .arg(ll.clone().unwrap());
+
+        if verbose {
+            eprintln!("\n{:?}\n", llc);
+        }
+
+        // TODO: better error handling, e.g., if `llc` is not installed/in path
+        let status = llc.status()?;
+        if !status.success() {
+            println!("llc failed: {:?}", status.code().unwrap_or(1));
+        } else {
+            // compile to executable for replay using `clang`
+            let mut clang = Command::new("clang");
+
+            obj = obj.with_extension("o");
+
+            clang
+                .arg(obj)
+                .arg("-lkleeRuntest")
+                .args(&["-o", replay_name.to_str().unwrap()]);
+
+            if verbose {
+                eprintln!("\n{:?}\n", clang);
+            }
+
+            // TODO: better error handling, e.g., if `clang` in not installed/in path
+            let status = clang.status()?;
+            if !status.success() {
+                println!("clang failed: {:?}", status.code().unwrap_or(1));
+            }
+        }
+    }
+
+    // klee analysis
+    if is_ktest || !is_replay {
+        let mut klee = Command::new("klee");
+        klee
+            // ll file to analyse
+            .arg(ll.unwrap());
+
+        // execute the command and unwrap the result into status
+        let status = klee.status()?;
+        if !status.success() {
+            return Ok(status.code().unwrap_or(1));
+        }
+    }
+
+    // replay execution in `gdb`
+    if is_gdb {
+        let mut gdb = Command::new("gdb");
+        if let Ok(cwd) = env::var("GDB_CWD") {
+            // set gdb current dir to `GDB_CWD`
+            gdb.current_dir(cwd);
+            // set replay name to be loaded by `gdb`
+            gdb.arg(replay_name);
+        } else {
+            // set gdb current dir to the target directory
+            gdb.current_dir(replay_name.parent().unwrap());
+            // set replay name to be loaded by gdb
+            gdb.arg(replay_name.file_name().unwrap());
+        };
+
+        if verbose {
+            eprintln!("\n{:?}\n", gdb);
+        }
+
+        // TODO: better error handling, e.g., if `gdb` is not installed/in path
+        let status = gdb.status()?;
+        if !status.success() {
+            println!("gdb failed: {:?}", status.code().unwrap_or(1));
+        }
+    }
+    // return to shell without error
+    Ok(0)
+}

klee-examples/Cargo.toml

+[package]
+name = "klee-examples"
+version = "0.2.0"
+authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>"]
+
+[dependencies]
+klee = {path=".."}
+#panic-abort = "0.3.1"
+
+[dependencies.volatile-register]
+#branch = "klee-analysis"
+version = "0.3.0"
+features = ["klee-analysis"]
+
+[patch.crates-io]
+#[replace]
+"volatile-register" = { path = "../../klee/volatile-register/" }
+
+# [dependencies.cortex-m]
+# version = "0.6.0"
+# #features = ["inline-asm", "klee-analysis"]
+
+# [dependencies.stm32f413]
+# version = "0.3.0"
+# path = "../stm32f413"
+
+#[patch.crates-io]
+#cortex-m = { path = "../cortex-m" }
+#volatile-register = { version = "0.3.0", path = "../volatile-register" }
+
+
+[[bin]]
+name = "main"
+path = "src/main.rs"
+
+[[bin]]
+name = "main2"
+path = "src/main2.rs"
+
+[profile.dev]
+incremental = false
+# lto = true
+
+[profile.release]
+debug = true
+panic = "abort"
+lto = true
+
+[features]
+#klee-analysis = ["stm32f413/klee-analysis", "cortex-m/klee-analysis", "klee/klee-analysis"]
+klee-analysis = ["klee/klee-analysis", "volatile-register/klee-analysis"]
+#klee-replay = ["klee/klee-replay"]
+#dummy1 = [] 
+#dummy2 = []
+#default = ["klee-analysis"]
\ No newline at end of file

klee-examples/src/main.rs

+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+use core::ptr;
+
+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 };
+
+    unsafe {
+        ptr::read_volatile(&f2(f1(u.a)));
+    }
+}
+
+// add 1 wrapping
+fn f1(u: u8) -> u8 {
+    u.wrapping_add(1)
+}
+
+fn f2(u: u8) -> u8 {
+    100 / u
+}

klee-examples/src/main2.rs

+//! showcase volatile register
+
+#![no_std]
+#![no_main]
+
+#[macro_use]
+extern crate klee;
+
+extern crate volatile_register;
+use volatile_register::RO;
+
+#[no_mangle]
+fn main() {
+    let rw: RO<u32> = unsafe { core::mem::uninitialized() };
+
+    if rw.read() == 0 {
+        if rw.read() == 0 {
+            panic!();
+        }
+    }
+}

src/lang_items.rs

+use core::intrinsics;
+use core::panic::PanicInfo;
+
+#[panic_handler]
+fn panic(_info: &PanicInfo) -> ! {
+    unsafe { intrinsics::abort() }
+}
+
+#[lang = "eh_personality"]
+extern "C" fn eh_personality() {}

src/lib.rs

+#![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;
+
+use core::mem;
+
+#[cfg(feature = "klee-analysis")]
+use core::ffi::c_void;
+
+#[doc(hidden)]
+pub use cstr_core::CStr;
+
+#[cfg(feature = "klee-analysis")]
+#[inline(always)]
+pub fn abort() -> ! {
+    unsafe { ll::abort() }
+}
+
+#[cfg(not(feature = "klee-analysis"))]
+pub fn abort() -> ! {
+    panic!(); // leads to the defined panic handler
+}
+
+#[cfg(feature = "klee-analysis")]
+pub fn kassume(cond: bool) {
+    unsafe {
+        ll::klee_assume(cond);
+    }
+}
+
+#[cfg(not(feature = "klee-analysis"))]
+pub fn kassume(_cond: bool) {}
+
+#[doc(hidden)]
+#[inline]
+#[cfg(feature = "klee-analysis")]
+pub fn ksymbol<T>(name: &CStr) -> T {
+    let mut t: T = unsafe { mem::uninitialized() };
+    unsafe {
+        ll::klee_make_symbolic(
+            &mut t as *mut T as *mut c_void,
+            mem::size_of::<T>(),
+            name.as_ptr(),
+        )
+    }
+    t
+}
+
+#[cfg(not(feature = "klee-analysis"))]
+pub fn ksymbol<T>(_name: &CStr) -> T {
+    unsafe { mem::uninitialized() }
+}
+
+#[cfg(feature = "klee-analysis")]
+pub fn kmksymbol<T>(t: &mut T, name: &CStr) {
+    unsafe {
+        ll::klee_make_symbolic(
+            t as *mut T as *mut c_void,
+            mem::size_of::<T>(),
+            name.as_ptr(),
+        )
+    }
+}
+
+#[cfg(not(feature = "klee-analysis"))]
+pub fn kmksymbol<T>(_t: &mut T, _name: &CStr) {}
+
+#[macro_export]
+macro_rules! ksymbol {
+    ($name:expr) => {
+        $crate::ksymbol(unsafe {
+            $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
+        })
+    };
+    (&mut $id:expr, $name:expr) => {
+        $crate::kmksymbol(unsafe { &mut $id }, unsafe {
+            $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
+        })
+    };
+}
+
+#[cfg(feature = "klee-analysis")]
+#[macro_export]
+macro_rules! kassert {
+    ($e:expr) => {
+        if !$e {
+            $crate::abort();
+        }
+    };
+}
+
+#[cfg(not(feature = "klee-analysis"))]
+#[macro_export]
+macro_rules! kassert {
+    ($e:expr) => {};
+}

src/ll.rs

+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);
+}