cargo-klee

cargo-klee/Cargo.lock

+[[package]]
+name = "cargo-klee"
+version = "0.1.0"
+dependencies = [
+ "libc 0.2.33 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
+[[package]]
+name = "libc"
+version = "0.2.33"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[metadata]
+"checksum libc 0.2.33 (registry+https://github.com/rust-lang/crates.io-index)" = "5ba3df4dcb460b9dfbd070d41c94c19209620c191b0340b929ce748a2bcd42d2"

cargo-klee/Cargo.toml

+[package]
+authors = ["Jorge Aparicio <jorge@japaric.io>"]
+name = "cargo-klee"
+version = "0.1.0"
+
+[dependencies]
+libc = "0.2.33"

cargo-klee/src/main.rs

+extern crate libc;
+
+use std::io::{self, Read, Write};
+use std::process::{Command, Stdio};
+use std::{env, str};
+
+fn main() {
+    // first argument is the path to this binary; the second argument is always "klee" -- both can
+    // be ignored
+    let args = env::args().skip(2).collect::<Vec<_>>();
+
+    // turn `cargo klee --example foo` into `xargo rustc --example foo -- (..)`
+    let mut c = Command::new("xargo");
+    c.arg("rustc")
+        .args(&args)
+        // verbose output for debugging purposes
+        .arg("-v")
+        .arg("--color=always")
+        .arg("--")
+        // ignore linking
+        .args(&["-C", "linker=true"])
+        // force LTO
+        .args(&["-C", "lto"])
+        // also output the LLVM-IR (.ll file) for debugging purposes
+        .arg("--emit=llvm-bc,llvm-ir")
+        // force panic=abort in all crates
+        .env("RUSTFLAGS", "-C panic=abort")
+        // collect stderr
+        .stderr(Stdio::piped());
+
+    // print full command for debugging purposes
+    eprintln!("{:?}", c);
+
+    // spawn process and drive it completion while replicating its stderr in ours
+    let mut p = c.spawn().unwrap();
+    let mut pstderr = p.stderr.take().unwrap();
+    let mut buf = [0; 1024];
+    let mut output = vec![];
+
+    let stderr = io::stderr();
+    let mut stderr = stderr.lock();
+    loop {
+        if let Ok(n) = pstderr.read(&mut buf) {
+            stderr.write(&buf[..n]).unwrap();
+            output.extend_from_slice(&buf[..n]);
+        }
+
+        if let Some(status) = p.try_wait().unwrap() {
+            assert!(status.success());
+            break;
+        }
+    }
+
+    // next we are going to try to run the .bc file using klee inside a docker container
+    // FIXME the way we find out which .bc file we have to use is pretty hacky; using Cargo as a
+    // library would be cleaner, I suppose
+
+    // find out the argument passed to `--example`, if used at all
+    let mut example = None;
+    let mut iargs = args.iter();
+    while let Some(arg) = iargs.next() {
+        if arg == "--example" {
+            example = iargs.next();
+            break;
+        }
+    }
+
+    // get the suffix of the example
+    let (example, suffix) = if let Some(example) = example {
+        let mut suffix = None;
+        let output = str::from_utf8(&output).unwrap();
+        for line in output.lines() {
+            if line.contains(&format!("examples/{}.rs", example)) {
+                for part in line.split(' ') {
+                    if part.starts_with("extra-filename=") {
+                        suffix = part.split('=').nth(1);
+                    }
+                }
+            }
+        }
+
+        (example, suffix.unwrap())
+    } else {
+        // nothing to do if the user didn't use `--example`
+        return;
+    };
+
+    let profile = if args.iter().any(|a| a == "--release") {
+        "release"
+    } else {
+        "debug"
+    };
+
+    let mut docker = Command::new("docker");
+    docker
+        .arg("run")
+        .arg("--rm")
+        .args(&["--user", &format!("{}:{}", uid(), gid())])
+        .args(&[
+            "-v",
+            &format!("{}:/mnt", env::current_dir().unwrap().display()),
+        ])
+        .args(&["-w", "/mnt"])
+        .arg("-it")
+        .arg("afoht/llvm-klee-4")
+        .args(&[
+            "/usr/bin/klee",
+            &format!("target/{}/examples/{}{}.bc", profile, example, suffix),
+        ]);
+
+    // print full command for debugging purposes
+    eprintln!("{:?}", docker);
+
+    assert!(docker.status().unwrap().success());
+}
+
+// NOTE from cross
+fn gid() -> u32 {
+    unsafe { libc::getgid() }
+}
+
+// NOTE from cross
+fn uid() -> u32 {
+    unsafe { libc::getuid() }
+}

cargo-klee/target/release/.fingerprint/cargo-klee-d43523cc68ba5454/bin-cargo_klee-d43523cc68ba5454

+52943ba1ed5d60f8
\ No newline at end of file

cargo-klee/target/release/.fingerprint/cargo-klee-d43523cc68ba5454/bin-cargo_klee-d43523cc68ba5454.json

+{"rustc":17623976161629326538,"features":"[]","target":1705371467523096570,"profile":1821645278138830359,"path":1036222786711178230,"deps":[["libc v0.2.33",6333674649589562741]],"local":[{"MtimeBased":[[1517186652,178668991],".fingerprint/cargo-klee-d43523cc68ba5454/dep-bin-cargo_klee-d43523cc68ba5454"]}],"rustflags":[]}
\ No newline at end of file

cargo-klee/target/release/.fingerprint/libc-b6e0c155bb2034af/lib-libc-b6e0c155bb2034af

+75bdae5b89bbe557
\ No newline at end of file

cargo-klee/target/release/.fingerprint/libc-b6e0c155bb2034af/lib-libc-b6e0c155bb2034af.json

+{"rustc":17623976161629326538,"features":"[\"default\", \"use_std\"]","target":5218373402463339046,"profile":1821645278138830359,"path":8945511764054114530,"deps":[],"local":[{"Precalculated":"0.2.33"}],"rustflags":[]}
\ No newline at end of file

cargo-klee/target/release/cargo-klee.d

+/home/pln/klee/klee-rust/cargo-klee/target/release/cargo-klee: /home/pln/klee/klee-rust/cargo-klee/src/main.rs

cargo-klee/target/release/deps/cargo_klee-d43523cc68ba5454.d

+/home/pln/klee/klee-rust/cargo-klee/target/release/deps/cargo_klee-d43523cc68ba5454: src/main.rs
+
+/home/pln/klee/klee-rust/cargo-klee/target/release/deps/cargo_klee-d43523cc68ba5454.d: src/main.rs
+
+src/main.rs:

cargo-klee/target/release/deps/libc-b6e0c155bb2034af.d

+/home/pln/klee/klee-rust/cargo-klee/target/release/deps/liblibc-b6e0c155bb2034af.rlib: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/lib.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/macros.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/dox.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/windows.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/redox/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/redox/net.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/uclibc/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/newlib/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/bsd/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/solaris/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/haiku/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/emscripten.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/android/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/musl/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/mips/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/s390x.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b32/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/aarch64.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/powerpc64.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/sparc64.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/x86_64.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/x32.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/not_x32.rs
+
+/home/pln/klee/klee-rust/cargo-klee/target/release/deps/libc-b6e0c155bb2034af.d: /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/lib.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/macros.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/dox.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/windows.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/redox/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/redox/net.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/uclibc/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/newlib/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/bsd/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/solaris/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/haiku/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/emscripten.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/android/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/musl/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/mips/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/s390x.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b32/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/mod.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/aarch64.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/powerpc64.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/sparc64.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/x86_64.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/x32.rs /home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/not_x32.rs
+
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/lib.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/macros.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/dox.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/windows.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/redox/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/redox/net.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/uclibc/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/newlib/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/bsd/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/solaris/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/haiku/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/emscripten.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/android/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/musl/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/mips/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/s390x.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b32/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/mod.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/aarch64.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/powerpc64.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/sparc64.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/x86_64.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/x32.rs:
+/home/pln/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.33/src/unix/notbsd/linux/other/b64/not_x32.rs:

cargo-klee/target/rls/.rustc_info.json

+{"rustc_fingerprint":13969051960857277561,"outputs":{"1164083562126845933":["rustc 1.32.0-nightly (00e03ee57 2018-11-22)\nbinary: rustc\ncommit-hash: 00e03ee57446d47667e5adba77fca8c13bfe7535\ncommit-date: 2018-11-22\nhost: x86_64-unknown-linux-gnu\nrelease: 1.32.0-nightly\nLLVM version: 8.0\n",""],"15337506775154344876":["___\nlib___.rlib\nlib___.so\nlib___.so\nlib___.a\nlib___.so\n/home/pln/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu\ndebug_assertions\nproc_macro\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"gnu\"\ntarget_family=\"unix\"\ntarget_feature=\"fxsr\"\ntarget_feature=\"mmx\"\ntarget_feature=\"sse\"\ntarget_feature=\"sse2\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"cas\"\ntarget_has_atomic=\"ptr\"\ntarget_os=\"linux\"\ntarget_pointer_width=\"64\"\ntarget_thread_local\ntarget_vendor=\"unknown\"\nunix\n",""],"1617349019360157463":["___\nlib___.rlib\nlib___.so\nlib___.so\nlib___.a\nlib___.so\n/home/pln/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu\ndebug_assertions\nproc_macro\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"gnu\"\ntarget_family=\"unix\"\ntarget_feature=\"fxsr\"\ntarget_feature=\"mmx\"\ntarget_feature=\"sse\"\ntarget_feature=\"sse2\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"cas\"\ntarget_has_atomic=\"ptr\"\ntarget_os=\"linux\"\ntarget_pointer_width=\"64\"\ntarget_thread_local\ntarget_vendor=\"unknown\"\nunix\n",""]},"successes":{}}
\ No newline at end of file

cargo-klee/target/rls/debug/.fingerprint/cargo-klee-c4d5658cd3f22ac9/test-bin-cargo_klee-c4d5658cd3f22ac9

+b088fa1b1e522975
\ No newline at end of file