search

rems-project / isla

Symbolic execution tool for Sail ISA specifications
Other
63 stars 10 forks source link

isla panics on an integer overflow during BL #15

Closed Trolldemorted closed 4 years ago

Trolldemorted commented 4 years ago

I have a BL instruction at 0x215F40 which should jump to 0x215F24, and I guess the arm model does that by doing a (wrapping) add to compute the (lower) address. This is completely valid, but overflowing arithmetics cause panics in rust's debug binaries:

thread '<unnamed>' panicked at 'attempt to add with overflow', isla-lib\src\concrete\bitvector64.rs:120:45
stack backtrace:
   0:     0x7ff72b55dd4f - backtrace::backtrace::trace_unsynchronized
                               at C:\Users\VssAdministrator\.cargo\registry\src\github.com-1ecc6299db9ec823\backtrace-0.3.46\src\backtrace\mod.rs:66
   1:     0x7ff72b55dd4f - std::sys_common::backtrace::_print_fmt
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\sys_common\backtrace.rs:78
   2:     0x7ff72b55dd4f - std::sys_common::backtrace::_print::{{impl}}::fmt
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\sys_common\backtrace.rs:59
   3:     0x7ff72b57476b - core::fmt::write
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libcore\fmt\mod.rs:1069
   4:     0x7ff72b55abcc - std::io::Write::write_fmt<std::sys::windows::stdio::Stderr>
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\io\mod.rs:1504
   5:     0x7ff72b560f2c - std::sys_common::backtrace::_print
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\sys_common\backtrace.rs:62
   6:     0x7ff72b560f2c - std::sys_common::backtrace::print
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\sys_common\backtrace.rs:49
   7:     0x7ff72b560f2c - std::panicking::default_hook::{{closure}}
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\panicking.rs:198
   8:     0x7ff72b560b6f - std::panicking::default_hook
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\panicking.rs:218
   9:     0x7ff72b561717 - std::panicking::rust_panic_with_hook
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\panicking.rs:511
  10:     0x7ff72b56129f - std::panicking::begin_panic_handler
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\panicking.rs:419
  11:     0x7ff72b572e00 - core::panicking::panic_fmt
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libcore\panicking.rs:111
  12:     0x7ff72b572d4c - core::panicking::panic
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libcore\panicking.rs:54
  13:     0x7ff72b26c14c - isla_lib::concrete::bitvector64::{{impl}}::add
                               at C:\Users\Benni\repositories\isla_orig\isla-lib\src\concrete\bitvector64.rs:120
  14:     0x7ff72b15163f - isla_lib::primop::add_bits<isla_lib::concrete::bitvector64::B64>
                               at C:\Users\Benni\repositories\isla_orig\isla-lib\src\primop.rs:147
  15:     0x7ff72b253dfb - isla_lib::executor::run_loop<isla_lib::concrete::bitvector64::B64>
                               at C:\Users\Benni\repositories\isla_orig\isla-lib\src\executor.rs:779
  16:     0x7ff72b250993 - isla_lib::executor::run<isla_lib::concrete::bitvector64::B64>
                               at C:\Users\Benni\repositories\isla_orig\isla-lib\src\executor.rs:652
  17:     0x7ff72b2517b2 - isla_lib::executor::do_work<isla_lib::concrete::bitvector64::B64,crossbeam_queue::seg_queue::SegQueue<core::result::Result<(isla_lib::executor::LocalFrame<isla_lib::concrete::bitvector64::B64>, isla_lib::smt::Checkpoint<isla_lib::concrete::bitvector64::B6
                               at C:\Users\Benni\repositories\isla_orig\isla-lib\src\executor.rs:1081
  18:     0x7ff72b2478f2 - isla_lib::executor::start_multi::{{closure}}::{{closure}}<isla_lib::concrete::bitvector64::B64,crossbeam_queue::seg_queue::SegQueue<core::result::Result<(isla_lib::executor::LocalFrame<isla_lib::concrete::bitvector64::B64>, isla_lib::smt::Checkpoint<isla_
                               at C:\Users\Benni\repositories\isla_orig\isla-lib\src\executor.rs:1139
  19:     0x7ff72b1d242e - crossbeam_utils::thread::{{impl}}::spawn::{{closure}}<closure-0,()>
                               at C:\Users\Benni\.cargo\registry\src\github.com-1ecc6299db9ec823\crossbeam-utils-0.7.2\src\thread.rs:415
  20:     0x7ff72b1d23af - crossbeam_utils::thread::{{impl}}::spawn::{{closure}}<closure-0,()>
                               at C:\Users\Benni\.cargo\registry\src\github.com-1ecc6299db9ec823\crossbeam-utils-0.7.2\src\thread.rs:423
  21:     0x7ff72b0adc40 - alloc::boxed::{{impl}}::call_mut<(),FnMut<()>>
                               at C:\Users\Benni\.rustup\toolchains\stable-x86_64-pc-windows-msvc\lib\rustlib\src\rust\src\liballoc\boxed.rs:1015
  22:     0x7ff72b1d25e3 - crossbeam_utils::thread::{{impl}}::spawn::{{closure}}<closure-0,()>
                               at C:\Users\Benni\.cargo\registry\src\github.com-1ecc6299db9ec823\crossbeam-utils-0.7.2\src\thread.rs:431
  23:     0x7ff72b108503 - std::sys_common::backtrace::__rust_begin_short_backtrace<closure-2,()>
                               at C:\Users\Benni\.rustup\toolchains\stable-x86_64-pc-windows-msvc\lib\rustlib\src\rust\src\libstd\sys_common\backtrace.rs:130
  24:     0x7ff72b208433 - std::thread::{{impl}}::spawn_unchecked::{{closure}}::{{closure}}<closure-2,()>
                               at C:\Users\Benni\.rustup\toolchains\stable-x86_64-pc-windows-msvc\lib\rustlib\src\rust\src\libstd\thread\mod.rs:475
  25:     0x7ff72b1d1b93 - std::panic::{{impl}}::call_once<(),closure-0>
                               at C:\Users\Benni\.rustup\toolchains\stable-x86_64-pc-windows-msvc\lib\rustlib\src\rust\src\libstd\panic.rs:318
  26:     0x7ff72b0f913b - std::panicking::try::do_call<std::panic::AssertUnwindSafe<closure-0>,()>
                               at C:\Users\Benni\.rustup\toolchains\stable-x86_64-pc-windows-msvc\lib\rustlib\src\rust\src\libstd\panicking.rs:331
  27:     0x7ff72b0f9327 - std::panicking::try::do_catch<std::panic::AssertUnwindSafe<closure-0>,()>
  28:     0x7ff72b0f8f5c - std::panicking::try<(),std::panic::AssertUnwindSafe<closure-0>>
                               at C:\Users\Benni\.rustup\toolchains\stable-x86_64-pc-windows-msvc\lib\rustlib\src\rust\src\libstd\panicking.rs:274
  29:     0x7ff72b1d1c13 - std::panic::catch_unwind<std::panic::AssertUnwindSafe<closure-0>,()>
                               at C:\Users\Benni\.rustup\toolchains\stable-x86_64-pc-windows-msvc\lib\rustlib\src\rust\src\libstd\panic.rs:394
  30:     0x7ff72b2082ac - std::thread::{{impl}}::spawn_unchecked::{{closure}}<closure-2,()>
                               at C:\Users\Benni\.rustup\toolchains\stable-x86_64-pc-windows-msvc\lib\rustlib\src\rust\src\libstd\thread\mod.rs:474
  31:     0x7ff72b1aa82e - core::ops::function::FnOnce::call_once<closure-0,()>
                               at C:\Users\Benni\.rustup\toolchains\stable-x86_64-pc-windows-msvc\lib\rustlib\src\rust\src\libcore\ops\function.rs:232
  32:     0x7ff72b563762 - alloc::boxed::{{impl}}::call_once
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\src\liballoc\boxed.rs:1008
  33:     0x7ff72b563762 - alloc::boxed::{{impl}}::call_once
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\src\liballoc\boxed.rs:1008
  34:     0x7ff72b563762 - std::sys::windows::thread::{{impl}}::new::thread_start
                               at /rustc/c7087fe00d2ba919df1d813c040a5d47e43b0fe7\/src\libstd\sys\windows\thread.rs:56
  35:     0x7ffb949e6fd4 - BaseThreadInitThunk
  36:     0x7ffb966dcec1 - RtlUserThreadStart

I fear all intentionally wrapping integer arithmetics have to be replaced with proper wrapping or calls to wrapping_add.

Alasdair commented 4 years ago

The only places we should be intentionally wrapping is where we are implementing sail bitvector addition/subtraction semantics which is only a few places fortunately.