Avoid updating irrelevant symbols when handling quantifiers (#4268)

Kani currently has a special `handle_quantifiers()` pass after codegen
that we need to recursively inline function calls inside quantifier
expressions as needed by our hooks. This has to be done for every value
in the symbol table, but our current implementation implicitly clones
**all `Stmt` type values**, even if they don't contain any quantifiers
and wouldn't need to change. This makes the pass currently take up **~7%
of codegen on crates that don't even use quantifiers**.

Now, the `handle_quantifiers_in_stmt()` function just returns an option
with a new `Stmt` if inlining was needed, or `None` otherwise, allowing
us to avoid any allocations and even needing to insert back into the
table in the common case where a `Stmt` doesn't contain any quantifiers.

### Results
Flamegraphing shows that this change reduces the `handle_quantifiers()`
pass from 7.1% to just 0.8% of codegen for the `s2n-codec` crate.

There was a much less significant change on larger codebases like the
standard library, which only saw **a <1% improvement in end to end
compile time** (at std commit
[177d0fd](model-checking/verify-rust-std@177d0fd),
assuming #4257 & #4259 are merged into Kani). That being said, there was
a significant **1-7% decrease in codegen time** for individual crates of
the standard library, so it seems to still make a difference, even if
not reflected in e2e time.

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/context/goto_ctx.rs

@@ -352,10 +352,10 @@ impl GotocCtx<'_> {
         let mut to_modify: BTreeMap<InternedString, SymbolValues> = BTreeMap::new();
         let mut suffix_count: u16 = 0;
         for (key, symbol) in self.symbol_table.iter() {
-            if let SymbolValues::Stmt(stmt) = &symbol.value {
-                let new_stmt_val =
-                    SymbolValues::Stmt(self.handle_quantifiers_in_stmt(stmt, &mut suffix_count));
-                to_modify.insert(*key, new_stmt_val);
+            if let SymbolValues::Stmt(stmt) = &symbol.value
+                && let Some(new_stmt) = self.handle_quantifiers_in_stmt(stmt, &mut suffix_count)
+            {
+                to_modify.insert(*key, SymbolValues::Stmt(new_stmt));
             }
         }
 
@@ -366,7 +366,8 @@ impl GotocCtx<'_> {
     }
 
     /// Find all quantifier expressions in `stmt` and recursively inline functions.
-    fn handle_quantifiers_in_stmt(&self, stmt: &Stmt, suffix_count: &mut u16) -> Stmt {
+    /// Returns a new [Stmt] if something has been changed (e.g. by inlining), or [None] if it should remain the same.
+    fn handle_quantifiers_in_stmt(&self, stmt: &Stmt, suffix_count: &mut u16) -> Option<Stmt> {
         match &stmt.body() {
             // According to the hook handling for quantifiers, quantifier expressions must be of form
             // lhs = typecast(qex, c_bool)
@@ -432,24 +433,44 @@ impl GotocCtx<'_> {
                             );
                             res.cast_to(Type::CInteger(CIntType::Bool))
                         }
-                        _ => rhs.clone(),
+                        _ => return None,
                     },
-                    _ => rhs.clone(),
+                    _ => return None,
                 };
-                Stmt::assign(lhs.clone(), new_rhs, *stmt.location())
+                Some(Stmt::assign(lhs.clone(), new_rhs, *stmt.location()))
             }
             // Recursively find quantifier expressions.
-            StmtBody::Block(stmts) => Stmt::block(
-                stmts
-                    .iter()
-                    .map(|stmt| self.handle_quantifiers_in_stmt(stmt, suffix_count))
-                    .collect(),
-                *stmt.location(),
-            ),
+            StmtBody::Block(old_stmts) => {
+                let mut replaced_sub_stmts: FxHashMap<usize, Stmt> = FxHashMap::default();
+
+                // For each block, add it and its index to the map if it should be replaced.
+                for (i, stmt) in old_stmts.iter().enumerate() {
+                    if let Some(new_stmt) = self.handle_quantifiers_in_stmt(stmt, suffix_count) {
+                        replaced_sub_stmts.insert(i, new_stmt);
+                    }
+                }
+
+                if replaced_sub_stmts.is_empty() {
+                    // We can skip doing anything if none of the blocks have to be replaced.
+                    None
+                } else {
+                    // Take the replacement block if replaced, otherwise just clone the old value.
+                    Some(Stmt::block(
+                        old_stmts
+                            .iter()
+                            .enumerate()
+                            .map(|(i, old_stmt)| {
+                                replaced_sub_stmts.remove(&i).unwrap_or_else(|| old_stmt.clone())
+                            })
+                            .collect(),
+                        *stmt.location(),
+                    ))
+                }
+            }
             StmtBody::Label { label, body } => {
-                self.handle_quantifiers_in_stmt(body, suffix_count).with_label(*label)
+                Some(self.handle_quantifiers_in_stmt(body, suffix_count)?.with_label(*label))
             }
-            _ => stmt.clone(),
+            _ => None,
         }
     }