Repository navigation
Delayed UB instrumentation regression: slices #3881
Description
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.
Activity
carolynzech commentedon Feb 10, 2025
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:I generated the dot graphs for both the 2/4 and 2/5 toolchains. I determined that both have this edge in their graphs:
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
to refer to
self.edgesinstead, so I could dump the edges flowing out ofnew_display, instead of the edges flowing into it.Then, I ran:
on both the 2/4 and 2/5 toolchains. These graphs shows how the slice index panic code calls this
_fmtmethod, which, in the 2/5 toolchain only, callsstd::result::Result::<usize, std::num::TryFromIntError>::expect, and that newexpectcall leads to thiscore::fmt::rt::Argument::<'_>::fmtcall.carolynzech commentedon Feb 10, 2025
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."
Upgrade toolchain to 2/10 (#3883)
Only skip toolchain update upon exact issue match