From f6ea3ecab382b12e0af1b8378267f6f417f39ef5 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Fri, 1 Oct 2021 23:04:41 +0000 Subject: [PATCH 1/3] Refactor out `new_tmp_symbol` into utils --- src/goto-instrument/contracts/contracts.cpp | 33 +++++++-------------- src/goto-instrument/contracts/contracts.h | 5 ---- src/goto-instrument/contracts/utils.cpp | 16 ++++++++++ src/goto-instrument/contracts/utils.h | 31 +++++++++++++------ 4 files changed, 49 insertions(+), 36 deletions(-) diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 33ebc0e2d70..bcf1c5a7566 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -169,14 +169,16 @@ void code_contractst::check_apply_loop_contracts( for(const auto &clause : decreases_clause.operands()) { const auto old_decreases_var = - new_tmp_symbol(clause.type(), loop_head->source_location, mode) + new_tmp_symbol( + clause.type(), loop_head->source_location, mode, symbol_table) .symbol_expr(); havoc_code.add( goto_programt::make_decl(old_decreases_var, loop_head->source_location)); old_decreases_vars.push_back(old_decreases_var); const auto new_decreases_var = - new_tmp_symbol(clause.type(), loop_head->source_location, mode) + new_tmp_symbol( + clause.type(), loop_head->source_location, mode, symbol_table) .symbol_expr(); havoc_code.add( goto_programt::make_decl(new_decreases_var, loop_head->source_location)); @@ -317,10 +319,8 @@ void code_contractst::add_quantified_variable( const auto &quantified_symbol = to_symbol_expr(quantified_variable); // 1. create fresh symbol - symbolt new_symbol = get_fresh_aux_symbol( + symbolt new_symbol = new_tmp_symbol( quantified_symbol.type(), - id2string(quantified_symbol.get_identifier()), - "tmp", quantified_symbol.source_location(), mode, symbol_table); @@ -370,7 +370,8 @@ void code_contractst::replace_history_parameter( // 1. Create a temporary symbol expression that represents the // history variable symbol_exprt tmp_symbol = - new_tmp_symbol(parameter.type(), location, mode).symbol_expr(); + new_tmp_symbol(parameter.type(), location, mode, symbol_table) + .symbol_expr(); // 2. Associate the above temporary variable to it's corresponding // expression @@ -609,20 +610,6 @@ void code_contractst::apply_loop_contract( } } -const symbolt &code_contractst::new_tmp_symbol( - const typet &type, - const source_locationt &source_location, - const irep_idt &mode) -{ - return get_fresh_aux_symbol( - type, - id2string(source_location.get_function()) + "::tmp_cc", - "tmp_cc", - source_location, - mode, - symbol_table); -} - symbol_tablet &code_contractst::get_symbol_table() { return symbol_table; @@ -962,7 +949,8 @@ void code_contractst::add_contract_check( symbol_exprt r = new_tmp_symbol( code_type.return_type(), skip->source_location, - function_symbol.mode) + function_symbol.mode, + symbol_table) .symbol_expr(); check.add(goto_programt::make_decl(r, skip->source_location)); @@ -986,7 +974,8 @@ void code_contractst::add_contract_check( symbol_exprt p = new_tmp_symbol( parameter_symbol.type, skip->source_location, - parameter_symbol.mode) + parameter_symbol.mode, + symbol_table) .symbol_expr(); check.add(goto_programt::make_decl(p, skip->source_location)); check.add(goto_programt::make_assignment( diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 75fff7612ba..8aa960023b6 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -96,11 +96,6 @@ class code_contractst void apply_loop_contracts(); - const symbolt &new_tmp_symbol( - const typet &type, - const source_locationt &source_location, - const irep_idt &mode); - void check_apply_loop_contracts( goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 4f4d772988a..b1c199229d5 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -10,6 +10,7 @@ Date: September 2021 #include "utils.h" +#include #include #include @@ -121,3 +122,18 @@ void insert_before_swap_and_advance( destination.insert_before_swap(target, payload); std::advance(target, offset); } + +const symbolt &new_tmp_symbol( + const typet &type, + const source_locationt &location, + const irep_idt &mode, + symbol_table_baset &symtab) +{ + return get_fresh_aux_symbol( + type, + id2string(location.get_function()) + "::tmp_cc", + "tmp_cc", + location, + mode, + symtab); +} diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index c82de0f0ce5..3be8c8f965d 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -53,10 +53,10 @@ class havoc_if_validt : public havoc_utilst /// over all dereferenced pointer expressions *(pexpr_1), *(pexpr_2), ... /// found in the AST of `expr`. /// -/// \param expr The expression that contains dereferences to be validated -/// \param ns The namespace that defines all symbols appearing in `expr` +/// \param expr: The expression that contains dereferences to be validated. +/// \param ns: The namespace that defines all symbols appearing in `expr`. /// \return A conjunctive expression that checks validity of all pointers -/// that are dereferenced within `expr` +/// that are dereferenced within `expr`. exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns); /// \brief Generate a lexicographic less-than comparison over ordered tuples @@ -65,9 +65,9 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns); /// comparison, lhs < rhs, between two ordered tuples of variables. /// This is used in instrumentation of decreases clauses. /// -/// \param lhs A vector of variables representing the LHS of the comparison -/// \param rhs A vector of variables representing the RHS of the comparison -/// \return A lexicographic less-than comparison expression: LHS < RHS +/// \param lhs: A vector of variables representing the LHS of the comparison. +/// \param rhs: A vector of variables representing the RHS of the comparison. +/// \return A lexicographic less-than comparison expression: LHS < RHS. exprt generate_lexicographic_less_than_check( const std::vector &lhs, const std::vector &rhs); @@ -81,12 +81,25 @@ exprt generate_lexicographic_less_than_check( /// After insertion, `target` is advanced by the size of the `payload`, /// and `payload` is destroyed. /// -/// \param destination The destination program for inserting the `payload` -/// \param target The instruction iterator at which to insert the `payload` -/// \param payload The goto program to be inserted into the `destination` +/// \param destination: The destination program for inserting the `payload`. +/// \param target: The instruction iterator at which to insert the `payload`. +/// \param payload: The goto program to be inserted into the `destination`. void insert_before_swap_and_advance( goto_programt &destination, goto_programt::targett &target, goto_programt &payload); +/// \brief Adds a new temporary symbol to the symbol table. +/// +/// \param type: The type of the new symbol. +/// \param location: The source location for the new symbol. +/// \param mode: The mode for the new symbol, e.g. ID_C, ID_java. +/// \param symtab: The symbol table to which the new symbol is to be added. +/// \return The new symbolt object. +const symbolt &new_tmp_symbol( + const typet &type, + const source_locationt &location, + const irep_idt &mode, + symbol_table_baset &symtab); + #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H From 3fca566a877ce938324c39c8af0be35e97a51f5e Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Fri, 1 Oct 2021 05:10:40 +0000 Subject: [PATCH 2/3] Implementation of assigns clauses based on CARs This change is a complete rewrite of the assigns clause, based on a new formalization. Each assigns clause target represents a "conditional address range" (CAR) that an address range guarded by a validity constraint. In this commit we also add support for __CPROVER_POINTER_OBJECT expressions in assigns clauses. --- .../contracts/assigns_enforce_18/test.desc | 9 +- .../contracts/assigns_enforce_23/main.c | 41 ++++ .../contracts/assigns_enforce_23/test.desc | 9 + .../assigns_enforce_arrays_02/main.c | 24 +- .../assigns_enforce_arrays_02/test.desc | 19 +- .../assigns_enforce_elvis_5/test.desc | 2 + .../assigns_enforce_function_calls/main.c | 2 +- .../assigns_enforce_function_calls/test.desc | 2 +- .../assigns_enforce_object_wrong_args/main.c | 15 ++ .../test.desc | 10 + .../assigns_enforce_offsets_1/test.desc | 2 +- .../assigns_enforce_side_effects_1/main.c | 2 +- .../assigns_enforce_side_effects_1/test.desc | 2 +- .../assigns_enforce_side_effects_2/test.desc | 2 +- .../assigns_enforce_side_effects_3/test.desc | 2 +- .../assigns_enforce_structs_06/main.c | 2 +- .../assigns_enforce_structs_07/main.c | 6 + .../contracts/assigns_replace_06/main.c | 5 +- .../assigns_type_checking_valid_cases/main.c | 2 +- regression/contracts/function_check_02/main.c | 2 +- .../history-pointer-both-01/test.desc | 5 - .../quantifiers-forall-ensures-enforce/main.c | 2 +- .../contracts/quantifiers-nested-01/main.c | 2 +- .../contracts/quantifiers-nested-03/main.c | 2 +- .../test_array_memory_enforce/main.c | 2 +- .../test_struct_member_enforce/main.c | 2 +- src/ansi-c/ansi_c_convert_type.cpp | 10 +- src/ansi-c/c_typecheck_base.cpp | 14 +- src/goto-instrument/contracts/assigns.cpp | 213 ++++++++++-------- src/goto-instrument/contracts/assigns.h | 81 +++++-- src/goto-instrument/contracts/contracts.cpp | 112 ++++++--- src/goto-instrument/contracts/contracts.h | 8 +- src/goto-instrument/havoc_utils.h | 2 +- 33 files changed, 411 insertions(+), 204 deletions(-) create mode 100644 regression/contracts/assigns_enforce_23/main.c create mode 100644 regression/contracts/assigns_enforce_23/test.desc create mode 100644 regression/contracts/assigns_enforce_object_wrong_args/main.c create mode 100644 regression/contracts/assigns_enforce_object_wrong_args/test.desc diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc index a5224854cf6..011006f19c6 100644 --- a/regression/contracts/assigns_enforce_18/test.desc +++ b/regression/contracts/assigns_enforce_18/test.desc @@ -3,21 +3,18 @@ main.c --enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check ^EXIT=10$ ^SIGNAL=0$ -^\[bar.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ +^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$ -^\[baz.\d+\] line \d+ Check that \*c is assignable: FAILURE$ +^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$ ^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$ -^.* 2 of \d+ failed \(\d+ iteration.*\)$ +^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$ -^\[foo.pointer\_primitives.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(tmp\_cc\$\d+\): FAILURE$ -^.* 3 of \d+ failed (\d+ iterations)$ -- Checks whether contract enforcement works with functions that deallocate memory. We had problems before when freeing a variable, but still keeping it on diff --git a/regression/contracts/assigns_enforce_23/main.c b/regression/contracts/assigns_enforce_23/main.c new file mode 100644 index 00000000000..9c346ec0f68 --- /dev/null +++ b/regression/contracts/assigns_enforce_23/main.c @@ -0,0 +1,41 @@ +#include +#include + +typedef struct +{ + uint8_t *buf; + size_t size; +} blob; + +void foo(blob *b, uint8_t *value) + // clang-format off +__CPROVER_requires(b->size == 5) +__CPROVER_assigns(__CPROVER_POINTER_OBJECT(b->buf)) +__CPROVER_assigns(__CPROVER_POINTER_OBJECT(value)) +__CPROVER_ensures(b->buf[0] == 1) +__CPROVER_ensures(b->buf[1] == 1) +__CPROVER_ensures(b->buf[2] == 1) +__CPROVER_ensures(b->buf[3] == 1) +__CPROVER_ensures(b->buf[4] == 1) +// clang-format on +{ + b->buf[0] = *value; + b->buf[1] = *value; + b->buf[2] = *value; + b->buf[3] = *value; + b->buf[4] = *value; + + *value = 2; +} + +int main() +{ + blob b; + b.size = 5; + b.buf = malloc(b.size * (sizeof(*(b.buf)))); + uint8_t value = 1; + + foo(&b, &value); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_23/test.desc b/regression/contracts/assigns_enforce_23/test.desc new file mode 100644 index 00000000000..b06d561e188 --- /dev/null +++ b/regression/contracts/assigns_enforce_23/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-contract foo +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that POINTER_OBJECT can be used both on arrays and scalars. diff --git a/regression/contracts/assigns_enforce_arrays_02/main.c b/regression/contracts/assigns_enforce_arrays_02/main.c index 2c1cdd94f1f..de5a2797aec 100644 --- a/regression/contracts/assigns_enforce_arrays_02/main.c +++ b/regression/contracts/assigns_enforce_arrays_02/main.c @@ -1,24 +1,24 @@ #include +#include -int idx = 4; +int *arr; -int nextIdx() __CPROVER_assigns(idx) +void f1(int *a, int len) __CPROVER_assigns(*a) { - idx++; - return idx; + a[0] = 0; + a[5] = 5; } -void f1(int a[], int len) __CPROVER_assigns(*a, idx) +void f2(int *a, int len) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a)) { - a[nextIdx()] = 5; + a[0] = 0; + a[5] = 5; + free(a); } int main() { - int arr[10]; - f1(arr, 10); - - assert(idx == 5); - - return 0; + arr = malloc(100 * sizeof(int)); + f1(arr, 100); + f2(arr, 100); } diff --git a/regression/contracts/assigns_enforce_arrays_02/test.desc b/regression/contracts/assigns_enforce_arrays_02/test.desc index 5ddc4e60a5a..abb9e92a686 100644 --- a/regression/contracts/assigns_enforce_arrays_02/test.desc +++ b/regression/contracts/assigns_enforce_arrays_02/test.desc @@ -1,14 +1,15 @@ CORE main.c ---enforce-contract f1 --enforce-contract nextIdx -^EXIT=0$ +--enforce-contract f1 --enforce-contract f2 +^\[f1.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$ +^\[f1.\d+\] line \d+ Check that a\[.*5\] is assignable: FAILURE$ +^\[f2.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$ +^\[f2.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$ +^\[f2.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ -- -- -Checks whether the instrumentation process does not duplicate function calls -used as part of array-index operations, i.e., if a function call is used in -the computation of the index of an array assignment, then instrumenting that -statement with an assigns clause will not result in multiple function calls. -This test also ensures that assigns clauses correctly check for global -variables modified by subcalls. +This test ensures that assigns clauses correctly check for global variables, +and access using *ptr vs POINTER_OBJECT(ptr). diff --git a/regression/contracts/assigns_enforce_elvis_5/test.desc b/regression/contracts/assigns_enforce_elvis_5/test.desc index e815a0c0523..10c0f7a376a 100644 --- a/regression/contracts/assigns_enforce_elvis_5/test.desc +++ b/regression/contracts/assigns_enforce_elvis_5/test.desc @@ -8,3 +8,5 @@ main.c -- Check that Elvis operator expressions of form '(cond ? *if_true : *if_false)' are supported in assigns clauses. + +BUG: `is_lvalue` in goto is not consistent with `target.get_bool(ID_C_lvalue)`. diff --git a/regression/contracts/assigns_enforce_function_calls/main.c b/regression/contracts/assigns_enforce_function_calls/main.c index c26805377ba..14e8d530642 100644 --- a/regression/contracts/assigns_enforce_function_calls/main.c +++ b/regression/contracts/assigns_enforce_function_calls/main.c @@ -17,5 +17,5 @@ int main() { int x; foo(&x); - return 0; + baz(&x); } diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc index 598fca5e6c8..f2547f2a9fb 100644 --- a/regression/contracts/assigns_enforce_function_calls/test.desc +++ b/regression/contracts/assigns_enforce_function_calls/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: Assigns clause is not side-effect free.$ +^.*error: illegal target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_object_wrong_args/main.c b/regression/contracts/assigns_enforce_object_wrong_args/main.c new file mode 100644 index 00000000000..404373b64e7 --- /dev/null +++ b/regression/contracts/assigns_enforce_object_wrong_args/main.c @@ -0,0 +1,15 @@ +#include +#include +#include + +int baz(int *x) __CPROVER_assigns(__CPROVER_POINTER_OBJECT()) +{ + *x = 0; + return 0; +} + +int main() +{ + int x; + baz(&x); +} diff --git a/regression/contracts/assigns_enforce_object_wrong_args/test.desc b/regression/contracts/assigns_enforce_object_wrong_args/test.desc new file mode 100644 index 00000000000..ae78712952d --- /dev/null +++ b/regression/contracts/assigns_enforce_object_wrong_args/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-contract baz +^EXIT=(1|64)$ +^SIGNAL=0$ +^.*error: pointer_object expects one argument$ +^CONVERSION ERROR$ +-- +-- +Check that `__CPROVER_POINTER_OBJECT` in assigns clauses are invoked correctly. diff --git a/regression/contracts/assigns_enforce_offsets_1/test.desc b/regression/contracts/assigns_enforce_offsets_1/test.desc index 6fe2141f856..875aaf1a281 100644 --- a/regression/contracts/assigns_enforce_offsets_1/test.desc +++ b/regression/contracts/assigns_enforce_offsets_1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --enforce-contract foo ^EXIT=10$ diff --git a/regression/contracts/assigns_enforce_side_effects_1/main.c b/regression/contracts/assigns_enforce_side_effects_1/main.c index e9b6445f84b..bfbb88df565 100644 --- a/regression/contracts/assigns_enforce_side_effects_1/main.c +++ b/regression/contracts/assigns_enforce_side_effects_1/main.c @@ -2,7 +2,7 @@ #include #include -int foo(bool a, int *x, long *y) __CPROVER_assigns(*(a ? x : y++)) +int foo(bool a, int *x, long long *y) __CPROVER_assigns(*(a ? x : y++)) { if(a) { diff --git a/regression/contracts/assigns_enforce_side_effects_1/test.desc b/regression/contracts/assigns_enforce_side_effects_1/test.desc index ad0e682709f..d6f3c98d246 100644 --- a/regression/contracts/assigns_enforce_side_effects_1/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_1/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: Assigns clause is not side-effect free.$ +^.*error: void-typed targets not permitted$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc index ad0e682709f..21ba293dd46 100644 --- a/regression/contracts/assigns_enforce_side_effects_2/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_2/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: Assigns clause is not side-effect free.$ +^.*error: illegal target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc index ad0e682709f..21ba293dd46 100644 --- a/regression/contracts/assigns_enforce_side_effects_3/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_3/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: Assigns clause is not side-effect free.$ +^.*error: illegal target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_06/main.c b/regression/contracts/assigns_enforce_structs_06/main.c index 340b50d9e21..9a8049574d5 100644 --- a/regression/contracts/assigns_enforce_structs_06/main.c +++ b/regression/contracts/assigns_enforce_structs_06/main.c @@ -8,7 +8,7 @@ struct pair size_t size; }; -void f1(struct pair *p) __CPROVER_assigns(*(p->buf)) +void f1(struct pair *p) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(p->buf)) { p->buf[0] = 0; p->buf[1] = 1; diff --git a/regression/contracts/assigns_enforce_structs_07/main.c b/regression/contracts/assigns_enforce_structs_07/main.c index f3ae51d8bc1..48ab563ee83 100644 --- a/regression/contracts/assigns_enforce_structs_07/main.c +++ b/regression/contracts/assigns_enforce_structs_07/main.c @@ -26,11 +26,17 @@ void f2(struct pair_of_pairs *pp) __CPROVER_assigns(*(pp->p->buf)) int main() { struct pair *p = malloc(sizeof(*p)); + if(p) + p->buf = malloc(100 * sizeof(uint8_t)); f1(p); struct pair_of_pairs *pp = malloc(sizeof(*pp)); if(pp) + { pp->p = malloc(sizeof(*(pp->p))); + if(pp->p) + pp->p->buf = malloc(100 * sizeof(uint8_t)); + } f2(pp); return 0; diff --git a/regression/contracts/assigns_replace_06/main.c b/regression/contracts/assigns_replace_06/main.c index 218313e9837..9b0fd9bb878 100644 --- a/regression/contracts/assigns_replace_06/main.c +++ b/regression/contracts/assigns_replace_06/main.c @@ -1,6 +1,7 @@ #include +#include -void foo(char c[]) __CPROVER_assigns(c) +void foo(char c[]) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(c)) { } @@ -28,6 +29,4 @@ int main() assert(b[1] == '1'); assert(b[2] == 'c'); assert(b[3] == '3'); - - return 0; } diff --git a/regression/contracts/assigns_type_checking_valid_cases/main.c b/regression/contracts/assigns_type_checking_valid_cases/main.c index f1a5b9d137d..69062b90dc4 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/main.c +++ b/regression/contracts/assigns_type_checking_valid_cases/main.c @@ -59,7 +59,7 @@ void foo7(int a, struct buf *buffer) __CPROVER_assigns(*buffer) buffer->len = 1; } -void foo8(int array[]) __CPROVER_assigns(*array) +void foo8(int array[]) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(array)) { array[0] = 1; array[1] = 1; diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c index d0b17f5fc34..7960696b6d1 100644 --- a/regression/contracts/function_check_02/main.c +++ b/regression/contracts/function_check_02/main.c @@ -6,7 +6,7 @@ // clang-format off int initialize(int *arr) - __CPROVER_assigns(*arr) + __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) __CPROVER_ensures( __CPROVER_forall { int i; diff --git a/regression/contracts/history-pointer-both-01/test.desc b/regression/contracts/history-pointer-both-01/test.desc index 168547f2e17..3854c9f2423 100644 --- a/regression/contracts/history-pointer-both-01/test.desc +++ b/regression/contracts/history-pointer-both-01/test.desc @@ -4,13 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -ASSUME .*::tmp_cc\$\d ≠ NULL -ASSERT foo::n ≠ NULL -ASSUME .*::tmp_cc = \*foo::n -ASSERT .*::tmp_cc\$\d = \*.*::tmp_cc\$\d -- -- -Verification: This test checks that history variables are supported for parameters of the the function under test. By using the --enforce-contract flag, the post-condition (which contains the history variable) is asserted. diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c index 78271197aec..db97d407e56 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/main.c +++ b/regression/contracts/quantifiers-forall-ensures-enforce/main.c @@ -4,7 +4,7 @@ // clang-format off int f1(int *arr, int len) - __CPROVER_assigns(*arr) + __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) __CPROVER_ensures(__CPROVER_forall { int i; // test enforcement with symbolic bound diff --git a/regression/contracts/quantifiers-nested-01/main.c b/regression/contracts/quantifiers-nested-01/main.c index d26dda4fb79..2e1d0667115 100644 --- a/regression/contracts/quantifiers-nested-01/main.c +++ b/regression/contracts/quantifiers-nested-01/main.c @@ -1,6 +1,6 @@ // clang-format off int f1(int *arr) - __CPROVER_assigns(*arr) + __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) __CPROVER_ensures(__CPROVER_forall { int i; __CPROVER_forall diff --git a/regression/contracts/quantifiers-nested-03/main.c b/regression/contracts/quantifiers-nested-03/main.c index ec26b365f81..e7bf048ddcf 100644 --- a/regression/contracts/quantifiers-nested-03/main.c +++ b/regression/contracts/quantifiers-nested-03/main.c @@ -1,6 +1,6 @@ // clang-format off int f1(int *arr) -__CPROVER_assigns(*arr) +__CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) __CPROVER_ensures( __CPROVER_return_value == 0 && __CPROVER_exists { diff --git a/regression/contracts/test_array_memory_enforce/main.c b/regression/contracts/test_array_memory_enforce/main.c index 0abfeefd0a3..7c1218d5a30 100644 --- a/regression/contracts/test_array_memory_enforce/main.c +++ b/regression/contracts/test_array_memory_enforce/main.c @@ -14,7 +14,7 @@ bool return_ok(int ret_value, int *x) // clang-format off int foo(int *x) - __CPROVER_assigns(*x) + __CPROVER_assigns(__CPROVER_POINTER_OBJECT(x)) __CPROVER_requires( __CPROVER_is_fresh(x, sizeof(int) * 10) && x[0] > 0 && diff --git a/regression/contracts/test_struct_member_enforce/main.c b/regression/contracts/test_struct_member_enforce/main.c index 54bf409fdfa..1133ef091cd 100644 --- a/regression/contracts/test_struct_member_enforce/main.c +++ b/regression/contracts/test_struct_member_enforce/main.c @@ -8,7 +8,7 @@ struct string // clang-format off int foo(struct string *x) - __CPROVER_assigns(*(x->str)) + __CPROVER_assigns(x->str[x->len-1]) __CPROVER_requires( x->len == 128 && __CPROVER_is_fresh(x->str, x->len * sizeof(char))) diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 3ed05251ef5..b9ae2799c02 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include @@ -255,15 +255,7 @@ void ansi_c_convert_typet::read_rec(const typet &type) static_cast(static_cast(type)); for(const exprt &target : to_unary_expr(as_expr).op().operands()) - { - if(has_subexpr(target, ID_side_effect)) - { - error().source_location = target.source_location(); - error() << "Assigns clause is not side-effect free." << eom; - throw 0; - } assigns.push_back(target); - } } else if(type.id() == ID_C_spec_ensures) { diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 492476fd7f7..c41bd51bbeb 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include "ansi_c_declaration.h" @@ -741,18 +742,29 @@ void c_typecheck_baset::typecheck_declaration( for(auto &target : code_type.assigns()) { typecheck_expr(target); + if(target.type().id() == ID_empty) { error().source_location = target.source_location(); error() << "void-typed targets not permitted" << eom; throw 0; } - if(!target.get_bool(ID_C_lvalue)) + else if(target.id() == ID_pointer_object) + { + // skip + } + else if(!target.get_bool(ID_C_lvalue)) { error().source_location = target.source_location(); error() << "illegal target in assigns clause" << eom; throw 0; } + else if(has_subexpr(target, ID_side_effect)) + { + error().source_location = target.source_location(); + error() << "assigns clause is not side-effect free" << eom; + throw 0; + } } if(!as_const(code_type).ensures().empty()) diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index 85996ab7691..49142f80aec 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -9,144 +9,177 @@ Date: July 2021 \*******************************************************************/ /// \file -/// Specify write set in function contracts +/// Specify write set in code contracts #include "assigns.h" -#include - #include +#include +#include #include #include -#include "utils.h" +static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns) +{ + // FIXME: Refactor these checks out to a common function that can be + // used both in compilation and instrumentation stages + if(expr.id() == ID_pointer_object) + { + const auto &arg = expr.operands().front(); + return { + minus_exprt{ + typecast_exprt::conditional_cast(arg, pointer_type(char_type())), + pointer_offset(arg)}, + typecast_exprt::conditional_cast(object_size(arg), signed_size_type())}; + } + else if(is_lvalue(expr)) + { + const auto &size = size_of_expr(expr.type(), ns); + + INVARIANT( + size.has_value(), + "`sizeof` must always be computable on l-value assigns clause targets."); + + return {typecast_exprt::conditional_cast( + address_of_exprt{expr}, pointer_type(char_type())), + typecast_exprt::conditional_cast(size.value(), signed_size_type())}; + } + + UNREACHABLE; +} + +const symbolt assigns_clauset::conditional_address_ranget::generate_new_symbol( + const typet &type, + const source_locationt &location) const +{ + return new_tmp_symbol( + type, + location, + parent.symbol_table.lookup_ref(parent.function_name).mode, + parent.symbol_table); +} -assigns_clauset::targett::targett( +assigns_clauset::conditional_address_ranget::conditional_address_ranget( const assigns_clauset &parent, const exprt &expr) - : address(address_of_exprt(normalize(expr))), - id(expr.id()), - parent(parent) + : source_expr(expr), + location(expr.source_location()), + parent(parent), + slice(normalize_to_slice(expr, parent.ns)), + validity_condition_var( + generate_new_symbol(bool_typet(), location).symbol_expr()), + lower_bound_address_var( + generate_new_symbol(slice.first.type(), location).symbol_expr()), + upper_bound_address_var( + generate_new_symbol(slice.first.type(), location).symbol_expr()) { } -exprt assigns_clauset::targett::normalize(const exprt &expr) +goto_programt +assigns_clauset::conditional_address_ranget::generate_snapshot_instructions() + const { - if(expr.id() != ID_address_of) - return expr; + goto_programt instructions; + + instructions.add(goto_programt::make_decl(validity_condition_var, location)); + instructions.add(goto_programt::make_decl(lower_bound_address_var, location)); + instructions.add(goto_programt::make_decl(upper_bound_address_var, location)); - const auto &object = to_address_of_expr(expr).object(); - if(object.id() != ID_index) - return object; + goto_programt skip_program; + const auto skip_target = skip_program.add(goto_programt::make_skip(location)); - return to_index_expr(object).array(); + const auto validity_check_expr = + and_exprt{all_dereferences_are_valid(source_expr, parent.ns), + w_ok_exprt{slice.first, slice.second}}; + instructions.add(goto_programt::make_assignment( + validity_condition_var, validity_check_expr, location)); + + instructions.add(goto_programt::make_goto( + skip_target, not_exprt{validity_condition_var}, location)); + + instructions.add(goto_programt::make_assignment( + lower_bound_address_var, slice.first, location)); + + instructions.add(goto_programt::make_assignment( + upper_bound_address_var, + minus_exprt{plus_exprt{slice.first, slice.second}, + from_integer(1, slice.second.type())}, + location)); + + instructions.destructive_append(skip_program); + return instructions; +} + +const exprt +assigns_clauset::conditional_address_ranget::generate_unsafe_inclusion_check( + const conditional_address_ranget &lhs) const +{ + return conjunction( + {validity_condition_var, + same_object(lower_bound_address_var, lhs.lower_bound_address_var), + same_object(lhs.upper_bound_address_var, upper_bound_address_var), + less_than_or_equal_exprt{lower_bound_address_var, + lhs.lower_bound_address_var}, + less_than_or_equal_exprt{lhs.upper_bound_address_var, + upper_bound_address_var}}); } assigns_clauset::assigns_clauset( const exprt::operandst &assigns, const messaget &log, - const namespacet &ns) - : log(log), ns(ns) + const namespacet &ns, + const irep_idt &function_name, + symbol_tablet &symbol_table) + : log(log), ns(ns), function_name(function_name), symbol_table(symbol_table) { for(const auto &target_expr : assigns) - { add_to_write_set(target_expr); - } } -void assigns_clauset::add_to_write_set(const exprt &target_expr) +assigns_clauset::write_sett::const_iterator +assigns_clauset::add_to_write_set(const exprt &target_expr) { - auto insertion_succeeded = write_set.emplace(*this, target_expr).second; + auto result = write_set.emplace(*this, target_expr); - if(!insertion_succeeded) + if(!result.second) { log.warning() << "Ignored duplicate expression '" << from_expr(ns, target_expr.id(), target_expr) << "' in assigns clause at " << target_expr.source_location().as_string() << messaget::eom; } + return result.first; } void assigns_clauset::remove_from_write_set(const exprt &target_expr) { - write_set.erase(targett(*this, target_expr)); + write_set.erase(conditional_address_ranget(*this, target_expr)); } -exprt assigns_clauset::targett::generate_containment_check( - const address_of_exprt &lhs_address) const +exprt assigns_clauset::generate_inclusion_check( + const conditional_address_ranget &lhs) const { - const auto address_validity = and_exprt{ - all_dereferences_are_valid(dereference_exprt{address}, parent.ns), - all_dereferences_are_valid(dereference_exprt{lhs_address}, parent.ns)}; - - exprt::operandst containment_check; - containment_check.push_back(same_object(lhs_address, address)); - - // If assigns target was a dereference, comparing objects is enough - // and the resulting condition will be: - // VALID(self) && VALID(lhs) ==> __CPROVER_same_object(lhs, self) - if(id != ID_dereference) - { - const auto lhs_offset = pointer_offset(lhs_address); - const auto own_offset = pointer_offset(address); - - // __CPROVER_offset(lhs) >= __CPROVER_offset(target) - containment_check.push_back( - binary_relation_exprt(lhs_offset, ID_ge, own_offset)); - - const auto lhs_region = plus_exprt( - typecast_exprt::conditional_cast( - size_of_expr(lhs_address.object().type(), parent.ns).value(), - lhs_offset.type()), - lhs_offset); - - const exprt own_region = plus_exprt( - typecast_exprt::conditional_cast( - size_of_expr(address.object().type(), parent.ns).value(), - own_offset.type()), - own_offset); - - // (sizeof(lhs) + __CPROVER_offset(lhs)) <= - // (sizeof(self) + __CPROVER_offset(self)) - containment_check.push_back( - binary_relation_exprt(lhs_region, ID_le, own_region)); - } - - // VALID(self) && VALID(lhs) - // ==> __CPROVER_same_object(lhs, self) - // && __CPROVER_offset(lhs) >= __CPROVER_offset(self) - // && (sizeof(lhs) + __CPROVER_offset(lhs)) <= - // (sizeof(self) + __CPROVER_offset(self)) - return or_exprt{not_exprt{address_validity}, conjunction(containment_check)}; -} + if(write_set.empty()) + return not_exprt{lhs.validity_condition_var}; -goto_programt -assigns_clauset::generate_havoc_code(const source_locationt &location) const -{ - modifiest modifies; + exprt::operandst conditions{not_exprt{lhs.validity_condition_var}}; for(const auto &target : write_set) - modifies.insert(target.address.object()); + conditions.push_back(target.generate_unsafe_inclusion_check(lhs)); - goto_programt havoc_statements; - havoc_if_validt havoc_gen(modifies, ns); - havoc_gen.append_full_havoc_code(location, havoc_statements); - - return havoc_statements; + return disjunction(conditions); } -exprt assigns_clauset::generate_containment_check(const exprt &lhs) const +void havoc_assigns_targetst::append_havoc_code_for_expr( + const source_locationt location, + const exprt &expr, + goto_programt &dest) const { - // If write set is empty, no assignment is allowed. - if(write_set.empty()) - return false_exprt(); - - const auto lhs_address = address_of_exprt(targett::normalize(lhs)); - - exprt::operandst condition; - for(const auto &target : write_set) + if(expr.id() == ID_pointer_object) { - condition.push_back(target.generate_containment_check(lhs_address)); + append_object_havoc_code_for_expr(location, expr.operands().front(), dest); + return; } - return disjunction(condition); + + havoc_utilst::append_havoc_code_for_expr(location, expr, dest); } diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h index 8ed37b21818..bdc97ead1d9 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -16,59 +16,100 @@ Date: July 2021 #include -#include - #include -#include + +#include "utils.h" + +typedef std::pair slicet; /// \brief A class for representing assigns clauses in code contracts class assigns_clauset { public: - /// \brief A class for representing targets for assigns clauses - class targett + /// \brief A class for representing Conditional Address Ranges + class conditional_address_ranget { public: - targett(const assigns_clauset &, const exprt &); + conditional_address_ranget(const assigns_clauset &, const exprt &); - static exprt normalize(const exprt &); + goto_programt generate_snapshot_instructions() const; - exprt generate_containment_check(const address_of_exprt &) const; - - bool operator==(const targett &other) const + bool operator==(const conditional_address_ranget &other) const { - return address == other.address; + return source_expr == other.source_expr; } struct hasht { - std::size_t operator()(const targett &target) const + std::size_t operator()(const conditional_address_ranget &target) const { - return irep_hash{}(target.address); + return irep_hash{}(target.source_expr); } }; - const address_of_exprt address; - const irep_idt &id; + const exprt source_expr; + const source_locationt &location; const assigns_clauset &parent; + + const slicet slice; + const symbol_exprt validity_condition_var; + const symbol_exprt lower_bound_address_var; + const symbol_exprt upper_bound_address_var; + + protected: + const exprt + generate_unsafe_inclusion_check(const conditional_address_ranget &) const; + + const symbolt + generate_new_symbol(const typet &, const source_locationt &) const; + + friend class assigns_clauset; }; + typedef std:: + unordered_set + write_sett; + assigns_clauset( const exprt::operandst &, const messaget &, - const namespacet &); + const namespacet &, + const irep_idt &, + symbol_tablet &); - void add_to_write_set(const exprt &); + write_sett::const_iterator add_to_write_set(const exprt &); void remove_from_write_set(const exprt &); - goto_programt generate_havoc_code(const source_locationt &) const; - exprt generate_containment_check(const exprt &) const; + exprt generate_inclusion_check(const conditional_address_ranget &) const; + + const write_sett &get_write_set() const + { + return write_set; + } const messaget &log; const namespacet &ns; + const irep_idt &function_name; protected: - std::unordered_set write_set; + symbol_tablet &symbol_table; + write_sett write_set; +}; + +/// \brief A class that further overrides the "safe" havoc utilities, +/// and adds support for havocing pointer_object expressions. +class havoc_assigns_targetst : public havoc_if_validt +{ +public: + havoc_assigns_targetst(const modifiest &mod, const namespacet &ns) + : havoc_if_validt(mod, ns) + { + } + + void append_havoc_code_for_expr( + const source_locationt location, + const exprt &expr, + goto_programt &dest) const override; }; #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_ASSIGNS_H diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index bcf1c5a7566..02bf8d824ad 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -433,6 +433,7 @@ code_contractst::create_ensures_instruction( bool code_contractst::apply_function_contract( const irep_idt &function, + const source_locationt &location, goto_programt &function_body, goto_programt::targett &target) { @@ -566,11 +567,17 @@ bool code_contractst::apply_function_contract( // in the assigns clause. if(!assigns.empty()) { - assigns_clauset assigns_clause(targets.operands(), log, ns); + assigns_clauset assigns_clause( + targets.operands(), log, ns, target_function, symbol_table); - // Havoc all targets in global write set - auto assigns_havoc = - assigns_clause.generate_havoc_code(target->source_location); + // Havoc all targets in the write set + modifiest modifies; + for(const auto &target : targets.operands()) + modifies.insert(target); + + goto_programt assigns_havoc; + havoc_assigns_targetst havoc_gen(modifies, ns); + havoc_gen.append_full_havoc_code(location, assigns_havoc); // Insert the non-deterministic assignment immediately before the call site. insert_before_swap_and_advance(function_body, target, assigns_havoc); @@ -643,7 +650,14 @@ void code_contractst::instrument_assign_statement( lhs_sym.is_static_lifetime && lhs_sym.location.get_function() == instruction_iterator->source_location.get_function()) - assigns_clause.add_to_write_set(lhs); + { + // TODO: Fix this. + // The CAR snapshot should be made only once at the beginning. + const auto car = assigns_clause.add_to_write_set(lhs); + auto snapshot_instructions = car->generate_snapshot_instructions(); + insert_before_swap_and_advance( + program, instruction_iterator, snapshot_instructions); + } } add_containment_check(program, assigns_clause, instruction_iterator, lhs); @@ -660,29 +674,37 @@ void code_contractst::instrument_call_statement( "The first argument of instrument_call_statement should always be " "a function call"); - irep_idt called_function = + const auto &callee_name = to_symbol_expr(instruction_it->call_function()).get_identifier(); - if(called_function == "malloc") + if(callee_name == "malloc") { - // malloc statments return a void pointer, which is then cast and assigned - // to a result variable. We iterate one line forward to grab the result of - // the malloc once it is cast. - instruction_it++; - if(instruction_it->is_assign()) + const auto &function_call = + to_code_function_call(instruction_it->get_code()); + if(function_call.lhs().is_not_nil()) { - instrument_assign_statement(instruction_it, body, assigns); - const exprt &lhs = instruction_it->assign_lhs(); - assigns.add_to_write_set(dereference_exprt(lhs)); + // grab the returned pointer from malloc + const auto &object = function_call.lhs(); + // move past the call and then insert the CAR + instruction_it++; + const auto car = assigns.add_to_write_set(pointer_object(object)); + auto snapshot_instructions = car->generate_snapshot_instructions(); + insert_before_swap_and_advance( + body, instruction_it, snapshot_instructions); + // since CAR was inserted *after* the malloc, + // move the instruction pointer backward, + // because the caller increments it in a `for` loop + instruction_it--; } - return; // assume malloc edits no pre-existing memory objects. + return; } - else if(called_function == "free") + else if(callee_name == "free") { - const exprt &lhs_dereference = dereference_exprt( - to_typecast_expr(instruction_it->call_arguments().front()).op()); - add_containment_check(body, assigns, instruction_it, lhs_dereference); - assigns.remove_from_write_set(lhs_dereference); + add_containment_check( + body, + assigns, + instruction_it, + pointer_object(instruction_it->call_arguments().front())); return; } } @@ -770,7 +792,11 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) // Get assigns clause for function const symbolt &target = ns.lookup(function); assigns_clauset assigns( - to_code_with_contract_type(target.type).assigns(), log, ns); + to_code_with_contract_type(target.type).assigns(), + log, + ns, + function, + symbol_table); // Adds formal parameters to freely assignable set for(auto ¶meter : to_code_type(target.type).parameters()) @@ -779,9 +805,17 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) ns.lookup(parameter.get_identifier()).symbol_expr()); } + auto instruction_it = function_obj->second.body.instructions.begin(); + for(const auto &car : assigns.get_write_set()) + { + auto snapshot_instructions = car.generate_snapshot_instructions(); + insert_before_swap_and_advance( + function_obj->second.body, instruction_it, snapshot_instructions); + }; + // Insert aliasing assertions check_frame_conditions( - function_obj->first, function_obj->second.body, assigns); + function_obj->first, function_obj->second.body, instruction_it, assigns); return false; } @@ -789,18 +823,27 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) void code_contractst::check_frame_conditions( const irep_idt &function, goto_programt &body, + goto_programt::targett &instruction_it, assigns_clauset &assigns) { goto_function_inline(goto_functions, function, ns, log.get_message_handler()); - for(auto instruction_it = body.instructions.begin(); - instruction_it != body.instructions.end(); - ++instruction_it) + for(; instruction_it != body.instructions.end(); ++instruction_it) { if(instruction_it->is_decl()) { - // Local variables are always freely assignable - assigns.add_to_write_set(instruction_it->get_decl().symbol()); + // grab the declared symbol + const auto &decl_symbol = instruction_it->get_decl().symbol(); + // move past the call and then insert the CAR + instruction_it++; + const auto car = assigns.add_to_write_set(decl_symbol); + auto snapshot_instructions = car->generate_snapshot_instructions(); + insert_before_swap_and_advance( + body, instruction_it, snapshot_instructions); + // since CAR was inserted *after* the DECL, + // move the instruction pointer backward, + // because the caller increments it in a `for` loop + instruction_it--; } else if(instruction_it->is_assign()) { @@ -821,7 +864,6 @@ void code_contractst::check_frame_conditions( const exprt &havoc_argument = dereference_exprt( to_typecast_expr(instruction_it->get_other().operands().front()).op()); add_containment_check(body, assigns, instruction_it, havoc_argument); - assigns.remove_from_write_set(havoc_argument); } } } @@ -832,9 +874,14 @@ void code_contractst::add_containment_check( goto_programt::instructionst::iterator &instruction_it, const exprt &expr) { + const assigns_clauset::conditional_address_ranget car{assigns, expr}; + auto snapshot_instructions = car.generate_snapshot_instructions(); + insert_before_swap_and_advance( + program, instruction_it, snapshot_instructions); + goto_programt assertion; assertion.add(goto_programt::make_assertion( - assigns.generate_containment_check(expr), instruction_it->source_location)); + assigns.generate_inclusion_check(car), instruction_it->source_location)); assertion.instructions.back().source_location.set_comment( "Check that " + from_expr(ns, expr.id(), expr) + " is assignable"); insert_before_swap_and_advance(program, instruction_it, assertion); @@ -1077,7 +1124,10 @@ bool code_contractst::replace_calls(const std::set &to_replace) continue; fail |= apply_function_contract( - goto_function.first, goto_function.second.body, ins); + goto_function.first, + ins->source_location, + goto_function.second.body, + ins); } } } diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 8aa960023b6..70d10e926a1 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -126,8 +126,11 @@ class code_contractst /// Insert assertion statements into the goto program to ensure that /// assigned memory is within the assignable memory frame. - void - check_frame_conditions(const irep_idt &, goto_programt &, assigns_clauset &); + void check_frame_conditions( + const irep_idt &, + goto_programt &, + goto_programt::targett &, + assigns_clauset &); /// Inserts an assertion into the goto program to ensure that /// an expression is within the assignable memory frame. @@ -171,6 +174,7 @@ class code_contractst /// based on ensures clauses. bool apply_function_contract( const irep_idt &, + const source_locationt &, goto_programt &, goto_programt::targett &); diff --git a/src/goto-instrument/havoc_utils.h b/src/goto-instrument/havoc_utils.h index 6bc1472b0de..0cdbdc699c9 100644 --- a/src/goto-instrument/havoc_utils.h +++ b/src/goto-instrument/havoc_utils.h @@ -73,7 +73,7 @@ class havoc_utilst /// \param location The source location to annotate on the havoc instruction /// \param expr The expression to havoc /// \param dest The destination goto program to append the instructions to - void append_havoc_code_for_expr( + virtual void append_havoc_code_for_expr( const source_locationt location, const exprt &expr, goto_programt &dest) const; From a307396850f9c1acf261c56fc44fcdee8dfbf9ff Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Sun, 3 Oct 2021 22:10:59 +0000 Subject: [PATCH 3/3] Fix CAR creation for local static symbols --- .../contracts/assigns_enforce_statics/main.c | 19 ++++++++ .../assigns_enforce_statics/test.desc | 13 ++++++ src/goto-instrument/contracts/contracts.cpp | 43 ++++++------------- 3 files changed, 45 insertions(+), 30 deletions(-) create mode 100644 regression/contracts/assigns_enforce_statics/main.c create mode 100644 regression/contracts/assigns_enforce_statics/test.desc diff --git a/regression/contracts/assigns_enforce_statics/main.c b/regression/contracts/assigns_enforce_statics/main.c new file mode 100644 index 00000000000..92f6f44afab --- /dev/null +++ b/regression/contracts/assigns_enforce_statics/main.c @@ -0,0 +1,19 @@ +#include +#include + +static int x; + +void foo() __CPROVER_assigns(x) +{ + int *y = &x; + + static int x; + x++; + + (*y)++; +} + +int main() +{ + foo(); +} diff --git a/regression/contracts/assigns_enforce_statics/test.desc b/regression/contracts/assigns_enforce_statics/test.desc new file mode 100644 index 00000000000..269b088542b --- /dev/null +++ b/regression/contracts/assigns_enforce_statics/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-contract foo _ --pointer-primitive-check +^EXIT=0$ +^SIGNAL=0$ +^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ +^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether static local and global variables are correctly tracked +in assigns clause verification. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 02bf8d824ad..bb7bf1d8c45 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -628,39 +628,17 @@ goto_functionst &code_contractst::get_goto_functions() } void code_contractst::instrument_assign_statement( - goto_programt::instructionst::iterator &instruction_iterator, + goto_programt::instructionst::iterator &instruction_it, goto_programt &program, assigns_clauset &assigns_clause) { INVARIANT( - instruction_iterator->is_assign(), + instruction_it->is_assign(), "The first instruction of instrument_assign_statement should always be" " an assignment"); - const exprt &lhs = instruction_iterator->assign_lhs(); - - // Local static variables are not declared locally, therefore, they are not - // included in the local write set during declaration. We check here whether - // lhs of the assignment is a local static variable and, if it is indeed - // true, we add lhs to our local write set before checking the assignment. - if(lhs.id() == ID_symbol) - { - auto lhs_sym = ns.lookup(lhs.get(ID_identifier)); - if( - lhs_sym.is_static_lifetime && - lhs_sym.location.get_function() == - instruction_iterator->source_location.get_function()) - { - // TODO: Fix this. - // The CAR snapshot should be made only once at the beginning. - const auto car = assigns_clause.add_to_write_set(lhs); - auto snapshot_instructions = car->generate_snapshot_instructions(); - insert_before_swap_and_advance( - program, instruction_iterator, snapshot_instructions); - } - } - - add_containment_check(program, assigns_clause, instruction_iterator, lhs); + add_containment_check( + program, assigns_clause, instruction_it, instruction_it->assign_lhs()); } void code_contractst::instrument_call_statement( @@ -798,11 +776,16 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) function, symbol_table); - // Adds formal parameters to freely assignable set - for(auto ¶meter : to_code_type(target.type).parameters()) + // Adds formal parameters to write set + for(const auto ¶m : to_code_type(target.type).parameters()) + assigns.add_to_write_set(ns.lookup(param.get_identifier()).symbol_expr()); + + // Adds local static declarations to write set + for(const auto &sym_pair : symbol_table) { - assigns.add_to_write_set( - ns.lookup(parameter.get_identifier()).symbol_expr()); + const auto &sym = sym_pair.second; + if(sym.is_static_lifetime && sym.location.get_function() == function) + assigns.add_to_write_set(sym.symbol_expr()); } auto instruction_it = function_obj->second.body.instructions.begin();