From 2a32be78c763ec1f94da50310483220c7c0bd7b5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 26 Nov 2025 10:49:00 +0000 Subject: [PATCH] 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 --- .../assigns-local-composite/main.c | 2 +- .../contracts-dfcc/assigns_enforce_15/main.c | 2 +- .../contracts-dfcc/assigns_enforce_17/main.c | 2 +- .../contracts-dfcc/assigns_enforce_20/main.c | 2 +- .../assigns_enforce_arrays_01/main.c | 2 +- .../assigns_enforce_arrays_03/main.c | 2 +- .../assigns_enforce_malloc_01/main.c | 2 +- .../assigns_enforce_malloc_02/main.c | 2 +- .../assigns_enforce_malloc_03/main.c | 2 +- .../assigns_enforce_statics/main.c | 2 +- .../assigns_enforce_structs_01/main.c | 2 +- .../assigns_enforce_structs_02/main.c | 2 +- .../assigns_enforce_structs_03/main.c | 2 +- .../assigns_enforce_subfunction_calls/main.c | 2 +- .../contracts-dfcc/assigns_replace_08/main.c | 2 +- .../assigns_type_checking_valid_cases/main.c | 8 ++-- .../test-enforce-warning-not-found.desc | 11 ----- .../havoc-conditional-target/replace-foo.c | 2 +- .../loop_assigns_function_paramters/main.c | 2 +- .../loop_assigns_target_base_idents/main.c | 2 +- .../main.c | 2 +- .../replace-call-no-contract/main.c | 13 ++++++ .../replace-call-no-contract/test.desc | 11 +++++ .../ternary-lhs-loop-contract/main.c | 2 +- .../main.c | 2 +- .../main.c | 2 +- src/goto-instrument/contracts/contracts.cpp | 18 +++++++++ .../contracts/doc/user/contracts-cli.md | 6 +-- .../dynamic-frames/dfcc_contract_handler.cpp | 40 +++++++------------ 29 files changed, 85 insertions(+), 66 deletions(-) delete mode 100644 regression/contracts-dfcc/function-contract-mapping/test-enforce-warning-not-found.desc create mode 100644 regression/contracts-dfcc/replace-call-no-contract/main.c create mode 100644 regression/contracts-dfcc/replace-call-no-contract/test.desc diff --git a/regression/contracts-dfcc/assigns-local-composite/main.c b/regression/contracts-dfcc/assigns-local-composite/main.c index 7b102af7cdd..8de950b2b11 100644 --- 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 index b940ae60b4a..2714219c049 100644 --- 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 index acd818b56d7..e3520b3ed52 100644 --- 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 index 5ff7211df3b..966f37375e4 100644 --- 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 index ee8405c3ce4..ad7803be144 100644 --- 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 index 2511fbe4103..502d47cacb7 100644 --- 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 index 7896a93b158..89c93b4e15c 100644 --- 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 -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 index 5b5ddfb6a69..da5cccb8831 100644 --- 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 -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 index 0c45c0b99a5..bf107794dda 100644 --- 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 -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 index 966c40b0332..3ca043e5812 100644 --- 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 index ee4a59c2b1f..a380394a2f6 100644 --- 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 index fd544aa9148..ccbc8af48d5 100644 --- 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 index a4d282edc25..2fb6eed04f5 100644 --- 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 index dda1ce6aff7..c08bc7fb7f0 100644 --- 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 index 4f6cc637f64..51a10d09672 100644 --- 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 index cc60cad45d0..a548f0f57e8 100644 --- 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 deleted file mode 100644 index 5bc122143e8..00000000000 --- a/regression/contracts-dfcc/function-contract-mapping/test-enforce-warning-not-found.desc +++ /dev/null @@ -1,11 +0,0 @@ -CORE dfcc-only -main.c ---malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contractt _ --pointer-check --pointer-primitive-check --pointer-overflow-check -^Contract 'my_contractt' not found, deriving empty pure contract 'contract::my_contractt' from function 'foo'$ -^VERIFICATION FAILED$ -^EXIT=10$ -^SIGNAL=0$ --- --- -Checks that we get a warning that a default contract is derived from the -signature of the function being checked when specifying a non-existing contract. diff --git a/regression/contracts-dfcc/havoc-conditional-target/replace-foo.c b/regression/contracts-dfcc/havoc-conditional-target/replace-foo.c index 34b9236caf9..111c1005afd 100644 --- 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 index e9384d2f712..e0950d3d62b 100644 --- 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 -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 index a785111100b..74d827d29e3 100644 --- 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 #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 index cd4b9ac8591..ad764ee8ed9 100644 --- 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 new file mode 100644 index 00000000000..e64e8f7af8a --- /dev/null +++ b/regression/contracts-dfcc/replace-call-no-contract/main.c @@ -0,0 +1,13 @@ +#include + +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 new file mode 100644 index 00000000000..592def990d1 --- /dev/null +++ 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 index d1d40996523..741e26c0f12 100644 --- 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 #include -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 index 25ef3bd9809..5f7b42b169d 100644 --- 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 index efd6c7db4de..c21eb201195 100644 --- 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 index 046bc714e97..834aab18df2 100644 --- 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 +#include #include #include #include @@ -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 index 262a48134e5..63a8146a97a 100644 --- 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 ] (--repl Where: - `--apply-loop-contracts` is optional and specifies to apply loop contracts globally; - `--enforce-contract ` is optional and specifies that `function` must be checked against its contract. -- `--replace-call-with-contract ` is optional and specifies that all calls to `function` must be replaced with its contract; +- `--replace-call-with-contract ` 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 [/]` 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 index 88e708417e1..f096e7c2189 100644 --- 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 + #include #include @@ -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."); } }