search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.13k stars 83 forks source link

ICE Resolving `proof_for_contract` target #3467

Open carolynzech opened 2 weeks ago

carolynzech commented 2 weeks ago

I tried this code:

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 commented 2 weeks ago

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 commented 2 hours ago

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.