ice: None , gats

[matthiaskrgr]

I tried this code:

// check-pass

use std::fmt::Debug;
use std::marker::PhantomData;

trait Foo {
    type Gat<'a>: ?Sized where Self: 'a;
}

struct Bar<'a, T: Foo + 'a>(T::Gat<'a>);

struct Baz<T: ?Sized>(PhantomData<T>);

impl<T: ?Sized> Foo for Baz<T> {
    type Gat<'a> = T where Self: 'a;
}

#[kani::proof]
fn main() {
    let x = Bar::<'_, Baz<()>>(());
    let y: &Bar<'_, Baz<dyn Debug>> = &x;
}

using the following command line invocation:

kani file.rs1

with Kani version: 0.40

I expected to see this happen: explanation

Instead, this happened: explanation

at 17:49:09 ❯ RUST_BACKTRACE=1 kani issue-75899-but-gats.rs
Kani Rust Verifier 0.40.0 (standalone)
warning: unused variable: `y`
  --> issue-75899-but-gats.rs:21:9
   |
21 |     let y: &Bar<'_, Baz<dyn Debug>> = &x;
   |         ^ help: if this is intentional, prefix it with an underscore: `_y`
   |
   = note: `#[warn(unused_variables)]` on by default

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:1175:82:
called `Option::unwrap()` on a `None` value
stack backtrace:
   0: rust_begin_unwind
             at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:645:5
   1: core::panicking::panic_fmt
             at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:72:14
   2: core::panicking::panic
             at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:127:5
   3: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_vtable_method_field
   4: core::ops::function::impls::<impl core::ops::function::FnMut<A> for &mut F>::call_mut
   5: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
   6: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_pointer_cast
   7: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue
   8: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement
   9: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
  10: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
  11: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
  12: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
  13: rustc_interface::passes::start_codegen
  14: <rustc_interface::queries::Queries>::ongoing_codegen
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] current codegen item: codegen_function: main
main
[Kani] current codegen location: Loc { file: "/tmp/icemaker/issue-75899-but-gats.rs", function: None, start_line: 19, start_col: Some(1), end_line: 19, end_col: Some(10) }
warning: 1 warning emitted

error: /home/matthias/.kani/kani-0.40.0/bin/kani-compiler exited with status exit status: 101

[zhassan-aws]

Relevant documentation of GATs: https://blog.rust-lang.org/2022/10/28/gats-stabilization.html