Support function implementations of known built-ins (#3945)

Kani should produce valid symbol tables in GOTO binaries when Rust code
provides an implementation for a built-in known to Kani. Without this
fix, goto-cc fails the following invariant:
```
--- begin invariant violation report ---
Invariant check failed
File: ../src/ansi-c/goto-conversion/goto_convert_functions.cpp:164 function: convert_function
Condition: parameter identifier should not be empty
Reason: !p.empty()
```

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

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

@@ -204,15 +204,22 @@ impl GotocCtx<'_> {
         let body = self.transformer.body(self.tcx, instance);
         self.set_current_fn(instance, &body);
         debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function");
-        self.ensure(instance.mangled_name(), |ctx, fname| {
-            Symbol::function(
-                fname,
-                ctx.fn_typ(instance, &body),
-                None,
-                instance.name(),
-                ctx.codegen_span_stable(instance.def.span()),
-            )
-        });
+        let fname = instance.mangled_name();
+        let sym = Symbol::function(
+            &fname,
+            self.fn_typ(instance, &body),
+            None,
+            instance.name(),
+            self.codegen_span_stable(instance.def.span()),
+        );
+        if !self.symbol_table.contains((&fname).into()) {
+            self.symbol_table.insert(sym);
+        } else {
+            let old_sym = self.symbol_table.lookup(fname).unwrap();
+            if old_sym.location.is_builtin() {
+                self.symbol_table.replace(|_| true, sym);
+            }
+        }
         self.reset_current_fn();
     }
 }

tests/kani/FunctionSymbols/builtin_name.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Function with the same name as a known built-in, but we provide an alternative implementation
+// instead of using the built-in.
+#[no_mangle]
+fn copysign(a: f64, _b: f64) -> f64 {
+    a
+}
+
+#[kani::proof]
+pub fn harness() {
+    let a: f64 = kani::any();
+    let b: f64 = kani::any();
+    copysign(a, b);
+}