Kani internal panic when calling somehwat complex library path with no symbolic inputs

[aaronjeline]

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 } } }.

[adpaco-aws]

Hi @aaronjeline , thanks for opening this issue! Do you recall in which scope were you defining the safe_indexing harness? Or a branch that allows me to directly reproduce the issue?

[aaronjeline]

Yes. I managed to minimize the test case:

    #[kani::proof]
    fn foo() {
        smol_str::SmolStr::new("foo");
    }

Causes:

error: could not compile `cedar-policy-core` (lib); 7 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 } } }.

[aaronjeline]

(Note that Name uses smolstr internally)

[adpaco-aws]

I see, this test did indeed crash for me too. Thank you for submitting this reproducer!

[celinval]

This seems to happen due to casting *const str <-> *const u8 that happens inside byte_sub. Here is a tiny reproducer:

#![feature(set_ptr_value)]

#[kani::proof]
fn check_cast() {
    let data = "hello";
    let ptr = data as *const str;
    // This cast is done inside byte_sub
    let _ = ptr.cast::<u8>().with_metadata_of(ptr);
}

[celinval]

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);
    }

@aaronjeline I created a fix, but I couldn't verify it with your original example, since it fails to find the extract_args function.