Kani + spade panic

[acgetchell]

I tried this code:

https://github.com/acgetchell/cdt-rs/blob/main/src/triangulation.rs#L191

using the following invocation:

https://github.com/acgetchell/cdt-rs/blob/main/.github/workflows/kani.yml

with Kani version:

I expected to see this happen (which was the previous run not using spade):

https://github.com/acgetchell/cdt-rs/actions/runs/6210804977/job/16859411642#step:4:157

Instead, this happened:

https://github.com/acgetchell/cdt-rs/actions/runs/6225368640/job/16895640750#step:4:205

[zhassan-aws]

Thanks for the bug report @acgetchell. This seems similar to the crash in https://github.com/model-checking/kani/issues/2680.

[zhassan-aws]

Here are the steps to reproduce on the spade crate:

1. cargo new spade_dep
2. cd spade_dep
3. cargo add spade
4. Replace src/main.rs with the following:

   
   use spade::{DelaunayTriangulation, Point2, Triangulation};

[kani::proof]

fn main() { let vertices = Vec::new(); let _: DelaunayTriangulation<Point2> = Triangulation::bulk_load(vertices).unwrap(); }

5. Run `cargo kani`

Result:

$ cargo kani Kani Rust Verifier 0.36.0 (cargo plugin) Compiling autocfg v1.1.0 Compiling robust v0.2.3 Compiling smallvec v1.11.0 Compiling optional v0.5.0 Compiling num-traits v0.2.16 Compiling spade v2.2.0 Compiling spade_dep v0.1.0 (/home/ubuntu/examples/iss2776-rep/spade_dep) 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-_318684191582490873510985105409507290320") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 32 }, location: None, size_of_annotation: None }] left: 3 right: 1 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: spade::delaunay_core::dcel_operations::create_single_face_between_edge_and_next::<spade::Point2, (), (), ()> _RINvNtNtCs5NXvurCwQF6_5spade13delaunay_core15dcel_operations40create_single_face_between_edge_and_nextINtNtB6_5point6Point2dEuuuECsj40BlSLqVyv_9spade_dep [Kani] current codegen location: Loc { file: "/home/ubuntu/.cargo/registry/src/index.crates.io-6f17d22bba15001f/spade-2.2.0/src/delaunay_core/dcel_operations.rs", function: None, start_line: 213, start_col: Some(1), end_line: 220, end_col: Some(16) } error: internal compiler error: Kani unexpectedly panicked at 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-_318684191582490873510985105409507290320") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 32 }, location: None, size_of_annotation: None }] left: 3 right: 1.

error: could not compile spade_dep (bin "spade_dep")

[rahulku]

This is being tracked. Closing as dup.

[acgetchell]

Where is it being tracked?

[zhassan-aws]

@acgetchell this was tracked by https://github.com/model-checking/kani/issues/2680, which has been fixed. Are you still seeing a crash with the latest version of Kani (0.40.0)?

[acgetchell]

Ah, thanks, updating Kani fixed it.