diff --git a/regression/contracts-dfcc/function-pointer-contracts-enforce-1/main.c b/regression/contracts-dfcc/function-pointer-contracts-enforce-1/main.c new file mode 100644 index 00000000000..e9560b441e2 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-enforce-1/main.c @@ -0,0 +1,52 @@ +#include +#include +#include + +typedef int (*fun_t)(int); + +int add_one(int x) + __CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1); + +int foo(fun_t f_in, int x, fun_t *f_out) + // clang-format off +__CPROVER_requires_contract(f_in, add_one, NULL) +__CPROVER_assigns(f_out) +__CPROVER_ensures(f_in ==>__CPROVER_return_value == __CPROVER_old(x) + 1) +__CPROVER_ensures(!f_in ==>__CPROVER_return_value == __CPROVER_old(x)) +__CPROVER_ensures_contract(*f_out, add_one, NULL) +// clang-format on +{ + *f_out = NULL; + if(f_in) + { + *f_out = f_in; + // this branch must be reachable + __CPROVER_assert(false, "then branch is reachable, expecting FAILURE"); + CALL_F_IN: + return f_in(x); + } + else + { + // this branch must be reachable + __CPROVER_assert(false, "else branch is reachable, expecting FAILURE"); + return x; + } +} + +int main() +{ + fun_t f_in; + int x; + fun_t f_out; + foo(f_in, x, &f_out); + if(f_out) + { + __CPROVER_assert(false, "then branch is reachable, expecting FAILURE"); + CALL_F_OUT: + __CPROVER_assert(f_out(1) == 2, "f_out satisfies add_one"); + } + else + { + __CPROVER_assert(false, "else branch is reachable, expecting FAILURE"); + } +} diff --git a/regression/contracts-dfcc/function-pointer-contracts-enforce-1/test.desc b/regression/contracts-dfcc/function-pointer-contracts-enforce-1/test.desc new file mode 100644 index 00000000000..514086a8a9d --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-enforce-1/test.desc @@ -0,0 +1,31 @@ +CORE +main.c +--restrict-function-pointer foo.CALL_F_IN/add_one --restrict-function-pointer main.CALL_F_OUT/add_one --dfcc main --enforce-contract foo +main.c function foo +^\[foo.postcondition.\d+\] line 14 Check ensures clause of contract contract::foo for function foo: SUCCESS$ +^\[foo.postcondition.\d+\] line 15 Check ensures clause of contract contract::foo for function foo: SUCCESS$ +^\[foo.postcondition.\d+\] line 16 Assert function pointer '\*f_out_wrapper' obeys contract 'add_one' or '\(fun_t\)NULL': SUCCESS$ +^\[foo.assigns.\d+\] line 19 Check that \*f_out is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 22 Check that \*f_out is assignable: FAILURE$ +^\[foo.assertion.\d+\] line 24 then branch is reachable, expecting FAILURE: FAILURE$ +^\[foo.pointer_dereference.\d+\] line 26 dereferenced function pointer must be add_one: SUCCESS$ +^\[foo.assertion.\d+\] line 31 else branch is reachable, expecting FAILURE: FAILURE$ +^\[main.assertion.\d+\] line 44 then branch is reachable, expecting FAILURE: FAILURE$ +^\[main.assertion.\d+\] line 46 f_out satisfies add_one: SUCCESS$ +^\[main.pointer_dereference.\d+\] line 46 dereferenced function pointer must be add_one: SUCCESS$ +^\[main.assertion.\d+\] line 50 else branch is reachable, expecting FAILURE: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +foo requires that function pointer f_in satisfies the contract add_one or is NULL. +When f_in is not NULL, foo calls f_in and the post condition of foo is that +of add_one `__CPROVER_return_value == old(x) + 1`. +When f_in is not NULL, foo returns x directly post condition of foo is that +of add_one `__CPROVER_return_value == old(x)`. +The function pointer f_out is ensured to satisfy the add_one contract or be NULL +as a post condition. +The main program calls f_out on a particular value if it is not null and asserts +that the add_one post condition holds for a particular value. +Assertions `assert(false)` are added to all branches to demonstrate reachability. diff --git a/regression/contracts-dfcc/function-pointer-contracts-replace-1/main.c b/regression/contracts-dfcc/function-pointer-contracts-replace-1/main.c new file mode 100644 index 00000000000..c7a8df79834 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-replace-1/main.c @@ -0,0 +1,57 @@ +#include +#include +#include + +typedef int (*fun_t)(int); + +int add_one(int x) + __CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1); + +// returns either a pointer to a function that satisfies add_one or NULL +fun_t get_add_one() + __CPROVER_ensures_contract(__CPROVER_return_value, add_one, NULL); + +int foo(int x, fun_t *f_out) + // clang-format off +__CPROVER_assigns(*f_out) +__CPROVER_ensures( + __CPROVER_return_value == __CPROVER_old(x) + 1 || + __CPROVER_return_value == __CPROVER_old(x)) +__CPROVER_ensures_contract(*f_out, add_one, NULL) +// clang-format on +{ + *f_out = NULL; + // obtain a pointer to a function that satisfies add_one; + fun_t f_in = get_add_one(); + if(f_in) + { + *f_out = f_in; + // this branch must be reachable + __CPROVER_assert(false, "then branch is reachable, expecting FAILURE"); + CALL_F_IN: + return f_in(x); + } + else + { + // this branch must be reachable + __CPROVER_assert(false, "else branch is reachable, expecting FAILURE"); + return x; + } +} + +int main() +{ + int x; + fun_t f_out; + foo(x, &f_out); + if(f_out) + { + __CPROVER_assert(false, "then branch is reachable, expecting FAILURE"); + CALL_F_OUT: + __CPROVER_assert(f_out(1) == 2, "f_out satisfies add_one"); + } + else + { + __CPROVER_assert(false, "else branch is reachable, expecting FAILURE"); + } +} diff --git a/regression/contracts-dfcc/function-pointer-contracts-replace-1/test.desc b/regression/contracts-dfcc/function-pointer-contracts-replace-1/test.desc new file mode 100644 index 00000000000..929c79fdca7 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-replace-1/test.desc @@ -0,0 +1,28 @@ +CORE +main.c +--restrict-function-pointer foo.CALL_F_IN/add_one --restrict-function-pointer main.CALL_F_OUT/add_one --dfcc main --enforce-contract foo --replace-call-with-contract get_add_one +^\[foo.postcondition.\d+\] line 18 Check ensures clause of contract contract::foo for function foo: SUCCESS$ +^\[foo.postcondition.\d+\] line 20 Assert function pointer '\*f_out_wrapper' obeys contract 'add_one' or '\(fun_t\)NULL': SUCCESS$ +^\[foo.assertion.\d+\] line 30 then branch is reachable, expecting FAILURE: FAILURE$ +^\[foo.pointer_dereference.\d+\] line 32 dereferenced function pointer must be add_one: SUCCESS$ +^\[foo.assertion.\d+\] line 37 else branch is reachable, expecting FAILURE: FAILURE$ +^\[main.assertion.\d+\] line 49 then branch is reachable, expecting FAILURE: FAILURE$ +^\[main.assertion.\d+\] line 51 f_out satisfies add_one: SUCCESS$ +^\[main.pointer_dereference.\d+\] line 51 dereferenced function pointer must be add_one: SUCCESS$ +^\[main.assertion.\d+\] line 55 else branch is reachable, expecting FAILURE: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +foo obtains function pointer f_in through get_add_one, which is replaced by +its contract. +When f_in is not NULL, foo calls f_in and the post condition of foo is that +of add_one `__CPROVER_return_value == old(x) + 1`. +When f_in is not NULL, foo returns x directly post condition of foo is that +of add_one `__CPROVER_return_value == old(x)`. +The function pointer f_out is ensured to satisfy the add_one contract or be NULL +as a post condition. +The main program calls f_out on a particular value if it is not null and asserts +that the add_one post condition holds for a particular value. +Assertions `assert(false)` are added to all branches to demonstrate reachability. diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h index 9ab48212c78..7994d043335 100644 --- a/src/ansi-c/c_expr.h +++ b/src/ansi-c/c_expr.h @@ -329,11 +329,11 @@ class function_pointer_obeys_contract_exprt : public exprt public: explicit function_pointer_obeys_contract_exprt( exprt _function_pointer, - exprt _contract) + exprt _contract_pointers) : exprt(ID_function_pointer_obeys_contract, empty_typet{}) { add_to_operands(std::move(_function_pointer)); - add_to_operands(std::move(_contract)); + add_to_operands(std::move(_contract_pointers)); } static void check( @@ -344,6 +344,13 @@ class function_pointer_obeys_contract_exprt : public exprt vm, expr.operands().size() == 2, "function pointer obeys contract expression must have two operands"); + + DATA_CHECK( + vm, + expr.operands()[1].id() == ID_expression_list, + "function pointer obeys contract expression second operand must be an " + "ID_expression_list expression, found " + + id2string(expr.operands()[1].id())); } static void validate( @@ -364,24 +371,14 @@ class function_pointer_obeys_contract_exprt : public exprt return op0(); } - const symbol_exprt &contract_symbol_expr() const - { - return to_symbol_expr(op1().operands().at(0)); - } - - symbol_exprt &contract_symbol_expr() + const exprt::operandst &contract_pointers() const { - return to_symbol_expr(op1().operands().at(0)); - } - - const exprt &address_of_contract() const - { - return op1(); + return op1().operands(); } - exprt &address_of_contract() + exprt::operandst &contract_pointers() { - return op1(); + return op1().operands(); } }; diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 434c83395eb..dc41a9da5c4 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -9,17 +9,17 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// C Language Type Checking -#include "c_typecheck_base.h" - #include #include #include #include #include +#include #include #include "ansi_c_declaration.h" #include "c_expr.h" +#include "c_typecheck_base.h" void c_typecheck_baset::start_typecheck_code() { @@ -1101,11 +1101,11 @@ void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract( { if(!can_cast_expr(expr)) { - error().source_location = expr.source_location(); - error() << "expected ID_function_pointer_obeys_contract expression in " - "requires_contract/ensures_contract clause, found " - << expr.id() << eom; - throw 0; + throw invalid_source_file_exceptiont( + "expected ID_function_pointer_obeys_contract expression in " + "requires_contract/ensures_contract clause, found " + + id2string(expr.id()), + expr.source_location()); } auto &obeys_expr = to_function_pointer_obeys_contract_expr(expr); @@ -1121,60 +1121,73 @@ void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract( function_pointer.type().id() != ID_pointer || to_pointer_type(function_pointer.type()).base_type().id() != ID_code) { - error().source_location = expr.source_location(); - error() << "the first parameter of the clause must be a function pointer " - "expression" - << eom; - throw 0; + throw invalid_source_file_exceptiont( + "the first parameter of the clause must be a function pointer expression", + expr.source_location()); } if(!function_pointer.get_bool(ID_C_lvalue)) { - error().source_location = function_pointer.source_location(); - error() << "first parameter of the clause must be an lvalue" << eom; - throw 0; + throw invalid_source_file_exceptiont( + "the first parameter of the clause must be an lvalue", + function_pointer.source_location()); } if(has_subexpr(function_pointer, ID_side_effect)) { - error().source_location = function_pointer.source_location(); - error() << "first parameter of the clause must have no side-effects" << eom; - throw 0; + throw invalid_source_file_exceptiont( + "the first parameter of the clause must have no side-effects", + function_pointer.source_location()); } if(has_subexpr(function_pointer, ID_if)) { - error().source_location = function_pointer.source_location(); - error() << "first parameter of the clause must have no ternary operator" - << eom; - throw 0; + throw invalid_source_file_exceptiont( + "the first parameter of the clause must have no ternary operator", + function_pointer.source_location()); } - // second parameter must be the address of a function symbol - auto &address_of_contract = obeys_expr.address_of_contract(); - typecheck_expr(address_of_contract); + // second parameter must be a list of size 1 or 2 with: + // - a function symbol with compatible type + // - a null value + auto contract_pointers_size = obeys_expr.contract_pointers().size(); + if(contract_pointers_size < 1 || contract_pointers_size > 2) + { + throw invalid_source_file_exceptiont( + "requires_contract/ensures_contract clauses must have two or three " + "parameters", + obeys_expr.source_location()); + } + auto &first_target = obeys_expr.contract_pointers().at(0); + typecheck_expr(first_target); if( - address_of_contract.id() != ID_address_of || - to_address_of_expr(address_of_contract).object().id() != ID_symbol || - address_of_contract.type().id() != ID_pointer || - to_pointer_type(address_of_contract.type()).base_type().id() != ID_code) - { - error().source_location = expr.source_location(); - error() << "the second parameter of the requires_contract/ensures_contract " - "clause must be a function symbol" - << eom; - throw 0; + first_target.id() != ID_address_of || + to_address_of_expr(first_target).object().id() != ID_symbol || + first_target.type().id() != ID_pointer || + to_pointer_type(first_target.type()).base_type().id() != ID_code || + function_pointer.type() != first_target.type()) + { + throw invalid_source_file_exceptiont( + "the second parameter of the clause must be a pointer to a contract " + "symbol with the same type as the first parameter", + first_target.source_location()); } - if(function_pointer.type() != address_of_contract.type()) + if(contract_pointers_size == 2) { - error().source_location = expr.source_location(); - error() << "the first and second parameter of the " - "requires_contract/ensures_contract clause must have the same " - "function pointer type " - << eom; - throw 0; + auto &second_target = obeys_expr.contract_pointers().at(1); + typecheck_expr(second_target); + auto simplified = simplify_expr(second_target, namespacet(symbol_table)); + if( + !simplified.is_constant() || + !is_null_pointer(to_constant_expr(simplified))) + throw invalid_source_file_exceptiont( + "the (optional) third parameter of the clause must be NULL", + second_target.source_location()); + // add typecast around NULL + obeys_expr.contract_pointers()[1] = + typecast_exprt(simplified, function_pointer.type()); } } diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 16fd64254d9..e2863941f7c 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -3299,7 +3299,7 @@ cprover_function_contract: set($$, ID_C_spec_requires); mto($$, $3); } - | TOK_CPROVER_ENSURES_CONTRACT '(' unary_expression ',' unary_expression ')' + | TOK_CPROVER_ENSURES_CONTRACT '(' unary_expression ',' unary_expression_list ')' { $$=$1; set($$, ID_C_spec_ensures_contract); @@ -3309,7 +3309,7 @@ cprover_function_contract: tmp.add_source_location()=parser_stack($$).source_location(); parser_stack($$).add_to_operands(std::move(tmp)); } - | TOK_CPROVER_REQUIRES_CONTRACT '(' unary_expression ',' unary_expression ')' + | TOK_CPROVER_REQUIRES_CONTRACT '(' unary_expression ',' unary_expression_list ')' { $$=$1; set($$, ID_C_spec_requires_contract); diff --git a/src/goto-instrument/contracts/doc/user/contracts-assigns.md b/src/goto-instrument/contracts/doc/user/contracts-assigns.md index 5ee8ea7bb3a..d5566ea5581 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-assigns.md +++ b/src/goto-instrument/contracts/doc/user/contracts-assigns.md @@ -502,6 +502,7 @@ int foo() - @ref contracts-functions - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract - @ref contracts-assigns - @ref contracts-frees - @ref contracts-loops diff --git a/src/goto-instrument/contracts/doc/user/contracts-decreases.md b/src/goto-instrument/contracts/doc/user/contracts-decreases.md index 1a90ab7fa04..a2e43d2f742 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-decreases.md +++ b/src/goto-instrument/contracts/doc/user/contracts-decreases.md @@ -179,6 +179,7 @@ then the weakest possible invariant (i.e, `true`) is used to model an arbitrary - @ref contracts-functions - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract - @ref contracts-assigns - @ref contracts-frees - @ref contracts-loops diff --git a/src/goto-instrument/contracts/doc/user/contracts-functions.md b/src/goto-instrument/contracts/doc/user/contracts-functions.md index 485d7bf4de7..90bb7075072 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-functions.md +++ b/src/goto-instrument/contracts/doc/user/contracts-functions.md @@ -154,6 +154,7 @@ program using contracts. - @ref contracts-functions - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract - @ref contracts-assigns - @ref contracts-frees - @ref contracts-loops diff --git a/src/goto-instrument/contracts/doc/user/contracts-history-variables.md b/src/goto-instrument/contracts/doc/user/contracts-history-variables.md index a82aef9be55..0e211ae26ac 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-history-variables.md +++ b/src/goto-instrument/contracts/doc/user/contracts-history-variables.md @@ -48,6 +48,7 @@ TODO: Document `__CPROVER_loop_entry` and `__CPROVER_loop_old`. - @ref contracts-functions - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract - @ref contracts-assigns - @ref contracts-frees - @ref contracts-loops diff --git a/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md b/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md index 76db14076ad..ac510bab45a 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md +++ b/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md @@ -157,6 +157,7 @@ A few things to note here: - @ref contracts-functions - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract - @ref contracts-assigns - @ref contracts-frees - @ref contracts-loops diff --git a/src/goto-instrument/contracts/doc/user/contracts-loops.md b/src/goto-instrument/contracts/doc/user/contracts-loops.md index 3f9c27ef1b5..a2bacde716b 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-loops.md +++ b/src/goto-instrument/contracts/doc/user/contracts-loops.md @@ -147,6 +147,7 @@ and finally we verify the instrumented GOTO binary with desired checks. - @ref contracts-functions - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract - @ref contracts-assigns - @ref contracts-frees - @ref contracts-loops diff --git a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md index 5bfa5a10ee8..e243b765102 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md +++ b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md @@ -124,6 +124,7 @@ int foo() - @ref contracts-functions - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract - @ref contracts-assigns - @ref contracts-frees - @ref contracts-loops diff --git a/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md b/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md index 8f356e4878b..09888b1bb19 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md +++ b/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md @@ -96,6 +96,7 @@ int bar_sat(int *arr, int len) - @ref contracts-functions - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract - @ref contracts-assigns - @ref contracts-frees - @ref contracts-loops diff --git a/src/goto-instrument/contracts/doc/user/contracts-requires-ensures-contract.md b/src/goto-instrument/contracts/doc/user/contracts-requires-ensures-contract.md new file mode 100644 index 00000000000..812db7f2a52 --- /dev/null +++ b/src/goto-instrument/contracts/doc/user/contracts-requires-ensures-contract.md @@ -0,0 +1,180 @@ +# Requires and Ensures Clauses {#contracts-requires-ensures-contract} + +Back to @ref contracts-user + +@tableofcontents + +## Syntax + +```c +__CPROVER_requires_contract(function_pointer, contract_id (, NULL)?) +``` + +A _requires contract_ clause specifies the precondition that a function pointer +points to a function satisfying a given contract, or is optionally NULL. + +```c +__CPROVER_ensures_contract(function_pointer, contract_id (, NULL)?) +``` + +A _ensures contract_ clause specifies the postcondition that a function pointer +points to a function satisfying a given contract, or is optionally NULL. + +## Semantics + +The semantics of _requires contract_ and _ensures contract_ clauses can be +understood in two contexts: enforcement and replacement. + +To illustrate these two perspectives, consider the following program: + +```c +#include +#include +#include + +typedef int (*fun_t)(int); + +int add_one(int x) +__CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1); + +// returns either a pointer to a function that satisfies add_one or NULL +fun_t get_add_one() +__CPROVER_ensures_contract(__CPROVER_return_value, add_one); + +int foo(fun_t f_in, int x, fun_t *f_out) +__CPROVER_requires_contract(f_in, add_one, NULL) +__CPROVER_assigns(*f_out) +__CPROVER_ensures(__CPROVER_return_value == __CPROVER_old(x) + 1) +__CPROVER_ensures_contract(*f_out, add_one) +{ + if (f_in) + { + *f_out = f_in; + } + else + { + *f_out = get_add_one(); + } + +CALL: + return (*f_out)(x); +} + +int main() +{ + fun_t f_in; + int x; + fun_t f_out; + foo(f_in, x, &f_out); +CALL: + __CPROVER_assert(f_out(1) == 2, "f_out satisfies add_one"); +} +``` + +The function `add_one` is a contract that describes a function that adds one +to its input. +The function `get_add_one` is a contract that describes a function returning a +pointer to a function satisfying the contract `add_one`. + +The Function `foo` takes a function pointer `f_in` as input and requires that +it either satisfies `add_one` or is NULL; +If `f_in` is not NULL, `foo` set `f_out` to `f_in`; +If `f_in` is NULL, `foo` calls `get_add_one` to set `f_out` to a non-NULL + pointer to a function that satisfies `add_one`; +The function `foo` returns the result of applying `f_out` to its input, which +allows to establish its post condition. +The `main` function calls `f_out(1)` and checks if the `add_one` contract holds +for this particular input. + +This program is instrumented using the following commands: + +``` +goto-cc main.c -o a.out +goto-instrument --dfcc main --restrict-function-pointer foo.CALL/add_one --restrict-function-pointer main.CALL/add_one --enforce-contract foo --replace-call-with-contract get_add_one a.out b.out +``` + +The function pointer restrictions are let CBMC know that the function pointers +in `foo` and `main` must be pointing to the function `add_one`, which serves as +the cannonical representation of the assumed contract. These assumptions will be +checked by CBMC, i.e. if it is possible that the function pointer points to +another function the analysis will fail. + +The analysis results are the following: + +``` +cbmc b.out + +... + +main.c function foo +[foo.postcondition.1] line 15 Check ensures clause of contract contract::foo for function foo: SUCCESS +[foo.postcondition.2] line 16 Assert function pointer '*f_out_wrapper' obeys contract 'add_one': SUCCESS +[foo.assigns.1] line 18 Check that *f_out is assignable: SUCCESS +[foo.assigns.3] line 20 Check that *f_out is assignable: SUCCESS +[foo.pointer_dereference.1] line 22 dereferenced function pointer must be add_one: SUCCESS + +main.c function main +[main.assertion.1] line 31 f_out satisfies add_one: SUCCESS +[main.pointer_dereference.1] line 31 dereferenced function pointer must be add_one: SUCCESS + +** 0 of 56 failed (1 iterations) +VERIFICATION SUCCESSFUL +``` + +### Enforcement + +When enforcing a contract, a clause + +```c +__CPROVER_requires(function_pointer, contract_id, NULL) +``` + +is turned into a non-deterministic assignment and inserted before the call site +of the function under verification: + + +```c +function_pointer = nondet() ? &contract_id : NULL; +``` + +That way, the function under verification receives a pointer to the +`contract_id` function. The instrumentation pass also generates a body for the +function `contract_id` from its contract clauses, so it becomes the canonical +representation of the contract. + +An _ensures contract_ clause: + +```c +__CPROVER_ensures(function_pointer, contract_id, NULL) +``` + +is turned into an assertion: + +```c +assert(function_pointer ==> function_pointer == &contract_id); +``` + +That checks that whenever the `function_pointer` is not null, it points to the +function `contract_id`, the canonical representation of the contract. + +### Replacement + +For contract replacement, the dual transformation is used: _requires contract_ +clauses are turned into assertions, and _ensures contract_ clauses are turned +into nondeterministic assignments. + +## Additional Resources + +- @ref contracts-functions + - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract + - @ref contracts-assigns + - @ref contracts-frees +- @ref contracts-loops + - @ref contracts-loop-invariants + - @ref contracts-decreases + - @ref contracts-assigns + - @ref contracts-frees +- @ref contracts-memory-predicates +- @ref contracts-history-variables +- @ref contracts-quantifiers diff --git a/src/goto-instrument/contracts/doc/user/contracts-requires-ensures.md b/src/goto-instrument/contracts/doc/user/contracts-requires-ensures.md index 89b3474dd36..cd1ee8a87cc 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-requires-ensures.md +++ b/src/goto-instrument/contracts/doc/user/contracts-requires-ensures.md @@ -179,6 +179,7 @@ int foo() - @ref contracts-functions - @ref contracts-requires-ensures + - @ref contracts-requires-ensures-contract - @ref contracts-assigns - @ref contracts-frees - @ref contracts-loops diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index 6ef75380955..2fe2804c6c9 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -877,22 +877,38 @@ void dfcc_wrapper_programt::assert_function_pointer_obeys_contract( const irep_idt &property_class, goto_programt &dest) { - function_pointer_contracts.insert( - expr.contract_symbol_expr().get_identifier()); source_locationt loc(expr.source_location()); loc.set_property_class(property_class); std::stringstream comment; comment << "Assert function pointer '" << from_expr_using_mode( ns, contract_symbol.mode, expr.function_pointer()) - << "' obeys contract '" - << from_expr_using_mode( - ns, contract_symbol.mode, expr.address_of_contract()) - << "'"; + << "' obeys contract "; + + exprt::operandst disjuncts; + + for(std::size_t i = 0; i < expr.contract_pointers().size(); i++) + { + const exprt &contract_pointer = expr.contract_pointers().at(i); + if(contract_pointer.id() == ID_address_of) + { + function_pointer_contracts.insert( + to_symbol_expr(to_address_of_expr(contract_pointer).object()) + .get_identifier()); + } + if(i > 0) + comment << " or "; + + comment << "'" + << from_expr_using_mode(ns, contract_symbol.mode, contract_pointer) + << "'"; + disjuncts.push_back(equal_exprt{expr.function_pointer(), contract_pointer}); + } loc.set_comment(comment.str()); - code_assertt assert_expr( - equal_exprt{expr.function_pointer(), expr.address_of_contract()}); + + code_assertt assert_expr{or_exprt{disjuncts}}; assert_expr.add_source_location() = loc; + goto_programt instructions; converter.goto_convert(assert_expr, instructions, contract_symbol.mode); dest.destructive_append(instructions); @@ -902,21 +918,60 @@ void dfcc_wrapper_programt::assume_function_pointer_obeys_contract( const function_pointer_obeys_contract_exprt &expr, goto_programt &dest) { - function_pointer_contracts.insert( - expr.contract_symbol_expr().get_identifier()); + for(std::size_t i = 0; i < expr.contract_pointers().size(); i++) + { + const exprt &contract_pointer = expr.contract_pointers().at(i); - source_locationt loc(expr.source_location()); - std::stringstream comment; - comment << "Assume function pointer '" - << from_expr_using_mode( - ns, contract_symbol.mode, expr.function_pointer()) - << "' obeys contract '" - << from_expr_using_mode( - ns, contract_symbol.mode, expr.contract_symbol_expr()) - << "'"; - loc.set_comment(comment.str()); - dest.add(goto_programt::make_assignment( - expr.function_pointer(), expr.address_of_contract(), loc)); + if(contract_pointer.id() == ID_address_of) + { + function_pointer_contracts.insert( + to_symbol_expr(to_address_of_expr(contract_pointer).object()) + .get_identifier()); + } + + const auto &loc = contract_pointer.source_location(); + if(i == 0) + { + // First is assignment unconditional + // ``` + // function_pointer := contract_pointer; + // ``` + dest.add(goto_programt::make_assignment( + expr.function_pointer(), contract_pointer, loc)); + } + else + { + // Remaining are nondet + // ``` + // DECL skip: bool + // ASSIGN skip = nondet_bool; + // IF skip goto skip_label; + // function_pointer = contract_pointer; + // skip_label: + // DEAD skip; + // ``` + const auto skip_var = utils + .create_symbol( + bool_typet(), + wrapped_symbol.name, + "skip", + loc, + wrapper_symbol.mode, + wrapper_symbol.module, + false) + .symbol_expr(); + dest.add(goto_programt::make_decl(skip_var, loc)); + dest.add(goto_programt::make_assignment( + skip_var, side_effect_expr_nondett(bool_typet(), loc), loc)); + auto goto_instr = + dest.add(goto_programt::make_incomplete_goto(skip_var, loc)); + dest.add(goto_programt::make_assignment( + expr.function_pointer(), contract_pointer, loc)); + auto skip_target = dest.add(goto_programt::make_skip(loc)); + goto_instr->complete_goto(skip_target); + dest.add(goto_programt::make_dead(skip_var, loc)); + } + } } void dfcc_wrapper_programt::encode_function_call()