Select Git revision
Forked from
Per Lindgren / klee-examples
Source project has a limited visibility.
struct.rs 2.33 KiB
// showcase partially symbolic structures
#![no_std]
#![no_main]
use klee_sys::*;
use panic_klee as _;
struct A {
a: u8,
b: u32,
}
#[no_mangle]
fn main() {
let mut a = 0;
klee_make_symbolic!(&mut a, "a");
let mut u = A { a: a, b: 0 };
u.b = 7;
let _ = f2(f1(u.a));
}
fn f1(u: u8) -> u8 {
u.wrapping_add(1)
}
fn f2(u: u8) -> u8 {
100 / u
}
// Often we may have structures with partially unknown data.
//
// Let us find out what valu of `u` that may cause a ponic by replay in gdb.
//
// > cargo klee --example struct -k -g -r
//
// KLEE: ERROR: /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8: abort failure
// KLEE: NOTE: now ignoring this error at this location
//
// KLEE: done: total instructions = 175
// KLEE: done: completed paths = 2
// KLEE: done: generated tests = 2
// ...
// Reading symbols from struct.replay...
// (gdb) set env KTEST_FILE=klee-last/test000001.ktest
// (gdb) run
// Starting program: /home/pln/rust/trustit/klee-examples/target/debug/examples/struct.replay
// [Inferior 1 (process 114832) exited with code 0144]
// (gdb) set env KTEST_FILE=klee-last/test000002.ktest
// (gdb) run
// Starting program: /home/pln/rust/trustit/klee-examples/target/debug/examples/struct.replay
// Program received signal SIGABRT, Aborted.
// 0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
// (gdb) bt
// #0 0x00007ffff7dd3f25 in raise () from /usr/lib/libc.so.6
// #1 0x00007ffff7dbd897 in abort () from /usr/lib/libc.so.6
// #2 0x000055555555533b in rust_begin_unwind (_info=0x7fffffffd308) at /home/pln/.cargo/git/checkouts/panic-klee-aa8d015442188497/3b0c897/src/lib.rs:8
// #3 0x000055555555529d in core::panicking::panic_fmt () at src/libcore/panicking.rs:139
// #4 0x0000555555555309 in core::panicking::panic () at src/libcore/panicking.rs:70
// #5 0x000055555555526d in struct::f2 (u=0) at examples/struct.rs:28
// #6 0x000055555555520f in main () at examples/struct.rs:20
//
// So it's f2(u=0) that crashes.
// Let us take a look at frame 6, calling f2(f1(u.a)).
//
// (gdb) f 6
// #6 0x000055555555520f in main () at examples/struct.rs:20
// 20 let _ = f2(f1(u.a));
// (gdb) i locals
// u = struct::A {a: 255, b: 7}
// a = 255
//
// So in this cose u.a = 255, causes a wraparound, and that in turn causes the crash.
// Not obvious to the naked eye.
// This is the way!