Skip to content
Snippets Groups Projects
Select Git revision
  • d2d86753ad17672def15b186fc6f21a8c346ab20
  • master default protected
2 results

struct.rs

Blame
  • 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!