model-checking
ICE Resolving `proof_for_contract` target
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.
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}>"
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.
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.
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();
}
}
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.
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.
@zhassan-aws is it possible to add an error message here? I thought we used to have a proper validation step.
NonNull::new(x as *mut i32).unwrap();
Thanks for the suggestion, it works! 👍
@zhassan-aws is it possible to add an error message here? I thought we used to have a proper validation step.
https://github.com/model-checking/kani/pull/3609
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.
This example now results in an error:
error: The function specified in the `proof_for_contract` attribute, `bar`, was not found.
Make sure the function is reachable from the harness.
--> iss3467.rs:6:5
|
6 | #[kani::proof_for_contract(bar)]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)
error: aborting due to 1 previous error
Per an offline discussion with @carolynzech, we likely won't support contracts on functions defined inside functions. Closing this issue as the ICE has been resolved.