From 5eab70198b4983effdc552685561bb20a8e7099b Mon Sep 17 00:00:00 2001
From: Justus Adam <justbldr@amazon.com>
Date: Tue, 30 Jan 2024 15:55:44 -0500
Subject: [PATCH] Fixing manes used by contracts metadata

---
 .../src/codegen_cprover_gotoc/compiler_interface.rs  |  4 ++--
 kani-compiler/src/kani_middle/metadata.rs            | 12 ++++++++----
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index e34c5945fbdd..4dd8b6c95bdd 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -7,7 +7,7 @@ use crate::args::ReachabilityType;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::analysis;
 use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes};
-use crate::kani_middle::metadata::gen_test_metadata;
+use crate::kani_middle::metadata::{canonical_mangled_name, gen_test_metadata};
 use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
     collect_reachable_items, filter_const_crate_items, filter_crate_items,
@@ -255,7 +255,7 @@ impl CodegenBackend for GotocCodegenBackend {
                             self.queries
                                 .lock()
                                 .unwrap()
-                                .add_modifies_contract(harness.name().intern(), assigns_contract);
+                                .add_modifies_contract(canonical_mangled_name(harness).intern(), assigns_contract);
                         }
                     }
                 }
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
index 925e79ba7aeb..02f5da107556 100644
--- a/kani-compiler/src/kani_middle/metadata.rs
+++ b/kani-compiler/src/kani_middle/metadata.rs
@@ -14,15 +14,19 @@ use stable_mir::CrateDef;
 
 use super::{attributes::KaniAttributes, SourceLocation};
 
+pub fn canonical_mangled_name(instance: Instance) -> String {
+    let pretty_name = instance.name();
+    // Main function a special case in order to support `--function main`
+    // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
+    if pretty_name == "main" { pretty_name } else { instance.mangled_name() }
+}
+
 /// 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;
     let attributes = KaniAttributes::for_instance(tcx, instance).harness_attributes();
     let pretty_name = instance.name();
-    // Main function a special case in order to support `--function main`
-    // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
-    let mangled_name =
-        if pretty_name == "main" { pretty_name.clone() } else { instance.mangled_name() };
+    let mangled_name = canonical_mangled_name(instance);
 
     // We get the body span to include the entire function definition.
     // This is required for concrete playback to properly position the generated test.