diff --git a/regression/contracts-dfcc/function-pointer-contracts-enforce/main.c b/regression/contracts-dfcc/function-pointer-contracts-enforce/main.c new file mode 100644 index 00000000000..469bb10071b --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-enforce/main.c @@ -0,0 +1,45 @@ +#include +#include + +// type of functions that manipulate arrays +typedef void (*arr_fun_t)(char *arr, size_t size); + +// A contract for the arr_fun_t type +// requires a fresh array and positive size +// resets the first element to zero +void arr_fun_contract(char *arr, size_t size) + // clang-format off +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0]) +__CPROVER_ensures(arr[0] == 0) + // clang-format on + ; + +// Testing pre-conditions constructs +// Takes a function pointer as input, uses it if its preconditions are met +// to establish post-conditions +int foo(char *arr, size_t size, arr_fun_t arr_fun) + // clang-format off +__CPROVER_requires(arr == NULL || __CPROVER_is_fresh(arr, size)) +__CPROVER_requires(__CPROVER_obeys_contract(arr_fun, arr_fun_contract)) +__CPROVER_assigns(arr && size > 0 : arr[0]) +__CPROVER_ensures((__CPROVER_return_value == 0) ==> (arr[0] == 0)) +// clang-format on +{ + int retval = -1; + if(arr && size > 0) + { + CALL: + arr_fun(arr, size); + retval = 0; + } + return retval; +} + +void main() +{ + size_t size; + char *arr; + arr_fun_t fun; + foo(arr, size, fun); +} diff --git a/regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc b/regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc new file mode 100644 index 00000000000..2a1130b1606 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--restrict-function-pointer foo.CALL/arr_fun_contract --dfcc main --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks that when a function taking a function pointer as input satisfying a given +contract is checked against its contract, the function pointer can be called +like a regular function pointer and establishes the post conditions specified +by its contract. 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..ef258461a5c --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-replace-1/main.c @@ -0,0 +1,38 @@ +#include +#include + +// type of functions that manipulate arrays +typedef void (*arr_fun_t)(char *arr, size_t size); + +// A contract for the arr_fun_t type +void arr_fun_contract(char *arr, size_t size) + // clang-format off +__CPROVER_requires((size > 0 && __CPROVER_is_fresh(arr, size))) +__CPROVER_assigns(arr[0]) +__CPROVER_ensures(arr[0] == 0) + // clang-format on + ; + +arr_fun_t foo(arr_fun_t infun, arr_fun_t *outfun) + // clang-format off +__CPROVER_requires(__CPROVER_obeys_contract(infun, arr_fun_contract)) +__CPROVER_ensures(__CPROVER_obeys_contract(*outfun, arr_fun_contract)) +__CPROVER_ensures(__CPROVER_obeys_contract(__CPROVER_return_value, arr_fun_contract)) +// clang-format on +{ + *outfun = arr_fun_contract; + return infun; +} + +void main() +{ + // establish pre-conditions before replacement + arr_fun_t infun = arr_fun_contract; + + arr_fun_t outfun1 = NULL; + arr_fun_t outfun2 = foo(infun, &outfun1); + + // checking post-conditions after replacement + assert(outfun1 == arr_fun_contract); + assert(outfun2 == arr_fun_contract); +} 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..59c119b8546 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-replace-1/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--dfcc main --replace-call-with-contract foo +^\[main.assertion.\d+\].*assertion outfun1 == arr_fun_contract: SUCCESS$ +^\[main.assertion.\d+\].*assertion outfun2 == arr_fun_contract: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that, when replacing a call by its contract, +requires_contract clauses are translated to equality checks +and that ensures_contract are translated to assignments of the function pointer +variable to the contract symbol. diff --git a/regression/contracts-dfcc/function-pointer-contracts-replace-2/main.c b/regression/contracts-dfcc/function-pointer-contracts-replace-2/main.c new file mode 100644 index 00000000000..13e6205c520 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-replace-2/main.c @@ -0,0 +1,66 @@ +#include + +// Type of functions that manipulate arrays of a given size +typedef void (*arr_fun_t)(char *arr, size_t size); + +// A contract for the arr_fun_t type +void arr_fun_contract(char *arr, size_t size) + // clang-format off + __CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) + __CPROVER_assigns(arr[0]) __CPROVER_ensures(arr[0] == 0) + // clang-format on + ; + +// Uses a function pointer +int foo(char *arr, size_t size, arr_fun_t arr_fun) + // clang-format off +__CPROVER_requires(arr ==> __CPROVER_is_fresh(arr, size)) +__CPROVER_requires( + arr_fun ==> __CPROVER_obeys_contract(arr_fun, arr_fun_contract)) +__CPROVER_assigns(arr && size > 0 && arr_fun: arr[0]) +__CPROVER_ensures(__CPROVER_return_value ==> (arr[0] == 0)) +// clang-format on +{ + if(arr && size > 0 && arr_fun) + { + CALL: + arr_fun(arr, size); + return 1; + } + return 0; +} + +// returns function pointer satisfying arr_fun_contract +arr_fun_t get_arr_fun() + // clang-format off +__CPROVER_ensures( + __CPROVER_obeys_contract(__CPROVER_return_value, arr_fun_contract)) + // clang-format on + ; + +// allocates an array and uses get_arr_fun and foo to initialise it +char *bar(size_t size) + // clang-format off +__CPROVER_ensures( + __CPROVER_return_value ==> size > 0 && + __CPROVER_is_fresh(__CPROVER_return_value, size) && + __CPROVER_return_value[0] == 0) +// clang-format on +{ + if(size > 0) + { + char *arr; + arr = malloc(size); + if(arr && foo(arr, size, get_arr_fun())) + return arr; + + return NULL; + } + return NULL; +} + +void main() +{ + size_t size; + char *arr = bar(size); +} diff --git a/regression/contracts-dfcc/function-pointer-contracts-replace-2/test.desc b/regression/contracts-dfcc/function-pointer-contracts-replace-2/test.desc new file mode 100644 index 00000000000..36bb450f58b --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-replace-2/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--dfcc main --enforce-contract bar --replace-call-with-contract foo --replace-call-with-contract get_arr_fun +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks that when a function returning a function pointer satisfying a given +contract is replaced by its contract, the returned function pointer can be +passed to another function requiring the same contract. diff --git a/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-1/main.c b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-1/main.c new file mode 100644 index 00000000000..814d1c53e4d --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-1/main.c @@ -0,0 +1,21 @@ +#include +#include + +// type of functions that manipulate arrays +typedef void (*fun_t)(char *arr, size_t size); + +void contract(char *arr, size_t size); + +int foo(char *arr, size_t size, fun_t fun) + __CPROVER_requires(__CPROVER_obeys_contract(fun, contract, contract)) +{ + return 0; +} + +void main() +{ + size_t size; + char *arr; + fun_t fun; + foo(arr, size, fun); +} diff --git a/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-1/test.desc b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-1/test.desc new file mode 100644 index 00000000000..8cb9df3d1c7 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-1/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo +^.*error: expected 2 arguments for __CPROVER_obeys_contract, found 3$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +Checks that malformed __CPROVER_obeys_contract predicate expressions are rejected. diff --git a/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-2/main.c b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-2/main.c new file mode 100644 index 00000000000..fc9d9937794 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-2/main.c @@ -0,0 +1,21 @@ +#include +#include + +// type of functions that manipulate arrays +typedef void (*fun_t)(char *arr, size_t size); + +void contract(char *arr, size_t size); + +int foo(char *arr, size_t size, fun_t fun) + __CPROVER_requires(__CPROVER_obeys_contract(true ? fun : fun, contract)) +{ + return 0; +} + +void main() +{ + size_t size; + char *arr; + fun_t fun; + foo(arr, size, fun); +} diff --git a/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-2/test.desc b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-2/test.desc new file mode 100644 index 00000000000..76dbc92806b --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-2/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo +^.*error: the first argument of __CPROVER_obeys_contract must have no ternary operator$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +Checks that malformed __CPROVER_obeys_contract predicate expressions are rejected. diff --git a/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-3/main.c b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-3/main.c new file mode 100644 index 00000000000..d9b15ed8475 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-3/main.c @@ -0,0 +1,28 @@ +#include +#include + +// type of functions that manipulate arrays +typedef void (*fun_t)(char *arr, size_t size); + +void contract(char *arr, size_t size); + +typedef void (*voidfun_t)(void); + +voidfun_t identity(voidfun_t fun) +{ + return fun; +} + +int foo(char *arr, size_t size, fun_t fun) + __CPROVER_requires(__CPROVER_obeys_contract(identity(fun), contract)) +{ + return 0; +} + +void main() +{ + size_t size; + char *arr; + fun_t fun; + foo(arr, size, fun); +} diff --git a/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-3/test.desc b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-3/test.desc new file mode 100644 index 00000000000..aa6a34bf80e --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-3/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo +^.*error: the first argument of __CPROVER_obeys_contract must be a function pointer lvalue expression$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +Checks that malformed __CPROVER_obeys_contract predicate expressions are rejected. diff --git a/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-4/main.c b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-4/main.c new file mode 100644 index 00000000000..7320d355a2a --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-4/main.c @@ -0,0 +1,28 @@ +#include +#include + +// type of functions that manipulate arrays +typedef void (*fun_t)(char *arr, size_t size); + +void contract(char *arr, size_t size, bool b); + +typedef void (*voidfun_t)(void); + +voidfun_t identity(voidfun_t fun) +{ + return fun; +} + +int foo(char *arr, size_t size, fun_t fun) + __CPROVER_requires(__CPROVER_obeys_contract(fun, contract)) +{ + return 0; +} + +void main() +{ + size_t size; + char *arr; + fun_t fun; + foo(arr, size, fun); +} diff --git a/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-4/test.desc b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-4/test.desc new file mode 100644 index 00000000000..dd06206a628 --- /dev/null +++ b/regression/contracts-dfcc/function-pointer-contracts-typecheck-error-4/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--dfcc main --enforce-contract foo +^.*error: the first and second arguments of __CPROVER_obeys_contract must have the same function pointer type$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +Checks that malformed __CPROVER_obeys_contract predicate expressions are rejected. diff --git a/regression/contracts/function-pointer-contracts-enforce/main.c b/regression/contracts/function-pointer-contracts-enforce/main.c new file mode 100644 index 00000000000..c6815c9ed73 --- /dev/null +++ b/regression/contracts/function-pointer-contracts-enforce/main.c @@ -0,0 +1,44 @@ +#include +#include + +// type of functions that manipulate arrays +typedef void (*arr_fun_t)(char *arr, size_t size); + +// A contract for the arr_fun_t type +// requires a fresh array and positive size +// resets the first element to zero +void arr_fun_contract(char *arr, size_t size) + // clang-format off +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0]) +__CPROVER_ensures(arr[0] == 0) +; + +// Testing pre-conditions constructs +// Takes a function pointer as input, uses it if its preconditions are met +// to establish post-conditions +int foo(char *arr, size_t size, arr_fun_t arr_fun) + // clang-format off +__CPROVER_requires(arr == NULL || __CPROVER_is_fresh(arr, size)) +__CPROVER_requires(__CPROVER_obeys_contract(arr_fun, arr_fun_contract)) +__CPROVER_assigns(arr && size > 0 : arr[0]) +__CPROVER_ensures((__CPROVER_return_value == 0) ==> (arr[0] == 0)) +// clang-format on +{ + int retval = -1; + if(arr && size > 0) + { + CALL: + arr_fun(arr, size); + retval = 0; + } + return retval; +} + +void main() +{ + size_t size; + char *arr; + arr_fun_t fun; + foo(arr, size, fun); +} diff --git a/regression/contracts/function-pointer-contracts-enforce/test.desc b/regression/contracts/function-pointer-contracts-enforce/test.desc new file mode 100644 index 00000000000..8868382bad6 --- /dev/null +++ b/regression/contracts/function-pointer-contracts-enforce/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-contract foo --restrict-function-pointer foo.CALL/arr_fun_contract --replace-call-with-contract arr_fun_contract +^file main.c line 23 function foo: __CPROVER_obeys_contract is not supported in this version +^EXIT=6$ +^SIGNAL=0$ +-- +-- +This test checks uses of the unsupported __CPROVER_obeys_contract predicate +trigger errors. diff --git a/regression/contracts/function-pointer-contracts-replace/main.c b/regression/contracts/function-pointer-contracts-replace/main.c new file mode 100644 index 00000000000..34c3fe212ed --- /dev/null +++ b/regression/contracts/function-pointer-contracts-replace/main.c @@ -0,0 +1,42 @@ +#include +#include + +// type of functions that manipulate arrays +typedef void (*arr_fun_t)(char *arr, size_t size); + +// A contract for the arr_fun_t type +void arr_fun_contract(char *arr, size_t size) + // clang-format off +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0]) +__CPROVER_ensures(arr[0] == 0) + // clang-format on + ; + +arr_fun_t get_arr_fun() + // clang-format off +__CPROVER_ensures( + __CPROVER_obeys_contract(__CPROVER_return_value, arr_fun_contract)) + // clang-format on + ; + +void foo(char *arr, size_t size) + // clang-format off +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0]) +__CPROVER_ensures(arr[0] == 0) +// clang-format on +{ + // obtain function pointer from provider + arr_fun_t arr_fun = get_arr_fun(); + // use it +CALL: + arr_fun(arr, size); +} + +void main() +{ + char *arr; + size_t size; + foo(arr, size); +} diff --git a/regression/contracts/function-pointer-contracts-replace/test.desc b/regression/contracts/function-pointer-contracts-replace/test.desc new file mode 100644 index 00000000000..92df89d7bed --- /dev/null +++ b/regression/contracts/function-pointer-contracts-replace/test.desc @@ -0,0 +1,10 @@ +CORE +main.c + --restrict-function-pointer foo.CALL/arr_fun_contract --enforce-contract foo --replace-call-with-contract get_arr_fun +^file main.c line 19 function get_arr_fun: __CPROVER_obeys_contract is not supported in this version$ +^EXIT=6$ +^SIGNAL=0$ +-- +-- +This test checks uses of the unsupported __CPROVER_obeys_contract predicate +trigger errors. diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 6ac270196cd..1f914066ae5 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -150,6 +150,9 @@ class c_typecheck_baset: // contracts virtual void typecheck_typed_target_call(side_effect_expr_function_callt &expr); + /// Checks an obeys_contract predicate occurrence + virtual void + typecheck_obeys_contract_call(side_effect_expr_function_callt &expr); /// Checks that no history expr or return_value exists in expr virtual void check_history_expr_return_value(const exprt &expr, std::string &clause_type); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index ad49c01a802..20ed506e7fe 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1979,6 +1979,72 @@ void c_typecheck_baset::typecheck_typed_target_call( expr.type() = empty_typet(); } +void c_typecheck_baset::typecheck_obeys_contract_call( + side_effect_expr_function_callt &expr) +{ + INVARIANT( + expr.function().id() == ID_symbol && + to_symbol_expr(expr.function()).get_identifier() == CPROVER_PREFIX + "obeys_contract", + "expression must be a " CPROVER_PREFIX "obeys_contract function call"); + + if(expr.arguments().size() != 2) + { + throw invalid_source_file_exceptiont{ + "expected 2 arguments for " CPROVER_PREFIX "obeys_contract, found " + + std::to_string(expr.arguments().size()), + expr.source_location()}; + } + + // the first parameter must be a function pointer typed assignable path + // expression, without side effects or ternary operator + auto &function_pointer = expr.arguments()[0]; + + if( + function_pointer.type().id() != ID_pointer || + to_pointer_type(function_pointer.type()).base_type().id() != ID_code || + !function_pointer.get_bool(ID_C_lvalue)) + { + throw invalid_source_file_exceptiont( + "the first argument of " CPROVER_PREFIX + "obeys_contract must be a function pointer lvalue expression", + function_pointer.source_location()); + } + + if(has_subexpr(function_pointer, ID_if)) + { + throw invalid_source_file_exceptiont( + "the first argument of " CPROVER_PREFIX + "obeys_contract must have no ternary operator", + function_pointer.source_location()); + } + + // second parameter must be the address of a function symbol + auto &address_of_contract = expr.arguments()[1]; + + 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) + { + throw invalid_source_file_exceptiont( + "the second argument of " CPROVER_PREFIX + "obeys_contract must must be a function symbol", + address_of_contract.source_location()); + } + + if(function_pointer.type() != address_of_contract.type()) + { + throw invalid_source_file_exceptiont( + "the first and second arguments of " CPROVER_PREFIX + "obeys_contract must have the same function pointer type", + expr.source_location()); + } + + expr.type() = bool_typet(); +} + void c_typecheck_baset::typecheck_side_effect_function_call( side_effect_expr_function_callt &expr) { @@ -2270,6 +2336,12 @@ exprt c_typecheck_baset::do_special_functions( typecheck_function_call_arguments(expr); return nil_exprt(); } + else if(identifier == CPROVER_PREFIX "obeys_contract") + { + typecheck_obeys_contract_call(expr); + // returning nil leaves the call expression in place + return nil_exprt(); + } else if(identifier == CPROVER_PREFIX "same_object") { if(expr.arguments().size()!=2) diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 96e1dbaa2f9..fc500a79148 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -49,6 +49,7 @@ void __CPROVER_fence(const char *kind, ...); __CPROVER_bool __CPROVER_is_freeable(const void *mem); __CPROVER_bool __CPROVER_was_freed(const void *mem); __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size); +__CPROVER_bool __CPROVER_obeys_contract(void (*)(void), void (*)(void)); void __CPROVER_old(const void *); void __CPROVER_loop_entry(const void *); diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index d07148f0fdb..37511e93bc8 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -1167,9 +1167,13 @@ __CPROVER_bool __CPROVER_contracts_is_fresh( __CPROVER_size_t size, __CPROVER_contracts_write_set_ptr_t write_set) { - if(!write_set) - return __VERIFIER_nondet_CPROVER_bool(); __CPROVER_HIDE:; + __CPROVER_assert( + (write_set != 0) & ((write_set->assume_requires_ctx == 1) | + (write_set->assert_requires_ctx == 1) | + (write_set->assume_ensures_ctx == 1) | + (write_set->assert_ensures_ctx == 1)), + "__CPROVER_is_fresh is used only in requires or ensures clauses"); #ifdef DFCC_DEBUG __CPROVER_assert( __CPROVER_rw_ok(write_set, sizeof(__CPROVER_contracts_write_set_t)), @@ -1416,4 +1420,48 @@ __CPROVER_HIDE:; #endif } } -#endif + +/// \brief Implementation of the `obeys_contract` front-end predicate. +/// \return True iff a function pointer points to the specified contract. +/// +/// \details If called in an assumption context, translates to an assignment +/// `function_pointer = contract`. If called in an assertion context, translates +/// to an `function_pointer == contract`. +/// The function pointer is taken by reference to be able to update it using a +/// side-effect in assumption contexts. +__CPROVER_bool __CPROVER_contracts_obeys_contract( + void (**function_pointer)(void), + void (*contract)(void), + __CPROVER_contracts_write_set_ptr_t set) +{ +__CPROVER_HIDE:; + __CPROVER_assert( + (set != 0) & + ((set->assume_requires_ctx == 1) | (set->assert_requires_ctx == 1) | + (set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)), + "__CPROVER_obeys_contract is used only in requires or ensures clauses"); + if((set->assume_requires_ctx == 1) | (set->assume_ensures_ctx == 1)) + { + // In assumption contexts, flip a coin to decide wehter the predicate + // shall hold or not + if(__VERIFIER_nondet_CPROVER_bool()) + { + // if it must hold, assign the function pointer to the contract function + *function_pointer = contract; + return 1; + } + else + { + // if it must not hold do not modify the pointer value + // function_pointer will keep whatever bit pattern and value set it had + // before evaluating the predicate + return 0; + } + } + else + { + // in assumption contexts, the pointer gets checked for equality + return *function_pointer == contract; + } +} +#endif // __CPROVER_contracts_library_defined diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 1784b8a9488..640a1a2e3e1 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -21,6 +21,7 @@ SRC = accelerate/accelerate.cpp \ contracts/dynamic-frames/dfcc_library.cpp \ contracts/dynamic-frames/dfcc_is_fresh.cpp \ contracts/dynamic-frames/dfcc_is_freeable.cpp \ + contracts/dynamic-frames/dfcc_obeys_contract.cpp \ contracts/dynamic-frames/dfcc_instrument.cpp \ contracts/dynamic-frames/dfcc_spec_functions.cpp \ contracts/dynamic-frames/dfcc_contract_functions.cpp \ diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index f7b1a2ffb48..7bbe5ee90f7 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -484,6 +484,24 @@ void code_contractst::check_apply_loop_contracts( } } +/// Throws an exception if a contract uses unsupported constructs like: +/// - obeys_contract predicates +static void throw_on_unsupported(const goto_programt &program) +{ + for(const auto &it : program.instructions) + { + if( + it.is_function_call() && it.call_function().id() == ID_symbol && + to_symbol_expr(it.call_function()).get_identifier() == CPROVER_PREFIX + "obeys_contract") + { + throw invalid_source_file_exceptiont( + CPROVER_PREFIX "obeys_contract is not supported in this version", + it.source_location()); + } + } +} + /// This function generates instructions for all contract constraint, i.e., /// assumptions and assertions based on requires and ensures clauses. static void generate_contract_constraints( @@ -513,6 +531,7 @@ static void generate_contract_constraints( } constraint.instructions.back().source_location_nonconst() = location; is_fresh_update(constraint); + throw_on_unsupported(constraint); program.destructive_append(constraint); } diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md index 76df7974016..aa4eb074557 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md @@ -29,6 +29,7 @@ Each of these translation passes is implemented in a specific class: @ref dfcc_instrumentt | Implements @ref contracts-dev-spec-dfcc for @ref goto_functiont, @ref goto_programt, or subsequences of instructions of @ref goto_programt @ref dfcc_is_fresht | Implements @ref contracts-dev-spec-is-fresh @ref dfcc_is_freeablet | Implements @ref contracts-dev-spec-is-freeable + @ref dfcc_obeys_contractt | Implements @ref contracts-dev-spec-obeys-contract @ref dfcc_spec_functionst | Implements @ref contracts-dev-spec-spec-rewriting @ref dfcc_wrapper_programt | Implements @ref contracts-dev-spec-contract-checking for contracts ^ | Implements @ref contracts-dev-spec-contract-replacement for contracts diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md index 6f3f242b9ec..333b954ce6d 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md @@ -162,10 +162,12 @@ skip_target: SKIP; CALL __CPROVER_deallocate(ptr); ``` -Calls to __CPROVER_was_freed or __CPROVER_is_freeable are rewritten as described +Calls to `__CPROVER_was_freed` or `__CPROVER_is_freeable` are rewritten as described in @subpage contracts-dev-spec-is-freeable -Calls to __CPROVER_is_fresh are rewritten as described in @subpage contracts-dev-spec-is-fresh +Calls to `__CPROVER_is_fresh` are rewritten as described in @subpage contracts-dev-spec-is-fresh + +Calls to `__CPROVER_obeys_contract` are rewritten as described in @subpage contracts-dev-spec-obeys-contract For all other function or function pointer calls, we proceed as follows. diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-obeys-contract.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-obeys-contract.md new file mode 100644 index 00000000000..2c01b4cfe6d --- /dev/null +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-obeys-contract.md @@ -0,0 +1,84 @@ +# Rewriting Calls to the __CPROVER_obeys_contract Predicate {#contracts-dev-spec-obeys-contract} + +Back to top @ref contracts-dev-spec + +@tableofcontents + + +The `__CPROVER_obeys_pointer` is defined as follows: +if the predicate holds then `function_pointer` points to a +function satisfying the `contract` passed as second argument. +If the predicate does not hold, then nothing can be assumed of the +`function_pointer` behaviour. + + +The instrumentation of `__CPROVER_obeys_contract` is supported by the +class @ref dfcc_obeys_contractt. In a GOTO program passed as argument, +this class rewrites calls to: + +```c +CALL retval := __CPROVER_obeys_contract(function_pointer, contract); +``` + +into calls to the library function implementation: + +```c +CALL retval := __CPROVER_contracts_obeys_contract( + &function_pointer, + contract, + write_set); +``` + +One thing to notice is that the library implementation function takes the +`function_pointer` argument by reference: + +```c +__CPROVER_contracts_obeys_contract( + void (**function_pointer)(void), + void (*contract)(void), + __CPROVER_contracts_write_set_ptr_t write_set); +``` + +This function implements the `__CPROVER_obeys_contract` behaviour for all +different contexts (contract checking vs replacement, requires vs ensures clause +context, as described by the flags carried by the write set parameter). + +In an assumption context, the predicate turns into a nondet assignment that +makes `function_pointer` point to the `contract` function: + +```c +if(nondet_bool()) { + *function_pointer = contract; + return true; +} else { + return false; +} +``` + +If the surrounding `__CPROVER_assume` statement enforces a true value for the +predicate, then the `function_pointer` will effectively point to the `contract` +function, which is known to satisfy its own specification. + +If the surrounding `__CPROVER_assume` statement enforces a false value for the +predicate, then nothing is enforced on the `function_pointer` +(it could be invalid, be NULL, point to any other function, etc.). + +In assertion contexts, the predicate turns into a pointer equality check: + +```c + return *function_pointer == contract; +``` + + +In addition to rewriting calls, the `dfcc_obeys_contractt` class reports all +contract functions discovered as second arguments of the predicates. +This information is then used in method +@ref dfcct#wrap_discovered_function_pointer_contracts to replace all discovered +contract functions by their actual contracts. That way, any call to a function +pointer assumed or succesfully asserted to satisfy the contract will actually +behave like the contract. + +--- + Prev | Next +:-----|:------ + @ref contracts-dev | @ref contracts-dev-spec-reminder \ No newline at end of file diff --git a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-reminder.md b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-reminder.md index 57b16f74659..6cca559bbb3 100644 --- a/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-reminder.md +++ b/src/goto-instrument/contracts/doc/developer/contracts-dev-spec-reminder.md @@ -27,11 +27,13 @@ __CPROVER_frees(F) - A `__CPROVER_requires` clause (@ref contracts-requires-ensures) specifies a precondition as boolean expression R that may only depend on program globals, - function parameters, [memory predicates](@ref contracts-memory-predicates) and + function parameters, [memory predicates](@ref contracts-memory-predicates), + [function pointer predicates](@ref contracts-function-pointer-predicates) and deterministic, side effect-free function calls; - A `__CPROVER_ensures` clause (@ref contracts-requires-ensures) specifies a postcondition as boolean expression E that may only depend on program globals, function parameters, [memory predicates](@ref contracts-memory-predicates), + [function pointer predicates](@ref contracts-function-pointer-predicates), deterministic, side effect-free function calls, [history variables](@ref contracts-history-variables), and the special variable `__CPROVER_return_value`; diff --git a/src/goto-instrument/contracts/doc/user/contracts-assigns.md b/src/goto-instrument/contracts/doc/user/contracts-assigns.md index 5ee8ea7bb3a..89c68c57c85 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-assigns.md +++ b/src/goto-instrument/contracts/doc/user/contracts-assigns.md @@ -510,5 +510,6 @@ int foo() - @ref contracts-assigns - @ref contracts-frees - @ref contracts-memory-predicates +- @ref contracts-function-pointer-predicates - @ref contracts-history-variables - @ref contracts-quantifiers diff --git a/src/goto-instrument/contracts/doc/user/contracts-decreases.md b/src/goto-instrument/contracts/doc/user/contracts-decreases.md index 1a90ab7fa04..b8f3cc4e7e2 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-decreases.md +++ b/src/goto-instrument/contracts/doc/user/contracts-decreases.md @@ -187,5 +187,6 @@ then the weakest possible invariant (i.e, `true`) is used to model an arbitrary - @ref contracts-assigns - @ref contracts-frees - @ref contracts-memory-predicates +- @ref contracts-function-pointer-predicates - @ref contracts-history-variables - @ref contracts-quantifiers diff --git a/src/goto-instrument/contracts/doc/user/contracts-function-pointer-predicates.md b/src/goto-instrument/contracts/doc/user/contracts-function-pointer-predicates.md new file mode 100644 index 00000000000..1401c04ff3e --- /dev/null +++ b/src/goto-instrument/contracts/doc/user/contracts-function-pointer-predicates.md @@ -0,0 +1,249 @@ +# Function Pointer Predicates {#contracts-function-pointer-predicates} + +Back to @ref contracts-user + +@tableofcontents + + +## Syntax + +The function contract language offers the following predicate to specify +preconditions and postconditions about function pointers in _requires clauses_ +and _ensures clauses_. + +```c +bool __CPROVER_obeys_contract(void (*f)(void), void (*c)(void)); +``` + +Informally, this predicate holds iff function pointer `f` is known to satisfy +contract `c`. + +### Parameters + +The predicate `__CPROVER_obeys_contract` takes two function pointers as arguments. +The first function pointer must be an lvalue, the second parameter must be a pointer +to a pure contract symbol. + +### Return Value + +It returns a `bool` value, indicating whether the function pointer is known to +satisfy contract `c`. + +## Semantics + +To illustrate the semantics of the predicate, let's consider the example below. + +The `arr_fun_contract` specifies the class of functions that take a non-`NULL` +array `arr` of size `size` as input and initialise its first element to zero. + +The function `foo` takes a possibly `NULL` array `arr` of given `size` and a +possibly `NULL` opaque function pointer `arr_fun`, assumed to satisfy the +contract `arr_fun_contract`. + +The function `foo` checks some condition and then calls `arr_fun`. +When `arr_fun` if called, the preconditions of its contract `arr_fun_contract` +will be checked, write set inclusion with respect to the contract of `foo` will +be checked, and its postconditions will be assumed, allowing to establish the +postconditions of `foo`. + +```c +// \file fptr.c +#include +#include + +// Type of functions that manipulate arrays of a given size +typedef void (*arr_fun_t)(char *arr, size_t size); + +// A contract for the arr_fun_t type +void arr_fun_contract(char *arr, size_t size) +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0]) +__CPROVER_ensures(arr[0] == 0) +; + +// Uses a function pointer satisfying arr_fun_contract +int foo(char *arr, size_t size, arr_fun_t arr_fun) +__CPROVER_requires(arr ==> __CPROVER_is_fresh(arr, size)) +__CPROVER_requires(arr_fun ==> __CPROVER_obeys_contract(arr_fun, arr_fun_contract)) +__CPROVER_assigns(arr && size > 0 && arr_fun : arr[0]) +__CPROVER_ensures(__CPROVER_return_value ==> (arr[0] == 0)) +{ + if (arr && size > 0 && arr_fun) { + CALL: + arr_fun(arr, size); + return true; + } + return false; +} + +void main() +{ + size_t size; + char *arr; + arr_fun_t arr_fun; + foo(arr, size, arr_fun); +} +``` + +### Enforcement + +To check that `foo` satisfies its contract, we compile, instrument and analyse the program as follows: + +```bash +goto-cc fptr.c +goto-instrument \ +--restrict-function-pointer foo.CALL/arr_fun_contract \ +--dfcc main \ +--enforce-contract foo \ +a.out b.out +cbmc b.out +``` + +The function pointer restriction directive is needed to inform CBMC that we only +expect the contract function `arr_fun_contratt` to be called where `arr_fun` +is called. + +We get the following analysis result: + +```bash +... + +fptr.c function arr_fun_contract +[arr_fun_contract.precondition.1] line 8 Check requires clause of contract contract::arr_fun_contract for function arr_fun_contract: SUCCESS +[arr_fun_contract.assigns.4] line 7 Check that the assigns clause of contract::arr_fun_contract is included in the caller's assigns clause: SUCCESS +[arr_fun_contract.frees.1] line 7 Check that the frees clause of contract::arr_fun_contract is included in the caller's frees clause: SUCCESS + +fptr.c function foo +[foo.postcondition.1] line 20 Check ensures clause of contract contract::foo for function foo: SUCCESS +[foo.pointer_dereference.1] line 24 dereferenced function pointer must be arr_fun_contract: SUCCESS + +... + +** 0 of 72 failed (1 iterations) +VERIFICATION SUCCESSFUL +``` + +### Replacement + +Let's now consider an extended example with two new functions: +- The function `get_arr_fun` returns a pointer to a function satisfying + `arr_fun_contract`; +- The function bar allocates an array and uses `get_arr_fun` and `foo` + to initialise it; + +Our goal is to check that `bar` satisfies its contract, assuming that `foo` +satisfies its contract and that `get_arr_fun` satisfies its contract. + +```c +#include + +// Type of functions that manipulate arrays of a given size +typedef void (*arr_fun_t)(char *arr, size_t size); + +// A contract for the arr_fun_t type +void arr_fun_contract(char *arr, size_t size) +__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(arr[0]) +__CPROVER_ensures(arr[0] == 0) +; + +// Uses a function pointer satisfying arr_fun_contract +int foo(char *arr, size_t size, arr_fun_t arr_fun) +__CPROVER_requires( + arr ==> __CPROVER_is_fresh(arr, size)) +__CPROVER_requires( + arr_fun ==> __CPROVER_obeys_contract(arr_fun, arr_fun_contract)) +__CPROVER_assigns(arr && size > 0 && arr_fun : arr[0]) +__CPROVER_ensures(__CPROVER_return_value ==> (arr[0] == 0)) +{ + if (arr && size > 0 && arr_fun) { + CALL: + arr_fun(arr, size); + return 1; + } + return 0; +} + +// Returns a function that satisfies arr_fun_contract +arr_fun_t get_arr_fun() +__CPROVER_ensures( + __CPROVER_obeys_contract(__CPROVER_return_value, arr_fun_contract)) +; + +// Creates an array and uses get_arr_fun and foo to initialise it +char *bar(size_t size) +__CPROVER_ensures( + __CPROVER_return_value ==> size > 0 && + __CPROVER_is_fresh(__CPROVER_return_value, size) && + __CPROVER_return_value[0] == 0) +{ + if (size > 0) { + char *arr; + arr = malloc(size); + if (arr && foo(arr, size, get_arr_fun())) + return arr; + + return NULL; + } + return NULL; +} + +void main() +{ + size_t size; + char *arr = bar(size); +} +``` +We compile, instrument and analyse the program as follows: + +```bash +goto-cc fptr.c +goto-instrument \ + --dfcc main \ + --enforce-contract bar \ + --replace-call-with-contract foo \ + --replace-call-with-contract get_arr_fun \ + a.out b.out +cbmc b.out +``` + +And obtain the following results: + +```bash +... + +fptr.c function get_arr_fun +[get_arr_fun.assigns.1] line 13 Check that the assigns clause of contract::get_arr_fun is included in the caller's assigns clause: SUCCESS +[get_arr_fun.frees.1] line 13 Check that the frees clause of contract::get_arr_fun is included in the caller's frees clause: SUCCESS + +fptr.c function bar +[bar.postcondition.1] line 36 Check ensures clause of contract contract::bar for function bar: SUCCESS + +fptr.c function foo +[foo.assigns.7] line 18 Check that the assigns clause of contract::foo is included in the caller's assigns clause: SUCCESS +[foo.frees.1] line 18 Check that the frees clause of contract::foo is included in the caller's frees clause: SUCCESS +[foo.precondition.1] line 20 Check requires clause of contract contract::foo for function foo: SUCCESS +[foo.precondition.2] line 22 Check requires clause of contract contract::foo for function foo: SUCCESS +... + +** 0 of 80 failed (1 iterations) +VERIFICATION SUCCESSFUL +``` + +Proving that `bar` satisfies its contract. + +## Additional Resources + +- @ref contracts-functions + - @ref contracts-requires-ensures + - @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-function-pointer-predicates +- @ref contracts-history-variables +- @ref contracts-quantifiers diff --git a/src/goto-instrument/contracts/doc/user/contracts-functions.md b/src/goto-instrument/contracts/doc/user/contracts-functions.md index 485d7bf4de7..5422f5736c7 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-functions.md +++ b/src/goto-instrument/contracts/doc/user/contracts-functions.md @@ -48,6 +48,8 @@ The following built-in constructs can also be used with functions contracts: - @ref contracts-history-variables allow to refer to past versions of function parameters, - @ref contracts-quantifiers allow to express quantified formulas, - @ref contracts-memory-predicates allow to describe simple heap structures; +- @ref contracts-function-pointer-predicates allow to describe function pointer properties; + In our example, the developer may require from the caller to properly allocate all arguments, thus, pointers must be valid. We can specify the preconditions of @@ -162,5 +164,6 @@ program using contracts. - @ref contracts-assigns - @ref contracts-frees - @ref contracts-memory-predicates +- @ref contracts-function-pointer-predicates - @ref contracts-history-variables - @ref contracts-quantifiers 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..29b0f127c4d 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-history-variables.md +++ b/src/goto-instrument/contracts/doc/user/contracts-history-variables.md @@ -56,5 +56,6 @@ TODO: Document `__CPROVER_loop_entry` and `__CPROVER_loop_old`. - @ref contracts-assigns - @ref contracts-frees - @ref contracts-memory-predicates +- @ref contracts-function-pointer-predicates - @ref contracts-history-variables - @ref contracts-quantifiers 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..abe4e439b48 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md +++ b/src/goto-instrument/contracts/doc/user/contracts-loop-invariants.md @@ -165,5 +165,6 @@ A few things to note here: - @ref contracts-assigns - @ref contracts-frees - @ref contracts-memory-predicates +- @ref contracts-function-pointer-predicates - @ref contracts-history-variables - @ref contracts-quantifiers 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..0cce76ee7fd 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md +++ b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md @@ -132,5 +132,6 @@ int foo() - @ref contracts-assigns - @ref contracts-frees - @ref contracts-memory-predicates +- @ref contracts-function-pointer-predicates - @ref contracts-history-variables - @ref contracts-quantifiers diff --git a/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md b/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md index 8f356e4878b..a384423747c 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md +++ b/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md @@ -104,5 +104,6 @@ int bar_sat(int *arr, int len) - @ref contracts-assigns - @ref contracts-frees - @ref contracts-memory-predicates +- @ref contracts-function-pointer-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..635bc221ea7 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-requires-ensures.md +++ b/src/goto-instrument/contracts/doc/user/contracts-requires-ensures.md @@ -28,8 +28,9 @@ the conjunction of the _ensures_ clauses, or `true` if none are specified. Both _requires_ clauses and _ensures_ clauses take a Boolean expression over the arguments of a function and/or global variables. The expression can include -calls to CBMC built-in functions or to -[Memory Predicates](@ref contracts-memory-predicates)). +calls to CBMC built-in functions, to +[Memory Predicates](@ref contracts-memory-predicates)) or to +[function pointer predicates](@ref contracts-function-pointer-predicates). User-defined functions can also be called inside _requires_ clauses as long as they are deterministic and do not have any side-effects (the absence of side effects is checked by the tool). In addition, _ensures_ @@ -187,5 +188,6 @@ int foo() - @ref contracts-assigns - @ref contracts-frees - @ref contracts-memory-predicates +- @ref contracts-function-pointer-predicates - @ref contracts-history-variables - @ref contracts-quantifiers diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 262b0a01c4c..99c0b2e4872 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -262,7 +262,9 @@ void dfcct::instrument_harness_function() // load the cprover library to make sure the model is complete log.status() << "Instrumenting harness function '" << harness_id << "'" << messaget::eom; - instrument.instrument_harness_function(harness_id); + + instrument.instrument_harness_function( + harness_id, function_pointer_contracts); other_symbols.erase(harness_id); } @@ -314,62 +316,71 @@ void dfcct::wrap_replaced_functions() void dfcct::wrap_discovered_function_pointer_contracts() { - // swap-and-wrap function pointer contracts with themselves - for(const auto &fp_contract : function_pointer_contracts) + std::set swapped; + while(!function_pointer_contracts.empty()) { - log.status() << "Discovered function pointer contract '" << fp_contract - << "'" << messaget::eom; + std::set new_contracts; + // swap-and-wrap function pointer contracts with themselves + for(const auto &fp_contract : function_pointer_contracts) + { + if(swapped.find(fp_contract) != swapped.end()) + continue; - // contracts for function pointers must be replaced with themselves - // so we need to check that: - // - the symbol exists as a function symbol - // - the symbol exists as a pure contract symbol - // - the function symbol is not already swapped for contract checking - // - the function symbol is not already swapped with another contract for - // replacement + // contracts for function pointers must be replaced with themselves + // so we need to check that: + // - the symbol exists as a function symbol + // - the symbol exists as a pure contract symbol + // - the function symbol is not already swapped for contract checking + // - the function symbol is not already swapped with another contract for + // replacement - const auto str = id2string(fp_contract); + const auto str = id2string(fp_contract); - // Is it already swapped with another function for contract checking ? - PRECONDITION_WITH_DIAGNOSTICS( - !to_check.has_value() || to_check.value().first != str, - "Function '" + str + - "' used as contract for function pointer cannot be itself the object " - "of a contract check."); - - // Is it already swapped with another function for contract checking ? - auto found = to_replace.find(str); - if(found != to_replace.end()) - { + // Is it already swapped with another function for contract checking ? PRECONDITION_WITH_DIAGNOSTICS( - found->first == found->second, + !to_check.has_value() || to_check.value().first != str, "Function '" + str + - "' used as contract for function pointer already the object of a " - "contract replacement with '" + - id2string(found->second) + "'"); - log.status() << "Function pointer contract '" << fp_contract - << "' already wrapped with itself in REPLACE mode" - << messaget::eom; - } - else - { - // we need to swap it with itself - PRECONDITION_WITH_DIAGNOSTICS( - utils.function_symbol_exists(str), - "Function pointer contract '" + str + "' not found."); - - // triggers signature compatibility checking - contract_handler.get_pure_contract_symbol(str); - - log.status() << "Wrapping function pointer contract '" << fp_contract - << "' with itself in REPLACE mode" << messaget::eom; - - swap_and_wrap.swap_and_wrap_replace( - fp_contract, fp_contract, function_pointer_contracts); - // remove it from the set of symbols to process - if(other_symbols.find(fp_contract) != other_symbols.end()) - other_symbols.erase(fp_contract); + "' used as contract for function pointer cannot be itself the object " + "of a contract check."); + + // Is it already swapped with another function for contract checking ? + auto found = to_replace.find(str); + if(found != to_replace.end()) + { + PRECONDITION_WITH_DIAGNOSTICS( + found->first == found->second, + "Function '" + str + + "' used as contract for function pointer already the object of a " + "contract replacement with '" + + id2string(found->second) + "'"); + log.status() << "Function pointer contract '" << fp_contract + << "' already wrapped with itself in REPLACE mode" + << messaget::eom; + } + else + { + // we need to swap it with itself + PRECONDITION_WITH_DIAGNOSTICS( + utils.function_symbol_exists(str), + "Function pointer contract '" + str + "' not found."); + + // triggers signature compatibility checking + contract_handler.get_pure_contract_symbol(str); + + log.status() << "Wrapping function pointer contract '" << fp_contract + << "' with itself in REPLACE mode" << messaget::eom; + + swap_and_wrap.swap_and_wrap_replace( + fp_contract, fp_contract, new_contracts); + swapped.insert(fp_contract); + + // remove it from the set of symbols to process + if(other_symbols.find(fp_contract) != other_symbols.end()) + other_symbols.erase(fp_contract); + } } + // process newly discovered contracts + function_pointer_contracts = new_contracts; } } @@ -386,7 +397,7 @@ void dfcct::instrument_other_functions() log.status() << "Instrumenting '" << function_id << "'" << messaget::eom; - instrument.instrument_function(function_id); + instrument.instrument_function(function_id, function_pointer_contracts); } goto_model.goto_functions.update(); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 3691afa56c6..9e3fd8f4797 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -30,6 +30,7 @@ Author: Remi Delmas, delmarsd@amazon.com #include "dfcc_is_freeable.h" #include "dfcc_is_fresh.h" #include "dfcc_library.h" +#include "dfcc_obeys_contract.h" #include "dfcc_utils.h" std::set dfcc_instrumentt::function_cache; @@ -220,7 +221,9 @@ bool dfcc_instrumentt::do_not_instrument(const irep_idt &id) const (is_cprover_symbol(id) || is_internal_symbol(id)); } -void dfcc_instrumentt::instrument_harness_function(const irep_idt &function_id) +void dfcc_instrumentt::instrument_harness_function( + const irep_idt &function_id, + std::set &function_pointer_contracts) { bool inserted = dfcc_instrumentt::function_cache.insert(function_id).second; if(!inserted) @@ -240,6 +243,10 @@ void dfcc_instrumentt::instrument_harness_function(const irep_idt &function_id) dfcc_is_freeablet is_freeable(library, message_handler); is_freeable.rewrite_calls(body, null_expr); + // rewrite obeys_contract calls + dfcc_obeys_contractt obeys_contract(library, message_handler); + obeys_contract.rewrite_calls(body, null_expr, function_pointer_contracts); + // rewrite calls Forall_goto_program_instructions(it, body) { @@ -269,23 +276,28 @@ dfcc_instrumentt::get_local_statics(const irep_idt &function_id) return local_statics; } -void dfcc_instrumentt::instrument_function(const irep_idt &function_id) +void dfcc_instrumentt::instrument_function( + const irep_idt &function_id, + std::set &function_pointer_contracts) { // use same name for local static search - instrument_function(function_id, function_id); + instrument_function(function_id, function_id, function_pointer_contracts); } void dfcc_instrumentt::instrument_wrapped_function( const irep_idt &wrapped_function_id, - const irep_idt &initial_function_id) + const irep_idt &initial_function_id, + std::set &function_pointer_contracts) { // use the initial name name for local static search - instrument_function(wrapped_function_id, initial_function_id); + instrument_function( + wrapped_function_id, initial_function_id, function_pointer_contracts); } void dfcc_instrumentt::instrument_function( const irep_idt &function_id, - const irep_idt &function_id_for_local_static_search) + const irep_idt &function_id_for_local_static_search, + std::set &function_pointer_contracts) { // never instrument a function twice bool inserted = dfcc_instrumentt::function_cache.insert(function_id).second; @@ -310,14 +322,19 @@ void dfcc_instrumentt::instrument_function( get_local_statics(function_id_for_local_static_search); instrument_function_body( - function_id, write_set.symbol_expr(), cfg_info, local_statics); + function_id, + write_set.symbol_expr(), + cfg_info, + local_statics, + function_pointer_contracts); } void dfcc_instrumentt::instrument_function_body( const irep_idt &function_id, const exprt &write_set, cfg_infot &cfg_info, - const std::set &local_statics) + const std::set &local_statics, + std::set &function_pointer_contracts) { auto &goto_function = goto_model.goto_functions.function_map.at(function_id); @@ -341,7 +358,8 @@ void dfcc_instrumentt::instrument_function_body( body.instructions.end(), cfg_info, // don't skip any instructions - {}); + {}, + function_pointer_contracts); // insert add/remove instructions for local statics auto begin = body.instructions.begin(); @@ -370,7 +388,8 @@ void dfcc_instrumentt::instrument_function_body( void dfcc_instrumentt::instrument_goto_program( const irep_idt &function_id, goto_programt &goto_program, - const exprt &write_set) + const exprt &write_set, + std::set &function_pointer_contracts) { goto_program_cfg_infot cfg_info(goto_program); @@ -382,7 +401,8 @@ void dfcc_instrumentt::instrument_goto_program( goto_program.instructions.end(), cfg_info, // no pred, don't skip any instructions - {}); + {}, + function_pointer_contracts); // cleanup remove_skip(goto_program); @@ -395,7 +415,8 @@ void dfcc_instrumentt::instrument_instructions( goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, cfg_infot &cfg_info, - const std::function &pred) + const std::function &pred, + std::set &function_pointer_contracts) { // rewrite is_fresh calls dfcc_is_fresht is_fresh(library, message_handler); @@ -407,6 +428,15 @@ void dfcc_instrumentt::instrument_instructions( is_freeable.rewrite_calls( goto_program, first_instruction, last_instruction, write_set); + // rewrite obeys_contract calls + dfcc_obeys_contractt obeys_contract(library, message_handler); + obeys_contract.rewrite_calls( + goto_program, + first_instruction, + last_instruction, + write_set, + function_pointer_contracts); + const namespacet ns(goto_model.symbol_table); auto &target = first_instruction; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h index 001a2e4ab0c..b27af5b7e0f 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h @@ -74,7 +74,13 @@ class dfcc_instrumentt /// This will trigger cascading checks in all functions called from the /// checked function thanks to the propagation of the write set through /// function calls and function pointer calls. - void instrument_harness_function(const irep_idt &function_id); + /// + /// \param function_id function to instrument + /// \param function_pointer_contracts contracts discovered in calls to + /// the obeys_contract predicate are added to this set. + void instrument_harness_function( + const irep_idt &function_id, + std::set &function_pointer_contracts); /// \brief Instruments a GOTO function by adding an extra write set parameter /// and inserting frame condition checks in its GOTO program, as well as @@ -87,7 +93,11 @@ class dfcc_instrumentt /// \param function_id The name of the function, used to retrieve the function /// to instrument and used as prefix when generating new symbols during /// instrumentation. - void instrument_function(const irep_idt &function_id); + /// \param function_pointer_contracts contracts discovered in calls to + /// the obeys_contract predicate are added to this set. + void instrument_function( + const irep_idt &function_id, + std::set &function_pointer_contracts); /// \brief Instruments a GOTO function by adding an extra write set parameter /// and inserting frame condition checks in its GOTO program, as well as @@ -104,9 +114,12 @@ class dfcc_instrumentt /// \param initial_function_id The initial name of the function, /// before mangling. This is the name used to identify statics symbols in the /// symbol table that were locally declared in the function. + /// \param function_pointer_contracts contracts discovered in calls to + /// the obeys_contract predicate are added to this set. void instrument_wrapped_function( const irep_idt &wrapped_function_id, - const irep_idt &initial_function_id); + const irep_idt &initial_function_id, + std::set &function_pointer_contracts); /// \brief Instruments a GOTO program against a given write set variable. /// @@ -123,10 +136,12 @@ class dfcc_instrumentt /// instrumentation. /// \param goto_program Goto program to instrument. /// \param write_set Write set variable to use for instrumentation. + /// \param function_pointer_contracts Discovered function pointer contracts void instrument_goto_program( const irep_idt &function_id, goto_programt &goto_program, - const exprt &write_set); + const exprt &write_set, + std::set &function_pointer_contracts); /// Adds the names of instrumented functions to \p dest. /// The names are kept track of in the \ref function_cache field. @@ -201,7 +216,8 @@ class dfcc_instrumentt /// and automatically to add/remove to the write set. void instrument_function( const irep_idt &function_id, - const irep_idt &function_id_for_local_static_search); + const irep_idt &function_id_for_local_static_search, + std::set &function_pointer_contracts); /// Instruments the body of a GOTO function against a given write set. /// Adds the given local statics to the write set in pre and removes them @@ -210,7 +226,8 @@ class dfcc_instrumentt const irep_idt &function_id, const exprt &write_set, cfg_infot &cfg_info, - const std::set &local_statics); + const std::set &local_statics, + std::set &function_pointer_contracts); /// \brief Instruments the instructions found between \p first_instruction and /// \p last_instruction in the instructions of \p goto_program against the @@ -226,6 +243,8 @@ class dfcc_instrumentt /// \param pred filter predicate for instructions. If \p pred is not provided, /// all instructions are instrumented. If \p pred is provided, only /// instructions satisfying \p pred are instrumented. + /// \param function_pointer_contracts contracts discovered in calls to + /// the obeys_contract predicate are added to this set. void instrument_instructions( const irep_idt &function_id, const exprt &write_set, @@ -233,7 +252,8 @@ class dfcc_instrumentt goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, // excluding the last cfg_infot &cfg_info, - const std::function &pred); + const std::function &pred, + std::set &function_pointer_contracts); /// Returns `true` if the symbol `x` in `DECL x` or `DEAD x` must be added /// explicitly to the write set. Returns `false` when assignments to `x` must diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index 9650a5331b7..6c4579cf463 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -126,7 +126,8 @@ const std::map create_dfcc_fun_to_name() {dfcc_funt::IS_FREEABLE, CONTRACTS_PREFIX "is_freeable"}, {dfcc_funt::WAS_FREED, CONTRACTS_PREFIX "was_freed"}, {dfcc_funt::REPLACE_ENSURES_WAS_FREED_PRECONDITIONS, - CONTRACTS_PREFIX "check_replace_ensures_was_freed_preconditions"}}; + CONTRACTS_PREFIX "check_replace_ensures_was_freed_preconditions"}, + {dfcc_funt::OBEYS_CONTRACT, CONTRACTS_PREFIX "obeys_contract"}}; } const std::map create_dfcc_hook() diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h index b59a72feb70..8af906c5873 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -130,7 +130,9 @@ enum class dfcc_funt /// \see __CPROVER_contracts_was_freed WAS_FREED, /// \see __CPROVER_contracts_check_replace_ensures_was_freed_preconditions - REPLACE_ENSURES_WAS_FREED_PRECONDITIONS + REPLACE_ENSURES_WAS_FREED_PRECONDITIONS, + /// \see __CPROVER_contracts_obeys_contract + OBEYS_CONTRACT, }; class goto_modelt; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp new file mode 100644 index 00000000000..42cc92ddfc3 --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp @@ -0,0 +1,99 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: August 2022 + +\*******************************************************************/ + +#include "dfcc_obeys_contract.h" + +#include +#include +#include +#include + +#include + +#include "dfcc_library.h" + +dfcc_obeys_contractt::dfcc_obeys_contractt( + dfcc_libraryt &library, + message_handlert &message_handler) + : library(library), message_handler(message_handler), log(message_handler) +{ +} + +void dfcc_obeys_contractt::rewrite_calls( + goto_programt &program, + const exprt &write_set, + std::set &function_pointer_contracts) +{ + rewrite_calls( + program, + program.instructions.begin(), + program.instructions.end(), + write_set, + function_pointer_contracts); +} + +void dfcc_obeys_contractt::get_contract_name( + const exprt &expr, + std::set &function_pointer_contracts) +{ + PRECONDITION(expr.id() == ID_typecast || expr.id() == ID_address_of); + + if(expr.id() == ID_typecast) + { + get_contract_name(to_typecast_expr(expr).op(), function_pointer_contracts); + } + else + { + PRECONDITION_WITH_DIAGNOSTICS( + to_address_of_expr(expr).object().id() == ID_symbol, + "symbol expression expected"); + function_pointer_contracts.insert( + to_symbol_expr(to_address_of_expr(expr).object()).get_identifier()); + } +} + +void dfcc_obeys_contractt::rewrite_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction, + const exprt &write_set, + std::set &function_pointer_contracts) +{ + for(auto &target = first_instruction; target != last_instruction; target++) + { + if(target->is_function_call()) + { + const auto &function = target->call_function(); + + if(function.id() == ID_symbol) + { + const irep_idt &fun_name = to_symbol_expr(function).get_identifier(); + + if(has_prefix(id2string(fun_name), CPROVER_PREFIX "obeys_contract")) + { + // add address_of on first operand + target->call_arguments()[0] = + address_of_exprt(target->call_arguments()[0]); + + // fix the function name. + to_symbol_expr(target->call_function()) + .set_identifier( + library.dfcc_fun_symbol[dfcc_funt::OBEYS_CONTRACT].name); + + // pass the write_set + target->call_arguments().push_back(write_set); + + // record discovered function contract + get_contract_name( + target->call_arguments()[1], function_pointer_contracts); + } + } + } + } +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h new file mode 100644 index 00000000000..a24c6bde562 --- /dev/null +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h @@ -0,0 +1,69 @@ +/*******************************************************************\ + +Module: Dynamic frame condition checking for function contracts + +Author: Remi Delmas, delmasrd@amazon.com +Date: August 2022 + +\*******************************************************************/ + +/// \file +/// Instruments occurrences of obeys_contract predicates in programs +/// encoding requires and ensures clauses of contracts + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_OBEYS_CONTRACT_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_OBEYS_CONTRACT_H + +#include + +#include + +class goto_modelt; +class message_handlert; +class dfcc_libraryt; +class exprt; + +/// Rewrites calls to obeys_contract predicates into calls +/// to the library implementation. +class dfcc_obeys_contractt +{ +public: + /// \param library The contracts instrumentation library + /// \param message_handler Used for messages + dfcc_obeys_contractt( + dfcc_libraryt &library, + message_handlert &message_handler); + + /// Rewrites calls to obeys_contract predicates into calls + /// to the library implementation in the given program, passing the + /// given write_set expression as parameter to the library function. + void rewrite_calls( + goto_programt &program, + const exprt &write_set, + std::set &function_pointer_contracts); + + /// Rewrites calls to obeys_contract predicates into calls + /// to the library implementation in the given program between + /// first_instruction (included) and last_instruction (excluded), passing the + /// given write_set expression as parameter to the library function. + void rewrite_calls( + goto_programt &program, + goto_programt::targett first_instruction, + const goto_programt::targett &last_instruction, + const exprt &write_set, + std::set &function_pointer_contracts); + +protected: + dfcc_libraryt &library; + message_handlert &message_handler; + messaget log; + + /// Extracts the name from the second argument of a call to + /// `obeys_contract` (modulo any intermediate typecast expressions). + /// and adds it to function_pointer_contracts + void get_contract_name( + const exprt &expr, + std::set &function_pointer_contracts); +}; + +#endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp index 1ef72e3491f..566d1b56d14 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -358,7 +358,11 @@ void dfcc_spec_functionst::to_spec_assigns_function( goto_model.goto_functions.update(); // instrument for side-effects checking - instrument.instrument_function(function_id); + std::set function_pointer_contracts; + instrument.instrument_function(function_id, function_pointer_contracts); + INVARIANT( + function_pointer_contracts.size() == 0, + "discovered function pointer contracts unexpectedly"); utils.set_hide(function_id, true); } @@ -412,7 +416,11 @@ void dfcc_spec_functionst::to_spec_frees_function( goto_model.goto_functions.update(); // instrument for side-effects checking - instrument.instrument_function(function_id); + std::set function_pointer_contracts; + instrument.instrument_function(function_id, function_pointer_contracts); + INVARIANT( + function_pointer_contracts.size() == 0, + "discovered function pointer contracts unexpectedly"); utils.set_hide(function_id, true); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp index 1b598f83686..93bbefd2f64 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp @@ -270,7 +270,8 @@ void dfcc_swap_and_wrapt::check_contract( utils.set_hide(wrapper_id, true); // instrument the wrapped function - instrument.instrument_wrapped_function(wrapped_id, wrapper_id); + instrument.instrument_wrapped_function( + wrapped_id, wrapper_id, function_pointer_contracts); goto_model.goto_functions.update(); } 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 967dc0fbbf3..46aa0654c3c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -26,8 +26,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_contract_functions.h" #include "dfcc_instrument.h" -#include "dfcc_is_freeable.h" -#include "dfcc_is_fresh.h" #include "dfcc_library.h" #include "dfcc_utils.h" @@ -700,20 +698,14 @@ void dfcc_wrapper_programt::encode_requires_clauses() codet requires_statement(statement_type, {std::move(requires)}, sl); converter.goto_convert(requires_statement, requires_program, language_mode); } - const auto address_of_requires_write_set = addr_of_requires_write_set; - // rewrite is_fresh predicates - dfcc_is_fresht is_fresh(library, message_handler); - is_fresh.rewrite_calls(requires_program, address_of_requires_write_set); - - // rewrite is_freeable predicates - dfcc_is_freeablet is_freeable(library, message_handler); - is_freeable.rewrite_calls(requires_program, address_of_requires_write_set); - // instrument for side effects instrument.instrument_goto_program( - wrapper_id, requires_program, address_of_requires_write_set); + wrapper_id, + requires_program, + address_of_requires_write_set, + function_pointer_contracts); // append resulting program to preconditions section preconditions.destructive_append(requires_program); @@ -763,31 +755,23 @@ void dfcc_wrapper_programt::encode_ensures_clauses() const auto address_of_ensures_write_set = addr_of_ensures_write_set; - // rewrite is_fresh predicates - dfcc_is_fresht is_fresh(library, message_handler); - is_fresh.rewrite_calls(ensures_program, address_of_ensures_write_set); - - // rewrite was_freed predicates // When checking an ensures clause we link the contract write set to the - // ensures write set to know what was deallocated by the function and pass - // it to the was_freed predicate and perform the checks - { - auto function_symbol = - library.dfcc_fun_symbol[dfcc_funt::LINK_DEALLOCATED].symbol_expr(); - code_function_callt call(function_symbol); - auto &arguments = call.arguments(); - arguments.emplace_back(address_of_ensures_write_set); - arguments.emplace_back(addr_of_contract_write_set); - link_deallocated_contract.add( - goto_programt::make_function_call(call, wrapper_sl)); - } - - dfcc_is_freeablet is_freeable(library, message_handler); - is_freeable.rewrite_calls(ensures_program, address_of_ensures_write_set); + // ensures write set to know what was deallocated by the function so that + // the was_freed predicate can perform its checks + code_function_callt call( + library.dfcc_fun_symbol[dfcc_funt::LINK_DEALLOCATED].symbol_expr()); + auto &arguments = call.arguments(); + arguments.emplace_back(address_of_ensures_write_set); + arguments.emplace_back(addr_of_contract_write_set); + link_deallocated_contract.add( + goto_programt::make_function_call(call, wrapper_sl)); // instrument for side effects instrument.instrument_goto_program( - wrapper_id, ensures_program, address_of_ensures_write_set); + wrapper_id, + ensures_program, + address_of_ensures_write_set, + function_pointer_contracts); // add the snapshot program in the history section history.destructive_append(history_snapshot_program); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h index 8b108d0a60d..f253fc4cf34 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h @@ -33,11 +33,10 @@ class dfcc_libraryt; class dfcc_utilst; class code_with_contract_typet; class conditional_target_group_exprt; -class function_pointer_obeys_contract_exprt; /// \brief Generates the body of a wrapper function from a contract -/// specified using requires, requires_contract, assigns, frees, ensures, -/// ensures_contract clauses attached to a function symbol. The desired mode +/// specified using requires, assigns, frees, ensures, +/// clauses attached to a function symbol. The desired mode /// CHECK or REPLACE is given to the constructor of the class. /// /// \details The body of the wrapper is divided into a number of sections