ICE Resolving `proof_for_contract` target

[carolynzech]

I tried this code:

#[safety::requires(a.is_power_of_two())]
pub(crate) const unsafe fn align_offset<T: Sized>(p: *const T, a: usize) -> usize {
    ...
    #[safety::requires(m.is_power_of_two())]
    #[safety::requires(x < m)]
    const unsafe fn mod_inv(x: usize, m: usize) -> usize { ... }

    #[cfg(kani)]
    #[kani::proof_for_contract(mod_inv)]
    fn check_mod_inv() {
        let x = kani::any::<usize>();
        let m = kani::any::<usize>();
        unsafe { mod_inv(x, m) };
    }
   ...
}

For the actual code (to run this locally), add the contract and proof above here.

using the following command line invocation:

kani verify-std -Z unstable-options ./library --target-dir /tmp/verify-rust-std -Z function-contracts -Z mem-predicates --harness check_mod_inv

with Kani version: 0.54

I expected to see this happen: verification success

Instead, this happened:

error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:14:
                                called `Option::unwrap()` on a `None` value.

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:14:
called `Option::unwrap()` on a `None` value
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::panicking::panic
   3: core::option::unwrap_failed
   4: core::option::Option<T>::unwrap
             at /rustc/60d146580c10036ce89e019422c6bc2fd9729b65/library/core/src/option.rs:967:21
   5: kani_compiler::codegen_cprover_gotoc::codegen::contract::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::handle_check_contract
             at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:35:22
   6: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}::{{closure}}
             at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:186:47
   7: core::option::Option<T>::map
             at /rustc/60d146580c10036ce89e019422c6bc2fd9729b65/library/core/src/option.rs:1107:29
   8: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}
             at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:186:17
   9: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
             at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:837:15
  10: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
             at /Users/cmzech/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:138:29
  11: <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:282:63
  12: rustc_smir::rustc_internal::init::{{closure}}
             at /rustc/60d146580c10036ce89e019422c6bc2fd9729b65/compiler/rustc_smir/src/rustc_internal/mod.rs:192:33
  13: scoped_tls::ScopedKey<T>::set
             at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
  14: rustc_smir::rustc_internal::init
             at /rustc/60d146580c10036ce89e019422c6bc2fd9729b65/compiler/rustc_smir/src/rustc_internal/mod.rs:192:5
  15: rustc_smir::rustc_internal::run::{{closure}}
             at /rustc/60d146580c10036ce89e019422c6bc2fd9729b65/compiler/rustc_smir/src/rustc_internal/mod.rs:223:53
  16: stable_mir::compiler_interface::run::{{closure}}
             at /rustc/60d146580c10036ce89e019422c6bc2fd9729b65/compiler/stable_mir/src/compiler_interface.rs:259:40
  17: scoped_tls::ScopedKey<T>::set
             at /rust/deps/scoped-tls-1.0.1/src/lib.rs:137:9
  18: stable_mir::compiler_interface::run
             at /rustc/60d146580c10036ce89e019422c6bc2fd9729b65/compiler/stable_mir/src/compiler_interface.rs:259:9
  19: rustc_smir::rustc_internal::run
             at /rustc/60d146580c10036ce89e019422c6bc2fd9729b65/compiler/rustc_smir/src/rustc_internal/mod.rs:223:5
  20: <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:251:23
  21: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
  22: rustc_interface::passes::start_codegen
  23: <rustc_interface::queries::Linker>::codegen_and_build_linker
  24: <rustc_middle::ty::context::GlobalCtxt>::enter::<rustc_driver_impl::run_compiler::{closure#0}::{closure#1}::{closure#6}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
  25: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#0}::{closure#1}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
  26: rustc_span::create_session_globals_then::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::util::run_in_thread_with_globals<rustc_interface::util::run_in_thread_pool_with_globals<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#0}>::{closure#1}, core::result::Result<(), rustc_span::ErrorGuaranteed>>::{closure#0}, core::result::Result<(), rustc_span::ErrorGuaranteed>>::{closure#0}::{closure#0}::{closure#0}>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] no current codegen item.
[Kani] no current codegen location.
error: could not compile `core` (lib)
error: Failed to compile `core` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:14:
                                called `Option::unwrap()` on a `None` value.

[carolynzech]

I determined that it returns None because this condition is false.

I added this code:

dbg!(&function_under_contract);
dbg!(&instance.name());

right before returning None here.

There was one function under contract for mod_inv:

[kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:45:25] &function_under_contract = DefId(0:25622 ~ core[6b6a]::ptr::align_offset::{closure#0}::{closure#1}::{closure#3}::mod_inv)

and the instances searched were:

[kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:25] &instance.name() = "ptr::align_offset::{closure#2}::{closure#3}::mod_inv"
[kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:25] &instance.name() = "ptr::align_offset::{closure#2}::{closure#3}::check_mod_inv"
[kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:25] &instance.name() = "ptr::align_offset::{closure#2}::{closure#3}::mod_inv::{closure#0}"
[kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:25] &instance.name() = "ptr::align_offset::{closure#2}::{closure#3}::mod_inv::{closure#1}"
[kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:25] &instance.name() = "ptr::align_offset::{closure#2}::{closure#3}::mod_inv::kani_register_contract::<usize, {closure@/Users/cmzech/verify-std/library/core/src/ptr/mod.rs:1932:5: 1932:45}>"
[kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:25] &instance.name() = "ptr::align_offset::{closure#2}::{closure#3}::mod_inv::{closure#2}"
[kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:25] &instance.name() = "ptr::align_offset::{closure#2}::{closure#3}::mod_inv::kani_register_contract::<usize, {closure@/Users/cmzech/verify-std/library/core/src/ptr/mod.rs:1932:5: 1932:45}>"
[kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs:46:25] &instance.name() = "ptr::align_offset::{closure#2}::{closure#3}::mod_inv::kani_register_contract::<usize, {closure@/Users/cmzech/verify-std/library/core/src/ptr/mod.rs:1932:5: 1932:45}>"

[carolynzech]

A smaller example for the same Kani line ICEing:

#[kani::requires(true)]
fn foo() {}

#[kani::proof_for_contract(foo)]
fn check_foo() {}

We should have a more graceful error message for the case where the harness doesn't invoke the target.

[carolynzech]

Smaller example for the original issue (the nested harness):

#[kani::requires(true)]
fn foo() {
    #[kani::requires(true)]
    fn bar() {}

    #[kani::proof_for_contract(bar)]
    fn bar_harness() {
        bar()
    }
}

If I comment out the contract on foo, verification succeeds.

[danielhumanmod]

Hi team, after discuss with @zhassan-aws , I found a issue might be the same cause, there is my function contract and proof harness

#[stable(feature = "nonnull", since = "1.25.0")]
    #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")]
    #[must_use]
    #[inline(always)]
    #[requires(ub_checks::can_dereference(self))]
    // #[ensures(|result: &&mut T| core::ptr::eq(*result, self.as_ptr()))]
    pub const unsafe fn as_mut<'a>(&mut self) -> &'a mut T {
        // SAFETY: the caller must guarantee that `self` meets all the
        // requirements for a mutable reference.
        unsafe { &mut *self.as_ptr() }
    }

#[kani::proof_for_contract(NonNull::as_mut)]
    pub fn non_null_check_as_mut() {
        let mut x: i32 = kani::any();
        let mut ptr = NonNull::new(x as *mut i32);

        unsafe {
            let result = ptr.as_mut();
        }
    }

[celinval]

Hi team, after discuss with @zhassan-aws , I found a issue might be the same cause, there is my function contract and proof harness

#[stable(feature = "nonnull", since = "1.25.0")]
    #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")]
    #[must_use]
    #[inline(always)]
    #[requires(ub_checks::can_dereference(self))]
    // #[ensures(|result: &&mut T| core::ptr::eq(*result, self.as_ptr()))]
    pub const unsafe fn as_mut<'a>(&mut self) -> &'a mut T {
        // SAFETY: the caller must guarantee that `self` meets all the
        // requirements for a mutable reference.
        unsafe { &mut *self.as_ptr() }
    }

#[kani::proof_for_contract(NonNull::as_mut)]
    pub fn non_null_check_as_mut() {
        let mut x: i32 = kani::any();
        let mut ptr = NonNull::new(x as *mut i32);

        unsafe {
            let result = ptr.as_mut();
        }
    }

I wonder if the problem you are seeing is due to the function being inlined. @zhassan-aws maybe we can disable the inline pass when contracts / stubbing are enabled for now.

[zhassan-aws]

Hi team, after discuss with @zhassan-aws , I found a issue might be the same cause, there is my function contract and proof harness

#[stable(feature = "nonnull", since = "1.25.0")]
    #[rustc_const_unstable(feature = "const_ptr_as_ref", issue = "91822")]
    #[must_use]
    #[inline(always)]
    #[requires(ub_checks::can_dereference(self))]
    // #[ensures(|result: &&mut T| core::ptr::eq(*result, self.as_ptr()))]
    pub const unsafe fn as_mut<'a>(&mut self) -> &'a mut T {
        // SAFETY: the caller must guarantee that `self` meets all the
        // requirements for a mutable reference.
        unsafe { &mut *self.as_ptr() }
    }

#[kani::proof_for_contract(NonNull::as_mut)]
    pub fn non_null_check_as_mut() {
        let mut x: i32 = kani::any();
        let mut ptr = NonNull::new(x as *mut i32);

        unsafe {
            let result = ptr.as_mut();
        }
    }

@danielhumanmod The issue in your example is that the harness is calling Option::as_mut as opposed to NonNull::as_mut. Note that the type of ptr on this line:

        let mut ptr = NonNull::new(x as *mut i32);

is Option<NonNull<i32>> and not NonNull<i32>. To fix this, add an unwrap, i.e.

        let mut ptr = NonNull::new(x as *mut i32).unwrap();

This should make the crash disappear.

[celinval]

@zhassan-aws is it possible to add an error message here? I thought we used to have a proper validation step.