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

Kani panics during Goto translation for code using bitvec #2364

Closed
weaversa opened this issue Apr 12, 2023 · 2 comments · Fixed by #2794
Closed

Kani panics during Goto translation for code using bitvec #2364

weaversa opened this issue Apr 12, 2023 · 2 comments · Fixed by #2794
Assignees
@celinval @adpaco-aws
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

@weaversa
Copy link

Kani panics during Goto translation for code using the bitvec library.

Kani versions tested: 0.24.0, 0.25.0

To reproduce, create a lib crate with the following Cargo.toml:

[package]
name = "kani-test"
version = "0.1.0"
edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
bitvec = "1"

Add the following to src/lib.rs:

use bitvec::prelude::{BitArr, BitArray, Msb0};

type MyStruct = BitArr!(for 1, in u8, Msb0);

fn f() -> MyStruct {
    BitArray::ZERO
}

#[cfg(kani)]
mod tests {
    use super::*;

    #[kani::proof]
    fn some_property() {
        let mut val = f();
        val.set(0, true);
    }
}

Run kani:

$ RUST_BACKTRACE=full cargo kani
   Compiling kani-test v0.1.0 (/home/ec2-user/dev/kani-test)
error: internal compiler error: Kani unexpectedly panicked at panicked at 'assertion failed: `(left == right)`
                                  left: `2`,
                                 right: `1`: Error in struct_expr; mismatch in number of fields and values.
                                    StructTag("tag-_15362072497429542738")
                                    [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None }]', cprover_bindings/src/goto_program/expr.rs:782:9.

thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `2`,
 right: `1`: Error in struct_expr; mismatch in number of fields and values.
	StructTag("tag-_15362072497429542738")
	[Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None }]', cprover_bindings/src/goto_program/expr.rs:782:9
stack backtrace:
   0:     0x7fe8956f732a - std::backtrace_rs::backtrace::libunwind::trace::h081f29f716721cea
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7fe8956f732a - std::backtrace_rs::backtrace::trace_unsynchronized::h1c7fc4c4ccf8cfff
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fe8956f732a - std::sys_common::backtrace::_print_fmt::hb7786e9419686803
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7fe8956f732a - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h94ad8e373d395c6e
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7fe89575945e - core::fmt::write::h46ba6a9e2a6d4adf
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/core/src/fmt/mod.rs:1232:17
   5:     0x7fe8956e7a75 - std::io::Write::write_fmt::h6f4267f20ec68788
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/io/mod.rs:1682:15
   6:     0x7fe8956f70f5 - std::sys_common::backtrace::_print::hb5c67b8e69014d61
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/sys_common/backtrace.rs:47:5
   7:     0x7fe8956f70f5 - std::sys_common::backtrace::print::h2ff0f6ec8fe8dee2
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/sys_common/backtrace.rs:34:9
   8:     0x7fe8956f9ebf - std::panicking::default_hook::{{closure}}::h8f2dc7f3e286efd1
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/panicking.rs:267:22
   9:     0x7fe8956f9bfb - std::panicking::default_hook::heeca694d4cd7d11c
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/panicking.rs:286:9
  10:     0x565317770f2d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::hb14bd8923604da61
  11:     0x56531777115b - kani_compiler::session::JSON_PANIC_HOOK::{{closure}}::{{closure}}::h83fbfacccda15e89
  12:     0x5653176f09b3 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h8598e9598da8eeb7
  13:     0x7fe8956fa6fa - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h9cd7f28d670041a2
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/alloc/src/boxed.rs:2002:9
  14:     0x7fe8956fa6fa - std::panicking::rust_panic_with_hook::h892e6adff61670d4
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/panicking.rs:692:13
  15:     0x7fe8956fa479 - std::panicking::begin_panic_handler::{{closure}}::he0859e3e131b2a3c
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/panicking.rs:579:13
  16:     0x7fe8956f77dc - std::sys_common::backtrace::__rust_end_short_backtrace::he7b65f460b4dc3cf
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/sys_common/backtrace.rs:137:18
  17:     0x7fe8956fa182 - rust_begin_unwind
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/panicking.rs:575:5
  18:     0x7fe895755e03 - core::panicking::panic_fmt::h4c3a1b54039d0595
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/core/src/panicking.rs:64:14
  19:     0x7fe895756309 - core::panicking::assert_failed_inner::he0ca732d156acafe
  20:     0x56531762fa4b - core::panicking::assert_failed::h60f7762499c7d476
  21:     0x5653178a5595 - cprover_bindings::goto_program::expr::Expr::struct_expr_from_values::h5313170e7983664e
  22:     0x56531767b7f5 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_single_variant_single_field::h856a55abda3a5749
  23:     0x56531767a3bf - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_scalar::hf8dcd8912855886e
  24:     0x565317678073 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_const_value::h2857335c8e791718
  25:     0x56531767756d - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand::h2d62e643e8e5a02d
  26:     0x5653176e7244 - core::ops::function::impls::<impl core::ops::function::FnMut<A> for &mut F>::call_mut::h21e9344438eb315c
  27:     0x565317738ebe - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::h407630fd894e7718
  28:     0x56531769b1c1 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_funcall_args::hc83057b12bf746a4
  29:     0x565317697cbd - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator::h4d86b2ff53a9f0e9
  30:     0x56531763c1f2 - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h4f53ea8d82ff8395
  31:     0x5653176e4480 - std::thread::local::LocalKey<T>::with::h40521ba7a02703d9
  32:     0x565317750be4 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h8b8bdfc55be3a56f
  33:     0x7fe893623081 - <rustc_session[4c51ba081ed00764]::session::Session>::time::<alloc[6e60c50040f84f8b]::boxed::Box<dyn core[be13c3a4a0166a5d]::any::Any>, rustc_interface[5e583a021ee4110c]::passes::start_codegen::{closure#0}>
  34:     0x7fe893622ba9 - rustc_interface[5e583a021ee4110c]::passes::start_codegen
  35:     0x7fe8936206b9 - <rustc_interface[5e583a021ee4110c]::passes::QueryContext>::enter::<<rustc_interface[5e583a021ee4110c]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[be13c3a4a0166a5d]::result::Result<alloc[6e60c50040f84f8b]::boxed::Box<dyn core[be13c3a4a0166a5d]::any::Any>, rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>>
  36:     0x7fe89361c59d - <rustc_interface[5e583a021ee4110c]::queries::Queries>::ongoing_codegen
  37:     0x7fe89361b4bf - rustc_span[90cd83e1cc6358cf]::with_source_map::<core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>, rustc_interface[5e583a021ee4110c]::interface::run_compiler<core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>, rustc_driver[d168a790576a7dcc]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  38:     0x7fe8936130f4 - <scoped_tls[51f5e5aadba18ca0]::ScopedKey<rustc_span[90cd83e1cc6358cf]::SessionGlobals>>::set::<rustc_interface[5e583a021ee4110c]::interface::run_compiler<core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>, rustc_driver[d168a790576a7dcc]::run_compiler::{closure#1}>::{closure#0}, core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>>
  39:     0x7fe8936127f2 - std[6b8bd2f9a6d311d6]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[5e583a021ee4110c]::util::run_in_thread_pool_with_globals<rustc_interface[5e583a021ee4110c]::interface::run_compiler<core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>, rustc_driver[d168a790576a7dcc]::run_compiler::{closure#1}>::{closure#0}, core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>>
  40:     0x7fe893c93d8c - <<std[6b8bd2f9a6d311d6]::thread::Builder>::spawn_unchecked_<rustc_interface[5e583a021ee4110c]::util::run_in_thread_pool_with_globals<rustc_interface[5e583a021ee4110c]::interface::run_compiler<core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>, rustc_driver[d168a790576a7dcc]::run_compiler::{closure#1}>::{closure#0}, core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[be13c3a4a0166a5d]::result::Result<(), rustc_errors[a3f9bdfc7e623733]::ErrorGuaranteed>>::{closure#1} as core[be13c3a4a0166a5d]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  41:     0x7fe895704793 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hf05b4b3c0eebe09f
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/alloc/src/boxed.rs:1988:9
  42:     0x7fe895704793 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h42d3453ce26899c4
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/alloc/src/boxed.rs:1988:9
  43:     0x7fe895704793 - std::sys::unix::thread::Thread::new::thread_start::h53c357220671f65c
                               at /rustc/f3126500f25114ba4e0ac3e76694dd45a22de56d/library/std/src/sys/unix/thread.rs:108:17
  44:     0x7fe890ca744b - start_thread
  45:     0x7fe8906a252f - __clone
  46:                0x0 - <unknown>

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::Mut, u8, bitvec::order::Msb0>::from_slice_mut
_RNvMs0_NtNtCsOWo2AhJUyI_6bitvec3ptr6singleINtB5_6BitPtrNtNtCs7wy8fYxGRNo_3wyz4comu3MuthNtNtB9_5order4Msb0E14from_slice_mutCs6bxxippQzXe_9kani_test
[Kani] current codegen location: Loc { file: "/home/ec2-user/.cargo/registry/src/github.com-1ecc6299db9ec823/bitvec-1.0.1/src/ptr/single.rs", function: None, start_line: 383, start_col: Some(5), end_line: 383, end_col: Some(51) }
error: could not compile `kani-test`
error: Failed to compile `kani-test` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at 'assertion failed: `(left == right)`
                                  left: `2`,
                                 right: `1`: Error in struct_expr; mismatch in number of fields and values.
                                    StructTag("tag-_15362072497429542738")
                                    [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None }]', cprover_bindings/src/goto_program/expr.rs:782:9.
@weaversa weaversa added the [C] Bug This is a bug. Something isn't working. label Apr 12, 2023
@zhassan-aws zhassan-aws added T-High Priority Tag issues that have high priority [F] Crash Kani crashed T-User Tag user issues / requests labels Apr 12, 2023
@zhassan-aws
Copy link
Contributor

The crash can also be reproduced through using the underlying BitPtr directly, e.g.:

use bitvec::prelude::BitPtr;

#[cfg(kani)]
mod tests {
    use super::*;

    #[kani::proof]
    fn some_property() {
        let _bp: bitvec::ptr::BitPtr<bitvec::ptr::Const> = BitPtr::from_slice(&[]);
    }
}

@celinval celinval self-assigned this Apr 13, 2023
@adpaco-aws
Copy link
Contributor

Going from @zhassan-aws' example, I was able to dig a bit deeper. Debug information shows that the crash happens when generating code for the BitIdx::MIN constant:

2023-09-22T21:15:13.056190Z DEBUG CodegenFunction{name="bitvec::ptr::BitPtr::from_slice"}:CodegenTerminator{statement=_0 = bitvec::ptr::BitPtr::<bitvec::ptr::Const, T, O>::new_unchecked(move _2, const _) -> [return: bb3, unwind unreachable]}: kani_compiler::codegen_cprover_gotoc::codegen::operand: codegen_const_unevaluated unevaluated=UnevaluatedConst { def: DefId(22:1213 ~ bitvec[2a78]::index::{impl#0}::MIN), args: [usize], promoted: None }
2023-09-22T21:15:13.056240Z DEBUG CodegenFunction{name="bitvec::ptr::BitPtr::from_slice"}:CodegenTerminator{statement=_0 = bitvec::ptr::BitPtr::<bitvec::ptr::Const, T, O>::new_unchecked(move _2, const _) -> [return: bb3, unwind unreachable]}: kani_compiler::codegen_cprover_gotoc::codegen::operand: codegen_scalar scalar=0x00 ty=Adt(bitvec::index::BitIdx, [usize]) kind=Adt(bitvec::index::BitIdx, [usize]) span=Some(/home/ubuntu/.cargo/registry/src/index.crates.io-6f17d22bba15001f/bitvec-1.0.1/src/ptr/single.rs:338:55: 338:66 (#0))
2023-09-22T21:15:13.056291Z DEBUG CodegenFunction{name="bitvec::ptr::BitPtr::from_slice"}:CodegenTerminator{statement=_0 = bitvec::ptr::BitPtr::<bitvec::ptr::Const, T, O>::new_unchecked(move _2, const _) -> [return: bb3, unwind unreachable]}: kani_compiler::codegen_cprover_gotoc::codegen::typ: variants are: [VariantDef { def_id: DefId(22:4161 ~ bitvec[2a78]::index::BitIdx), ctor: None, name: "BitIdx", discr: Relative(0), fields: [FieldDef { did: DefId(22:4163 ~ bitvec[2a78]::index::BitIdx::idx), name: "idx", vis: Restricted(DefId(22:1188 ~ bitvec[2a78]::index)) }, FieldDef { did: DefId(22:4164 ~ bitvec[2a78]::index::BitIdx::_ty), name: "_ty", vis: Restricted(DefId(22:1188 ~ bitvec[2a78]::index)) }], flags: NO_VARIANT_FLAGS }]
2023-09-22T21:15:13.056355Z DEBUG CodegenFunction{name="bitvec::ptr::BitPtr::from_slice"}:CodegenTerminator{statement=_0 = bitvec::ptr::BitPtr::<bitvec::ptr::Const, T, O>::new_unchecked(move _2, const _) -> [return: bb3, unwind unreachable]}: kani_compiler::codegen_cprover_gotoc::codegen::operand: codegen_scalar scalar=0x00 ty=u8 kind=u8 span=Some(/home/ubuntu/.cargo/registry/src/index.crates.io-6f17d22bba15001f/bitvec-1.0.1/src/ptr/single.rs:338:55: 338:66 (#0))
thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9:
assertion `left == right` failed: Error in struct_expr; mismatch in number of fields and values.
	StructTag("tag-_47075545449858702057406817955082988886")
	[Field { name: "idx", typ: Unsignedbv { width: 8 } }, Field { name: "_ty", typ: StructTag("tag-_151955634556605180765404590810835494927") }]
	[Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]
  left: 2
 right: 1

(Note that I've changed the assertion code to also print the fields.) The definition for BitIdx::MIN is here. We think that this issue and #2680 have the same root cause.

@adpaco-aws adpaco-aws mentioned this issue Sep 28, 2023
Merged
adpaco-aws added a commit that referenced this issue Sep 29, 2023
@adpaco-aws
Avoid mismatch when generating structs that represent scalar data but…
a20437a 
… 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
Assignees

@celinval celinval

@adpaco-aws adpaco-aws

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
Kani 2023-05-08
Status: No status
Kani 2023-10-03
Status: No status
Milestone
No milestone
4 participants
@weaversa @celinval @adpaco-aws @zhassan-aws