Commit 543a2707 authored by Per Lindgren's avatar Per Lindgren

Initial commit

parents
Pipeline #75 failed with stages
/target
**/*.rs.bk
[[package]]
name = "cfg-if"
version = "0.1.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "cstr_core"
version = "0.1.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
"memchr 2.1.1 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "cty"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
[[package]]
name = "klee"
version = "0.1.0"
dependencies = [
"cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "memchr"
version = "2.1.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
dependencies = [
"cfg-if 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)",
"version_check 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)",
]
[[package]]
name = "version_check"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
[metadata]
"checksum cfg-if 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)" = "082bb9b28e00d3c9d39cc03e64ce4cea0f1bb9b3fde493f0cbc008472d22bdf4"
"checksum cstr_core 0.1.2 (registry+https://github.com/rust-lang/crates.io-index)" = "6ebe7158ee57e848621d24d0ed87910edb97639cb94ad9977edf440e31226035"
"checksum cty 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "c4e1d41c471573612df00397113557693b5bf5909666a8acb253930612b93312"
"checksum memchr 2.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "0a3eb002f0535929f1199681417029ebea04aadc0c7a4224b46be99c7f5d6a16"
"checksum version_check 0.1.5 (registry+https://github.com/rust-lang/crates.io-index)" = "914b1a6776c4c929a602fafd8bc742e06365d4bcbe48c30f9cca5824f70dc9dd"
[package]
name = "klee"
version = "0.1.0"
authors = ["Per Lindgren <per.lindgren@ltu.se>, Jorge Aparicio <jorge@japaric.io>"]
edition = "2018"
[dependencies]
cstr_core = "0.1.2"
# 1 minute introduction
## requirements
- docker
- nightly toolchain (nightly-2018-01-10)
## usage
``` console
$ systemctl start docker.service # if not already started/enabled
$ cargo install --path cargo-klee # add -f, if already installed
$ cd klee-examples
$ cargo klee --example foo --release
KLEE: output directory is "/mnt/target/release/examples/klee-out-0"
KLEE: Using STP solver backend
KLEE: ERROR: /home/pln/klee/klee-rust/klee/src/lib.rs:24: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 20
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
$ more target/release/examples/klee-out-0/test000001.abort.err
Error: abort failure
File: /home/pln/klee/klee-rust/klee/src/lib.rs
Line: 24
assembly.ll line: 76
Stack:
#000000076 in _ZN4core9panicking9panic_fmt17hc7d7358b749037fdE () at /home/pln/klee/klee-rust/klee/src/lib.rs:24
#100000070 in _ZN4core9panicking5panic17h4680eb5ae9b0e3d0E () at HOME/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/src/libcore/pani
cking.rs:51
#200000044 in main (=1, =94362321163792) at PWD/klee-examples/examples/foo.rs:22
```
The error found is at line 22.
``` rust
#![no_std]
#[macro_use]
extern crate klee;
use core::ptr;
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 // <- error found here is a Rust div 0 panic! .
}
```
\ No newline at end of file
use core::intrinsics;
use core::panic::PanicInfo;
#[panic_handler]
fn panic(_info: &PanicInfo) -> ! {
unsafe { intrinsics::abort() }
}
#![no_std]
#![feature(compiler_builtins_lib)]
#![feature(lang_items)]
#![feature(core_intrinsics)]
extern crate cstr_core;
// extern crate cty;
mod lang_items;
mod ll;
use core::mem;
use core::ffi::c_void;
#[doc(hidden)]
pub use cstr_core::CStr;
pub fn abort() -> ! {
unsafe { ll::abort() }
}
pub fn kassume(cond: bool) {
unsafe {
ll::klee_assume(cond);
}
}
#[doc(hidden)]
#[inline]
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
}
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(),
)
}
}
#[macro_export]
macro_rules! ksymbol {
($name:expr) => {
$crate::ksymbol(unsafe {
$crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes())
})
};
(&mut $id:ident, $name:expr) => {
$crate::kmksymbol(
unsafe { &mut $id },
unsafe { $crate::CStr::from_bytes_with_nul_unchecked(concat!($name, "\0").as_bytes()) }
)
}
}
#[macro_export]
macro_rules! kassert {
($e:expr) => {
if !$e {
$crate::abort();
}
}
}
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);
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment