Autoharness: use SHA-1 to produce codegen unit file names (#4370)

File names previously had the full Rust access path encoded in the name.
This may exceed (OS-specific) file name length limits. SHA-1 hash the
(mangled) access path for constant-width file names instead (while
maintaining low probability of collision).

Resolves: #4367

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

Cargo.lock

@@ -175,6 +175,15 @@ version = "2.9.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2261d10cca569e4643e526d8dc2e62e433cc8aba21ab764233731f8d369bf394"
 
+[[package]]
+name = "block-buffer"
+version = "0.10.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3078c7629b62d3f0439517fa394996acacc5cbc91c5a20d8c658e77abd503a71"
+dependencies = [
+ "generic-array",
+]
+
 [[package]]
 name = "brownstone"
 version = "3.0.0"
@@ -435,6 +444,12 @@ dependencies = [
  "windows-sys 0.61.0",
 ]
 
+[[package]]
+name = "const-oid"
+version = "0.9.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c2459377285ad874054d797f3ccebf984978aa39129f6eafde5cdc8315b612f8"
+
 [[package]]
 name = "convert_case"
 version = "0.6.0"
@@ -466,6 +481,15 @@ dependencies = [
  "tracing",
 ]
 
+[[package]]
+name = "cpufeatures"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "59ed5838eebb26a2bb2e58f6d5b5316989ae9d08bab10e0e6d103e656d1b0280"
+dependencies = [
+ "libc",
+]
+
 [[package]]
 name = "crossbeam-deque"
 version = "0.8.6"
@@ -514,6 +538,16 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "crypto-common"
+version = "0.1.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1bfb12502f3fc46cca1bb51ac28df9d618d813cdc3d2f25b9fe775a34af26bb3"
+dependencies = [
+ "generic-array",
+ "typenum",
+]
+
 [[package]]
 name = "csv"
 version = "1.3.1"
@@ -608,6 +642,17 @@ version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6184e33543162437515c2e2b48714794e37845ec9851711914eec9d308f6ebe8"
 
+[[package]]
+name = "digest"
+version = "0.10.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292"
+dependencies = [
+ "block-buffer",
+ "const-oid",
+ "crypto-common",
+]
+
 [[package]]
 name = "displaydoc"
 version = "0.2.5"
@@ -747,6 +792,16 @@ dependencies = [
  "percent-encoding",
 ]
 
+[[package]]
+name = "generic-array"
+version = "0.14.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "85649ca51fd72272d7821adaf274ad91c288277713d9c18820d8499a7ff69e9a"
+dependencies = [
+ "typenum",
+ "version_check",
+]
+
 [[package]]
 name = "getopts"
 version = "0.2.24"
@@ -1107,6 +1162,7 @@ dependencies = [
  "regex",
  "serde",
  "serde_json",
+ "sha1-checked",
  "strum",
  "strum_macros",
  "syn",
@@ -1927,6 +1983,27 @@ dependencies = [
  "unsafe-libyaml",
 ]
 
+[[package]]
+name = "sha1"
+version = "0.10.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e3bf829a2d51ab4a5ddf1352d8470c140cadc8301b2ae1789db023f01cedd6ba"
+dependencies = [
+ "cfg-if",
+ "cpufeatures",
+ "digest",
+]
+
+[[package]]
+name = "sha1-checked"
+version = "0.10.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "89f599ac0c323ebb1c6082821a54962b839832b03984598375bff3975b804423"
+dependencies = [
+ "digest",
+ "sha1",
+]
+
 [[package]]
 name = "sharded-slab"
 version = "0.1.7"
@@ -2369,6 +2446,12 @@ version = "1.0.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bc7d623258602320d5c55d1bc22793b57daff0ec7efc270ea7d55ce1d5f5471c"
 
+[[package]]
+name = "typenum"
+version = "1.18.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1dccffe3ce07af9386bfd29e80c0ab1a8205a2fc34e4bcd40364df902cfa8f3f"
+
 [[package]]
 name = "unicode-ident"
 version = "1.0.19"

kani-compiler/Cargo.toml

@@ -20,6 +20,7 @@ quote = "1.0.36"
 regex = "1.11.1"
 serde = { version = "1", optional = true }
 serde_json = "1"
+sha1-checked = "0.10.0"
 strum = "0.27.1"
 strum_macros = "0.27.1"
 syn = { version = "2.0.72", features = ["parsing", "extra-traits"] }

kani-compiler/src/kani_middle/metadata.rs

@@ -14,6 +14,8 @@ use rustc_middle::ty::TyCtxt;
 use rustc_public::mir::mono::Instance;
 use rustc_public::{CrateDef, CrateItems, DefId};
 
+use sha1_checked::Sha1;
+
 /// Create the harness metadata for a proof harness for a given function.
 pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
     let def = instance.def;
@@ -122,8 +124,13 @@ pub fn gen_automatic_proof_metadata(
 
     // Leave the concrete playback instrumentation for now, but this feature does not actually support concrete playback.
     let loc = SourceLocation::new(fn_to_verify.body().unwrap().span);
-    let file_stem =
-        format!("{}_{mangled_name}_autoharness", base_name.file_stem().unwrap().to_str().unwrap());
+    let sha1_result = Sha1::try_digest(mangled_name);
+    assert!(!sha1_result.has_collision());
+    let file_stem = format!(
+        "{}_{:x}_autoharness",
+        base_name.file_stem().unwrap().to_str().unwrap(),
+        sha1_result.hash()
+    );
     let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto);
 
     let kani_attributes = KaniAttributes::for_instance(tcx, *fn_to_verify);