Require explicit contract for --replace-call-with-contract

Change --replace-call-with-contract to produce a hard error instead of a
warning when used with functions lacking explicit contracts.  This
change addresses a soundness issue where CBMC would previously assume a
trivial contract automatically.

Users that really need a trivial contract with no constraints should use

````c
int my_function(int x)
  __CPROVER_requires(1)
  __CPROVER_ensures(1)
{
  return x + 1;
}
````

Fixes: #8728

Author: tautschnig

regression/contracts-dfcc/replace-call-no-contract/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+int foo(int x)
+{
+  return x + 1;
+}
+
+int main()
+{
+  int result = foo(5);
+  assert(result == 6);
+  return 0;
+}

regression/contracts-dfcc/replace-call-no-contract/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--replace-call-with-contract foo
+^Function 'foo' does not have a contract\. When using --replace-call-with-contract, a contract must be explicitly provided\. If you need a trivial contract, please add explicit __CPROVER_requires and __CPROVER_ensures clauses to the function\.$
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+Checks that attempting to replace a function call without a contract produces
+an error instead of assuming a trivial contract. This addresses the soundness
+risk identified in issue https://github.com/diffblue/cbmc/issues/8728.

src/goto-instrument/contracts/contracts.cpp

@@ -14,6 +14,7 @@ Date: February 2016
 #include "contracts.h"
 
 #include <util/c_types.h>
+#include <util/exception_utils.h>
 #include <util/format_expr.h>
 #include <util/fresh_symbol.h>
 #include <util/mathematical_expr.h>
@@ -616,6 +617,22 @@ void code_contractst::apply_function_contract(
   // Isolate each component of the contract.
   const auto &type = get_contract(target_function, ns);
 
+  // Check if the function actually has a contract
+  // If not, produce a hard error for soundness
+  const symbolt *contract_sym;
+  if(ns.lookup("contract::" + id2string(target_function), contract_sym))
+  {
+    // no contract provided in the source - this is a soundness issue
+    // when using --replace-call-with-contract
+    throw invalid_input_exceptiont(
+      "Function '" + id2string(target_function) +
+      "' does not have a contract. " +
+      "When using --replace-call-with-contract, a contract must be "
+      "explicitly " +
+      "provided. If you need a trivial contract, please add explicit " +
+      "__CPROVER_requires and __CPROVER_ensures clauses to the function.");
+  }
+
   // Prepare to instantiate expressions in the callee
   // with expressions from the call site (e.g. the return value).
   exprt::operandst instantiation_values;

src/goto-instrument/contracts/doc/user/contracts-cli.md

@@ -11,7 +11,8 @@ goto-instrument [--apply-loop-contracts] [--enforce-contract <function>] (--repl
 Where:
 - `--apply-loop-contracts` is optional and specifies to apply loop contracts globally;
 - `--enforce-contract <function>` is optional and specifies that `function` must be checked against its contract.
-- `--replace-call-with-contract <function>` is optional and specifies that all calls to `function` must be replaced with its contract;
+- `--replace-call-with-contract <function>` is optional and specifies that all calls to `function` must be replaced with its contract.
+  It is an error if `function` does not have a contract.
 
 ## Applying the function contracts transformation (with the dynamic frames method)
 
@@ -27,5 +28,4 @@ Where:
   When `contract` is not specfied, the contract is assumed to be carried by the `function` itself.
 - `--replace-call-with-contract <function>[/<contract>]` is optional and specifies that all calls to `function` must be replaced with `contract`.
   When `contract` is not specfied, the contract is assumed to be carried by the `function` itself.
-
-
+  It is an error if `function` does not have a contract.

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp

@@ -9,6 +9,8 @@ Date: August 2022
 
 #include "dfcc_contract_handler.h"
 
+#include <util/exception_utils.h>
+
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_function_pointers.h>
 
@@ -118,7 +120,8 @@ const symbolt &dfcc_contract_handlert::get_pure_contract_symbol(
   {
     // The contract symbol might not have been created if the function had
     // no contract or a contract with all empty clauses (which is equivalent).
-    // in that case we create a fresh symbol again with empty clauses.
+    // This is a soundness issue when using --replace-call-with-contract
+    // because we should not assume a trivial contract.
     PRECONDITION_WITH_DIAGNOSTICS(
       function_id_opt.has_value(),
       "Contract '" + pure_contract_id +
@@ -129,27 +132,14 @@ const symbolt &dfcc_contract_handlert::get_pure_contract_symbol(
     const auto &function_symbol =
       dfcc_utilst::get_function_symbol(goto_model.symbol_table, function_id);
 
-    log.warning() << "Contract '" << contract_id
-                  << "' not found, deriving empty pure contract '"
-                  << pure_contract_id << "' from function '" << function_id
-                  << "'" << messaget::eom;
-
-    symbolt new_symbol{
-      pure_contract_id, function_symbol.type, function_symbol.mode};
-    new_symbol.base_name = pure_contract_id;
-    new_symbol.pretty_name = pure_contract_id;
-    new_symbol.is_property = true;
-    new_symbol.module = function_symbol.module;
-    new_symbol.location = function_symbol.location;
-    auto entry = goto_model.symbol_table.insert(std::move(new_symbol));
-    INVARIANT(
-      entry.second,
-      "contract '" + id2string(function_symbol.display_name()) +
-        "' already set at " + id2string(entry.first.location.as_string()));
-    // this lookup will work and set the pointer
-    // no need to check for signature compatibility
-    ns.lookup(pure_contract_id, pure_contract_symbol);
-    return *pure_contract_symbol;
+    // Produce a hard error instead of assuming a trivial contract
+    // to address soundness risk
+    throw invalid_input_exceptiont(
+      "Function '" + id2string(function_id) + "' does not have a contract. " +
+      "When using --replace-call-with-contract, a contract must be "
+      "explicitly " +
+      "provided. If you need a trivial contract, please add explicit " +
+      "__CPROVER_requires and __CPROVER_ensures clauses to the function.");
   }
 }