Autoharness crashes due to long filename

[zhassan-aws]

I tried these steps:

1. git clone https://github.com/cedar-policy/cedar
2. cd cedar
3. git checkout cbbb8459a16d9d3725facfa46b214c88fab4484c
4. cargo kani autoharness -Z autoharness

with Kani version: bfb22f1

Kani crashed:

$ cargo kani autoharness -Zautoharness
Kani Rust Verifier 0.65.0 (cargo plugin)
   Compiling cedar-language-server v0.0.1 (/home/ubuntu/git/tmp/cedar/cedar-language-server)
warning: unused variable: `expr`
   --> cedar-policy-core/src/evaluator.rs:329:13
    |
329 |             expr => unreachable!("internal invariant violation: BorrowedRestrictedExpr somehow contained this expr case: {expr:?}"),
    |             ^^^^ help: if this is intentional, prefix it with an underscore: `_expr`
    |
    = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default


thread '<unnamed>' (12343) panicked at kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:642:44:
called `Result::unwrap()` on an `Err` value: Os { code: 36, kind: InvalidFilename, message: "File name too long" }
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] no current codegen item.
[Kani] no current codegen location.
error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:642:44:
                                called `Result::unwrap()` on an `Err` value: Os { code: 36, kind: InvalidFilename, message: "File name too long" }.


thread '<unnamed>' (12345) panicked at kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:642:44:
called `Result::unwrap()` on an `Err` value: Os { code: 36, kind: InvalidFilename, message: "File name too long" }

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] no current codegen item.
[Kani] no current codegen location.

thread '<unnamed>' (12344) panicked at kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:642:44:
called `Result::unwrap()` on an `Err` value: Os { code: 36, kind: InvalidFilename, message: "File name too long" }

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] no current codegen item.
[Kani] no current codegen location.

thread '<unnamed>' (12346) panicked at kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:642:44:
called `Result::unwrap()` on an `Err` value: Os { code: 36, kind: InvalidFilename, message: "File name too long" }

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] no current codegen item.
[Kani] no current codegen location.

[tautschnig]

An example of such a failing name file name is [...]/cedar.git/target/kani/x86_64-unknown-linux-gnu/debug/deps/cedar_language_server-c8366cd73b3525f2__RNvXs0_NtNtNtNtCs2kPvvzHW1G7_21cedar_language_server6policy10completion5items9operatorsNtNtCs35WEYWJCgDy_9lsp_types10completion14CompletionItemINtNtCs44HDJcpWwvY_4core7convert4FromNtB5_17HasCompletionItemE4from_autoharness.pretty_name_map.json. We need to look at ways to use, e.g., stable hashes instead of including the verbatim Rust access path in the file name.
My understanding is that, in order to facilitate such a change in file name constructions, we need to override https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html#method.output_filenames. I believe that means we'll need providers.output_filenames = output_filenames_sha; with a suitably defined function output_filenames_sha in kani-compiler/src/kani_middle/provide.rs.
Edit: I think we need to change how gen_automatic_proof_metadata works.