Emit explicit contract:: symbols for functions with contracts (#4612)

CBMC's DFCC contract instrumentation (`--enforce-contract` /
`--replace-call-with-contract`) expects a dedicated `contract::<fn>`
symbol to exist for any function carrying a contract. For C inputs this
symbol is created by the ANSI-C typechecker, which also moves the
contract clauses (e.g. `c_spec_assigns`) onto it.

Kani builds goto-programs directly and never runs that typechecker, so
the symbol was absent. CBMC used to paper over this by deriving an empty
contract symbol from the function on the fly, but that fallback was
removed for soundness in diffblue/cbmc#8739, turning the missing symbol
into a hard error and breaking every `#[kani::proof_for_contract]`
harness.

Synthesize the companion `contract::<name>` symbol during symbol-table
serialization. It shares the function's contract-bearing type, has no
body, and is marked as a property, reconstructing exactly the symbol
CBMC's typechecker (and its old fallback) produced.

This is a necessary (though not necessarily sufficient) change to enable
upgrading to newer CBMC versions.

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

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

cprover_bindings/src/irep/to_irep.rs

@@ -700,12 +700,73 @@ impl goto_program::Symbol {
     }
 }
 
+impl goto_program::Symbol {
+    /// Build the dedicated `contract::<name>` symbol that CBMC's contract
+    /// instrumentation expects to exist for any function that carries a
+    /// contract.
+    ///
+    /// When CBMC processes C inputs, its ANSI-C typechecker creates this
+    /// symbol (see `c_typecheck_baset` in CBMC) and moves the contract clauses
+    /// (e.g. `c_spec_assigns`) onto it. Kani builds goto-programs directly and
+    /// thus never goes through that typechecker, so we synthesize the symbol
+    /// here. The symbol shares the function's (contract-bearing) type, has no
+    /// body, and is marked as a property.
+    ///
+    /// Historically CBMC would derive this symbol on the fly when it was
+    /// missing, but that fallback was removed for soundness in
+    /// <https://github.com/diffblue/cbmc/pull/8739>, turning the missing
+    /// symbol into a hard error during `--enforce-contract` /
+    /// `--replace-call-with-contract`.
+    ///
+    /// `function_irep` is this symbol already lowered to its `irep` form. We
+    /// reuse its (contract-bearing) type and metadata so the function body is
+    /// not serialized a second time — the contract symbol drops it anyway.
+    fn to_contract_irep(&self, function_irep: &super::Symbol) -> super::Symbol {
+        super::Symbol {
+            // Share the function's contract-bearing type; the contract symbol
+            // is a pure specification with no body.
+            typ: function_irep.typ.clone(),
+            value: Irep::nil(),
+            location: function_irep.location.clone(),
+            name: format!("contract::{}", self.name).into(),
+            is_property: true,
+            // Everything else is copied verbatim from the function symbol.
+            module: function_irep.module,
+            base_name: function_irep.base_name,
+            pretty_name: function_irep.pretty_name,
+            mode: function_irep.mode,
+            is_type: function_irep.is_type,
+            is_macro: function_irep.is_macro,
+            is_exported: function_irep.is_exported,
+            is_input: function_irep.is_input,
+            is_output: function_irep.is_output,
+            is_state_var: function_irep.is_state_var,
+            is_static_lifetime: function_irep.is_static_lifetime,
+            is_thread_local: function_irep.is_thread_local,
+            is_lvalue: function_irep.is_lvalue,
+            is_file_local: function_irep.is_file_local,
+            is_extern: function_irep.is_extern,
+            is_volatile: function_irep.is_volatile,
+            is_parameter: function_irep.is_parameter,
+            is_auxiliary: function_irep.is_auxiliary,
+            is_weak: function_irep.is_weak,
+        }
+    }
+}
+
 impl goto_program::SymbolTable {
     pub fn to_irep(&self) -> super::SymbolTable {
         let mm = self.machine_model();
         let mut st = super::SymbolTable::new();
         for (_key, value) in self.iter() {
-            st.insert(value.to_irep(mm))
+            let symbol_irep = value.to_irep(mm);
+            // Functions carrying a contract need a companion `contract::<name>`
+            // symbol so that CBMC's DFCC contract instrumentation can find it.
+            // See `goto_program::Symbol::to_contract_irep` for details.
+            if value.contract.is_some() {
+                st.insert(value.to_contract_irep(&symbol_irep));
+            }
+            st.insert(symbol_irep);
         }
         st
     }