Share body cache between harnesses within a codegen unit (#4276)

Improves on #4259 by fully sharing the body cache between harnesses in
the same codegen unit.

This cache initially only stored bodies which had been modified by our
transformations, with the goal being to avoid doing those
transformations multiple times. It does this job well, having a hit rate
of **~66% on queries for modified bodies**[^1].

However, I observed that even just querying to get the initial `Body`
for a given `Instance` was a bottleneck, even if no passes needed to be
applied. And, in this regard, the cache is much less effective, having a
hit rate of **only 1.8% if you count non-modified bodies**[^1].

Thus, this PR also _adds all bodies to the cache, even those which were
not modified_ by our passes.

### Results
This change causes a further **7.7% reduction in the end to end compile
time** of the standard library (@ commit
[177d0fd](model-checking/verify-rust-std@177d0fd)).
The body cache has an **average hit rate of 95.3%** on that workload
and, on a hit, we (at most) have to do an inexpensive clone from the
cache rather than querying `rustc_public`.

As a caching solution, this comes with some memory overhead. Since we're
sharing a cache and caching more bodies, the peak size of this cache has
gone from **0.88 MB to 3.75 MB**. This may seem like a significant
increase (and I'm definitely open to feedback on whether it's
acceptable), but given the fact that Kani hovered around 2.5-3.5 GB of
RAM for that same run, this bigger cache would make up just 0.11%-0.15%
of our total memory use.

[^1]: when verifying the standard library (@ commit
[177d0fd](model-checking/verify-rust-std@177d0fd))

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

Author: AlexanderPortland

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -107,7 +107,7 @@ impl PropertyClass {
     }
 }
 
-impl GotocCtx<'_> {
+impl GotocCtx<'_, '_> {
     /// Generates a CBMC assertion. Note: Does _NOT_ assume.
     pub fn codegen_assert(
         &self,

kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs

@@ -10,7 +10,7 @@ pub fn bb_label(bb: BasicBlockIdx) -> String {
     format!("bb{bb}")
 }
 
-impl GotocCtx<'_> {
+impl GotocCtx<'_, '_> {
     /// Generates Goto-C for a basic block.
     ///
     /// A MIR basic block consists of 0 or more statements followed by a terminator.

kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs

@@ -12,7 +12,7 @@ use rustc_public::mir::{Local, VarDebugInfoContents};
 use rustc_public::rustc_internal;
 use rustc_public::ty::{FnDef, RigidTy, TyKind};
 
-impl GotocCtx<'_> {
+impl GotocCtx<'_, '_> {
     /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
     /// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol
     /// for which it needs to be enforced.
@@ -91,7 +91,7 @@ impl GotocCtx<'_> {
         let contract_attrs =
             KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?;
         let mut find_closure = |inside: Instance, name: &str| {
-            let body = self.transformer.body(self.tcx, inside);
+            let body = self.transformer.body_ref(self.tcx, inside);
             body.var_debug_info.iter().find_map(|var_info| {
                 if var_info.name.as_str() == name {
                     let ty = match &var_info.value {

kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs

@@ -40,7 +40,7 @@ lazy_static! {
     };
 }
 
-impl GotocCtx<'_> {
+impl GotocCtx<'_, '_> {
     /// Generate the symbol and symbol table entry for foreign items.
     ///
     /// CBMC built-in functions that are supported by Kani are always added to the symbol table, and

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -16,7 +16,7 @@ use std::collections::BTreeMap;
 use tracing::{debug, debug_span};
 
 /// Codegen MIR functions into gotoc
-impl GotocCtx<'_> {
+impl GotocCtx<'_, '_> {
     /// Declare variables according to their index.
     /// - Index 0 represents the return value.
     /// - Indices [1, N] represent the function parameters where N is the number of parameters.

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -26,7 +26,7 @@ enum VTableInfo {
     Align,
 }
 
-impl GotocCtx<'_> {
+impl GotocCtx<'_, '_> {
     fn binop<F: FnOnce(Expr, Expr) -> Expr>(
         &mut self,
         place: &Place,

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -27,7 +27,7 @@ enum AllocData<'a> {
     Expr(Expr),
 }
 
-impl<'tcx> GotocCtx<'tcx> {
+impl<'tcx, 'r> GotocCtx<'tcx, 'r> {
     /// Generate a goto expression from a MIR operand.
     ///
     /// A MIR operand is either a constant (literal or `const` declaration) or a place

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -217,7 +217,7 @@ impl TypeOrVariant {
     }
 }
 
-impl GotocCtx<'_> {
+impl GotocCtx<'_, '_> {
     /// Codegen field access for types that allow direct field projection.
     ///
     /// I.e.: Algebraic data types, closures, and coroutines.

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -33,7 +33,7 @@ use rustc_public::ty::{
 use std::collections::BTreeMap;
 use tracing::{debug, trace, warn};
 
-impl GotocCtx<'_> {
+impl GotocCtx<'_, '_> {
     fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand, e2: &Operand) -> Expr {
         let left_op = self.codegen_operand_stable(e1);
         let right_op = self.codegen_operand_stable(e2);

kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs

@@ -31,7 +31,7 @@ lazy_static! {
          ("pointer-primitive", "disable:pointer-primitive-check")].iter().copied().collect();
 }
 
-impl GotocCtx<'_> {
+impl GotocCtx<'_, '_> {
     pub fn codegen_span(&self, sp: &Span) -> Location {
         self.codegen_span_stable(rustc_internal::stable(sp))
     }