ICE Resolving `proof_for_contract` target #3467

carolynzech · 2024-08-29T17:33:37Z

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.

The text was updated successfully, but these errors were encountered:

carolynzech · 2024-08-29T17:47:42Z

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 · 2024-09-17T18:18:36Z

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 · 2024-09-30T16:29:12Z

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 · 2024-10-11T19:42:18Z

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 · 2024-10-15T19:48:06Z

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 · 2024-10-15T22:42:34Z

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 · 2024-10-15T23:00:15Z

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

danielhumanmod · 2024-10-16T18:15:33Z

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

Thanks for the suggestion, it works! 👍

zhassan-aws · 2024-10-17T18:44:39Z

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

#3609

Currently, Kani panics if the function specified in the `proof_for_contract` attribute is not found (e.g. because the function is not reachable) (see #3467). This PR adds an error message pointing out the issue. Towards #3467 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

carolynzech added the [C] Bug This is a bug. Something isn't working. label Aug 29, 2024

carolynzech mentioned this issue Aug 29, 2024

align_offset Contracts model-checking/verify-rust-std#69

Merged

carolynzech added the Z-Contracts Issue related to code contracts label Aug 30, 2024

feliperodri added this to the Function Contracts milestone Sep 5, 2024

zhassan-aws mentioned this issue Sep 20, 2024

Challenge 6: Safety of NonNull model-checking/verify-rust-std#53

Open

celinval assigned celinval and zhassan-aws and unassigned celinval Oct 15, 2024

zhassan-aws mentioned this issue Oct 17, 2024

Emit an error when proof_for_contract function is not found #3609

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

ICE Resolving `proof_for_contract` target #3467

ICE Resolving `proof_for_contract` target #3467

carolynzech commented Aug 29, 2024 •

edited

Loading

carolynzech commented Aug 29, 2024 •

edited

Loading

carolynzech commented Sep 17, 2024 •

edited

Loading

carolynzech commented Sep 30, 2024

danielhumanmod commented Oct 11, 2024

celinval commented Oct 15, 2024

zhassan-aws commented Oct 15, 2024

celinval commented Oct 15, 2024

danielhumanmod commented Oct 16, 2024

zhassan-aws commented Oct 17, 2024

ICE Resolving proof_for_contract target #3467

ICE Resolving proof_for_contract target #3467

Comments

carolynzech commented Aug 29, 2024 • edited Loading

carolynzech commented Aug 29, 2024 • edited Loading

carolynzech commented Sep 17, 2024 • edited Loading

carolynzech commented Sep 30, 2024

danielhumanmod commented Oct 11, 2024

celinval commented Oct 15, 2024

zhassan-aws commented Oct 15, 2024

celinval commented Oct 15, 2024

danielhumanmod commented Oct 16, 2024

zhassan-aws commented Oct 17, 2024

ICE Resolving `proof_for_contract` target #3467

ICE Resolving `proof_for_contract` target #3467

carolynzech commented Aug 29, 2024 •

edited

Loading

carolynzech commented Aug 29, 2024 •

edited

Loading

carolynzech commented Sep 17, 2024 •

edited

Loading