Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Invalid stub cause different ICE while monomorphizing the code #2589

Closed
celinval opened this issue Jul 7, 2023 · 1 comment · Fixed by #2787
Closed

Invalid stub cause different ICE while monomorphizing the code #2589

celinval opened this issue Jul 7, 2023 · 1 comment · Fixed by #2787
Assignees
@JustusAdam
Labels
[C] Bug This is a bug. Something isn't working.
Milestone
Stubbing

Comments

@celinval
Copy link
Contributor

celinval commented Jul 7, 2023

I tried this code:

fn original<T>() {}

trait Dummy {
    const TRUE: bool = true;
}

fn stub<T: Dummy>() {
    // Do nothing.
    assert!(T::TRUE)
}

#[kani::proof]
#[kani::stub(original, stub)]
fn check_mismatch() {
    original::<String>();
}

using the following command line invocation:

kani --enable-unstable --enable-stubbing

with Kani version: 0.31.0 (dev)

I expected to see this happen: Kani should print a trait mismatch error

Instead, this happened: Kani compiler crashed with the following error:

error: internal compiler error: kani-compiler/src/kani_middle/reachability.rs:443:54: Unexpected polymorphic constant: Unevaluated(UnevaluatedConst { def: DefId(0:16 ~ trait_mismatch[1bfd]::Dummy::TRUE), substs: [std::string::String], promoted: None }, bool)
  --> trait_mismatch.rs:36:5
   |
36 |     assert!(T::TRUE)
   |     ^^^^^^^^^^^^^^^^
   |
   = note: this error: internal compiler error originates in the macro `assert` (in Nightly builds, run with -Z macro-backtrace for more info)

thread 'rustc' panicked at 'Box<dyn Any>', /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_errors/src/lib.rs:994:33
Stack backtrace 
stack backtrace:
   0: std::panicking::begin_panic
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/std/src/panicking.rs:625:12
   1: std::panic::panic_any
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/std/src/panic.rs:63:5
   2: rustc_errors::HandlerInner::span_bug
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_errors/src/lib.rs:1588:9
   3: rustc_errors::Handler::span_bug
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_errors/src/lib.rs:994:9
   4: rustc_middle::util::bug::opt_span_bug_fmt::{{closure}}
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/util/bug.rs:34:40
   5: rustc_middle::ty::context::tls::with_opt::{{closure}}
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/ty/context/tls.rs:154:36
   6: rustc_middle::ty::context::tls::with_context_opt
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/ty/context/tls.rs:100:18
   7: rustc_middle::ty::context::tls::with_opt
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/ty/context/tls.rs:154:5
   8: rustc_middle::util::bug::opt_span_bug_fmt
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/util/bug.rs:31:5
   9: rustc_middle::util::bug::span_bug_fmt
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/util/bug.rs:22:5
  10: <kani_compiler::kani_middle::reachability::MonoItemsFnCollector as rustc_middle::mir::visit::Visitor>::visit_constant
             at /kani/kani-compiler/src/kani_middle/reachability.rs:443:54
  11: rustc_middle::mir::visit::Visitor::super_operand
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:779:25
  12: rustc_middle::mir::visit::Visitor::visit_operand
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:146:17
  13: rustc_middle::mir::visit::Visitor::super_rvalue
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:701:25
  14: <kani_compiler::kani_middle::reachability::MonoItemsFnCollector as rustc_middle::mir::visit::Visitor>::visit_rvalue
             at /kani/kani-compiler/src/kani_middle/reachability.rs:415:9
  15: rustc_middle::mir::visit::Visitor::super_assign
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:461:17
  16: rustc_middle::mir::visit::Visitor::visit_assign
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:114:17
  17: rustc_middle::mir::visit::Visitor::super_statement
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:378:25
  18: rustc_middle::mir::visit::Visitor::visit_statement
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:105:17
  19: rustc_middle::mir::visit::Visitor::super_basic_block_data
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:307:21
  20: rustc_middle::mir::visit::Visitor::visit_basic_block_data
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:90:17
  21: rustc_middle::mir::visit::Visitor::super_body
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:292:17
  22: rustc_middle::mir::visit::Visitor::visit_body
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:80:17
  23: kani_compiler::kani_middle::reachability::MonoItemsCollector::visit_fn
             at /kani/kani-compiler/src/kani_middle/reachability.rs:200:9
  24: kani_compiler::kani_middle::reachability::MonoItemsCollector::reachable_items
             at /kani/kani-compiler/src/kani_middle/reachability.rs:178:47
  25: kani_compiler::kani_middle::reachability::MonoItemsCollector::collect
             at /kani/kani-compiler/src/kani_middle/reachability.rs:168:9
  26: kani_compiler::kani_middle::reachability::collect_reachable_items
             at /kani/kani-compiler/src/kani_middle/reachability.rs:49:9
  27: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:86:16
  28: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:738:15
  29: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:85:21
  30: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:242:25
  31: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
  32: rustc_interface::passes::start_codegen
  33: <rustc_middle::ty::context::GlobalCtxt>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_span::ErrorGuaranteed>>
  34: <rustc_interface::queries::Queries>::ongoing_codegen
  35: rustc_span::set_source_map::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{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: aborting due to previous error; 5 warnings emitted
@celinval celinval added the [C] Bug This is a bug. Something isn't working. label Jul 7, 2023
@celinval celinval added this to the Stubbing milestone Jul 7, 2023
@celinval celinval changed the title Invalid stub cause ICE: Unexpected polymorphic constant Invalid stub cause different ICE while monomorphizing the code Jul 7, 2023
@celinval
Copy link
Contributor Author

celinval commented Jul 7, 2023

BTW, this happens because String does not implement Dummy trait. So we failed to monomorphize the constant.

BTW, I think the best solution here is to find a better error handling for stub trait resolution instead of adding extra checks to the reachability algorithm. In theory, any place where we monomorphize an item, it can fail. Here is another example:

fn original<T>() {}

trait Dummy {
    fn true_val() -> bool {
        true
    }
}

fn stub<T: Dummy>() {
    // Do nothing.
    assert!(T::true_val())
}

#[kani::proof]
#[kani::stub(original, stub)]
fn check_mismatch() {
    original::<String>();
}
Stack backtrack 
thread 'rustc' panicked at 'index out of bounds: the len is 0 but the index is 0', kani-compiler/src/kani_middle/reachability.rs:482:50
stack backtrace:
   0: rust_begin_unwind
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/std/src/panicking.rs:593:5
   1: core::panicking::panic_fmt
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/panicking.rs:67:14
   2: core::panicking::panic_bounds_check
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/panicking.rs:162:5
   3: <usize as core::slice::index::SliceIndex<[T]>>::index
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/slice/index.rs:258:10
   4: core::slice::index::<impl core::ops::index::Index<I> for [T]>::index
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/slice/index.rs:18:9
   5: <alloc::vec::Vec<T,A> as core::ops::index::Index<I>>::index
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/alloc/src/vec/mod.rs:2674:9
   6: <kani_compiler::kani_middle::reachability::MonoItemsFnCollector as rustc_middle::mir::visit::Visitor>::visit_terminator
             at /kani/kani-compiler/src/kani_middle/reachability.rs:482:50
   7: rustc_middle::mir::visit::Visitor::super_basic_block_data
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:313:21
   8: rustc_middle::mir::visit::Visitor::visit_basic_block_data
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:90:17
   9: rustc_middle::mir::visit::Visitor::super_body
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:292:17
  10: rustc_middle::mir::visit::Visitor::visit_body
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/compiler/rustc_middle/src/mir/visit.rs:80:17
  11: kani_compiler::kani_middle::reachability::MonoItemsCollector::visit_fn
             at /kani/kani-compiler/src/kani_middle/reachability.rs:200:9
  12: kani_compiler::kani_middle::reachability::MonoItemsCollector::reachable_items
             at /kani/kani-compiler/src/kani_middle/reachability.rs:178:47
  13: kani_compiler::kani_middle::reachability::MonoItemsCollector::collect
             at /kani/kani-compiler/src/kani_middle/reachability.rs:168:9
  14: kani_compiler::kani_middle::reachability::collect_reachable_items
             at /kani/kani-compiler/src/kani_middle/reachability.rs:49:9
  15: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:86:16
  16: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:738:15
  17: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:85:21
  18: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:242:25
  19: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
  20: rustc_interface::passes::start_codegen
  21: <rustc_middle::ty::context::GlobalCtxt>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_span::ErrorGuaranteed>>
  22: <rustc_interface::queries::Queries>::ongoing_codegen
  23: rustc_span::set_source_map::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{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.

@JustusAdam JustusAdam mentioned this issue Sep 22, 2023
Merged
4 tasks
@celinval celinval mentioned this issue Nov 25, 2023
Merged
celinval added a commit that referenced this issue Nov 30, 2023
@celinval @adpaco-aws @zhassan-aws
Change reachability module to use StableMIR (#2894)
bd2d8d5 
Rewrite the reachability module to use Stable APIs wherever possible.
Note that in StableMIR the instance body is already monomorphized and
constants are already evaluated, which simplifies the code for most of
it, except to handle stubbing issue #2589.

For the stubbing issue, we still use a mix of stable and internal APIs
to detect an invalid monomorphization.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@JustusAdam JustusAdam

Labels
[C] Bug This is a bug. Something isn't working.
Projects
No open projects
Kani 2023-10-03
Status: No status
Milestone
Stubbing
Development

Successfully merging a pull request may close this issue.

Fix issue 2589 JustusAdam/kani
2 participants
@JustusAdam @celinval