From 9060de1399a6b5282c8d92226f8d6651b319bd05 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 21 Dec 2021 20:13:28 +0000 Subject: [PATCH 1/3] Function contracts: allow history variables for typecast and constant expressions. --- regression/contracts/history-constant/main.c | 15 ++++++++++++ .../contracts/history-constant/test.desc | 10 ++++++++ regression/contracts/history-typecast/main.c | 23 +++++++++++++++++++ .../contracts/history-typecast/test.desc | 10 ++++++++ src/goto-instrument/contracts/contracts.cpp | 5 ++-- 5 files changed, 61 insertions(+), 2 deletions(-) create mode 100644 regression/contracts/history-constant/main.c create mode 100644 regression/contracts/history-constant/test.desc create mode 100644 regression/contracts/history-typecast/main.c create mode 100644 regression/contracts/history-typecast/test.desc diff --git a/regression/contracts/history-constant/main.c b/regression/contracts/history-constant/main.c new file mode 100644 index 00000000000..3806fc67c58 --- /dev/null +++ b/regression/contracts/history-constant/main.c @@ -0,0 +1,15 @@ +#include + +int foo(int l) __CPROVER_requires(-10 <= l && l <= 10) __CPROVER_ensures( + __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(10)) +{ + return l + 10; +} + +int main() +{ + int l; + __CPROVER_assume(-10 <= l && l <= 10); + foo(l); + return 0; +} diff --git a/regression/contracts/history-constant/test.desc b/regression/contracts/history-constant/test.desc new file mode 100644 index 00000000000..bedf99c897e --- /dev/null +++ b/regression/contracts/history-constant/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^Tracking history of constant expressions is not supported yet +-- +This test checks that history variables are supported for constant expressions. diff --git a/regression/contracts/history-typecast/main.c b/regression/contracts/history-typecast/main.c new file mode 100644 index 00000000000..db496514605 --- /dev/null +++ b/regression/contracts/history-typecast/main.c @@ -0,0 +1,23 @@ +#include + +long bar(long l, long r) __CPROVER_requires(-10 <= l && l <= 10) + __CPROVER_requires(-10 <= r && r <= 10) __CPROVER_ensures( + __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r)) +{ + return l + r; +} + +int foo(int l, int r) __CPROVER_requires(-10 <= l && l <= 10) + __CPROVER_requires(-10 <= r && r <= 10) __CPROVER_ensures( + __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r)) +{ + return bar((long)l, (long)r); +} + +int main() +{ + int n; + __CPROVER_assume(-10 <= n && n <= 10); + foo(n, n); + return 0; +} diff --git a/regression/contracts/history-typecast/test.desc b/regression/contracts/history-typecast/test.desc new file mode 100644 index 00000000000..cb588223265 --- /dev/null +++ b/regression/contracts/history-typecast/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--replace-call-with-contract bar --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^Tracking history of typecast expressions is not supported yet +-- +This test checks that history variables are supported for typecast expressions. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 6c74c51d0c5..f962a50d6e3 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -562,9 +562,10 @@ void code_contractst::replace_history_parameter( { const auto ¶meter = to_history_expr(expr, id).expression(); + const auto &id = parameter.id(); if( - parameter.id() == ID_dereference || parameter.id() == ID_member || - parameter.id() == ID_symbol || parameter.id() == ID_ptrmember) + id == ID_dereference || id == ID_member || id == ID_symbol || + id == ID_ptrmember || id == ID_constant || id == ID_typecast) { auto it = parameter2history.find(parameter); From c65d0ffa88a54394dda7376291d1697f1cdc332f Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 21 Dec 2021 20:15:56 +0000 Subject: [PATCH 2/3] Function contracts: add missing DECL/DEAD instructions for `ignored_return_value` variables introduced by contract replacement (these would previously appear as global variables). --- .../main.c | 37 +++++++++++++++++++ .../test.desc | 13 +++++++ src/goto-instrument/contracts/contracts.cpp | 21 +++++++++++ 3 files changed, 71 insertions(+) create mode 100644 regression/contracts/assigns-replace-ignored-return-value/main.c create mode 100644 regression/contracts/assigns-replace-ignored-return-value/test.desc diff --git a/regression/contracts/assigns-replace-ignored-return-value/main.c b/regression/contracts/assigns-replace-ignored-return-value/main.c new file mode 100644 index 00000000000..2ebe8aa5e84 --- /dev/null +++ b/regression/contracts/assigns-replace-ignored-return-value/main.c @@ -0,0 +1,37 @@ +#include +#include + +int bar(int l, int r) __CPROVER_requires(0 <= l && l <= 10) + __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures( + __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r)) +{ + return l + r; +} + +int *baz(int l, int r) __CPROVER_requires(0 <= l && l <= 10) + __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures( + *__CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r)) +{ + int *res = malloc(sizeof(int)); + *res = l + r; + return res; +} + +int foo(int l, int r) __CPROVER_requires(0 <= l && l <= 10) + __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures( + __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r)) +{ + bar(l, r); + bar(l, r); + baz(l, r); + baz(l, r); + return l + r; +} + +int main() +{ + int l; + int r; + foo(l, r); + return 0; +} diff --git a/regression/contracts/assigns-replace-ignored-return-value/test.desc b/regression/contracts/assigns-replace-ignored-return-value/test.desc new file mode 100644 index 00000000000..c08d1bf63dc --- /dev/null +++ b/regression/contracts/assigns-replace-ignored-return-value/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^[.*] Check that .*ignored_return_value.* is assignable: FAILURE +-- +This test checks that when replacing a call by a contract for a call that +ignores the return value of the function, the temporary introduced to +receive the call result does not trigger errors with assigns clause Checking +in the function under verification. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index f962a50d6e3..7d4820bf3c1 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -672,6 +672,9 @@ bool code_contractst::apply_function_contract( // keep track of the call's return expression to make it nondet later optionalt call_ret_opt = {}; + // if true, the call return variable variable was created during replacement + bool call_ret_is_fresh_var = false; + if(type.return_type() != empty_typet()) { // Check whether the function's return value is not disregarded. @@ -696,6 +699,7 @@ bool code_contractst::apply_function_contract( { // The postcondition does mention __CPROVER_return_value, so mint a // fresh variable to replace __CPROVER_return_value with. + call_ret_is_fresh_var = true; const symbolt &fresh = get_fresh_aux_symbol( type.return_type(), id2string(target_function), @@ -803,6 +807,12 @@ bool code_contractst::apply_function_contract( auto &call_ret = call_ret_opt.value(); auto &loc = call_ret.source_location(); auto &type = call_ret.type(); + + // Declare if fresh + if(call_ret_is_fresh_var) + havoc_instructions.add( + goto_programt::make_decl(to_symbol_expr(call_ret), loc)); + side_effect_expr_nondett expr(type, location); auto target = havoc_instructions.add( goto_programt::make_assignment(call_ret, expr, loc)); @@ -819,6 +829,17 @@ bool code_contractst::apply_function_contract( is_fresh.update_ensures(ensures_pair.first); insert_before_swap_and_advance(function_body, target, ensures_pair.first); } + + // Kill return value variable if fresh + if(call_ret_is_fresh_var) + { + function_body.output_instruction(ns, "", log.warning(), *target); + auto dead_inst = + goto_programt::make_dead(to_symbol_expr(call_ret_opt.value()), location); + function_body.insert_before_swap(target, dead_inst); + ++target; + } + *target = goto_programt::make_skip(); // Add this function to the set of replaced functions. From 22c020b5166920531ec2fd20e077d8847d173002 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 21 Dec 2021 20:19:00 +0000 Subject: [PATCH 3/3] Function contracts: new method for havocking assigns clause targets that works when there are dependencies between targets. We now take a snapshot of the target addresses if they are valid and havoc them in a second step if they are valid. Previously we were havocking targets directly in an arbitrary sequence, and havocking s->ptr before *(s->ptr) before __CPROVER_POINTER_OBJECT(s->ptr) would cause spurious errors. --- .../contracts/assigns_enforce_21/test.desc | 4 +- .../contracts/assigns_replace_08/test.desc | 2 +- .../contracts/assigns_replace_09/test.desc | 2 +- .../enforce.desc | 9 + .../main_enforce.c | 9 + .../main_replace.c | 8 + .../replace.desc | 16 ++ .../vect.h | 48 ++++ .../enforce.desc | 9 + .../main_enforce.c | 9 + .../main_replace.c | 8 + .../replace.desc | 16 ++ .../vect.h | 48 ++++ src/goto-instrument/Makefile | 1 + src/goto-instrument/contracts/contracts.cpp | 38 ++- .../havoc_assigns_clause_targets.cpp | 250 ++++++++++++++++++ .../contracts/havoc_assigns_clause_targets.h | 62 +++++ 17 files changed, 524 insertions(+), 15 deletions(-) create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_fail/enforce.desc create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_enforce.c create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_replace.c create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_enforce.c create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_replace.c create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc create mode 100644 regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h create mode 100644 src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp create mode 100644 src/goto-instrument/contracts/havoc_assigns_clause_targets.h diff --git a/regression/contracts/assigns_enforce_21/test.desc b/regression/contracts/assigns_enforce_21/test.desc index 7e2b828b342..a75ef140a6c 100644 --- a/regression/contracts/assigns_enforce_21/test.desc +++ b/regression/contracts/assigns_enforce_21/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=10$ ^SIGNAL=0$ main.c function bar -^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ -^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$ +^\[bar\.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[bar\.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_replace_08/test.desc b/regression/contracts/assigns_replace_08/test.desc index 8d092c72be5..16b3fc738fa 100644 --- a/regression/contracts/assigns_replace_08/test.desc +++ b/regression/contracts/assigns_replace_08/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check ^EXIT=10$ ^SIGNAL=0$ -\[foo.\d+\] line \d+ Check that \*z is assignable: FAILURE$ +\[foo.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: FAILURE$ ^.* 1 of \d+ failed \(\d+ iteration.*\)$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/assigns_replace_09/test.desc b/regression/contracts/assigns_replace_09/test.desc index 9d04ed22a32..4d16659c1c8 100644 --- a/regression/contracts/assigns_replace_09/test.desc +++ b/regression/contracts/assigns_replace_09/test.desc @@ -3,7 +3,7 @@ main.c --replace-call-with-contract bar --enforce-contract foo ^EXIT=0$ ^SIGNAL=0$ -\[foo.\d+\] line \d+ Check that \*z is assignable: SUCCESS$ +\[foo.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^Condition: \!not\_found$ diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_fail/enforce.desc b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/enforce.desc new file mode 100644 index 00000000000..efca0a7366c --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/enforce.desc @@ -0,0 +1,9 @@ +CORE +main_enforce.c +--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Verifies the contract being replaced in `replace.desc`. diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_enforce.c b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_enforce.c new file mode 100644 index 00000000000..9780886b632 --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_enforce.c @@ -0,0 +1,9 @@ +#include "vect.h" + +int main() +{ + vect *v; + size_t incr; + resize_vec(v, incr); + return 0; +} diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_replace.c b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_replace.c new file mode 100644 index 00000000000..f6060603800 --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_replace.c @@ -0,0 +1,8 @@ +#include "vect.h" + +int main() +{ + vect *v; + resize_vec_incr10(v); + return 0; +} diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc new file mode 100644 index 00000000000..f3cd8965f37 --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc @@ -0,0 +1,16 @@ +CORE +main_replace.c +--replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check +^\[.*\] .* Check that v->size \(assigned by the contract of resize_vec\) is assignable: SUCCESS +^\[.*\] .* Check that v->arr \(assigned by the contract of resize_vec\) is assignable: FAILURE +^\[.*\] .* Check that POINTER_OBJECT\(\(const void \*\)v->arr\) \(assigned by the contract of resize_vec\) is assignable: FAILURE +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Shows that when an assigns clause contains targets that are dependent, +in this case, a pointer variable `v->arr` and +the object it points to `__CPROVER_POINTER_OBJECT(v->arr)`, we can correctly +havoc them when replacing the call by the contract. +In this version of the test the inclusion check must fail. diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h new file mode 100644 index 00000000000..73560893b05 --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h @@ -0,0 +1,48 @@ +#include +#include + +typedef struct vect +{ + char *arr; + size_t size; +} vect; + +void resize_vec(vect *v, size_t incr) + // clang-format off +__CPROVER_requires( + __CPROVER_is_fresh(v, sizeof(vect)) && + 0 < v->size && v->size <= __CPROVER_max_malloc_size && + 0 < incr && incr < __CPROVER_max_malloc_size - v->size && + __CPROVER_is_fresh(v->arr, v->size) +) +__CPROVER_assigns(v->size, v->arr, __CPROVER_POINTER_OBJECT(v->arr)) +__CPROVER_ensures( + v->size == __CPROVER_old(v->size) + __CPROVER_old(incr) && + __CPROVER_is_fresh(v->arr, v->size) +) +// clang-format on +{ + free(v->arr); + v->size += incr; + v->arr = malloc(v->size); + return; +} + +void resize_vec_incr10(vect *v) + // clang-format off +__CPROVER_requires( + __CPROVER_is_fresh(v, sizeof(vect)) && + 0 < v->size && v->size <= __CPROVER_max_malloc_size && + v->size + 10 < __CPROVER_max_malloc_size && + __CPROVER_is_fresh(v->arr, v->size) +) +__CPROVER_assigns(v->size) +__CPROVER_ensures( + v->size == __CPROVER_old(v->size) + 10 && + __CPROVER_is_fresh(v->arr, v->size) +) +// clang-format on +{ + resize_vec(v, 10); + return; +} diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc new file mode 100644 index 00000000000..efca0a7366c --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc @@ -0,0 +1,9 @@ +CORE +main_enforce.c +--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Verifies the contract being replaced in `replace.desc`. diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_enforce.c b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_enforce.c new file mode 100644 index 00000000000..9780886b632 --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_enforce.c @@ -0,0 +1,9 @@ +#include "vect.h" + +int main() +{ + vect *v; + size_t incr; + resize_vec(v, incr); + return 0; +} diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_replace.c b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_replace.c new file mode 100644 index 00000000000..f6060603800 --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_replace.c @@ -0,0 +1,8 @@ +#include "vect.h" + +int main() +{ + vect *v; + resize_vec_incr10(v); + return 0; +} diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc new file mode 100644 index 00000000000..207acb976ae --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc @@ -0,0 +1,16 @@ +CORE +main_replace.c +--replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check +^VERIFICATION SUCCESSFUL$ +^\[.*\] .* Check that v->size \(assigned by the contract of resize_vec\) is assignable: SUCCESS +^\[.*\] .* Check that v->arr \(assigned by the contract of resize_vec\) is assignable: SUCCESS +^\[.*\] .* Check that POINTER_OBJECT\(\(const void \*\)v->arr\) \(assigned by the contract of resize_vec\) is assignable: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Shows that when an assigns clause contains targets that are dependent, +in this case, a pointer variable `v->arr` and +the object it points to `__CPROVER_POINTER_OBJECT(v->arr)`, we can correctly +havoc them when replacing the call by the contract. +In this version of the test the inclusion check must pass. diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h new file mode 100644 index 00000000000..8591628104b --- /dev/null +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h @@ -0,0 +1,48 @@ +#include +#include + +typedef struct vect +{ + char *arr; + size_t size; +} vect; + +void resize_vec(vect *v, size_t incr) + // clang-format off +__CPROVER_requires( + __CPROVER_is_fresh(v, sizeof(vect)) && + 0 < v->size && v->size <= __CPROVER_max_malloc_size && + 0 < incr && incr < __CPROVER_max_malloc_size - v->size && + __CPROVER_is_fresh(v->arr, v->size) +) +__CPROVER_assigns(v->size, v->arr, __CPROVER_POINTER_OBJECT(v->arr)) +__CPROVER_ensures( + v->size == __CPROVER_old(v->size) + __CPROVER_old(incr) && + __CPROVER_is_fresh(v->arr, v->size) +) +// clang-format on +{ + free(v->arr); + v->size += incr; + v->arr = malloc(v->size); + return; +} + +void resize_vec_incr10(vect *v) + // clang-format off +__CPROVER_requires( + __CPROVER_is_fresh(v, sizeof(vect)) && + 0 < v->size && v->size <= __CPROVER_max_malloc_size && + v->size + 10 < __CPROVER_max_malloc_size && + __CPROVER_is_fresh(v->arr, v->size) +) +__CPROVER_assigns(*v, __CPROVER_POINTER_OBJECT(v->arr)) +__CPROVER_ensures( + v->size == __CPROVER_old(v->size) + 10 && + __CPROVER_is_fresh(v->arr, v->size) +) +// clang-format on +{ + resize_vec(v, 10); + return; +} diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 9a7ca193ea8..c7cd8e63aa8 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -18,6 +18,7 @@ SRC = accelerate/accelerate.cpp \ call_sequences.cpp \ contracts/assigns.cpp \ contracts/contracts.cpp \ + contracts/havoc_assigns_clause_targets.cpp \ contracts/memory_predicates.cpp \ contracts/utils.cpp \ concurrency.cpp \ diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 7d4820bf3c1..f857962818e 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -43,6 +43,7 @@ Date: February 2016 #include #include +#include "havoc_assigns_clause_targets.h" #include "memory_predicates.h" #include "utils.h" @@ -790,15 +791,17 @@ bool code_contractst::apply_function_contract( // ...for assigns clause targets if(!assigns_clause.empty()) { - assigns_clauset assigns_clause( - targets.operands(), log, ns, target_function, symbol_table); - - // Havoc all targets in the write set - assignst assigns; - assigns.insert(targets.operands().cbegin(), targets.operands().cend()); - - havoc_assigns_targetst havoc_gen(assigns, ns); - havoc_gen.append_full_havoc_code(location, havoc_instructions); + // Havoc all targets in the assigns clause + // TODO: handle local statics possibly touched by this function + havoc_assigns_clause_targets( + target_function, + targets.operands(), + havoc_instructions, + // context parameters + location, + mode, + ns, + symbol_table); } // ...for the return value @@ -840,6 +843,7 @@ bool code_contractst::apply_function_contract( ++target; } + // Erase original function call *target = goto_programt::make_skip(); // Add this function to the set of replaced functions. @@ -1422,8 +1426,20 @@ code_contractst::add_inclusion_check( source_locationt location_no_checks = instruction_it->source_location_nonconst(); disable_pointer_checks(location_no_checks); - location_no_checks.set_comment( - "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable"); + + // does this assignment come from some contract replacement ? + const auto &comment = location_no_checks.get_comment(); + if(is_assigns_clause_replacement_tracking_comment(comment)) + { + location_no_checks.set_comment( + "Check that " + id2string(comment) + " is assignable"); + } + else + { + location_no_checks.set_comment( + "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable"); + } + assertion.add(goto_programt::make_assertion( assigns.generate_inclusion_check(car, cfg_info_opt), location_no_checks)); insert_before_swap_and_advance(program, instruction_it, assertion); diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp new file mode 100644 index 00000000000..7b6d3c8820c --- /dev/null +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp @@ -0,0 +1,250 @@ +/*******************************************************************\ + +Module: Havoc multiple and possibly dependent targets simultaneously + +Author: Remi Delmas, delmasrd@amazon.com + +\*******************************************************************/ + +/// \file +/// Havoc multiple and possibly dependent targets simultaneously + +#include "havoc_assigns_clause_targets.h" + +#include + +#include + +#include +#include +#include +#include +#include +#include +#include + +#include "utils.h" + +static const char ASSIGNS_CLAUSE_REPLACEMENT_TRACKING[] = + " (assigned by the contract of "; + +static irep_idt make_tracking_comment( + const exprt &target, + const irep_idt &function_id, + const namespacet &ns) +{ + return from_expr(ns, target.id(), target) + + ASSIGNS_CLAUSE_REPLACEMENT_TRACKING + id2string(function_id) + ")"; +} + +bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment) +{ + return id2string(comment).find(ASSIGNS_CLAUSE_REPLACEMENT_TRACKING) != + std::string::npos; +} + +/// Returns a pointer expression to the start address of the target +/// +/// - If the target is a `pointer_object(p)` expression, +/// return a pointer to the same object with offset zero +/// - else, if the target is a sized and assignable expression, +/// return its address +/// - else trigger an error. +/// +static exprt build_address_of( + const exprt &target, + // context parameters + const namespacet &ns) +{ + if(target.id() == ID_pointer_object) + { + const auto &ptr = target.operands().front(); + // bring the offset back to zero + return minus_exprt{ptr, pointer_offset(ptr)}; + } + else if(is_assignable(target)) + { + INVARIANT( + size_of_expr(target.type(), ns).has_value(), + "`sizeof` must always be computable on assignable assigns clause " + "targets."); + + return address_of_exprt{target}; + } + UNREACHABLE; +} + +/// \brief Generates instructions to conditionally snapshot the value +/// of `target_pointer` into `target_snapshot_var`. +/// +/// ``` +/// DECL target_valid_var : bool +/// DECL target_snapshot_var : +/// ASSIGN target_valid_var := +/// ASSIGN target_snapshot_var := NULL +/// IF !target_valid_var GOTO skip_target +/// ASSIGN target_snapshot_var := target_pointer; +/// skip_target: SKIP +/// ``` +/// +static void snapshot_if_valid( + const symbol_exprt &target_valid_var, + const symbol_exprt &target_snapshot_var, + const exprt &target_pointer, + goto_programt &dest, + // context parameters + const source_locationt &source_location, + const namespacet &ns) +{ + source_locationt source_location_no_checks(source_location); + disable_pointer_checks(source_location_no_checks); + + dest.add(goto_programt::make_decl(target_valid_var)); + + dest.add(goto_programt::make_decl(target_snapshot_var)); + + dest.add(goto_programt::make_assignment( + target_valid_var, + all_dereferences_are_valid(target_pointer, ns), + source_location_no_checks)); + + dest.add(goto_programt::make_assignment( + target_snapshot_var, + null_pointer_exprt{to_pointer_type(target_pointer.type())}, + source_location_no_checks)); + + goto_programt skip_program; + const auto skip_target = + skip_program.add(goto_programt::make_skip(source_location_no_checks)); + + dest.add(goto_programt::make_goto( + skip_target, not_exprt{target_valid_var}, source_location_no_checks)); + + dest.add(goto_programt::make_assignment( + target_snapshot_var, target_pointer, source_location_no_checks)); + + dest.destructive_append(skip_program); +} + +/// \brief Generates instructions to conditionally havoc +/// the given `target_snapshot_var`. +/// +/// Generates these instructions if target is a `__CPROVER_POINTER_OBJECT(...)`: +/// +/// ``` +/// IF !target_valid_var GOTO skip_target +/// OTHER havoc_object(target_snapshot_var) +/// skip_target: SKIP +/// DEAD target_valid_var +/// DEAD target_snapshot_var +/// ``` +/// +/// And generate these instructions otherwise: +/// +/// ``` +/// IF !target_valid_var GOTO skip_target +/// ASSIGN *target_snapshot_var = nondet() +/// skip_target: SKIP +/// DEAD target_valid_var +/// DEAD target_snapshot_var +/// ``` +/// Adds a special comment on the havoc instructions in order to trace back +/// the havoc to the replaced function. +static void havoc_if_valid( + const symbol_exprt &target_valid_var, + const symbol_exprt &target_snapshot_var, + const exprt &target, + const irep_idt &tracking_comment, + goto_programt &dest, + // context parameters + const source_locationt &source_location, + const namespacet &ns) +{ + source_locationt source_location_no_checks(source_location); + disable_pointer_checks(source_location_no_checks); + + goto_programt skip_program; + const auto skip_target = + skip_program.add(goto_programt::make_skip(source_location_no_checks)); + + dest.add(goto_programt::make_goto( + skip_target, not_exprt{target_valid_var}, source_location_no_checks)); + + if(target.id() == ID_pointer_object) + { + // OTHER __CPROVER_havoc_object(target_snapshot_var) + codet code(ID_havoc_object, {target_snapshot_var}); + const auto &inst = + dest.add(goto_programt::make_other(code, source_location)); + inst->source_location_nonconst().set_comment(tracking_comment); + } + else + { + // ASSIGN *target_snapshot_var = nondet() + side_effect_expr_nondett nondet(target.type(), source_location); + const auto &inst = dest.add(goto_programt::make_assignment( + dereference_exprt{target_snapshot_var}, nondet, source_location)); + inst->source_location_nonconst().set_comment(tracking_comment); + } + + dest.destructive_append(skip_program); + + dest.add( + goto_programt::make_dead(target_valid_var, source_location_no_checks)); + + dest.add( + goto_programt::make_dead(target_snapshot_var, source_location_no_checks)); +} + +void havoc_assigns_clause_targets( + const irep_idt &replaced_function_id, + const std::vector &targets, + goto_programt &dest, + // context parameters + const source_locationt &source_location, + const irep_idt &mode, + namespacet &ns, + symbol_tablet &st) +{ + goto_programt snapshot_program; + goto_programt havoc_program; + + for(const auto &target : targets) + { + const auto &tracking_comment = + make_tracking_comment(target, replaced_function_id, ns); + + const auto target_pointer = build_address_of(target, ns); + const auto target_snapshot_var = new_tmp_symbol( + target_pointer.type(), + source_location, + mode, + st, + "__target_snapshot_var", + true) + .symbol_expr(); + const auto target_valid_var = + new_tmp_symbol( + bool_typet(), source_location, mode, st, "__target_valid_var", true) + .symbol_expr(); + + snapshot_if_valid( + target_valid_var, + target_snapshot_var, + target_pointer, + snapshot_program, + source_location, + ns); + havoc_if_valid( + target_valid_var, + target_snapshot_var, + target, + tracking_comment, + havoc_program, + source_location, + ns); + } + + dest.destructive_append(snapshot_program); + dest.destructive_append(havoc_program); +} diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h new file mode 100644 index 00000000000..2a3c6272bda --- /dev/null +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h @@ -0,0 +1,62 @@ +/*******************************************************************\ + +Module: Havoc multiple and possibly dependent targets simultaneously + +Author: Remi Delmas, delmasrd@amazon.com + +\*******************************************************************/ + +/// \file +/// Havoc function assigns clauses + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H + +#include + +class namespacet; +class symbol_tablet; +class goto_programt; + +/// Generates havocking instructions for target expressions of a +/// function contract's assign clause (replacement). +/// +/// \param replaced_function_id Name of the replaced function +/// \param targets Assigns clause targets +/// \param dest Destination program where the instructions are generated +/// \param source_location Source location of the replaced function call +/// (added to all generated instructions) +/// \param mode Language mode to use for newly generated symbols +/// \param ns Namespace of the model +/// \param st Symbol table of the model (new symbols will be added) +/// +/// Assigns clause targets can be interdependent as shown in this example: +/// +/// ``` +/// typedef struct vect { int *arr; int size; } vect; +/// void resize(vect *v) +/// __CPROVER_assigns(v->arr, v->size, __CPROVER_POINTER_OBJECT(v->arr)) +/// { +/// free(v->arr); +/// v->size += 10 * sizeof(int); +/// v->arr = malloc(v->size); +/// } +/// ``` +/// +/// To havoc these dependent targets simultaneously, we first take snapshots +/// of their addresses, and havoc them in a second time. +/// Snapshotting and havocking are both guarded by the validity of the target. +/// +void havoc_assigns_clause_targets( + const irep_idt &replaced_function_id, + const std::vector &targets, + goto_programt &dest, + // context parameters + const source_locationt &source_location, + const irep_idt &mode, + namespacet &ns, + symbol_tablet &st); + +bool is_assigns_clause_replacement_tracking_comment(const irep_idt &comment); + +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H