Kani internal panic when calling somehwat complex library path with no symbolic inputs #3312
Description
I tried this code:
#[kani::proof]
#[kani::unwind(101)]
fn safe_indexing() {
let args_len: usize = kani::any();
kani::assume(args_len < 100);
let mut args: Vec<i32> = vec![];
for _ in 0..args_len {
args.push(kani::any());
}
let name = "foo".parse().unwrap();
// All we care is that this doesn't panic
let _ = CedarValueJson::extract_arg(&args, &name);
}Where .parse() is created a value of type Name from cedar-policy-core
using the following command line invocation:
cargo kani
with Kani version:
I expected to see this happen: either proof succeeds or fails
Instead, this happened:
error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/stmt.rs:172:9:
assertion `left == right` failed: Error: assign statement with unequal types lhs StructTag("tag-refstr") rhs Pointer { typ: FlexibleArray { typ: Unsignedbv { width: 8 } } }
left: StructTag("tag-refstr")
right: Pointer { typ: FlexibleArray { typ: Unsignedbv { width: 8 } } }.
thread 'rustc' panicked at cprover_bindings/src/goto_program/stmt.rs:172:9:
assertion `left == right` failed: Error: assign statement with unequal types lhs StructTag("tag-refstr") rhs Pointer { typ: FlexibleArray { typ: Unsignedbv { width: 8 } } }
left: StructTag("tag-refstr")
right: Pointer { typ: FlexibleArray { typ: Unsignedbv { width: 8 } } }
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: std::ptr::from_raw_parts::<str>
_RINvNtNtCscBmSNMcqgUz_4core3ptr8metadata14from_raw_partseECs9jBWyIwnR1b_14regex_automata
[Kani] current codegen location: Loc { file: "/github/home/.rustup/toolchains/nightly-2024-05-28-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/metadata.rs", function: None, start_line: 113, start_col: Some(1), end_line: 116, end_col: Some(14) }
error: could not compile `cedar-policy-core` (lib); 8 warnings emitted
error: Failed to compile `cedar_policy_core` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/stmt.rs:172:9:
assertion `left == right` failed: Error: assign statement with unequal types lhs StructTag("tag-refstr") rhs Pointer { typ: FlexibleArray { typ: Unsignedbv { width: 8 } } }
left: StructTag("tag-refstr")
right: Pointer { typ: FlexibleArray { typ: Unsignedbv { width: 8 } } }.