Delayed UB instrumentation regression: slices

[carolynzech]

I tried this code:

#[kani::proof]
fn delayed_ub_slices() {
    unsafe {
        // Create an array.
        let mut arr = [0u128; 4];
        // Get a pointer to a part of the array.
        let ptr = &mut arr[0..2][0..1][0] as *mut _ as *mut (u8, u32);
        *ptr = (4, 4);
        let arr_copy = arr; // UB: This reads a padding value inside the array!
    }
}

using the following command line invocation:

cargo run -p compiletest -- --suite expected --mode expected delayed-ub

or, alternatively:

kani delayed_ub.rs -Z ghost-state -Z uninit-checks

with Kani version: 0.60-dev, after upgrading the toolchain to 2/5/2025.

I expected to see this happen: Verification fails with this message:

delayed_ub_slices.assertion.\
	 - Status: FAILURE\
	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`"

and thus the test succeeds.

Instead, this happened:

thread 'rustc' panicked at kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs:105:75:
called `Result::unwrap()` on an `Err` value: "Kani was not able to resolve the instance of the function operand `Ty { id: 92, kind: RigidTy(FnPtr(Binder { value: FnSig { inputs_and_output: [Ty { id: 94, kind: RigidTy(Adt(AdtDef(DefId { id: 269, name: \"std::ptr::NonNull\" }), GenericArgs([Type(Ty { id: 3, kind: RigidTy(Tuple([])) })]))) }, Ty { id: 96, kind: RigidTy(Ref(Region { kind: ReBound(0, BoundRegion { var: 0, kind: BrAnon }) }, Ty { id: 828, kind: RigidTy(Adt(AdtDef(DefId { id: 332, name: \"std::fmt::Formatter\" }), GenericArgs([Lifetime(Region { kind: ReBound(0, BoundRegion { var: 1, kind: BrAnon }) })]))) }, Mut)) }, Ty { id: 89, kind: RigidTy(Adt(AdtDef(DefId { id: 273, name: \"std::result::Result\" }), GenericArgs([Type(Ty { id: 3, kind: RigidTy(Tuple([])) }), Type(Ty { id: 112, kind: RigidTy(Adt(AdtDef(DefId { id: 341, name: \"std::fmt::Error\" }), GenericArgs([]))) })]))) }], c_variadic: false, safety: Unsafe, abi: Rust }, bound_vars: [Region(BrAnon), Region(BrAnon)] })) }`. Currently, memory initialization checks in presence of function pointers and vtable calls are not supported. For more information about planned support, see https://github.com/model-checking/kani/issues/3300."
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::result::unwrap_failed
   3: core::result::Result<T,E>::unwrap
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/result.rs:1109:23
   4: <kani_compiler::kani_middle::transform::check_uninit::delayed_ub::initial_target_visitor::InitialTargetVisitor as stable_mir::mir::visit::MirVisitor>::visit_terminator
             at /Users/cmzech/kani/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs:105:28
   5: stable_mir::mir::visit::MirVisitor::super_basic_block
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/stable_mir/src/mir/visit.rs:172:9
   6: stable_mir::mir::visit::MirVisitor::visit_basic_block
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/stable_mir/src/mir/visit.rs:48:9
   7: stable_mir::mir::visit::MirVisitor::super_body
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/stable_mir/src/mir/visit.rs:146:13
   8: stable_mir::mir::visit::MirVisitor::visit_body
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/stable_mir/src/mir/visit.rs:44:9
   9: <kani_compiler::kani_middle::transform::check_uninit::delayed_ub::DelayedUbPass as kani_compiler::kani_middle::transform::GlobalPass>::transform::{{closure}}
             at /Users/cmzech/kani/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs:67:17
  10: core::iter::adapters::map::map_fold::{{closure}}
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:88:28
  11: <core::slice::iter::Iter<T> as core::iter::traits::iterator::Iterator>::fold
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:232:27
  12: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:128:9
  13: <core::iter::adapters::fuse::Fuse<I> as core::iter::traits::iterator::Iterator>::fold
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/adapters/fuse.rs:98:19
  14: core::iter::adapters::flatten::FlattenCompat<I,U>::iter_fold
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/adapters/flatten.rs:450:15
  15: <core::iter::adapters::flatten::FlattenCompat<I,U> as core::iter::traits::iterator::Iterator>::fold
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/adapters/flatten.rs:636:9
  16: <core::iter::adapters::flatten::FlatMap<I,U,F> as core::iter::traits::iterator::Iterator>::fold
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/adapters/flatten.rs:87:9
  17: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:128:9
  18: core::iter::traits::iterator::Iterator::for_each
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:800:9
  19: <hashbrown::map::HashMap<K,V,S,A> as core::iter::traits::collect::Extend<(K,V)>>::extend
             at /rust/deps/hashbrown-0.15.2/src/map.rs:4492:9
  20: <hashbrown::set::HashSet<T,S,A> as core::iter::traits::collect::Extend<T>>::extend
             at /rust/deps/hashbrown-0.15.2/src/set.rs:1308:9
  21: <std::collections::hash::set::HashSet<T,S> as core::iter::traits::collect::Extend<T>>::extend
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/collections/hash/set.rs:1118:9
  22: <std::collections::hash::set::HashSet<T,S> as core::iter::traits::collect::FromIterator<T>>::from_iter
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/collections/hash/set.rs:1069:13
  23: core::iter::traits::iterator::Iterator::collect
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:1971:9
  24: <kani_compiler::kani_middle::transform::check_uninit::delayed_ub::DelayedUbPass as kani_compiler::kani_middle::transform::GlobalPass>::transform
             at /Users/cmzech/kani/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs:62:35
  25: kani_compiler::kani_middle::transform::GlobalPasses::run_global_passes
             at /Users/cmzech/kani/kani-compiler/src/kani_middle/transform/mod.rs:219:13
  26: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
             at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:112:9
  27: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
             at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:280:63
  28: rustc_smir::rustc_internal::init::{{closure}}
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:196:33
  29: scoped_tls::ScopedKey<T>::set
             at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
  30: rustc_smir::rustc_internal::init
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:196:5
  31: rustc_smir::rustc_internal::run::{{closure}}
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:227:53
  32: stable_mir::compiler_interface::run::{{closure}}
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/stable_mir/src/compiler_interface.rs:265:40
  33: scoped_tls::ScopedKey<T>::set
             at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
  34: stable_mir::compiler_interface::run
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/stable_mir/src/compiler_interface.rs:265:9
  35: rustc_smir::rustc_internal::run
             at /Users/cmzech/.rustup/toolchains/nightly-2025-02-10-aarch64-apple-darwin/lib/rustlib/src/rust/compiler/rustc_smir/src/rustc_internal/mod.rs:227:5
  36: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:237:23
  37: <rustc_interface::queries::Linker>::codegen_and_build_linker
  38: rustc_interface::passes::create_and_enter_global_ctxt::<core::option::Option<rustc_interface::queries::Linker>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2}>
  39: rustc_interface::interface::run_compiler::<(), rustc_driver_impl::run_compiler::{closure#0}>::{closure#1}
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

[carolynzech]

I did some debugging.

TL;DR: this upstream change rust-lang/rust#135265 causes this regression. The problem is that our delayed UB instrumentation panics if there are any reachable function pointers. Previously, this test didn't have any, but the new calls to expect introduce some.

More Detail
First, I added a debug! statement here to print the name of the instance, then ran with --debug, which showed that the Instance that causes this panic is:

DEBUG kani_compiler::kani_middle::transform::check_uninit::delayed_ub name="core::fmt::rt::Argument::<'_>::fmt"

I generated the dot graphs for both the 2/4 and 2/5 toolchains. I determined that both have this edge in their graphs:

"core::slice::index::slice_end_index_len_fail::do_panic::runtime" -> "core::fmt::rt::Argument::<'_>::new_display::<usize>" [label=DirectCall] 

after which point they diverge, and the 2/5 toolchain ends up encountering this problematic function pointer.

I then did the following:

Changed this line:

kani/kani-compiler/src/kani_middle/reachability.rs

Line 645 in a66bb06

self.back_edges

to refer to self.edges instead, so I could dump the edges flowing out of new_display, instead of the edges flowing into it.
Then, I ran:

TARGET_ITEM="core::fmt::rt::Argument::<'_>::new_display::<usize>"
KANI_REACH_DEBUG="${TARGET_ITEM}" kani delayed-ub.rs -Z ghost-state -Z uninit-checks
dot -Tpng delayed_ub.dot -o dot_graph.png

on both the 2/4 and 2/5 toolchains. These graphs shows how the slice index panic code calls this _fmt method, which, in the 2/5 toolchain only, callsstd::result::Result::<usize, std::num::TryFromIntError>::expect, and that new expect call leads to this core::fmt::rt::Argument::<'_>::fmt call.

[carolynzech]

Thankfully, this doesn't cause unsoundness, since we panic rather than report verification success. It's a bit of a shame though, since we shouldn't actually need to investigate this panic code to find the UB. We could consider modifying this instrumentation to just report verification failure if it encounters a function pointer, instead of panicking. I think(?) that if we do that, we should be able to report the UB and then print some message like "Note that we couldn't fully investigate everything, so if we say there's UB, there's UB, but even if we didn't find UB, we failed anyway since we encountered a function pointer and therefore couldn't be sure if there was UB or not."