diff --git a/regression/contracts/assigns-enforce-malloc-zero/main.c b/regression/contracts/assigns-enforce-malloc-zero/main.c index d84d5657718..9592997ddd5 100644 --- a/regression/contracts/assigns-enforce-malloc-zero/main.c +++ b/regression/contracts/assigns-enforce-malloc-zero/main.c @@ -6,7 +6,7 @@ int foo(char *a, int size) // clang-format off __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size) __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size)) - __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a)) + __CPROVER_assigns(a: __CPROVER_POINTER_OBJECT(a)) __CPROVER_ensures( a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0) // clang-format on diff --git a/regression/contracts/assigns_enforce_free_dead/main.c b/regression/contracts/assigns_enforce_free_dead/main.c index d62c5553ab1..1bf61b45efd 100644 --- a/regression/contracts/assigns_enforce_free_dead/main.c +++ b/regression/contracts/assigns_enforce_free_dead/main.c @@ -1,7 +1,7 @@ #include #include -int foo(int *x, int **p) __CPROVER_assigns(*x, *p, **p) +int foo(int *x, int **p) __CPROVER_assigns(*x; p : *p; p && *p : **p) { if(p && *p) **p = 0; @@ -44,12 +44,12 @@ int foo(int *x, int **p) __CPROVER_assigns(*x, *p, **p) // q goes DEAD here, unconditionally } - free(z); + free(z); // should not fail because free(NULL) is allowed in C z = malloc(sizeof(int)); if(nondet_bool()) { - free(z); + free(z); // should not fail because free(NULL) is allowed in C // here z is deallocated, conditionally } diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc index b4cee3c92a3..9c6a1f0066c 100644 --- a/regression/contracts/assigns_enforce_free_dead/test.desc +++ b/regression/contracts/assigns_enforce_free_dead/test.desc @@ -1,8 +1,8 @@ CORE main.c --enforce-contract foo _ --malloc-may-fail --malloc-fail-null --pointer-primitive-check -^\[foo.\d+\] line \d+ Check that \*\(\*p\) is assignable: SUCCESS$ -^\[foo.\d+\] line \d+ Check that \*\(\*p\) is assignable: FAILURE$ +^\[foo.\d+\] line 7 Check that \*\(\*p\) is assignable: SUCCESS$ +^\[foo.\d+\] line 24 Check that \*\(\*p\) is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that \*p is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*q is assignable: SUCCESS$ ^\[foo.\d+\] line \d+ Check that \*w is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_offsets_2/test.desc b/regression/contracts/assigns_enforce_offsets_2/test.desc index 6fe2141f856..9edeb40efd6 100644 --- a/regression/contracts/assigns_enforce_offsets_2/test.desc +++ b/regression/contracts/assigns_enforce_offsets_2/test.desc @@ -1,10 +1,15 @@ -KNOWNBUG +CORE main.c ---enforce-contract foo +--enforce-contract foo _ --pointer-check +^\[.*\d+\].* line 5 Check assigns target validity 'TRUE: \*x': SUCCESS$ +^\[.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$ +^\[.*\d+\].* line 8 Check assigns target validity 'TRUE: x\[\(.*\)1\]': FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- -- -Check that a write at *x fails when the assigns clause specifies *(x + 1) and -the actual underlying object is of size 1. +Check that a write at *x+1 fails when the assigns clause specifies a valid *x +and the actual underlying object is of size 1. +In this case the specified target is valid, the lhs of the assignment is invalid +so the inclusion check passes, but the pointer check must fail with an OOB. diff --git a/regression/contracts/assigns_enforce_offsets_4/main.c b/regression/contracts/assigns_enforce_offsets_4/main.c index ef3ed29417e..e55c9b4895a 100644 --- a/regression/contracts/assigns_enforce_offsets_4/main.c +++ b/regression/contracts/assigns_enforce_offsets_4/main.c @@ -13,8 +13,8 @@ int main() { int *x = malloc(2 * sizeof(int)); *x = 0; - *(x + 1) == 0 - // write should fail because x points to a size 2 object and the contracts expects size 10 at least. - foo(x); + *(x + 1) == 0; + // write should fail because x points to a size 2 object and the contracts expects size 10 at least. + foo(x); return 0; } diff --git a/regression/contracts/assigns_enforce_offsets_4/test.desc b/regression/contracts/assigns_enforce_offsets_4/test.desc index b37ae494ea4..c7795c03c7c 100644 --- a/regression/contracts/assigns_enforce_offsets_4/test.desc +++ b/regression/contracts/assigns_enforce_offsets_4/test.desc @@ -1,9 +1,13 @@ -KNOWNBUG +CORE main.c ---enforce-contract foo +--enforce-contract foo _ --pointer-check +^\[.*\d+\].* line 8 Check assigns target validity 'TRUE: x\[\(.*\)10\]': FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- -- -Check that a write at *x fails when the assigns clause specifies *(x + 1) and the actual underlying object is of size 1. +Check that a write at *(x+10) fails when the assigns clause specifies *(x + 10) +and the actual underlying object is too small. +In that case the target inclusion succeeds because the LHS is in an invalid +state, but the target validity check must fail. diff --git a/regression/contracts/assigns_enforce_structs_07/test.desc b/regression/contracts/assigns_enforce_structs_07/test.desc index 21a9569c860..7a0d41839e0 100644 --- a/regression/contracts/assigns_enforce_structs_07/test.desc +++ b/regression/contracts/assigns_enforce_structs_07/test.desc @@ -3,13 +3,14 @@ main.c --enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check ^EXIT=10$ ^SIGNAL=0$ -^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in p->buf\[\(.*\)0\]: FAILURE$ -^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$ -^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in pp->p->buf\[\(.*\)0\]: FAILURE$ +^\[f1.*\d+\].*line 18 Check assigns target validity 'TRUE: p->buf\[\(.*\)0\]': FAILURE$ +^\[f2.*\d+\].*line 23 Check assigns target validity 'TRUE: pp->p->buf\[\(.*\)0\]': FAILURE$ ^VERIFICATION FAILED$ -- -- -Checks whether CBMC properly evaluates write set of members -from invalid objects. In this case, they are not writable. +In f1, the assigns clause specifies `*(p->buf)` as target (which can be invalid) +and assigns `p->buf[0]` unconditionally. When both target and lhs are invalid, +its inclusion check can be trivially satisfied (or not) but we expect the target +validity check to fail. + +In f2 tests this behaviour with chained dereferences. diff --git a/regression/contracts/assigns_enforce_structs_08/main.c b/regression/contracts/assigns_enforce_structs_08/main.c new file mode 100644 index 00000000000..1ea4a832155 --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_08/main.c @@ -0,0 +1,48 @@ +#include +#include +#include + +struct pair +{ + uint8_t *buf; + size_t size; +}; + +struct pair_of_pairs +{ + struct pair *p; +}; + +void f1(struct pair *p) __CPROVER_assigns(p && p->buf : *(p->buf)) +{ + if(p && p->buf) + p->buf[0] = 0; +} + +void f2(struct pair_of_pairs *pp) + // clang-format off +__CPROVER_assigns(pp && pp->p && pp->p->buf: *(pp->p->buf)) +// clang-format on +{ + if(pp && pp->p && pp->p->buf) + pp->p->buf[0] = 0; +} + +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_enforce_structs_08/test.desc b/regression/contracts/assigns_enforce_structs_08/test.desc new file mode 100644 index 00000000000..0272e14736a --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_08/test.desc @@ -0,0 +1,21 @@ +CORE +main.c +--enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check +^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$ +^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in p->buf\[\(.*\)0\]: FAILURE$ +^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in pp->p->buf\[\(.*\)0\]: FAILURE$ +^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in pp->p->buf\[\(.*\)0\]: FAILURE$ +-- +In f1, the assigns clause specifies `*(p->buf)` as target (which can be invalid) +and assigns `p->buf[0]` unconditionally. When both target and lhs are invalid, +its inclusion check can be trivially satisfied or not but we expect in all +cases a null pointer failure and an invalid pointer error to occur +on the assignment. + +In f2 tests this behaviour with chained dereferences. diff --git a/regression/contracts/assigns_enforce_subfunction_calls/test.desc b/regression/contracts/assigns_enforce_subfunction_calls/test.desc index 9411d1e4536..f1668d7397c 100644 --- a/regression/contracts/assigns_enforce_subfunction_calls/test.desc +++ b/regression/contracts/assigns_enforce_subfunction_calls/test.desc @@ -4,15 +4,13 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^main.c function baz$ -^\[baz.1\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[baz.2\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[baz.3\] line \d+ Check that \*x is assignable: FAILURE$ -^\[baz.4\] line \d+ Check that \*x is assignable: FAILURE$ +^\[baz.\d+\] line 6 Check that \*x is assignable: SUCCESS$ +^\[baz.\d+\] line 6 Check that \*x is assignable: FAILURE$ ^main.c function foo$ -^\[foo.assertion.1\] line \d+ foo.x.set: SUCCESS$ -^\[foo.assertion.2\] line \d+ foo.local.set: SUCCESS$ -^\[foo.assertion.3\] line \d+ foo.y.set: SUCCESS$ -^\[foo.assertion.4\] line \d+ foo.z.set: SUCCESS$ +^\[foo.assertion.\d+\] line 20 foo.x.set: SUCCESS$ +^\[foo.assertion.\d+\] line 25 foo.local.set: SUCCESS$ +^\[foo.assertion.\d+\] line 29 foo.y.set: SUCCESS$ +^\[foo.assertion.\d+\] line 33 foo.z.set: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_replace_04/main.c b/regression/contracts/assigns_replace_04/main.c index 6ec35cf8d29..a462e9cdc84 100644 --- a/regression/contracts/assigns_replace_04/main.c +++ b/regression/contracts/assigns_replace_04/main.c @@ -1,6 +1,6 @@ #include -void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5) +void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 == 10) { *x2 = 10; } @@ -28,6 +28,7 @@ int main() } assert(p > 100); assert(q == 2); + __CPROVER_assert(0, "reachability test"); return 0; } diff --git a/regression/contracts/assigns_replace_04/test.desc b/regression/contracts/assigns_replace_04/test.desc index ca87d5918c6..b284bf324ef 100644 --- a/regression/contracts/assigns_replace_04/test.desc +++ b/regression/contracts/assigns_replace_04/test.desc @@ -1,9 +1,16 @@ CORE main.c --replace-call-with-contract f2 --replace-call-with-contract f3 -^EXIT=0$ +main.c function main +^\[.*\d+\] line 29 assertion p > 100: SUCCESS$ +^\[.*\d+\] line 30 assertion q == 2: SUCCESS$ +^\[.*\d+\] line 31 reachability test: FAILURE$ +^\*\* 1 of 3 failed +^VERIFICATION FAILED$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ -- -- -This test checks that verification succeeds when an assigns clause is combined with a function contract in a loop properly. +This test checks that replacing function calls with their contracts within a +loop, when the contracts impose contradictory post conditions at different loop +iterations on a same program variable, do not cause vacuity. diff --git a/regression/contracts/assigns_replace_05/main.c b/regression/contracts/assigns_replace_05/main.c index 42d98843653..500edd9b80b 100644 --- a/regression/contracts/assigns_replace_05/main.c +++ b/regression/contracts/assigns_replace_05/main.c @@ -1,8 +1,8 @@ #include -void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5) +void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 < 5) { - *x2 = 10; + *x2 = 1; } void f3(int *x3, int *y3) __CPROVER_ensures(*x3 > 100) @@ -26,8 +26,9 @@ int main() f3(&p, &q); } } - assert(p > 100); - assert(q == 2); + assert(p < 0); + assert(q == 32); + __CPROVER_assert(0, "reachability test"); return 0; } diff --git a/regression/contracts/assigns_replace_05/test.desc b/regression/contracts/assigns_replace_05/test.desc index 227ce756ce7..1e11b3be2dd 100644 --- a/regression/contracts/assigns_replace_05/test.desc +++ b/regression/contracts/assigns_replace_05/test.desc @@ -1,12 +1,16 @@ -KNOWNBUG +CORE main.c --replace-call-with-contract f2 --replace-call-with-contract f3 -^EXIT=10$ +main.c function main +^\[.*\d+\] line 29 assertion p < 0: SUCCESS$ +^\[.*\d+\] line 30 assertion q == 32: SUCCESS$ +^\[.*\d+\] line 31 reachability test: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ ^SIGNAL=0$ -^VERIFICATION FAILED$ -- -- -This test checks that verification fails when assigns clauses are combined with function contracts -in a loop improperly, i.e., always assumes memory not mention in ensures clauses are unchanged. - -BUG: Currently, function call replacement using 'ensures' specifications encodes an implicit assumption that any memory not mentioned in the ensures clause remains unchanged throughout the function, even when an 'assigns' clause is not present. +This test demonstrates that replacing a function call with a contract that has +an empty assigns clause and a post condition involving its input parameters can +causes vacuous proofs. Checking the contract against the function would fail +the assigns clause checks. *This is not a bug*. diff --git a/regression/contracts/loop_contracts_binary_search/test.desc b/regression/contracts/loop_contracts_binary_search/test.desc index d95106cc389..f727ec04174 100644 --- a/regression/contracts/loop_contracts_binary_search/test.desc +++ b/regression/contracts/loop_contracts_binary_search/test.desc @@ -6,9 +6,9 @@ main.c ^\[binary_search\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[binary_search\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[binary_search\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ -^\[binary_search\.2\] .* Check that lb is assignable: SUCCESS$ -^\[binary_search\.3\] .* Check that ub is assignable: SUCCESS$ -^\[binary_search\.4\] .* Check that mid is assignable: SUCCESS$ +^\[binary_search\.\d+\] .* Check that lb is assignable: SUCCESS$ +^\[binary_search\.\d+\] .* Check that ub is assignable: SUCCESS$ +^\[binary_search\.\d+\] .* Check that mid is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion buf\[idx\] == val: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/variant_init_inside_loop/test.desc b/regression/contracts/variant_init_inside_loop/test.desc index 877d1d22045..78465a6cf95 100644 --- a/regression/contracts/variant_init_inside_loop/test.desc +++ b/regression/contracts/variant_init_inside_loop/test.desc @@ -4,10 +4,10 @@ main.c ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ -^\[main\.2\] .* Check that i is assignable: SUCCESS$ -^\[main\.overflow\.1\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$ -^\[main\.overflow\.3\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$ -^\[main\.overflow\.2\] .* arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS$ +^\[main\.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$ +^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$ +^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index 4305d99bf01..c401bde4d29 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -25,6 +25,7 @@ Date: July 2021 #include #include #include +#include static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns) { @@ -126,14 +127,10 @@ assigns_clauset::conditional_address_ranget::conditional_address_ranget( } goto_programt -assigns_clauset::conditional_address_ranget::generate_snapshot_instructions() - const +assigns_clauset::conditional_address_ranget::generate_snapshot_instructions( + check_target_validityt check_target_validity) const { goto_programt instructions; - // adding pragmas to the location to selectively disable checks - // where it is sound to do so - source_locationt location_no_checks = location; - disable_pointer_checks(location_no_checks); // clean up side effects from the guard expression if needed cleanert cleaner(parent.symbol_table, parent.log.get_message_handler()); @@ -148,54 +145,67 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions() // we want checks on the guard because it is user code clean_guard.add_source_location() = location; - instructions.add( - goto_programt::make_decl(validity_condition_var, location_no_checks)); - instructions.add( - goto_programt::make_decl(lower_bound_address_var, location_no_checks)); - instructions.add( - goto_programt::make_decl(upper_bound_address_var, location_no_checks)); + // adding pragmas to the location to selectively disable checks + // where it is sound to do so + source_locationt location_no_checks(location); + disable_pointer_checks(location_no_checks); - instructions.add(goto_programt::make_assignment( - lower_bound_address_var, - null_pointer_exprt{to_pointer_type(guarded_slice.start_adress.type())}, - location_no_checks)); - instructions.add(goto_programt::make_assignment( - upper_bound_address_var, - null_pointer_exprt{to_pointer_type(guarded_slice.start_adress.type())}, - location_no_checks)); + // If requested, we check that when guard condition is true, + // the target's `start_address` pointer satisfies w_ok with the expected size + // (or is NULL if we allow it explicitly). + // This assertion will be falsified whenever `start_address` is invalid or + // not of the right size (or is NULL if we dot not allow it expliclitly). + auto validity_check_expr = + check_target_validity == check_target_validityt::YES_ALLOW_NULL + ? or_exprt{not_exprt{clean_guard}, + null_pointer(guarded_slice.start_adress), + w_ok_exprt{guarded_slice.start_adress, guarded_slice.size}} + : or_exprt{not_exprt{clean_guard}, + w_ok_exprt{guarded_slice.start_adress, guarded_slice.size}}; + + if(check_target_validity != check_target_validityt::NO) + { + auto target_validity_assert = + instructions.add(goto_programt::make_assertion( + simplify_expr(validity_check_expr, parent.ns), location_no_checks)); + + target_validity_assert->source_location_nonconst().set_comment( + "Check assigns target validity '" + + from_expr(parent.ns, "", guarded_slice.guard) + ": " + + from_expr(parent.ns, "", guarded_slice.expr) + "'"); + } - goto_programt skip_program; - const auto skip_target = - skip_program.add(goto_programt::make_skip(location_no_checks)); + // ~~~ From then on we implicitly assume that the assertion holds ~~~ // - const auto validity_check_expr = - and_exprt{clean_guard, - all_dereferences_are_valid(guarded_slice.expr, parent.ns), - w_ok_exprt{guarded_slice.start_adress, guarded_slice.size}}; + // We snapshot the validity condition, lower bound and upper bound addresses + instructions.add( + goto_programt::make_decl(validity_condition_var, location_no_checks)); instructions.add(goto_programt::make_assignment( - validity_condition_var, validity_check_expr, location_no_checks)); + validity_condition_var, + simplify_expr( + and_exprt{clean_guard, + not_exprt{null_pointer(guarded_slice.start_adress)}}, + parent.ns), + location_no_checks)); - instructions.add(goto_programt::make_goto( - skip_target, not_exprt{validity_condition_var}, location_no_checks)); + instructions.add( + goto_programt::make_decl(lower_bound_address_var, location_no_checks)); instructions.add(goto_programt::make_assignment( lower_bound_address_var, guarded_slice.start_adress, location_no_checks)); - // the computation of the CAR upper bound can overflow into the object ID bits - // of the pointer with very large allocation sizes. - // We enable pointer overflow checks to detect such cases. - source_locationt location_overflow_check = location; - location_overflow_check.add_pragma("enable:pointer-overflow-check"); + instructions.add( + goto_programt::make_decl(upper_bound_address_var, location_no_checks)); instructions.add(goto_programt::make_assignment( upper_bound_address_var, - plus_exprt{guarded_slice.start_adress, guarded_slice.size}, - location_overflow_check)); - instructions.destructive_append(skip_program); + simplify_expr( + plus_exprt{guarded_slice.start_adress, guarded_slice.size}, parent.ns), + location_no_checks)); - // The assignments above are only performed on locally defined temporaries - // and need not be checked for inclusion in the enclosing scope's write set. + // The snapshot assignments involve only instrumentation variables + // need not be checked against the surrounding assigns clause. add_pragma_disable_assigns_check(instructions); return instructions; } @@ -259,12 +269,18 @@ void assigns_clauset::remove_from_write_set(const exprt &target_expr) exprt assigns_clauset::generate_inclusion_check( const conditional_address_ranget &lhs, + check_target_validityt allow_null_target, optionalt &cfg_info_opt) const { if(write_set.empty()) - return not_exprt{lhs.validity_condition_var}; + { + if(allow_null_target == check_target_validityt::YES_ALLOW_NULL) + return false_exprt{}; + else + return null_pointer(lhs.guarded_slice.start_adress); + } - exprt::operandst conditions{not_exprt{lhs.validity_condition_var}}; + exprt::operandst conditions; if(cfg_info_opt.has_value()) { @@ -279,7 +295,12 @@ exprt assigns_clauset::generate_inclusion_check( conditions.push_back(target.generate_unsafe_inclusion_check(lhs)); } - return disjunction(conditions); + if(allow_null_target == check_target_validityt::YES_ALLOW_NULL) + return or_exprt{ + null_pointer(lhs.guarded_slice.start_adress), + and_exprt{lhs.validity_condition_var, disjunction(conditions)}}; + else + return and_exprt{lhs.validity_condition_var, disjunction(conditions)}; } void havoc_assigns_targetst::append_havoc_code_for_expr( diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h index 9e92136af1b..9dc0cc85367 100644 --- a/src/goto-instrument/contracts/assigns.h +++ b/src/goto-instrument/contracts/assigns.h @@ -47,13 +47,36 @@ typedef struct guarded_slicet class assigns_clauset { public: + enum class check_target_validityt + { + YES, + YES_ALLOW_NULL, + NO + }; + /// \brief A class for representing Conditional Address Ranges class conditional_address_ranget { public: conditional_address_ranget(const assigns_clauset &, const exprt &); - goto_programt generate_snapshot_instructions() const; + /// \brief Returns a program that computes a snapshot of the CAR. + /// + /// In addition, if check_target_validity is Yes, generates: + /// ``` + /// ASSERT + /// condition ==> w_ok(target_start_address, target_size) + /// ``` + // + /// else if check_target_validity is YesAlloNull, generates: + /// ``` + /// ASSERT + /// condition ==> + /// (target_start_address==NULL || + /// w_ok(target_start_address, target_size)) + /// ``` + goto_programt generate_snapshot_instructions( + check_target_validityt check_target_validity) const; bool operator==(const conditional_address_ranget &other) const { @@ -110,6 +133,7 @@ class assigns_clauset exprt generate_inclusion_check( const conditional_address_ranget &lhs, + check_target_validityt allow_null_target, optionalt &cfg_info_opt) const; const write_sett &get_write_set() const diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index b55aad00eda..1eb98ce57a4 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -304,7 +304,8 @@ void code_contractst::check_apply_loop_contracts( // This must be done before havocing the write set. for(const auto &car : loop_assigns.get_write_set()) { - auto snapshot_instructions = car.generate_snapshot_instructions(); + auto snapshot_instructions = car.generate_snapshot_instructions( + assigns_clauset::check_target_validityt::YES_ALLOW_NULL); insert_before_swap_and_advance( goto_function.body, loop_head, snapshot_instructions); }; @@ -956,6 +957,7 @@ void code_contractst::instrument_assign_statement( assigns_clause, instruction_it, instruction_it->assign_lhs(), + allow_null_lhst::NO, cfg_info_opt); } @@ -985,7 +987,9 @@ void code_contractst::instrument_call_statement( // 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(); + auto snapshot_instructions = car->generate_snapshot_instructions( + // no check because malloc always returns a null or valid pointer + assigns_clauset::check_target_validityt::NO); insert_before_swap_and_advance( body, instruction_it, snapshot_instructions); // since CAR was inserted *after* the malloc call, @@ -1003,6 +1007,8 @@ void code_contractst::instrument_call_statement( assigns, instruction_it, pointer_object(instruction_it->call_arguments().front()), + // NULL pointers are a allowed and a no-op with free + allow_null_lhst::YES, cfg_info_opt); // skip all invalidation business if we're freeing invalid memory @@ -1214,7 +1220,8 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) auto instruction_it = function_body.instructions.begin(); for(const auto &car : assigns.get_write_set()) { - auto snapshot_instructions = car.generate_snapshot_instructions(); + auto snapshot_instructions = car.generate_snapshot_instructions( + assigns_clauset::check_target_validityt::YES_ALLOW_NULL); insert_before_swap_and_advance( function_body, instruction_it, snapshot_instructions); }; @@ -1336,7 +1343,10 @@ void code_contractst::check_frame_conditions( // 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(); + // we do not need to check target validity because DECL + // are always backed by adequately sized objects + auto snapshot_instructions = car->generate_snapshot_instructions( + assigns_clauset::check_target_validityt::NO); insert_before_swap_and_advance( body, instruction_it, snapshot_instructions); // since CAR was inserted *after* the DECL instruction, @@ -1400,7 +1410,12 @@ void code_contractst::check_frame_conditions( const auto havoc_argument = pointer_object(instruction_it->get_other().operands().front()); add_inclusion_check( - body, assigns, instruction_it, havoc_argument, cfg_info_opt); + body, + assigns, + instruction_it, + havoc_argument, + allow_null_lhst::NO, + cfg_info_opt); } // Move to the next instruction @@ -1416,10 +1431,18 @@ code_contractst::add_inclusion_check( const assigns_clauset &assigns, goto_programt::targett &instruction_it, const exprt &lhs, + allow_null_lhst allow_null_lhs, optionalt &cfg_info_opt) { const assigns_clauset::conditional_address_ranget car{assigns, lhs}; - auto snapshot_instructions = car.generate_snapshot_instructions(); + + auto check_target_validity = + allow_null_lhs == allow_null_lhst::YES + ? assigns_clauset::check_target_validityt::YES_ALLOW_NULL + : assigns_clauset::check_target_validityt::YES; + + auto snapshot_instructions = + car.generate_snapshot_instructions(check_target_validity); insert_before_swap_and_advance( program, instruction_it, snapshot_instructions); @@ -1442,7 +1465,8 @@ code_contractst::add_inclusion_check( } assertion.add(goto_programt::make_assertion( - assigns.generate_inclusion_check(car, cfg_info_opt), location_no_checks)); + assigns.generate_inclusion_check(car, check_target_validity, cfg_info_opt), + location_no_checks)); insert_before_swap_and_advance(program, instruction_it, assertion); return car; diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index bc0313c9595..67f5c7b7f9b 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -157,6 +157,13 @@ class code_contractst skipt skip_parameter_assigns, optionalt &cfg_info_opt); + /// Allow or do not allow NULL targets in inclusion checks + enum class allow_null_lhst + { + YES, + NO + }; + /// Inserts an assertion into the goto program to ensure that /// an expression is within the assignable memory frame. const assigns_clauset::conditional_address_ranget add_inclusion_check( @@ -164,6 +171,7 @@ class code_contractst const assigns_clauset &assigns, goto_programt::targett &instruction_it, const exprt &lhs, + allow_null_lhst allow_null_lhs, optionalt &cfg_info_opt); /// Check if there are any malloc statements which may be repeated because of diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp index bca49d297ee..a5d02adf564 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp @@ -109,9 +109,12 @@ static void snapshot_if_valid( dest.add(goto_programt::make_decl(target_snapshot_var)); + const not_exprt not_null(null_pointer(target_pointer)); + const not_exprt not_invalid{is_invalid_pointer_exprt{target_pointer}}; + dest.add(goto_programt::make_assignment( target_valid_var, - and_exprt{condition, all_dereferences_are_valid(target_pointer, ns)}, + and_exprt{condition, not_null, not_invalid}, source_location_no_checks)); dest.add(goto_programt::make_assignment( diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 8757502b873..31902f60d25 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -161,6 +161,9 @@ void disable_pointer_checks(source_locationt &source_location) source_location.add_pragma("disable:pointer-check"); source_location.add_pragma("disable:pointer-primitive-check"); source_location.add_pragma("disable:pointer-overflow-check"); + source_location.add_pragma("disable:signed-overflow-check"); + source_location.add_pragma("disable:unsigned-overflow-check"); + source_location.add_pragma("disable:conversion-check"); } void simplify_gotos(goto_programt &goto_program, namespacet &ns)