From 0bb699369a107621739caf566e3c5e07e3772fca Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Mon, 18 Apr 2022 09:37:29 -0400 Subject: [PATCH] CONTRACTS: Support slice expressions in assigns clauses. Introduces __CPROVER_object_from and __CPROVER_object_slice target expression in assigns clauses. Both get compiled to __CPROVER_havoc_slice for contract replacement. --- doc/cprover-manual/contracts-assigns.md | 24 +++++ .../assigns-slice-targets/main-enforce.c | 53 ++++++++++ .../assigns-slice-targets/main-replace.c | 96 +++++++++++++++++++ .../assigns-slice-targets/test-enforce.desc | 32 +++++++ .../assigns-slice-targets/test-replace.desc | 34 +++++++ .../assigns_enforce_address_of/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../assigns_enforce_function_calls/test.desc | 3 +- .../assigns_enforce_literal/test.desc | 2 +- .../assigns_enforce_side_effects_1/test.desc | 2 +- .../assigns_enforce_side_effects_2/test.desc | 3 +- .../assigns_enforce_side_effects_3/test.desc | 3 +- .../test.desc | 2 +- src/ansi-c/c_typecheck_code.cpp | 82 +++++++++++----- src/ansi-c/cprover_builtin_headers.h | 4 + .../havoc_assigns_clause_targets.cpp | 22 ++++- .../contracts/havoc_assigns_clause_targets.h | 10 ++ .../contracts/instrument_spec_assigns.cpp | 65 ++++++++++--- .../contracts/instrument_spec_assigns.h | 17 +++- src/goto-instrument/contracts/utils.h | 9 ++ 21 files changed, 419 insertions(+), 50 deletions(-) create mode 100644 regression/contracts/assigns-slice-targets/main-enforce.c create mode 100644 regression/contracts/assigns-slice-targets/main-replace.c create mode 100644 regression/contracts/assigns-slice-targets/test-enforce.desc create mode 100644 regression/contracts/assigns-slice-targets/test-replace.desc diff --git a/doc/cprover-manual/contracts-assigns.md b/doc/cprover-manual/contracts-assigns.md index 2b820731643..de8930f269a 100644 --- a/doc/cprover-manual/contracts-assigns.md +++ b/doc/cprover-manual/contracts-assigns.md @@ -13,6 +13,30 @@ design is based on the former. This means that memory not captured by an _assigns_ clause must not be written within the given function, even if the value(s) therein are not modified. +### Object slice expressions + +The following functions can be used in assigns clause to specify ranges of +assignable addresses. + +Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_from(ptr)` +specifies that all bytes starting from the given pointer and until the end of +the object are assignable: +```c +__CPROVER_size_t __CPROVER_object_from(void *ptr); +``` + +Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_from(ptr, size)` +specifies that `size` bytes starting from the given pointer and until the end of the object are assignable. +The `size` value must such that `size <= __CPROVER_object_size(ptr) - __CPROVER_pointer_offset(ptr)` holds: + +```c +__CPROVER_size_t __CPROVER_object_slice(void *ptr, __CPROVER_size_t size); +``` + +Caveats and limitations: The slices in question must *not* +be interpreted as pointers by the program. During call-by-contract replacement, +`__CPROVER_havoc_slice(ptr, size)` is used to havoc these targets, +and `__CPROVER_havoc_slice` does not support havocing pointers. ### Parameters An _assigns_ clause currently supports simple variable types and their pointers, diff --git a/regression/contracts/assigns-slice-targets/main-enforce.c b/regression/contracts/assigns-slice-targets/main-enforce.c new file mode 100644 index 00000000000..7f39d6f06cd --- /dev/null +++ b/regression/contracts/assigns-slice-targets/main-enforce.c @@ -0,0 +1,53 @@ +struct st +{ + int a; + char arr1[10]; + int b; + char arr2[10]; + int c; +}; + +void foo(struct st *s) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s))) + __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5)) + __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5)) +// clang-format on +{ + // PASS + s->arr1[0] = 0; + s->arr1[1] = 0; + s->arr1[2] = 0; + s->arr1[3] = 0; + s->arr1[4] = 0; + + // FAIL + s->arr1[5] = 0; + s->arr1[6] = 0; + s->arr1[7] = 0; + s->arr1[8] = 0; + s->arr1[9] = 0; + + // FAIL + s->arr2[0] = 0; + s->arr2[1] = 0; + s->arr2[2] = 0; + s->arr2[3] = 0; + s->arr2[4] = 0; + + // PASS + s->arr2[5] = 0; + s->arr2[6] = 0; + s->arr2[7] = 0; + s->arr2[8] = 0; + s->arr2[9] = 0; +} + +int main() +{ + struct st s; + + foo(&s); + + return 0; +} diff --git a/regression/contracts/assigns-slice-targets/main-replace.c b/regression/contracts/assigns-slice-targets/main-replace.c new file mode 100644 index 00000000000..5f21100ee7c --- /dev/null +++ b/regression/contracts/assigns-slice-targets/main-replace.c @@ -0,0 +1,96 @@ +struct st +{ + int a; + char arr1[10]; + int b; + char arr2[10]; + int c; +}; + +void foo(struct st *s) + // clang-format off + __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s))) + __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5)) + __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5)) +// clang-format on +{ + s->arr1[0] = 0; + s->arr1[1] = 0; + s->arr1[2] = 0; + s->arr1[3] = 0; + s->arr1[4] = 0; + + s->arr2[5] = 0; + s->arr2[6] = 0; + s->arr2[7] = 0; + s->arr2[8] = 0; + s->arr2[9] = 0; +} + +int main() +{ + struct st s; + s.a = 0; + s.arr1[0] = 0; + s.arr1[1] = 0; + s.arr1[2] = 0; + s.arr1[3] = 0; + s.arr1[4] = 0; + s.arr1[5] = 0; + s.arr1[6] = 0; + s.arr1[7] = 0; + s.arr1[8] = 0; + s.arr1[9] = 0; + + s.arr2[0] = 0; + s.arr2[1] = 0; + s.arr2[2] = 0; + s.arr2[3] = 0; + s.arr2[4] = 0; + s.arr2[5] = 0; + s.arr2[6] = 0; + s.arr2[7] = 0; + s.arr2[8] = 0; + s.arr2[9] = 0; + s.c = 0; + + foo(&s); + + // PASS + assert(s.a == 0); + + // FAIL + assert(s.arr1[0] == 0); + assert(s.arr1[1] == 0); + assert(s.arr1[2] == 0); + assert(s.arr1[3] == 0); + assert(s.arr1[4] == 0); + + // PASS + assert(s.arr1[5] == 0); + assert(s.arr1[6] == 0); + assert(s.arr1[7] == 0); + assert(s.arr1[8] == 0); + assert(s.arr1[9] == 0); + + // PASS + assert(s.b == 0); + + // PASS + assert(s.arr2[0] == 0); + assert(s.arr2[1] == 0); + assert(s.arr2[2] == 0); + assert(s.arr2[3] == 0); + assert(s.arr2[4] == 0); + + // FAIL + assert(s.arr2[5] == 0); + assert(s.arr2[6] == 0); + assert(s.arr2[7] == 0); + assert(s.arr2[8] == 0); + assert(s.arr2[9] == 0); + + // PASS + assert(s.c == 0); + return 0; +} diff --git a/regression/contracts/assigns-slice-targets/test-enforce.desc b/regression/contracts/assigns-slice-targets/test-enforce.desc new file mode 100644 index 00000000000..5b8f4fe5f58 --- /dev/null +++ b/regression/contracts/assigns-slice-targets/test-enforce.desc @@ -0,0 +1,32 @@ +CORE +main-enforce.c +--enforce-contract foo +^\[foo.assigns.\d+\].* Check that __CPROVER_object_slice\(\(void \*\)s->arr1, \(.*\)5\) is valid: SUCCESS$ +^\[foo.assigns.\d+\].* Check that __CPROVER_object_from\(\(void \*\)\(s->arr2 \+ \(.*\)5\)\) is valid: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)3\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)4\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)5\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)6\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)7\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)8\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)9\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)1\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)2\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)3\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)4\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)5\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)6\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that assigns clause checking of slice expressions works as expected when +enforcing a contract. diff --git a/regression/contracts/assigns-slice-targets/test-replace.desc b/regression/contracts/assigns-slice-targets/test-replace.desc new file mode 100644 index 00000000000..1f23fb0ae7e --- /dev/null +++ b/regression/contracts/assigns-slice-targets/test-replace.desc @@ -0,0 +1,34 @@ +CORE +main-replace.c +--replace-call-with-contract foo +^\[main.assertion.\d+\].*assertion s.a == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)0\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)1\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)2\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)3\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)4\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)5\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)6\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)7\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)8\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)9\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion s.b == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)0\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)1\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)2\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)3\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)4\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)5\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)6\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)7\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)8\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)9\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion s.c == 0: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Checks that havocking of slice expressions works as expected when +replacing a call by a contract. We manually express frame conditions as +assertions in the main function. diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc index 7ddb24bb269..7500be4b1e4 100644 --- a/regression/contracts/assigns_enforce_address_of/test.desc +++ b/regression/contracts/assigns_enforce_address_of/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$ +^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc index 4f48ab39f7d..2a9141844c9 100644 --- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc +++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$ +^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc index 4f48ab39f7d..2a9141844c9 100644 --- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$ +^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc index dae80dd0935..5f482125c08 100644 --- a/regression/contracts/assigns_enforce_function_calls/test.desc +++ b/regression/contracts/assigns_enforce_function_calls/test.desc @@ -3,8 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$ -^.*error: side-effects not allowed in assigns clause targets$ +^.*error: function calls in assigns clause targets must be to __CPROVER_object_from, __CPROVER_object_slice$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc index 96b830b76af..74d1d576235 100644 --- a/regression/contracts/assigns_enforce_literal/test.desc +++ b/regression/contracts/assigns_enforce_literal/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$ +^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_1/test.desc b/regression/contracts/assigns_enforce_side_effects_1/test.desc index 5b0fe231fe9..02be4389035 100644 --- a/regression/contracts/assigns_enforce_side_effects_1/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_1/test.desc @@ -2,7 +2,7 @@ CORE main.c --enforce-contract foo activate-multi-line-match -.*error: (dereferencing void pointer|void-typed expressions not allowed as assigns clause targets\n.*\n.*error: side-effects not allowed in assigns clause targets\n.*\n.*error: ternary expressions not allowed in assigns clause targets\n) +.*error: (dereferencing void pointer|void-typed expressions not allowed as assigns clause targets) ^CONVERSION ERROR$ ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc index 6894b4933b5..8cab6884f92 100644 --- a/regression/contracts/assigns_enforce_side_effects_2/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_2/test.desc @@ -3,8 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$ -^.*error: side-effects not allowed in assigns clause targets$ +^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ ^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 6894b4933b5..8cab6884f92 100644 --- a/regression/contracts/assigns_enforce_side_effects_3/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_3/test.desc @@ -3,8 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$ -^.*error: side-effects not allowed in assigns clause targets$ +^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc index 3d83d1cf5e7..51c84807dcb 100644 --- a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc +++ b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc @@ -4,6 +4,6 @@ main.c ^EXIT=(1|64)$ ^SIGNAL=0$ ^CONVERSION ERROR$ -^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$ +^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$ -- Checks whether type checking rejects literal constants in assigns clause. diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index dc42dacfe7b..ff0d9666057 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -909,44 +909,80 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) typecheck_expr(target); // fatal errors - bool must_throw = false; if(target.type().id() == ID_empty) { - must_throw = true; error().source_location = target.source_location(); error() << "void-typed expressions not allowed as assigns clause targets" << eom; + throw 0; } - if(!target.get_bool(ID_C_lvalue) && target.id() != ID_pointer_object) + // throws exception if expr contains side effect or ternary expr + auto throw_on_side_effects = [&](const exprt &expr) { + if(has_subexpr(expr, ID_side_effect)) + { + error().source_location = expr.source_location(); + error() << "side-effects not allowed in assigns clause targets" + << messaget::eom; + throw 0; + } + if(has_subexpr(expr, ID_if)) + { + error().source_location = expr.source_location(); + error() << "ternary expressions not allowed in assigns " + "clause targets" + << messaget::eom; + throw 0; + } + }; + + if(target.get_bool(ID_C_lvalue)) { - must_throw = true; - error().source_location = target.source_location(); - error() << "assigns clause target must be an lvalue or " CPROVER_PREFIX - "POINTER_OBJECT expression" - << eom; + throw_on_side_effects(target); } - - // Remark: an expression can be an lvalue and still contain side effects - // or ternary expressions. We detect them in a second step. - if(has_subexpr(target, ID_side_effect)) + else if(target.id() == ID_pointer_object) { - must_throw = true; - error().source_location = target.source_location(); - error() << "side-effects not allowed in assigns clause targets" << eom; + throw_on_side_effects(target); } - - if(has_subexpr(target, ID_if)) + else if(can_cast_expr(target)) + { + const auto &funcall = to_side_effect_expr_function_call(target); + if(can_cast_expr(funcall.function())) + { + const auto &ident = to_symbol_expr(funcall.function()).get_identifier(); + if( + ident == CPROVER_PREFIX "object_from" || ident == CPROVER_PREFIX + "object_slice") + { + for(const auto &argument : funcall.arguments()) + throw_on_side_effects(argument); + } + else + { + error().source_location = target.source_location(); + error() << "function calls in assigns clause targets must be " + "to " CPROVER_PREFIX "object_from, " CPROVER_PREFIX + "object_slice" + << eom; + throw 0; + } + } + else + { + error().source_location = target.source_location(); + error() << "function pointer calls not allowed in assigns targets" << eom; + throw 0; + } + } + else { - must_throw = true; error().source_location = target.source_location(); - error() << "ternary expressions not allowed in assigns " - "clause targets" + error() << "assigns clause target must be an lvalue or a " CPROVER_PREFIX + "POINTER_OBJECT, " CPROVER_PREFIX "object_from, " CPROVER_PREFIX + "object_slice expression" << eom; - } - - if(must_throw) throw 0; + } } void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 51de0f7bbfb..ceec83d14d3 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -122,4 +122,8 @@ __CPROVER_bool __CPROVER_overflow_unary_minus(); // enumerations __CPROVER_bool __CPROVER_enum_is_in_range(); + +// contracts +__CPROVER_size_t __CPROVER_object_from(void *); +__CPROVER_size_t __CPROVER_object_slice(void *, __CPROVER_size_t); // clang-format on diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp index 57e86a4ec28..b387f7a3552 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp @@ -79,7 +79,7 @@ void havoc_assigns_clause_targetst::havoc_if_valid( dest.add(goto_programt::make_goto( skip_target, not_exprt{car.valid_var()}, source_location_no_checks)); - if(car.target().id() == ID_pointer_object) + if(car.havoc_method == car_havoc_methodt::HAVOC_OBJECT) { // OTHER __CPROVER_havoc_object(target_snapshot_var) codet code(ID_havoc_object, {car.lower_bound_var()}); @@ -87,8 +87,22 @@ void havoc_assigns_clause_targetst::havoc_if_valid( dest.add(goto_programt::make_other(code, source_location)); inst->source_location_nonconst().set_comment(tracking_comment); } - else + else if(car.havoc_method == car_havoc_methodt::HAVOC_SLICE) + { + // This is a slice target. We use goto convert's do_havoc_slice() + // code generation, provided by cleanert. + cleanert cleaner(st, log.get_message_handler()); + const auto &mode = st.lookup_ref(function_id).mode; + const auto &funcall = to_side_effect_expr_function_call(car.target()); + const auto &function = to_symbol_expr(funcall.function()); + exprt::operandst arguments; + arguments.push_back(car.lower_bound_var()); + arguments.push_back(car.target_size()); + cleaner.do_havoc_slice(function, arguments, dest, mode); + } + else if(car.havoc_method == car_havoc_methodt::NONDET_ASSIGN) { + // a target where the size is derived from the type of the target // ASSIGN *(target.type() *)__car_lb = nondet(car.target().type()) const auto &target_type = car.target().type(); side_effect_expr_nondett nondet(target_type, source_location); @@ -99,6 +113,10 @@ void havoc_assigns_clause_targetst::havoc_if_valid( source_location)); inst->source_location_nonconst().set_comment(tracking_comment); } + else + { + UNREACHABLE; + } dest.destructive_append(skip_program); diff --git a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h index 55dc76c568a..d41f11d3735 100644 --- a/src/goto-instrument/contracts/havoc_assigns_clause_targets.h +++ b/src/goto-instrument/contracts/havoc_assigns_clause_targets.h @@ -86,6 +86,16 @@ class havoc_assigns_clause_targetst : public instrument_spec_assignst /// DEAD __car_ub /// ``` /// + /// Generates these instructions for an object slice target: + /// ``` + /// IF !__car_writable GOTO skip_target + /// __CPROVER_havoc_slize(__car_lb, car.target_size) + /// skip_target: SKIP + /// DEAD __car_writable + /// DEAD __car_lb + /// DEAD __car_ub + /// ``` + /// /// And generate these instructions otherwise: /// /// ``` diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 7264dbd7998..8a9ac63f8be 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -478,10 +478,51 @@ car_exprt instrument_spec_assignst::create_car_expr( minus_exprt( typecast_exprt::conditional_cast(arg, pointer_type(char_type())), pointer_offset(arg)), - typecast_exprt::conditional_cast(object_size(arg), signed_size_type()), + typecast_exprt::conditional_cast(object_size(arg), size_type()), valid_var, lower_bound_var, - upper_bound_var}; + upper_bound_var, + car_havoc_methodt::HAVOC_OBJECT}; + } + else if(can_cast_expr(target)) + { + const auto &funcall = to_side_effect_expr_function_call(target); + if(can_cast_expr(funcall.function())) + { + const auto &ident = to_symbol_expr(funcall.function()).get_identifier(); + if(ident == CPROVER_PREFIX "object_from") + { + const auto &ptr = funcall.arguments().at(0); + return { + condition, + target, + typecast_exprt::conditional_cast(ptr, pointer_type(char_type())), + typecast_exprt::conditional_cast( + minus_exprt{ + typecast_exprt::conditional_cast( + object_size(ptr), signed_size_type()), + pointer_offset(ptr)}, + size_type()), + valid_var, + lower_bound_var, + upper_bound_var, + car_havoc_methodt::HAVOC_SLICE}; + } + if(ident == CPROVER_PREFIX "object_slice") + { + const auto &ptr = funcall.arguments().at(0); + const auto &size = funcall.arguments().at(1); + return { + condition, + target, + typecast_exprt::conditional_cast(ptr, pointer_type(char_type())), + typecast_exprt::conditional_cast(size, size_type()), + valid_var, + lower_bound_var, + upper_bound_var, + car_havoc_methodt::HAVOC_SLICE}; + } + } } else if(is_assignable(target)) { @@ -491,15 +532,17 @@ car_exprt instrument_spec_assignst::create_car_expr( size.has_value(), "no definite size for lvalue target:\n" + target.pretty()); - return {condition, - target, - typecast_exprt::conditional_cast( - address_of_exprt{target}, pointer_type(char_type())), - typecast_exprt::conditional_cast(size.value(), signed_size_type()), - valid_var, - lower_bound_var, - upper_bound_var}; - }; + return { + condition, + target, + typecast_exprt::conditional_cast( + address_of_exprt{target}, pointer_type(char_type())), + typecast_exprt::conditional_cast(size.value(), size_type()), + valid_var, + lower_bound_var, + upper_bound_var, + car_havoc_methodt::NONDET_ASSIGN}; + } UNREACHABLE; } diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.h b/src/goto-instrument/contracts/instrument_spec_assigns.h index f5db34c9ab4..1c8ce50e298 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.h +++ b/src/goto-instrument/contracts/instrument_spec_assigns.h @@ -57,6 +57,14 @@ class conditional_target_exprt : public exprt } }; +/// method to use to havoc a target +enum class car_havoc_methodt +{ + HAVOC_OBJECT, + HAVOC_SLICE, + NONDET_ASSIGN +}; + /// Class that represents a normalized conditional address range, with: /// - condition expression /// - target expression @@ -73,7 +81,8 @@ class car_exprt : public exprt const exprt &_target_size, const symbol_exprt &_validity_var, const symbol_exprt &_lower_bound_var, - const symbol_exprt &_upper_bound_var) + const symbol_exprt &_upper_bound_var, + const car_havoc_methodt _havoc_method) : exprt( irep_idt{}, typet{}, @@ -83,11 +92,15 @@ class car_exprt : public exprt _target_size, _validity_var, _lower_bound_var, - _upper_bound_var}) + _upper_bound_var}), + havoc_method(_havoc_method) { add_source_location() = _target.source_location(); } + /// Method to use to havod the target + const car_havoc_methodt havoc_method; + /// Condition expression. When this condition holds the target is allowed const exprt &condition() const { diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 9487ddb9475..2ae1592a490 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -219,6 +219,15 @@ class cleanert : public goto_convertt { goto_convertt::clean_expr(guard, dest, mode, true); } + + void do_havoc_slice( + const symbol_exprt &function, + const exprt::operandst &arguments, + goto_programt &dest, + const irep_idt &mode) + { + goto_convertt::do_havoc_slice(nil_exprt{}, function, arguments, dest, mode); + } }; /// Returns an \ref irep_idt that essentially says that