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.

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

ICE: mismatch in number of fields and values. #2680

Closed
XAMPPRocky opened this issue Aug 14, 2023 · 6 comments · Fixed by #2794
Closed

ICE: mismatch in number of fields and values. #2680

XAMPPRocky opened this issue Aug 14, 2023 · 6 comments · Fixed by #2794
Assignees
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-High Priority Tag issues that have high priority T-User Tag user issues / requests

Comments

@XAMPPRocky
Copy link

XAMPPRocky commented Aug 14, 2023

I tried this code: tests/kani.rs

#[cfg(kani)]
#[kani::proof]
fn kani() {

    let input: kani::slice::AnySlice<u8, { usize::MAX }> = kani::slice::any_slice();

    if let Ok(value) = rasn::der::decode::<rasn_pkix::Certificate>(&input) {
        assert_eq!(value, rasn::der::decode(&rasn::der::encode(&value).unwrap()).unwrap());
    }

    if let Ok(value) = rasn::uper::decode::<rasn_pkix::Certificate>(&input) {
        assert_eq!(value, rasn::uper::decode(&rasn::uper::encode(&value).unwrap()).unwrap());
    }

    if let Ok(value) = rasn::aper::decode::<rasn_pkix::Certificate>(&input) {
        assert_eq!(value, rasn::aper::decode(&rasn::aper::encode(&value).unwrap()).unwrap());
    }
}

using the following command line invocation:

cargo kani --tests

with Kani version:

I expected to see this happen: it works

Instead, this happened:

error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
                                assertion failed: `(left == right)`
                                  left: `2`,
                                 right: `1`: Error in struct_expr; mismatch in number of fields and values.
                                    StructTag("tag-_161424092592971241517604180463813633314")
                                    [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }].

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
assertion failed: `(left == right)`
  left: `2`,
 right: `1`: Error in struct_expr; mismatch in number of fields and values.
	StructTag("tag-_161424092592971241517604180463813633314")
	[Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]
stack backtrace:
   0: _rust_begin_unwind
   1: core::panicking::panic_fmt
   2: core::panicking::assert_failed_inner
   3: core::panicking::assert_failed
   4: cprover_bindings::goto_program::expr::Expr::struct_expr_from_values
   5: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_single_variant_single_field
   6: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_scalar
   7: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_const_value
   8: kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand
   9: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
  10: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
  11: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue
  12: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement
  13: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
  14: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
  15: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
  16: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
  17: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
  18: rustc_interface::passes::start_codegen
  19: <rustc_middle::ty::context::GlobalCtxt>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_span::ErrorGuaranteed>>
  20: <rustc_interface::queries::Queries>::ongoing_codegen
  21: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
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: bitvec::domain::Domain::<'_, wyz::comu::Mut, u8>::new
_RNvMs4_NtCs4MAoNlLLqrn_6bitvec6domainINtB5_6DomainNtNtCsfYGE6EJ4wD9_3wyz4comu3MuthE3newCscrWoMilNx7E_4rasn
[Kani] current codegen location: Loc { file: "/Users/ep/.cargo/registry/src/index.crates.io-6f17d22bba15001f/bitvec-1.0.1/src/domain.rs", function: None, start_line: 377, start_col: Some(5), end_line: 378, end_col: Some(67) }
error: could not compile `rasn` (test "kani")
error: Failed to compile `kani` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
                                assertion failed: `(left == right)`
                                  left: `2`,
                                 right: `1`: Error in struct_expr; mismatch in number of fields and values.
                                    StructTag("tag-_161424092592971241517604180463813633314")
                                    [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }].
@XAMPPRocky XAMPPRocky added the [C] Bug This is a bug. Something isn't working. label Aug 14, 2023
@zhassan-aws zhassan-aws added [F] Crash Kani crashed T-User Tag user issues / requests labels Aug 14, 2023
@zhassan-aws
Copy link
Contributor

Hi @XAMPPRocky. Thanks for reporting this issue. This seems to be the same as #1594. We'll look into it.

@zhassan-aws
Copy link
Contributor

For the record, here are the steps to reproduce the crash:

  1. cargo new iss
  2. cd iss
  3. cargo add rasn rasn-pkix
  4. Paste the code from the OP into src/main.rs
  5. Run cargo kani

@zhassan-aws
Copy link
Contributor

Here is a smaller reproducer involving the bitvec crate directly:

  1. cargo new bv_dep
  2. cd bv_dep
  3. cargo add bitvec
  4. Put the following code in src/main.rs:
use bitvec::prelude::*;

#[kani::proof]
fn main() {
    let five = [0u8; 5];
    for _ in five.view_bits::<Msb0>().chunks(5) {}
}
  1. Run cargo kani

This produces:

$ cargo kani
Kani Rust Verifier 0.34.0 (cargo plugin)
   Compiling radium v0.7.0
   Compiling tap v1.0.1
   Compiling funty v2.0.0
   Compiling wyz v0.5.1
   Compiling bitvec v1.0.1
   Compiling bv_dep v0.1.0 (/home/ubuntu/examples/iss2680/bv_dep)
thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
assertion failed: `(left == right)`
  left: `2`,
 right: `1`: Error in struct_expr; mismatch in number of fields and values.
        StructTag("tag-_253093904408944338824472977755012738789")
        [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]
note: run with `RUST_BACKTRACE=1` environment variable to display a 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: bitvec::ptr::BitPtr::<bitvec::ptr::Const, u8, bitvec::order::Msb0>::from_slice
_RNvMs_NtNtCs48PfiW7PQl1_6bitvec3ptr6singleINtB4_6BitPtrNtNtCs9XbHBV8qLa5_3wyz4comu5ConsthNtNtB8_5order4Msb0E10from_sliceCsdgaxU4DwtDG_6bv_dep
[Kani] current codegen location: Loc { file: "/home/ubuntu/.cargo/registry/src/index.crates.io-6f17d22bba15001f/bitvec-1.0.1/src/ptr/single.rs", function: None, start_line: 336, start_col: Some(5), end_line: 336, end_col: Some(43) }
error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
                                assertion failed: `(left == right)`
                                  left: `2`,
                                 right: `1`: Error in struct_expr; mismatch in number of fields and values.
                                    StructTag("tag-_253093904408944338824472977755012738789")
                                    [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }].

error: could not compile `bv_dep` (bin "bv_dep")
error: Failed to compile `bv_dep` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
                                assertion failed: `(left == right)`
                                  left: `2`,
                                 right: `1`: Error in struct_expr; mismatch in number of fields and values.
                                    StructTag("tag-_253093904408944338824472977755012738789")
                                    [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }].

@XAMPPRocky
Copy link
Author

For the record, here are the steps to reproduce the crash:

Thanks it would be good to have a separate issue template for ICEs that includes those steps.

@zhassan-aws
Copy link
Contributor

Here's a stand-alone minimal reproducer:

use std::marker::PhantomData;

pub struct Foo<R> {
    x: u8,
    _t: PhantomData<R>,
}

#[kani::proof]
fn main() {
    const C: Foo<usize> = Foo {
        x: 0,
        _t: PhantomData,
    };
    assert_eq!(C.x, 0);
}
$ kani test.rs 
Kani Rust Verifier 0.34.0 (standalone)
thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
assertion failed: `(left == right)`
  left: `2`,
 right: `1`: Error in struct_expr; mismatch in number of fields and values.
        StructTag("tag-_167866918129339558870712826959134448718")
        [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]
note: run with `RUST_BACKTRACE=1` environment variable to display a 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: "/home/ubuntu/examples/iss2680/test.rs", function: None, start_line: 9, start_col: Some(1), end_line: 9, end_col: Some(10) }

@celinval celinval added the T-High Priority Tag issues that have high priority label Aug 23, 2023
@celinval
Copy link
Contributor

@remi-delmas-3000 any update here? This seems to be causing a crash in a second crate. Thanks

adpaco-aws added a commit that referenced this issue Sep 29, 2023
… also include ZSTs (#2794)

This change considers another case for the code generation of scalar data.
In particular, when the expected type is an ADT, we previously
considered two cases: either there is no field or there is one. But in
cases where the ADT includes a ZST, the ADT will contain multiple
fields: one associated to the scalar data, and other fields associated
to the ZSTs. In those cases, we ended up crashing as in #2680:

```rust
error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
                                assertion failed: `(left == right)`
                                  left: `2`,
                                 right: `1`: Error in struct_expr; mismatch in number of fields and values.
                                    StructTag("tag-_161424092592971241517604180463813633314")
                                    [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }].

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
assertion failed: `(left == right)`
  left: `2`,
 right: `1`: Error in struct_expr; mismatch in number of fields and values.
	StructTag("tag-_161424092592971241517604180463813633314")
	[Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]
```

With the changes in this PR, that's no longer the case.

Resolves #2364 
Resolves #2680
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed T-High Priority Tag issues that have high priority T-User Tag user issues / requests
Projects
No open projects
Status: No status
Status: No status
4 participants