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

tautschnig · tautschnig · commit 2a32be78c763 · 2025-12-01T17:28:43.000Z
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
diff --git a/regression/contracts-dfcc/assigns-local-composite/main.c b/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];
diff --git a/regression/contracts-dfcc/assigns_enforce_15/main.c b/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;
 }
diff --git a/regression/contracts-dfcc/assigns_enforce_17/main.c b/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++;
diff --git a/regression/contracts-dfcc/assigns_enforce_20/main.c b/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;
diff --git a/regression/contracts-dfcc/assigns_enforce_arrays_01/main.c b/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;
diff --git a/regression/contracts-dfcc/assigns_enforce_arrays_03/main.c 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;
 }
diff --git a/regression/contracts-dfcc/assigns_enforce_malloc_01/main.c b/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;
diff --git a/regression/contracts-dfcc/assigns_enforce_malloc_02/main.c b/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)
   {
diff --git a/regression/contracts-dfcc/assigns_enforce_malloc_03/main.c b/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);
diff --git a/regression/contracts-dfcc/assigns_enforce_statics/main.c b/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;
 
diff --git a/regression/contracts-dfcc/assigns_enforce_structs_01/main.c b/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);
diff --git a/regression/contracts-dfcc/assigns_enforce_structs_02/main.c b/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));
diff --git a/regression/contracts-dfcc/assigns_enforce_structs_03/main.c b/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));
diff --git a/regression/contracts-dfcc/assigns_enforce_subfunction_calls/main.c b/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);
diff --git a/regression/contracts-dfcc/assigns_replace_08/main.c b/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();
 }
diff --git a/regression/contracts-dfcc/assigns_type_checking_valid_cases/main.c b/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;
diff --git a/regression/contracts-dfcc/function-contract-mapping/test-enforce-warning-not-found.desc b/regression/contracts-dfcc/function-contract-mapping/test-enforce-warning-not-found.desc
diff --git a/regression/contracts-dfcc/havoc-conditional-target/replace-foo.c b/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;
diff --git a/regression/contracts-dfcc/loop_assigns_function_paramters/main.c b/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
diff --git a/regression/contracts-dfcc/loop_assigns_target_base_idents/main.c b/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];
diff --git a/regression/contracts-dfcc/memory-predicates-user-defined-ensures-replace/main.c b/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;
diff --git a/regression/contracts-dfcc/replace-call-no-contract/main.c b/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;
+}
diff --git a/regression/contracts-dfcc/replace-call-no-contract/test.desc b/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.
diff --git a/regression/contracts-dfcc/ternary-lhs-loop-contract/main.c b/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];
diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/main.c b/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];
diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/main.c b/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];
diff --git a/src/goto-instrument/contracts/contracts.cpp b/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;
diff --git a/src/goto-instrument/contracts/doc/user/contracts-cli.md b/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.
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp b/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.");
   }
 }
 

Original file line number	Diff line number	Diff line change
`@@ -40,7 +40,7 @@ struct taggedt {`
`40`	`40`	`};`
`41`	`41`	`// clang-format on`
`42`	`42`
`43`		`-int foo(int i) __CPROVER_assigns()`
	`43`	`+int foo(int i) __CPROVER_ensures(1) __CPROVER_assigns()`
`44`	`44`	`{`
`45`	`45`	`// all accesses to locals should pass`
`46`	`46`	`int arr[10];`
Original file line number	Diff line number	Diff line change
`@@ -20,7 +20,7 @@ int baz() __CPROVER_ensures(__CPROVER_return_value == global)`
`20`	`20`	`return global;`
`21`	`21`	`}`
`22`	`22`
`23`		`-void qux(void) __CPROVER_assigns()`
	`23`	`+void qux(void) __CPROVER_ensures(1) __CPROVER_assigns()`
`24`	`24`	`{`
`25`	`25`	`global = global + 1;`
`26`	`26`	`}`
Original file line number	Diff line number	Diff line change
`@@ -2,7 +2,7 @@`
`2`	`2`
`3`	`3`	`int x;`
`4`	`4`
`5`		`-void pure() __CPROVER_assigns()`
	`5`	`+void pure() __CPROVER_ensures(1) __CPROVER_assigns()`
`6`	`6`	`{`
`7`	`7`	`int x;`
`8`	`8`	`x++;`
Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,7 @@`
`3`	`3`
`4`	`4`	`int x = 0;`
`5`	`5`
`6`		`-void foo(int *y) __CPROVER_assigns()`
	`6`	`+void foo(int *y) __CPROVER_ensures(1) __CPROVER_assigns()`
`7`	`7`	`{`
`8`	`8`	`__CPROVER_havoc_object(y);`
`9`	`9`	`x = 2;`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-void f1(int a[], int len) __CPROVER_assigns()`
	`1`	`+void f1(int a[], int len) __CPROVER_ensures(1) __CPROVER_assigns()`
`2`	`2`	`{`
`3`	`3`	`int b[10];`
`4`	`4`	`a = b;`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-void assign_out_under(int a[], int len) __CPROVER_assigns()`
	`1`	`+void assign_out_under(int a[], int len) __CPROVER_ensures(1) __CPROVER_assigns()`
`2`	`2`	`{`
`3`	`3`	`a[1] = 5;`
`4`	`4`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`#include <stdlib.h>`
`2`	`2`
`3`		`-int f(int *a) __CPROVER_assigns()`
	`3`	`+int f(int *a) __CPROVER_ensures(1) __CPROVER_assigns()`
`4`	`4`	`{`
`5`	`5`	`a = (int *)malloc(sizeof(int));`
`6`	`6`	`*a = 5;`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`#include <stdlib.h>`
`2`	`2`
`3`		`-int f(int n, int *ptr) __CPROVER_assigns()`
	`3`	`+int f(int n, int *ptr) __CPROVER_ensures(1) __CPROVER_assigns()`
`4`	`4`	`{`
`5`	`5`	`while(n > 0)`
`6`	`6`	`{`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`#include <stdlib.h>`
`2`	`2`
`3`		`-void foo() __CPROVER_assigns()`
	`3`	`+void foo() __CPROVER_ensures(1) __CPROVER_assigns()`
`4`	`4`	`{`
`5`	`5`	`char *loc1 = malloc(1);`
`6`	`6`	`char *loc2 = malloc(1);`
Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`static int x = 0;`
`2`	`2`
`3`		`-void foo() __CPROVER_assigns()`
	`3`	`+void foo() __CPROVER_ensures(1) __CPROVER_assigns()`
`4`	`4`	`{`
`5`	`5`	`int *y = &x;`
`6`	`6`