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

regression/contracts-dfcc/assigns-local-composite/main.c

@@ -40,7 +40,7 @@ struct taggedt {
 };
 // clang-format on
 
-int foo(int i) __CPROVER_assigns()
+int foo(int i) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   // all accesses to locals should pass
   int arr[10];

regression/contracts-dfcc/assigns_enforce_15/main.c

@@ -20,7 +20,7 @@ int baz() __CPROVER_ensures(__CPROVER_return_value == global)
   return global;
 }
 
-void qux(void) __CPROVER_assigns()
+void qux(void) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   global = global + 1;
 }

regression/contracts-dfcc/assigns_enforce_17/main.c

@@ -2,7 +2,7 @@
 
 int x;
 
-void pure() __CPROVER_assigns()
+void pure() __CPROVER_ensures(1) __CPROVER_assigns()
 {
   int x;
   x++;

regression/contracts-dfcc/assigns_enforce_20/main.c

@@ -3,7 +3,7 @@
 
 int x = 0;
 
-void foo(int *y) __CPROVER_assigns()
+void foo(int *y) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   __CPROVER_havoc_object(y);
   x = 2;

regression/contracts-dfcc/assigns_enforce_arrays_01/main.c

@@ -1,4 +1,4 @@
-void f1(int a[], int len) __CPROVER_assigns()
+void f1(int a[], int len) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   int b[10];
   a = b;

regression/contracts-dfcc/assigns_enforce_arrays_03/main.c

@@ -1,4 +1,4 @@
-void assign_out_under(int a[], int len) __CPROVER_assigns()
+void assign_out_under(int a[], int len) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   a[1] = 5;
 }

regression/contracts-dfcc/assigns_enforce_malloc_01/main.c

@@ -1,6 +1,6 @@
 #include <stdlib.h>
 
-int f(int *a) __CPROVER_assigns()
+int f(int *a) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   a = (int *)malloc(sizeof(int));
   *a = 5;

regression/contracts-dfcc/assigns_enforce_malloc_02/main.c

@@ -1,6 +1,6 @@
 #include <stdlib.h>
 
-int f(int n, int *ptr) __CPROVER_assigns()
+int f(int n, int *ptr) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   while(n > 0)
   {

regression/contracts-dfcc/assigns_enforce_malloc_03/main.c

@@ -1,6 +1,6 @@
 #include <stdlib.h>
 
-void foo() __CPROVER_assigns()
+void foo() __CPROVER_ensures(1) __CPROVER_assigns()
 {
   char *loc1 = malloc(1);
   char *loc2 = malloc(1);

regression/contracts-dfcc/assigns_enforce_statics/main.c

@@ -1,6 +1,6 @@
 static int x = 0;
 
-void foo() __CPROVER_assigns()
+void foo() __CPROVER_ensures(1) __CPROVER_assigns()
 {
   int *y = &x;
 

regression/contracts-dfcc/assigns_enforce_structs_01/main.c

@@ -6,7 +6,7 @@ struct pair
   int y;
 };
 
-int f(int *a) __CPROVER_assigns()
+int f(int *a) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   struct pair *p = (struct pair *)malloc(sizeof(struct pair));
   a = &(p->y);

regression/contracts-dfcc/assigns_enforce_structs_02/main.c

@@ -12,7 +12,7 @@ struct pair_of_pairs
   struct pair p2;
 };
 
-int f(int *a) __CPROVER_assigns()
+int f(int *a) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   struct pair_of_pairs *pop =
     (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));

regression/contracts-dfcc/assigns_enforce_structs_03/main.c

@@ -12,7 +12,7 @@ struct pair_of_pairs
   struct pair p2;
 };
 
-int f(struct pair *a) __CPROVER_assigns()
+int f(struct pair *a) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   struct pair_of_pairs *pop =
     (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));

regression/contracts-dfcc/assigns_enforce_subfunction_calls/main.c

@@ -13,7 +13,7 @@ void bar(int *x, int y)
   return;
 }
 
-void foo(int *x) __CPROVER_assigns()
+void foo(int *x) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   // not allowed, failed check in baz
   bar(x, 2);

regression/contracts-dfcc/assigns_replace_08/main.c

@@ -6,7 +6,7 @@ void bar() __CPROVER_assigns(*z)
 {
 }
 
-void foo() __CPROVER_assigns()
+void foo() __CPROVER_ensures(1) __CPROVER_assigns()
 {
   bar();
 }

regression/contracts-dfcc/assigns_type_checking_valid_cases/main.c

@@ -14,12 +14,12 @@ struct buf
   struct blob aux;
 };
 
-void foo1(int a) __CPROVER_assigns()
+void foo1(int a) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   a = 0;
 }
 
-void foo2(int *b) __CPROVER_assigns()
+void foo2(int *b) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   b = NULL;
 }
@@ -39,7 +39,7 @@ void foo4(int a, int *b, int *c) __CPROVER_requires(c != NULL)
   *x = 0;
 }
 
-void foo5(struct buf buffer) __CPROVER_assigns()
+void foo5(struct buf buffer) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   // these are assignments to the function parameter which is a local symbol
   // and should not generate checks
@@ -75,7 +75,7 @@ void foo8(int array[]) __CPROVER_assigns(__CPROVER_object_whole(array))
   array[9] = 1;
 }
 
-void foo9(int array[]) __CPROVER_assigns()
+void foo9(int array[]) __CPROVER_ensures(1) __CPROVER_assigns()
 {
   int *new_array = NULL;
   array = new_array;

regression/contracts-dfcc/havoc-conditional-target/replace-foo.c

@@ -13,7 +13,7 @@ __CPROVER_ensures(out ==> *out == 1)
 
 int nondet_int();
 
-void bar()
+void bar() __CPROVER_ensures(1)
 {
   int i = 0;
   int *out = nondet_int() ? &i : NULL;

regression/contracts-dfcc/loop_assigns_function_paramters/main.c

@@ -1,6 +1,6 @@
 #include <stdlib.h>
 
-void decr(size_t n)
+void decr(size_t n) __CPROVER_ensures(1)
 {
   for(; n--;)
     // clang-format off

regression/contracts-dfcc/loop_assigns_target_base_idents/main.c

@@ -1,7 +1,7 @@
 #include <stdlib.h>
 
 #define SIZE 32
-int foo() __CPROVER_assigns()
+int foo() __CPROVER_ensures(1) __CPROVER_assigns()
 {
   char buf1[SIZE];
   char buf2[SIZE];

regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/main.c

@@ -92,7 +92,7 @@ __CPROVER_ensures(is_double_buffer(*b))
   *b = create_double_buffer(1, 10);
 }
 
-void bar()
+void bar() __CPROVER_ensures(1)
 {
   list_t *l = NULL;
   double_buffer_t *b = NULL;

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.

regression/contracts-dfcc/ternary-lhs-loop-contract/main.c

@@ -1,7 +1,7 @@
 #include <stdbool.h>
 #include <stdlib.h>
 
-void foo(int a, int b)
+void foo(int a, int b) __CPROVER_ensures(1)
 {
   char arr1[10];
   char arr2[10];

regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/main.c

@@ -12,7 +12,7 @@ __CPROVER_ensures(a[2] == b[2])
 
 int nondet_int();
 
-void bar()
+void bar() __CPROVER_ensures(1)
 {
   int a[6];
   int b[3];

regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/main.c

@@ -12,7 +12,7 @@ __CPROVER_ensures(a[2] == b[2])
 
 int nondet_int();
 
-void bar()
+void bar() __CPROVER_ensures(1)
 {
   int a[6];
   int b[3];

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,23 @@ 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_PREFIX "requires and " CPROVER_PREFIX
+                     "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,38 +120,24 @@ 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 +
         "' not found, the identifier of an existing function must be provided "
         "to derive a default contract");
 
-    auto function_id = function_id_opt.value();
-    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_opt) +
+      "' 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_PREFIX "requires and " CPROVER_PREFIX
+                     "ensures clauses to the function.");
   }
 }