From 39118f4b44c209eb3f4c5f7969204d31ac5cb79f Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 13 Sep 2022 10:42:41 -0400 Subject: [PATCH] CONTRACTS: support slice operators in loop assigns clauses Changes: - Drop support for __CPROVER_POINTER_OBJECT in assigns clauses in the front-end - Add methods to havoc __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, __CPROVER_object_upto in havoc_assigns_targett. - update tests - add new tests --- .../assigns_enforce_address_of/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../assigns_enforce_literal/test.desc | 2 +- .../assigns_enforce_side_effects_2/test.desc | 2 +- .../assigns_enforce_side_effects_3/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../assigns_enforce_address_of/test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 2 +- .../assigns_enforce_literal/test.desc | 2 +- .../assigns_enforce_side_effects_2/test.desc | 2 +- .../assigns_enforce_side_effects_3/test.desc | 2 +- .../test.desc | 2 +- .../invar_havoc_dynamic_array/main.c | 2 +- .../contracts/invar_havoc_static_array/main.c | 2 +- .../main.c | 2 +- regression/contracts/loop_assigns-01/main.c | 2 +- regression/contracts/loop_assigns-03/main.c | 2 +- regression/contracts/loop_assigns-04/main.c | 2 +- .../loop_assigns-slice-assignable-ptr/main.c | 42 +++++++++ .../test.desc | 22 +++++ .../main.c | 40 ++++++++ .../test.desc | 23 +++++ .../contracts/loop_assigns-slice-from/main.c | 37 ++++++++ .../loop_assigns-slice-from/test.desc | 19 ++++ .../loop_assigns-slice-upto-fail/main.c | 42 +++++++++ .../loop_assigns-slice-upto-fail/test.desc | 21 +++++ .../loop_assigns-slice-upto-pass/main.c | 38 ++++++++ .../loop_assigns-slice-upto-pass/test.desc | 18 ++++ .../contracts/quantifiers-loop-01/main.c | 2 +- .../contracts/quantifiers-loop-02/main.c | 2 +- .../contracts/quantifiers-loop-03/main.c | 2 +- .../test.desc | 2 +- src/ansi-c/c_typecheck_code.cpp | 10 +- src/goto-instrument/contracts/contracts.cpp | 3 +- src/goto-instrument/contracts/utils.cpp | 91 ++++++++++++++++++- src/goto-instrument/contracts/utils.h | 85 +++++++++++------ src/goto-instrument/havoc_utils.cpp | 4 +- src/goto-instrument/havoc_utils.h | 7 +- 41 files changed, 481 insertions(+), 71 deletions(-) create mode 100644 regression/contracts/loop_assigns-slice-assignable-ptr/main.c create mode 100644 regression/contracts/loop_assigns-slice-assignable-ptr/test.desc create mode 100644 regression/contracts/loop_assigns-slice-assignable-scalar/main.c create mode 100644 regression/contracts/loop_assigns-slice-assignable-scalar/test.desc create mode 100644 regression/contracts/loop_assigns-slice-from/main.c create mode 100644 regression/contracts/loop_assigns-slice-from/test.desc create mode 100644 regression/contracts/loop_assigns-slice-upto-fail/main.c create mode 100644 regression/contracts/loop_assigns-slice-upto-fail/test.desc create mode 100644 regression/contracts/loop_assigns-slice-upto-pass/main.c create mode 100644 regression/contracts/loop_assigns-slice-upto-pass/test.desc diff --git a/regression/contracts-dfcc/assigns_enforce_address_of/test.desc b/regression/contracts-dfcc/assigns_enforce_address_of/test.desc index 49df58734e7..0ad0d352516 100644 --- a/regression/contracts-dfcc/assigns_enforce_address_of/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_address_of/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target/test.desc index b9ee423738e..386c2c0b75d 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target_list/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target_list/test.desc index b9ee423738e..386c2c0b75d 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target_list/test.desc +++ b/regression/contracts-dfcc/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 a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_literal/test.desc b/regression/contracts-dfcc/assigns_enforce_literal/test.desc index 289616526e2..3aa3d380ae2 100644 --- a/regression/contracts-dfcc/assigns_enforce_literal/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_literal/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_side_effects_2/test.desc b/regression/contracts-dfcc/assigns_enforce_side_effects_2/test.desc index 88cdc250dca..aba4e1906e1 100644 --- a/regression/contracts-dfcc/assigns_enforce_side_effects_2/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_side_effects_2/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_side_effects_3/test.desc b/regression/contracts-dfcc/assigns_enforce_side_effects_3/test.desc index 88cdc250dca..aba4e1906e1 100644 --- a/regression/contracts-dfcc/assigns_enforce_side_effects_3/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_side_effects_3/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts-dfcc/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts-dfcc/assigns_type_checking_invalid_case_01/test.desc index 853af05bb8d..56da0f5bfaa 100644 --- a/regression/contracts-dfcc/assigns_type_checking_invalid_case_01/test.desc +++ b/regression/contracts-dfcc/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 a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ -- Checks whether type checking rejects literal constants in assigns clause. diff --git a/regression/contracts-dfcc/reject_history_expr_in_assigns_clause/test.desc b/regression/contracts-dfcc/reject_history_expr_in_assigns_clause/test.desc index 2788121bb93..f215cd94255 100644 --- a/regression/contracts-dfcc/reject_history_expr_in_assigns_clause/test.desc +++ b/regression/contracts-dfcc/reject_history_expr_in_assigns_clause/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^main.c.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^CONVERSION ERROR$ ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc index 5bb4428f231..5295d870506 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 a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^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 b9ee423738e..386c2c0b75d 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 a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^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 b9ee423738e..386c2c0b75d 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 a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc index 78c33a0aa62..0e84a9b8555 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 a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^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 6449125a7fd..ae70fd05475 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 target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^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 6449125a7fd..ae70fd05475 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 target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^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 92a3ee83d44..95a72acfebc 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 a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ -- Checks whether type checking rejects literal constants in assigns clause. diff --git a/regression/contracts/invar_havoc_dynamic_array/main.c b/regression/contracts/invar_havoc_dynamic_array/main.c index e69388b3673..0aed03906df 100644 --- a/regression/contracts/invar_havoc_dynamic_array/main.c +++ b/regression/contracts/invar_havoc_dynamic_array/main.c @@ -10,7 +10,7 @@ void main() for(unsigned i = 0; i < SIZE; i++) // clang-format off - __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data)) + __CPROVER_assigns(i, __CPROVER_object_whole(data)) __CPROVER_loop_invariant(i <= SIZE) // clang-format on { diff --git a/regression/contracts/invar_havoc_static_array/main.c b/regression/contracts/invar_havoc_static_array/main.c index 8d4be0cc55a..a1b3762bfc2 100644 --- a/regression/contracts/invar_havoc_static_array/main.c +++ b/regression/contracts/invar_havoc_static_array/main.c @@ -10,7 +10,7 @@ void main() for(unsigned i = 0; i < SIZE; i++) // clang-format off - __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data)) + __CPROVER_assigns(i, __CPROVER_object_whole(data)) __CPROVER_loop_invariant(i <= SIZE) // clang-format on { diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c index ad95ac3048e..004d3c22ecc 100644 --- a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c +++ b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c @@ -11,7 +11,7 @@ void main() data[4][5][6] = 0; for(unsigned i = 0; i < SIZE; i++) - __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data)) + __CPROVER_assigns(i, __CPROVER_object_whole(data)) __CPROVER_loop_invariant(i <= SIZE) { data[4][i][6] = 1; diff --git a/regression/contracts/loop_assigns-01/main.c b/regression/contracts/loop_assigns-01/main.c index 896e34dace1..d9dab3a0e06 100644 --- a/regression/contracts/loop_assigns-01/main.c +++ b/regression/contracts/loop_assigns-01/main.c @@ -16,7 +16,7 @@ void main() b->data[5] = 0; for(unsigned i = 0; i < SIZE; i++) // clang-format off - __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(b->data)) + __CPROVER_assigns(i, __CPROVER_object_whole(b->data)) __CPROVER_loop_invariant(i <= SIZE) // clang-format on { diff --git a/regression/contracts/loop_assigns-03/main.c b/regression/contracts/loop_assigns-03/main.c index d3b137376f3..5f64342902d 100644 --- a/regression/contracts/loop_assigns-03/main.c +++ b/regression/contracts/loop_assigns-03/main.c @@ -16,7 +16,7 @@ void main() b->data[5] = 0; for(unsigned i = 0; i < SIZE; i++) // clang-format off - __CPROVER_assigns(__CPROVER_POINTER_OBJECT(b->data)) + __CPROVER_assigns(__CPROVER_object_whole(b->data)) __CPROVER_loop_invariant(i <= SIZE) // clang-format on { diff --git a/regression/contracts/loop_assigns-04/main.c b/regression/contracts/loop_assigns-04/main.c index 26ac38f8a93..255d7aed40e 100644 --- a/regression/contracts/loop_assigns-04/main.c +++ b/regression/contracts/loop_assigns-04/main.c @@ -17,7 +17,7 @@ void main() b->data[5] = 0; for(unsigned i = 0; i < SIZE; i++) // clang-format off - __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(b->data)) + __CPROVER_assigns(i, __CPROVER_object_whole(b->data)) __CPROVER_loop_invariant(i <= SIZE) // clang-format on { diff --git a/regression/contracts/loop_assigns-slice-assignable-ptr/main.c b/regression/contracts/loop_assigns-slice-assignable-ptr/main.c new file mode 100644 index 00000000000..fe1d973e536 --- /dev/null +++ b/regression/contracts/loop_assigns-slice-assignable-ptr/main.c @@ -0,0 +1,42 @@ +#include +#include + +#define SIZE 5 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + b->data[0] = 0; + b->data[1] = 1; + b->data[2] = 2; + b->data[3] = 3; + b->data[4] = 4; + + char *start = b->data; + char *end = b->data + SIZE; + + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, + __CPROVER_object_upto(b->data, SIZE), + __CPROVER_typed_target(b->data)) + __CPROVER_loop_invariant( + i <= SIZE && + start <= b->data && b->data < end) + // clang-format on + { + b->data = b->data; // must pass + *(b->data) = 0; // must pass + } + + // must pass + assert(start <= b->data && b->data <= end); + // must fail + assert(b->data == start); +} diff --git a/regression/contracts/loop_assigns-slice-assignable-ptr/test.desc b/regression/contracts/loop_assigns-slice-assignable-ptr/test.desc new file mode 100644 index 00000000000..9a49850f1c3 --- /dev/null +++ b/regression/contracts/loop_assigns-slice-assignable-ptr/test.desc @@ -0,0 +1,22 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.\d+\] .* Check that loop instrumentation was not truncated: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is valid: SUCCESS$ +^\[main.assigns.\d+\] .* Check that __CPROVER_object_upto\(\(.*\)b->data, \(.*\)5\) is valid: SUCCESS$ +^\[main.assigns.\d+\] .* Check that __CPROVER_assignable\(\(.*\)&b->data, (4|8).*, TRUE\) is valid: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*b->data is assignable: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data == start: FAILURE$ +^\[main.assertion.\d+\] .* assertion start <= b->data && b->data <= end: SUCCESS$ +^VERIFICATION FAILED$ +-- +-- +This test checks that __CPROVER_typed_target(ptr) is supported in loop contracts +for pointer typed targets and gets translated to +__CPROVER_assignable(address_of(ptr), sizeof(ptr), TRUE). diff --git a/regression/contracts/loop_assigns-slice-assignable-scalar/main.c b/regression/contracts/loop_assigns-slice-assignable-scalar/main.c new file mode 100644 index 00000000000..e3ec6910f8f --- /dev/null +++ b/regression/contracts/loop_assigns-slice-assignable-scalar/main.c @@ -0,0 +1,40 @@ +#include +#include + +#define SIZE 5 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + b->data[0] = 0; + b->data[1] = 0; + b->data[2] = 0; + b->data[3] = 0; + b->data[4] = 0; + + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, __CPROVER_typed_target(b->data[0])) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + // must pass + b->data[0] = 1; + // must fail + b->data[i] = 1; + } + + // must fail + assert(b->data[0] == 0); + // must pass + assert(b->data[1] == 0); + assert(b->data[2] == 0); + assert(b->data[3] == 0); + assert(b->data[4] == 0); +} diff --git a/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc b/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc new file mode 100644 index 00000000000..09f56c97fad --- /dev/null +++ b/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc @@ -0,0 +1,23 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)0\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)i\] is assignable: FAILURE$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assigns.\d+\] .* Check that __CPROVER_assignable\(\(.*\)&b->data\[\(.*\)0\], 1ul?l?, FALSE\) is valid: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[3\] == 0: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[4\] == 0: SUCCESS$ +^VERIFICATION FAILED$ +-- +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILED$ +-- +This test shows that __CPROVER_typed_target is supported in loop contracts, +and gets translated to __CPROVER_assignable(&target, sizeof(target), FALSE) +for scalar targets. diff --git a/regression/contracts/loop_assigns-slice-from/main.c b/regression/contracts/loop_assigns-slice-from/main.c new file mode 100644 index 00000000000..d75deef74cb --- /dev/null +++ b/regression/contracts/loop_assigns-slice-from/main.c @@ -0,0 +1,37 @@ +#include +#include + +#define SIZE 5 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + b->data[0] = 0; + b->data[1] = 0; + b->data[2] = 0; + b->data[3] = 0; + b->data[4] = 0; + + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_from(b->data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + // must pass + b->data[i] = 1; + } + + // these should all fail + assert(b->data[0] == 0); + assert(b->data[1] == 0); + assert(b->data[2] == 0); + assert(b->data[3] == 0); + assert(b->data[4] == 0); +} diff --git a/regression/contracts/loop_assigns-slice-from/test.desc b/regression/contracts/loop_assigns-slice-from/test.desc new file mode 100644 index 00000000000..dca584fe348 --- /dev/null +++ b/regression/contracts/loop_assigns-slice-from/test.desc @@ -0,0 +1,19 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[3\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[4\] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ +-- +This test shows that __CPROVER_object_from is supported in loop contracts. diff --git a/regression/contracts/loop_assigns-slice-upto-fail/main.c b/regression/contracts/loop_assigns-slice-upto-fail/main.c new file mode 100644 index 00000000000..2e59fe38975 --- /dev/null +++ b/regression/contracts/loop_assigns-slice-upto-fail/main.c @@ -0,0 +1,42 @@ +#include +#include + +#define SIZE 5 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + b->data[0] = 0; + b->data[1] = 0; + b->data[2] = 0; + b->data[3] = 0; + b->data[4] = 0; + + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_upto(b->data, SIZE-2)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + // must pass + b->data[0] = 1; + b->data[1] = 1; + b->data[2] = 1; + // must fail + b->data[i] = 1; + } + + // must fail + assert(b->data[0] == 0); + assert(b->data[1] == 0); + assert(b->data[2] == 0); + // must pass + assert(b->data[3] == 0); + assert(b->data[4] == 0); +} diff --git a/regression/contracts/loop_assigns-slice-upto-fail/test.desc b/regression/contracts/loop_assigns-slice-upto-fail/test.desc new file mode 100644 index 00000000000..7b9a85314ad --- /dev/null +++ b/regression/contracts/loop_assigns-slice-upto-fail/test.desc @@ -0,0 +1,21 @@ +CORE +main.c +--apply-loop-contracts +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)0\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)1\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)2\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)i\] is assignable: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[3\] == 0: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[4\] == 0: SUCCESS$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test shows that __CPROVER_object_upto is supported in loop contracts. diff --git a/regression/contracts/loop_assigns-slice-upto-pass/main.c b/regression/contracts/loop_assigns-slice-upto-pass/main.c new file mode 100644 index 00000000000..3922020407e --- /dev/null +++ b/regression/contracts/loop_assigns-slice-upto-pass/main.c @@ -0,0 +1,38 @@ +#include +#include + +#define SIZE 5 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + b->data[0] = 0; + b->data[1] = 0; + b->data[2] = 0; + b->data[3] = 0; + b->data[4] = 0; + + for(unsigned i = 0; i < 3; i++) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_upto(b->data, 3)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + // must pass + b->data[i] = 1; + } + + // must fail + assert(b->data[0] == 0); + assert(b->data[1] == 0); + assert(b->data[2] == 0); + // must pass + assert(b->data[3] == 0); + assert(b->data[4] == 0); +} diff --git a/regression/contracts/loop_assigns-slice-upto-pass/test.desc b/regression/contracts/loop_assigns-slice-upto-pass/test.desc new file mode 100644 index 00000000000..a9aea6e7386 --- /dev/null +++ b/regression/contracts/loop_assigns-slice-upto-pass/test.desc @@ -0,0 +1,18 @@ +CORE +main.c +--apply-loop-contracts +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)i\] is assignable: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion b->data\[3\] == 0: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[4\] == 0: SUCCESS$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test hows that __CPROVER_object_upto is supported in loop contracts. diff --git a/regression/contracts/quantifiers-loop-01/main.c b/regression/contracts/quantifiers-loop-01/main.c index 4a75dec55d1..67287a83167 100644 --- a/regression/contracts/quantifiers-loop-01/main.c +++ b/regression/contracts/quantifiers-loop-01/main.c @@ -9,7 +9,7 @@ void main() for(int i = 0; i < N; ++i) // clang-format off - __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(a)) + __CPROVER_assigns(i, __CPROVER_object_whole(a)) __CPROVER_loop_invariant( (0 <= i) && (i <= N) && __CPROVER_forall { diff --git a/regression/contracts/quantifiers-loop-02/main.c b/regression/contracts/quantifiers-loop-02/main.c index 0e58dd6a5cc..ca7b41d0ec5 100644 --- a/regression/contracts/quantifiers-loop-02/main.c +++ b/regression/contracts/quantifiers-loop-02/main.c @@ -8,7 +8,7 @@ void main() for(int i = 0; i < N; ++i) // clang-format off - __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(a)) + __CPROVER_assigns(i, __CPROVER_object_whole(a)) __CPROVER_loop_invariant( (0 <= i) && (i <= N) && __CPROVER_forall { diff --git a/regression/contracts/quantifiers-loop-03/main.c b/regression/contracts/quantifiers-loop-03/main.c index 4a9cecd5769..efd006cda80 100644 --- a/regression/contracts/quantifiers-loop-03/main.c +++ b/regression/contracts/quantifiers-loop-03/main.c @@ -12,7 +12,7 @@ void main() for(int i = 0; i < N; ++i) // clang-format off - __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(a)) + __CPROVER_assigns(i, __CPROVER_object_whole(a)) __CPROVER_loop_invariant( (0 <= i) && (i <= N) && (i != 0 ==> __CPROVER_exists { diff --git a/regression/contracts/reject_history_expr_in_assigns_clause/test.desc b/regression/contracts/reject_history_expr_in_assigns_clause/test.desc index 2788121bb93..f215cd94255 100644 --- a/regression/contracts/reject_history_expr_in_assigns_clause/test.desc +++ b/regression/contracts/reject_history_expr_in_assigns_clause/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^main.c.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$ +^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$ ^CONVERSION ERROR$ ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index b5354e043c0..d5b285f983a 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -1013,11 +1013,6 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) throw_on_side_effects(target); return; } - else if(target.id() == ID_pointer_object) - { - throw_on_side_effects(target); - return; - } else if(can_cast_expr(target)) { const auto &funcall = to_side_effect_expr_function_call(target); @@ -1044,9 +1039,8 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) { // if we reach this point the target did not pass the checks throw invalid_source_file_exceptiont( - "assigns clause target must be a non-void lvalue, a call " - "to " CPROVER_PREFIX - "POINTER_OBJECT or a call to a function returning void", + "assigns clause target must be a non-void lvalue or a call to a function " + "returning void", target.source_location()); } } diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index c48e074aab9..1b3c2b4e9de 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -314,7 +314,8 @@ void code_contractst::check_apply_loop_contracts( goto_programt::make_decl(in_loop_havoc_block, loop_head_location)); pre_loop_head_instrs.add( goto_programt::make_assignment(in_loop_havoc_block, true_exprt{})); - havoc_assigns_targetst havoc_gen(to_havoc, ns); + havoc_assigns_targetst havoc_gen( + to_havoc, symbol_table, log.get_message_handler(), mode); havoc_gen.append_full_havoc_code(loop_head_location, pre_loop_head_instrs); pre_loop_head_instrs.add( goto_programt::make_assignment(in_loop_havoc_block, false_exprt{})); diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index 55cbe6bdcb8..c1164d085a6 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 #include @@ -47,6 +48,40 @@ static void append_safe_havoc_code_for_expr( dest.destructive_append(skip_program); } +void havoc_assigns_targetst::append_havoc_slice_code( + const source_locationt location, + const exprt &ptr, + const exprt &size, + goto_programt &dest) +{ + append_safe_havoc_code_for_expr( + location, + ns, + ptr, + dest, + // clang-format off + [&]() { + symbol_exprt function{CPROVER_PREFIX "havoc_slice", empty_typet()}; + function.add_source_location() = location; + // havoc slice is lowered to array operations during goto conversion + // so we use goto_convertt directly as provided by clearnert + cleaner.do_havoc_slice(function, {ptr, size}, dest, mode); + }); + // clang-format on +} + +void havoc_assigns_targetst::append_havoc_pointer_code( + const source_locationt location, + const exprt &ptr_to_ptr, + goto_programt &dest) +{ + append_safe_havoc_code_for_expr(location, ns, ptr_to_ptr, dest, [&]() { + auto ptr = dereference_exprt(ptr_to_ptr); + dest.add(goto_programt::make_assignment( + ptr, side_effect_expr_nondett(ptr.type(), location), location)); + }); +} + void havoc_if_validt::append_object_havoc_code_for_expr( const source_locationt location, const exprt &expr, @@ -70,16 +105,68 @@ void havoc_if_validt::append_scalar_havoc_code_for_expr( void havoc_assigns_targetst::append_havoc_code_for_expr( const source_locationt location, const exprt &expr, - goto_programt &dest) const + goto_programt &dest) { if(expr.id() == ID_pointer_object) { + // pointer_object is still used internally to support malloc/free append_object_havoc_code_for_expr( location, to_pointer_object_expr(expr).pointer(), dest); return; } + else if(can_cast_expr(expr)) + { + const auto &funcall = to_side_effect_expr_function_call(expr); + // type-checking ensures the function expression is necessarily a symbol + const auto &ident = to_symbol_expr(funcall.function()).get_identifier(); + if(ident == CPROVER_PREFIX "object_whole") + { + append_object_havoc_code_for_expr( + location, funcall.arguments().at(0), dest); + } + else if(ident == CPROVER_PREFIX "object_from") + { + const auto ptr = typecast_exprt::conditional_cast( + funcall.arguments().at(0), pointer_type(char_type())); - havoc_utilst::append_havoc_code_for_expr(location, expr, dest); + exprt obj_size = object_size(ptr); + minus_exprt size{ + obj_size, + typecast_exprt::conditional_cast(pointer_offset(ptr), obj_size.type())}; + + append_havoc_slice_code(expr.source_location(), ptr, size, dest); + } + else if(ident == CPROVER_PREFIX "object_upto") + { + const auto ptr = typecast_exprt::conditional_cast( + funcall.arguments().at(0), pointer_type(char_type())); + const auto size = typecast_exprt::conditional_cast( + funcall.arguments().at(1), size_type()); + append_havoc_slice_code(expr.source_location(), ptr, size, dest); + } + else if(ident == CPROVER_PREFIX "assignable") + { + const auto &ptr = funcall.arguments().at(0); + const auto &size = funcall.arguments().at(1); + if(funcall.arguments().at(2).is_true()) + { + append_havoc_pointer_code(expr.source_location(), ptr, dest); + } + else + { + append_havoc_slice_code(expr.source_location(), ptr, size, dest); + } + } + else + { + UNREACHABLE; + } + } + else + { + // we have an lvalue expression, make nondet assignment + havoc_utilst::append_havoc_code_for_expr(location, expr, dest); + } } exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns) diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 8e2af7a4a89..ed7a7adf27d 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -13,6 +13,8 @@ Date: September 2021 #include +#include + #include #include @@ -22,6 +24,33 @@ Date: September 2021 #define IN_LOOP_HAVOC_BLOCK "__in_loop_havoc_block" #define INIT_INVARIANT "__init_invariant" +/// Class that allows to clean expressions of side effects and to generate +/// havoc_slice expressions. +class cleanert : public goto_convertt +{ +public: + cleanert( + symbol_table_baset &_symbol_table, + message_handlert &_message_handler) + : goto_convertt(_symbol_table, _message_handler) + { + } + + void clean(exprt &guard, goto_programt &dest, const irep_idt &mode) + { + 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); + } +}; + /// \brief A class that overrides the low-level havocing functions in the base /// utility class, to havoc only when expressions point to valid memory, /// i.e. if all dereferences within an expression are valid @@ -52,15 +81,39 @@ class havoc_if_validt : public havoc_utilst class havoc_assigns_targetst : public havoc_if_validt { public: - havoc_assigns_targetst(const assignst &mod, const namespacet &ns) - : havoc_if_validt(mod, ns) + havoc_assigns_targetst( + const assignst &mod, + symbol_tablet &st, + message_handlert &message_handler, + const irep_idt &mode) + : havoc_if_validt(mod, ns), + ns(st), + cleaner(st, message_handler), + log(message_handler), + mode(mode) { } + void append_havoc_pointer_code( + const source_locationt location, + const exprt &ptr_to_ptr, + goto_programt &dest); + + void append_havoc_slice_code( + const source_locationt location, + const exprt &ptr, + const exprt &size, + goto_programt &dest); + void append_havoc_code_for_expr( const source_locationt location, const exprt &expr, - goto_programt &dest) const override; + goto_programt &dest); + + namespacet ns; + cleanert cleaner; + messaget log; + const irep_idt &mode; }; /// \brief Generate a validity check over all dereferences in an expression @@ -162,32 +215,6 @@ bool is_loop_free( namespacet &ns, messaget &log); -/// Allows to clean expressions of side effects. -class cleanert : public goto_convertt -{ -public: - cleanert( - symbol_table_baset &_symbol_table, - message_handlert &_message_handler) - : goto_convertt(_symbol_table, _message_handler) - { - } - - void clean(exprt &guard, goto_programt &dest, const irep_idt &mode) - { - 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 /// `target` was assigned by the contract of `function_id`. irep_idt make_assigns_clause_replacement_tracking_comment( diff --git a/src/goto-instrument/havoc_utils.cpp b/src/goto-instrument/havoc_utils.cpp index f7d6dc5c5c7..0c712e3e81e 100644 --- a/src/goto-instrument/havoc_utils.cpp +++ b/src/goto-instrument/havoc_utils.cpp @@ -20,7 +20,7 @@ Date: July 2021 void havoc_utilst::append_full_havoc_code( const source_locationt location, - goto_programt &dest) const + goto_programt &dest) { for(const auto &expr : assigns) append_havoc_code_for_expr(location, expr, dest); @@ -29,7 +29,7 @@ void havoc_utilst::append_full_havoc_code( void havoc_utilst::append_havoc_code_for_expr( const source_locationt location, const exprt &expr, - goto_programt &dest) const + goto_programt &dest) { if(expr.id() == ID_index || expr.id() == ID_dereference) { diff --git a/src/goto-instrument/havoc_utils.h b/src/goto-instrument/havoc_utils.h index e5b425c9996..d0b02301109 100644 --- a/src/goto-instrument/havoc_utils.h +++ b/src/goto-instrument/havoc_utils.h @@ -61,9 +61,8 @@ class havoc_utilst /// /// \param location The source location to annotate on the havoc instruction /// \param dest The destination goto program to append the instructions to - void append_full_havoc_code( - const source_locationt location, - goto_programt &dest) const; + void + append_full_havoc_code(const source_locationt location, goto_programt &dest); /// \brief Append goto instructions to havoc a single expression `expr` /// @@ -79,7 +78,7 @@ class havoc_utilst virtual void append_havoc_code_for_expr( const source_locationt location, const exprt &expr, - goto_programt &dest) const; + goto_programt &dest); /// \brief Append goto instructions to havoc the underlying object of `expr` ///