Add option --stack-trace to print the stack trace of a failure

[celinval]

Requested feature: Enable Kani to print stack traces when a failure occur
Use case: Debugging failures can be very painful, especially for things that cannot be easily reproduced with concrete playback or very generic errors such as unwrap() on None value. Providing a stack trace of a failure can really help narrow down the exact location of a failure.

Test case: Debugging the following harness from this PR:

    #[kani::proof_for_contract(copy_nonoverlapping)]
    fn check_copy_nonoverlapping() {
        run_with_arbitrary_ptrs::<char>(|src, dst| unsafe {
            copy_nonoverlapping(src, dst, kani::any())
        });
    }

    fn run_with_arbitrary_ptrs<T: Arbitrary>(harness: impl Fn(*mut T, *mut T)) {
        let mut generator1 = PointerGenerator::<100>::new();
        let mut generator2 = PointerGenerator::<100>::new();
        let ArbitraryPointer {
            ptr: src,
            status: src_status,
            ..
        } = generator1.any_alloc_status::<T>();
        let ArbitraryPointer {
            ptr: dst,
            status: dst_status,
            ..
        } = if kani::any() {
            generator1.any_alloc_status::<T>()
        } else {
            generator2.any_alloc_status::<T>()
        };
        kani::assume(supported_status(src_status));
        kani::assume(supported_status(dst_status));
        harness(src, dst);
    }

I was getting the following failure:

Checking harness intrinsics::verify::check_copy_nonoverlapping...

VERIFICATION RESULT:
 ** 1 of 856 failed (3 unreachable)
Failed Checks: Only a single top-level call to function _RNCNCINvNtCsf4mLL5B4Lhf_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_ when checking contract _RNCNCINvNtCsf4mLL5B4Lhf_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_
2024-11-02T01:43:52.2508870Z  File: "/Users/runner/work/verify-rust-std/verify-rust-std/head/library/core/src/intrinsics.rs", line 3311, in _RNCNCINvNtCsf4mLL5B4Lhf_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_

VERIFICATION:- FAILED

This is pointing to the #[modifies] clause in the contract, which is the following:

#[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]

Concrete playback wouldn't help me in this one since the modifies clause is an artifact of contract checking. The failure is also very CBMC instrumentation specific, which doesn't help at all. I tried the trace / visualize, but I got a trace with over 3000 steps. 😞

The best way I found to narrow this down was to use the --stack-trace option from CBMC, however, the trace is all mangled and hard to parse. It would be fantastic if Kani could provide a more user friendly trace here.

[celinval]

BTW, here is the stack trace I got back:

Trace for _RNCNCINvNtCs7zWGgSDH9R5_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_.single_top_level_call.1:
  assertion failure file /tmp/workspace/kani-project/verify-std/library/core/src/intrinsics.rs line 3311 column 18 function _RNCNCINvNtCs7zWGgSDH9R5_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_
  _RNCNCINvNtCs7zWGgSDH9R5_4core10intrinsics19copy_nonoverlappinghEs0_0s_0B8_(&__kani_modifies_copy_nonoverlapping!0@2, { .0={ .data=(unsigned char *)((char *)&[email protected] + 76), .len=sizeof(int) /*4ul*/  } }, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/library/core/src/intrinsics.rs line 3311 column 18 function intrinsics::copy_nonoverlapping::<u8>::{closure#2}
  _RNCINvNtCs7zWGgSDH9R5_4core10intrinsics19copy_nonoverlappinghEs0_0B6_(&var_1!0@2, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/library/core/src/intrinsics.rs:3311:18: 3311:78} as ops::function::FnOnce<()>>::call_once
  _RNvYNCINvNtCs7zWGgSDH9R5_4core10intrinsics19copy_nonoverlappinghEs0_0INtNtNtB9_3ops8function6FnOnceuE9call_onceB9_({ .0=&count!0@2, .1=&src!0@2, .2=&dst!0@2 }, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/library/core/src/intrinsics.rs:3311:18: 3311:78}>
  _RINvNvNtCs7zWGgSDH9R5_4core10intrinsics19copy_nonoverlapping22kani_register_contractuNCIB2_hEs0_0EB6_({ .0=&count!0@2, .1=&src!0@2, .2=&dst!0@2 }, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/library/core/src/intrinsics.rs line 3311 column 18 function intrinsics::copy_nonoverlapping::<u8>
  _RINvNtCs7zWGgSDH9R5_4core10intrinsics19copy_nonoverlappinghEB4_((unsigned char *)&src!0@2, (unsigned char *)((char *)&[email protected] + 76), sizeof(int) /*4ul*/ , ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/library/core/src/ptr/mod.rs line 1740 column 9 function ptr::write_unaligned::<char>
  _RINvNtCs7zWGgSDH9R5_4core3ptr15write_unalignedcEB4_((signed int *)((char *)&[email protected] + 76), -1, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/library/core/src/ptr/mut_ptr.rs line 1446 column 18 function ptr::mut_ptr::<impl *mut char>::write_unaligned
  _RNvMNtNtCs7zWGgSDH9R5_4core3ptr7mut_ptrOc15write_unalignedB6_((signed int *)((char *)&[email protected] + 76), -1, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/kani_build/library/kani_core/src/arbitrary/pointer.rs line 338 column 30 function kani::arbitrary_ptr::PointerGenerator::<100>::create_in_bounds_ptr::<char>
  _RINvMNtNtCs7zWGgSDH9R5_4core4kani13arbitrary_ptrINtB3_16PointerGeneratorKj64_E20create_in_bounds_ptrcEB7_(&generator1!0@1, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/kani_build/library/kani_core/src/arbitrary/pointer.rs line 277 column 32 function kani::arbitrary_ptr::PointerGenerator::<100>::any_alloc_status::<char>
  _RINvMNtNtCs7zWGgSDH9R5_4core4kani13arbitrary_ptrINtB3_16PointerGeneratorKj64_E16any_alloc_statuscEB7_(&generator1!0@1, ((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/library/core/src/intrinsics.rs:3605:41: 3605:51}>
  _RINvNtNtCs7zWGgSDH9R5_4core10intrinsics6verify23run_with_arbitrary_ptrscNCNvB2_25check_copy_nonoverlapping0EB6_(((__CPROVER_contracts_write_set_ptr_t)NULL)) file /tmp/workspace/kani-project/verify-std/library/core/src/intrinsics.rs line 3605 column 9 function intrinsics::verify::check_copy_nonoverlapping
  _RNvNtNtCs7zWGgSDH9R5_4core10intrinsics6verify25check_copy_nonoverlapping() file /tmp/workspace/kani-project/verify-std/library/core/src/intrinsics.rs line 3604 column 5 function intrinsics::verify::check_copy_nonoverlapping