diff --git a/regression/contracts/assigns_enforce_20/test.desc b/regression/contracts/assigns_enforce_20/test.desc index b8da1fa1031..1cca96c1c7f 100644 --- a/regression/contracts/assigns_enforce_20/test.desc +++ b/regression/contracts/assigns_enforce_20/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^\[foo.\d+\] line \d+ Check that \*y is assignable: FAILURE$ +^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$ ^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc index 4c3cfa2b9b4..9e9033a30f9 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: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc index 4a485acff3f..4fe133f4914 100644 --- a/regression/contracts/assigns_enforce_arrays_05/test.desc +++ b/regression/contracts/assigns_enforce_arrays_05/test.desc @@ -1,6 +1,6 @@ CORE main.c ---enforce-contract assigns_ptr --enforce-contract assigns_range +--enforce-contract assigns_range ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_elvis_4/test.desc b/regression/contracts/assigns_enforce_elvis_4/test.desc index 6504078edc2..b2f68af4a92 100644 --- a/regression/contracts/assigns_enforce_elvis_4/test.desc +++ b/regression/contracts/assigns_enforce_elvis_4/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: void-typed targets not permitted$ +^.*error: void-typed targets not permitted in assigns clause$ -- -- Check that Elvis operator expressions '*(cond ? if_true : if_false)' with different types in true and false branches are rejected. diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc index f2547f2a9fb..a18e73b93cf 100644 --- a/regression/contracts/assigns_enforce_function_calls/test.desc +++ b/regression/contracts/assigns_enforce_function_calls/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc index 45e09d5d0da..e5fa1712864 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: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^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 d6f3c98d246..57965527d2a 100644 --- a/regression/contracts/assigns_enforce_side_effects_1/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_1/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: void-typed targets not permitted$ +^.*error: void-typed targets not permitted in assigns clause$ ^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 21ba293dd46..c0ee204ba71 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: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc index 21ba293dd46..c0ee204ba71 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: illegal target in assigns clause$ +^.*error: non-lvalue target in assigns clause$ ^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 2cdc55e7c5f..c77f85d72c7 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: illegal target in assigns clause +error: non-lvalue target in assigns clause -- Checks whether type checking reports illegal target in assigns clause. diff --git a/regression/contracts/invar_assigns_alias_analysis/test.desc b/regression/contracts/invar_assigns_alias_analysis/test.desc deleted file mode 100644 index 961be46b17c..00000000000 --- a/regression/contracts/invar_assigns_alias_analysis/test.desc +++ /dev/null @@ -1,14 +0,0 @@ -KNOWNBUG -main.c ---apply-loop-contracts -^EXIT=0$ -^SIGNAL=0$ -^\[main.1\] .* Check loop invariant before entry: SUCCESS$ -^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.assertion.1\] .* assertion b->data[5] == 0: FAILURE$ -^VERIFICATION FAILED$ --- --- -This test shows the need for assigns clauses. Currently we only -parse the assigns clause for loops, but there is no implementation -to actually enforce them. In the future, we will add this feature. diff --git a/regression/contracts/invar_assigns_empty/main.c b/regression/contracts/invar_assigns_empty/main.c index ba05010b0a0..4a41b2ea796 100644 --- a/regression/contracts/invar_assigns_empty/main.c +++ b/regression/contracts/invar_assigns_empty/main.c @@ -2,14 +2,8 @@ int main() { - int r; - __CPROVER_assume(r >= 0); - while(r > 0) - __CPROVER_assigns() __CPROVER_loop_invariant(r >= 0) + while(1 == 1) + __CPROVER_assigns() __CPROVER_loop_invariant(1 == 1) { - r--; } - assert(r == 0); - - return 0; } diff --git a/regression/contracts/invar_assigns_empty/test.desc b/regression/contracts/invar_assigns_empty/test.desc index 19eddb6eb55..69966423ea5 100644 --- a/regression/contracts/invar_assigns_empty/test.desc +++ b/regression/contracts/invar_assigns_empty/test.desc @@ -5,7 +5,6 @@ main.c ^SIGNAL=0$ ^\[main.1\] .* Check loop invariant before entry: SUCCESS$ ^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.assertion.1\] .* assertion r == 0: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/invar_assigns_opt/test.desc b/regression/contracts/invar_assigns_opt/test.desc index e5e6d920973..da69d71761f 100644 --- a/regression/contracts/invar_assigns_opt/test.desc +++ b/regression/contracts/invar_assigns_opt/test.desc @@ -3,14 +3,16 @@ main.c --apply-loop-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[main.1\] .* Check loop invariant before entry: SUCCESS$ -^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$ -^\[main.assertion.1\] .* assertion r1 == 0: SUCCESS$ -^\[main.4\] .* Check loop invariant before entry: SUCCESS$ -^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$ -^\[main.assertion.2\] .* assertion r2 == 0: SUCCESS$ +^\[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.assertion.\d+\] .* assertion r1 == 0: SUCCESS$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that s2 is assignable: SUCCESS$ +^\[main.\d+\] .* Check that r2 is assignable: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$ +^\[main.assertion.\d+\] .* assertion r2 == 0: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc index 174fa755423..1606615be95 100644 --- a/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc +++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc @@ -18,4 +18,9 @@ to pass -- we should not mistakenly havoc the allocations, just their values. However, the `data[1][2][3] == 0` assertion is expected to fail since `data` is havoced. -Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`. +Blocked on #6326: +The assigns clause in this case would have an entire 3D space, +and some of it must be re-established, to the original objects +but with different values at certain locations, by the loop invariant. +However, currently we cannot restrict same_object for pointers +within loop invariants. diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c index 1717ab001d8..02f03ffa58f 100644 --- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c +++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c @@ -17,7 +17,10 @@ void main() data[4][5][6] = 0; for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, data[4][5][6]) __CPROVER_loop_invariant(i <= SIZE) + // clang-format on { data[4][5][6] = 1; } diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc index f57ca4872a7..441b05eea40 100644 --- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc +++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc @@ -1,12 +1,14 @@ -KNOWNBUG +CORE main.c --apply-loop-contracts ^EXIT=10$ ^SIGNAL=0$ -^\[main.1\] .* Check loop invariant before entry: SUCCESS$ -^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.assertion.1\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ -^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check that data\[(.*)4\]\[(.*)5\]\[(.*)6\] is assignable: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ ^VERIFICATION FAILED$ -- -- @@ -17,5 +19,3 @@ The `data[4][5][6] == 0` assertion is expected to fail since `data[4][5][6]` is havoced and the invariant does not reestablish its value. However, the `data[1][2][3] == 0` assertion is expected to pass -- we should not havoc the entire `data` array, if only a constant index if being modified. - -Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`. diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc index 0e180ad0d42..ac12b40c298 100644 --- a/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc +++ b/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc @@ -19,4 +19,9 @@ We _could_ do a more precise analysis in future where we only havoc `data[4][5][6]` but not `data[1][2][3]` since the latter clearly cannot be modified in the given loop. -Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`. +Blocked on #6326: +The assigns clause in this case would have an entire 2D grid, +and some of it must be re-established, to the original objects +but with different values at certain locations, by the loop invariant. +However, currently we cannot restrict same_object for pointers +within loop invariants. diff --git a/regression/contracts/loop_assigns-01/main.c b/regression/contracts/loop_assigns-01/main.c new file mode 100644 index 00000000000..896e34dace1 --- /dev/null +++ b/regression/contracts/loop_assigns-01/main.c @@ -0,0 +1,27 @@ +#include +#include + +#define SIZE 8 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + + b->data[5] = 0; + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(b->data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts/loop_assigns-01/test.desc b/regression/contracts/loop_assigns-01/test.desc new file mode 100644 index 00000000000..8e242fd5b3d --- /dev/null +++ b/regression/contracts/loop_assigns-01/test.desc @@ -0,0 +1,16 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`, +and so we must manually annotate an assigns clause on the loop. diff --git a/regression/contracts/loop_assigns-02/main.c b/regression/contracts/loop_assigns-02/main.c new file mode 100644 index 00000000000..d4b45140be3 --- /dev/null +++ b/regression/contracts/loop_assigns-02/main.c @@ -0,0 +1,27 @@ +#include +#include + +#define SIZE 8 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + + b->data[5] = 0; + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, b->data[i]) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts/loop_assigns-02/test.desc b/regression/contracts/loop_assigns-02/test.desc new file mode 100644 index 00000000000..e1ecdc4b04b --- /dev/null +++ b/regression/contracts/loop_assigns-02/test.desc @@ -0,0 +1,20 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`, +and so we must manually annotate an assigns clause on the loop. + +Note that the annotated assigns clause in this case is an underapproximation, +per the current semantics of the assigns clause -- it must model ALL memory +being assigned to by the loop, not just a single symbolic iteration. diff --git a/regression/contracts/loop_assigns-03/main.c b/regression/contracts/loop_assigns-03/main.c new file mode 100644 index 00000000000..d3b137376f3 --- /dev/null +++ b/regression/contracts/loop_assigns-03/main.c @@ -0,0 +1,27 @@ +#include +#include + +#define SIZE 8 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + + b->data[5] = 0; + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(__CPROVER_POINTER_OBJECT(b->data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts/loop_assigns-03/test.desc b/regression/contracts/loop_assigns-03/test.desc new file mode 100644 index 00000000000..632e889b1b4 --- /dev/null +++ b/regression/contracts/loop_assigns-03/test.desc @@ -0,0 +1,17 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that i is assignable: FAILURE$ +^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^VERIFICATION FAILED$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`, +and so we must manually annotate an assigns clause on the loop. + +Note that the annotated assigns clause in this case is an underapproximation, +because `i` is also assigned in the loop and should be marked as assignable. diff --git a/regression/contracts/loop_assigns-04/main.c b/regression/contracts/loop_assigns-04/main.c new file mode 100644 index 00000000000..26ac38f8a93 --- /dev/null +++ b/regression/contracts/loop_assigns-04/main.c @@ -0,0 +1,41 @@ +#include +#include + +#define SIZE 8 + +struct blob +{ + char *data; +}; + +void main() +{ + int y; + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + + b->data[5] = 0; + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(b->data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + + int x; + for(unsigned j = 0; j < i; j++) + // clang-format off + // y is not assignable by outer loop, so this should be flagged + __CPROVER_assigns(j, y, x, b->data[i]) + __CPROVER_loop_invariant(j <= i) + // clang-format on + { + x = b->data[j] * b->data[j]; + b->data[i] += x; + y += j; + } + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts/loop_assigns-04/test.desc b/regression/contracts/loop_assigns-04/test.desc new file mode 100644 index 00000000000..fef5d6e0572 --- /dev/null +++ b/regression/contracts/loop_assigns-04/test.desc @@ -0,0 +1,18 @@ +CORE +main.c +--apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.\d+\] .* Check that j is assignable: SUCCESS$ +^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[main.\d+\] .* Check that y is assignable: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`, +and so we must manually annotate an assigns clause on the loop. + +Note that the annotated assigns clause in this case is an underapproximation, +because `i` is also assigned in the loop and should be marked as assignable. diff --git a/regression/contracts/invar_assigns_alias_analysis/main.c b/regression/contracts/loop_assigns-fail/main.c similarity index 92% rename from regression/contracts/invar_assigns_alias_analysis/main.c rename to regression/contracts/loop_assigns-fail/main.c index d2a81998022..43f17c4bf7c 100644 --- a/regression/contracts/invar_assigns_alias_analysis/main.c +++ b/regression/contracts/loop_assigns-fail/main.c @@ -16,7 +16,6 @@ void main() b->data[5] = 0; for(unsigned i = 0; i < SIZE; i++) // clang-format off - __CPROVER_assigns(b->data) __CPROVER_loop_invariant(i <= SIZE) // clang-format on { diff --git a/regression/contracts/loop_assigns-fail/test.desc b/regression/contracts/loop_assigns-fail/test.desc new file mode 100644 index 00000000000..b1f4751987d --- /dev/null +++ b/regression/contracts/loop_assigns-fail/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-loop-contracts +activate-multi-line-match +Failed to infer variables being modified by the loop at file main.c line \d+ function main\.\nPlease specify an assigns clause\.\nReason:\nAlias analysis returned UNKNOWN! +^EXIT=6$ +^SIGNAL=0$ +-- +-- +This test (taken from #6021) shows the need for assigns clauses on loops. +The alias analysis in this case returns `unknown`. diff --git a/regression/contracts/loop_contracts_do_while/main.c b/regression/contracts/loop_contracts_do_while/main.c new file mode 100644 index 00000000000..88477df7fc2 --- /dev/null +++ b/regression/contracts/loop_contracts_do_while/main.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int x = 0; + + do + { + x++; + } while(x < 10) __CPROVER_loop_invariant(0 <= x && x <= 10); + + assert(x == 10); +} diff --git a/regression/contracts/loop_contracts_do_while/test.desc b/regression/contracts/loop_contracts_do_while/test.desc new file mode 100644 index 00000000000..488a91f377f --- /dev/null +++ b/regression/contracts/loop_contracts_do_while/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +main.c +--apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that loop contracts work correctly on do/while loops. diff --git a/regression/contracts/variant_missing_invariant_warning/test.desc b/regression/contracts/variant_missing_invariant_warning/test.desc index be05a219c40..4af9a7823c3 100644 --- a/regression/contracts/variant_missing_invariant_warning/test.desc +++ b/regression/contracts/variant_missing_invariant_warning/test.desc @@ -1,7 +1,8 @@ CORE main.c --apply-loop-contracts -^The loop at file main.c line 4 function main does not have a loop invariant, but has a decreases clause. Hence, a default loop invariant \('true'\) is being used.$ +activate-multi-line-match +^The loop at file main.c line 4 function main does not have an invariant.*.\nHence, a default invariant \('true'\) is being used to prove those.$ ^\[main.1\].*Check loop invariant before entry: SUCCESS$ ^\[main.2\].*Check that loop invariant is preserved: SUCCESS$ ^\[main.3\].*Check decreases clause on loop iteration: SUCCESS$ diff --git a/regression/contracts/variant_multi_instruction_loop_head/main.c b/regression/contracts/variant_multi_instruction_loop_head/main.c new file mode 100644 index 00000000000..705dd64d99a --- /dev/null +++ b/regression/contracts/variant_multi_instruction_loop_head/main.c @@ -0,0 +1,14 @@ +int main() +{ + int x = 0; + int *y = &x; + + while(*y <= 0 && *y < 10) + // clang-format off + __CPROVER_loop_invariant(1 == 1) + __CPROVER_decreases(10 - x) + // clang-format on + { + x++; + } +} diff --git a/regression/contracts/variant_multi_instruction_loop_head/test.desc b/regression/contracts/variant_multi_instruction_loop_head/test.desc new file mode 100644 index 00000000000..dfcc8fcf847 --- /dev/null +++ b/regression/contracts/variant_multi_instruction_loop_head/test.desc @@ -0,0 +1,19 @@ +CORE +main.c +--apply-loop-contracts +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails even without the fix proposed in the commit, so it should be improved. +It is expected to fail because the proposed invariant isn't strong enough to help prove +termination using the specified variant. + +The test highlights a case where a C loop guard is compiled to multiple GOTO instructions. +Therefore the loop_head pointer needs to be advanced multiple times to get to the loop body, +where the initial value of the loop variant (/ ranking function) must be recorded. + +The proposed fix advances the pointer until the source_location differs from the original +loop_head's source_location. However, this might still not work if the loop guard in the +original C code was split across multiple lines in the first place. diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index c41bd51bbeb..1cad4a50b7b 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -739,33 +739,7 @@ void c_typecheck_baset::typecheck_declaration( CPROVER_PREFIX "loop_entry is not allowed in preconditions."); } - for(auto &target : code_type.assigns()) - { - typecheck_expr(target); - - if(target.type().id() == ID_empty) - { - error().source_location = target.source_location(); - error() << "void-typed targets not permitted" << eom; - throw 0; - } - else if(target.id() == ID_pointer_object) - { - // skip - } - else if(!target.get_bool(ID_C_lvalue)) - { - error().source_location = target.source_location(); - error() << "illegal target in assigns clause" << eom; - throw 0; - } - else if(has_subexpr(target, ID_side_effect)) - { - error().source_location = target.source_location(); - error() << "assigns clause is not side-effect free" << eom; - throw 0; - } - } + typecheck_spec_assigns(code_type.assigns()); if(!as_const(code_type).ensures().empty()) { diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 405940c81fe..1b92f0e633a 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -144,6 +144,9 @@ class c_typecheck_baset: virtual void typecheck_while(code_whilet &code); virtual void typecheck_dowhile(code_dowhilet &code); virtual void typecheck_start_thread(codet &code); + + // contracts + virtual void typecheck_spec_assigns(exprt::operandst &targets); virtual void typecheck_spec_loop_invariant(codet &code); virtual void typecheck_spec_decreases(codet &code); diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 6fd492371ce..233cf3a1afc 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -493,6 +494,12 @@ void c_typecheck_baset::typecheck_for(codet &code) typecheck_spec_loop_invariant(code); typecheck_spec_decreases(code); + + if(code.find(ID_C_spec_assigns).is_not_nil()) + { + typecheck_spec_assigns( + static_cast(code.add(ID_C_spec_assigns)).op().operands()); + } } void c_typecheck_baset::typecheck_label(code_labelt &code) @@ -782,6 +789,12 @@ void c_typecheck_baset::typecheck_while(code_whilet &code) typecheck_spec_loop_invariant(code); typecheck_spec_decreases(code); + + if(code.find(ID_C_spec_assigns).is_not_nil()) + { + typecheck_spec_assigns( + static_cast(code.add(ID_C_spec_assigns)).op().operands()); + } } void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) @@ -816,6 +829,43 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) typecheck_spec_loop_invariant(code); typecheck_spec_decreases(code); + + if(code.find(ID_C_spec_assigns).is_not_nil()) + { + typecheck_spec_assigns( + static_cast(code.add(ID_C_spec_assigns)).op().operands()); + } +} + +void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) +{ + for(auto &target : targets) + { + typecheck_expr(target); + + if(target.type().id() == ID_empty) + { + error().source_location = target.source_location(); + error() << "void-typed targets not permitted in assigns clause" << eom; + throw 0; + } + else if(target.id() == ID_pointer_object) + { + // skip + } + else if(!target.get_bool(ID_C_lvalue)) + { + error().source_location = target.source_location(); + error() << "non-lvalue target in assigns clause" << eom; + throw 0; + } + else if(has_subexpr(target, ID_side_effect)) + { + error().source_location = target.source_location(); + error() << "assigns clause is not side-effect free" << eom; + throw 0; + } + } } void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code) diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index 6d9157f3633..17b2bf89be1 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -2453,6 +2453,9 @@ iteration_statement: statement($$, ID_while); parser_stack($$).add_to_operands(std::move(parser_stack($3)), std::move(parser_stack($8))); + if(!parser_stack($5).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($5).operands()); + if(!parser_stack($6).operands().empty()) static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($6).operands()); @@ -2468,6 +2471,9 @@ iteration_statement: statement($$, ID_dowhile); parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2))); + if(!parser_stack($7).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($7).operands()); + if(!parser_stack($8).operands().empty()) static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands()); @@ -2499,6 +2505,9 @@ iteration_statement: mto($$, $7); mto($$, $12); + if(!parser_stack($9).operands().empty()) + static_cast(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($9).operands()); + if(!parser_stack($10).operands().empty()) static_cast(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($10).operands()); diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index c79354e9621..ac87d9c4a35 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -117,6 +117,10 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions() location)); instructions.destructive_append(skip_program); + + // The assignments above are only performed on locally defined temporaries + // and need not be checked for inclusion in the enclosing scope's write set. + add_pragma_disable_assigns_check(instructions); return instructions; } diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 6b1724a4c4f..4cb4af3d077 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -30,6 +30,7 @@ Date: February 2016 #include #include #include +#include #include #include #include @@ -41,6 +42,7 @@ Date: February 2016 #include "utils.h" void code_contractst::check_apply_loop_contracts( + const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, @@ -57,23 +59,29 @@ void code_contractst::check_apply_loop_contracts( t->location_number > loop_end->location_number) loop_end = t; - // see whether we have an invariant and a decreases clause + // check for assigns, invariant, and decreases clauses + auto assigns = static_cast( + loop_end->get_condition().find(ID_C_spec_assigns)); auto invariant = static_cast( loop_end->get_condition().find(ID_C_spec_loop_invariant)); auto decreases_clause = static_cast( loop_end->get_condition().find(ID_C_spec_decreases)); + assigns_clauset loop_assigns( + assigns.operands(), log, ns, function_name, symbol_table); + if(invariant.is_nil()) { - if(decreases_clause.is_nil()) + if(decreases_clause.is_nil() && assigns.is_nil()) return; else { invariant = true_exprt(); log.warning() << "The loop at " << loop_head->source_location().as_string() - << " does not have a loop invariant, but has a decreases clause. " - << "Hence, a default loop invariant ('true') is being used." + << " does not have an invariant, but has other clauses" + << " specified in its contract.\n" + << "Hence, a default invariant ('true') is being used to prove those." << messaget::eom; } } @@ -97,23 +105,20 @@ void code_contractst::check_apply_loop_contracts( // to // initialize loop_entry variables; // H: assert(invariant); + // snapshot(write_set); // havoc; // assume(invariant); // if(guard) goto E: - // old_decreases_value = decreases_clause(current_environment); - // loop; - // new_decreases_value = decreases_clause(current_environment); + // old_decreases_value = decreases_clause_expr; + // loop with optional write_set inclusion checks; + // new_decreases_value = decreases_clause_expr; // assert(invariant); // assert(new_decreases_value < old_decreases_value); // assume(false); // E: ... - // find out what can get changed in the loop - modifiest modifies; - get_modifies(local_may_alias, loop, modifies); - - // build the havocking code - goto_programt havoc_code; + // an intermediate goto_program to store generated instructions + goto_programt generated_code; // process quantified variables correctly (introduce a fresh temporary) // and return a copy of the invariant @@ -133,26 +138,73 @@ void code_contractst::check_apply_loop_contracts( parameter2history, loop_head->source_location(), mode, - havoc_code, + generated_code, ID_loop_entry); - // Create 'loop_entry' history variables - insert_before_swap_and_advance(goto_function.body, loop_head, havoc_code); - // Generate: assert(invariant) just before the loop // We use a block scope to create a temporary assertion, // and immediately convert it to goto instructions. { code_assertt assertion{invariant_expr()}; assertion.add_source_location() = loop_head->source_location(); - converter.goto_convert(assertion, havoc_code, mode); - havoc_code.instructions.back().source_location_nonconst().set_comment( + converter.goto_convert(assertion, generated_code, mode); + generated_code.instructions.back().source_location_nonconst().set_comment( "Check loop invariant before entry"); } + // Add 'loop_entry' history variables and base case assertion. + // These variables are local and thus + // need not be checked against the enclosing scope's write set. + insert_before_swap_and_advance( + goto_function.body, + loop_head, + add_pragma_disable_assigns_check(generated_code)); + // havoc the variables that may be modified - havoc_if_validt havoc_gen(modifies, ns); - havoc_gen.append_full_havoc_code(loop_head->source_location(), havoc_code); + modifiest modifies; + if(assigns.is_nil()) + { + try + { + get_modifies(local_may_alias, loop, modifies); + } + catch(const analysis_exceptiont &exc) + { + log.error() << "Failed to infer variables being modified by the loop at " + << loop_head->source_location() + << ".\nPlease specify an assigns clause.\nReason:" + << messaget::eom; + throw exc; + } + } + else + { + modifies.insert(assigns.operands().cbegin(), assigns.operands().cend()); + + // Create snapshots of write set CARs. + // 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(); + insert_before_swap_and_advance( + goto_function.body, loop_head, snapshot_instructions); + }; + } + + havoc_assigns_targetst havoc_gen(modifies, ns); + havoc_gen.append_full_havoc_code( + loop_head->source_location(), generated_code); + + // Add the havocing code, but only check against the enclosing scope's + // write set if it was manually specified. + if(assigns.is_nil()) + insert_before_swap_and_advance( + goto_function.body, + loop_head, + add_pragma_disable_assigns_check(generated_code)); + else + insert_before_swap_and_advance( + goto_function.body, loop_head, generated_code); // Generate: assume(invariant) just after havocing // We use a block scope to create a temporary assumption, @@ -160,7 +212,7 @@ void code_contractst::check_apply_loop_contracts( { code_assumet assumption{invariant_expr()}; assumption.add_source_location() = loop_head->source_location(); - converter.goto_convert(assumption, havoc_code, mode); + converter.goto_convert(assumption, generated_code, mode); } // Create fresh temporary variables that store the multidimensional @@ -171,7 +223,7 @@ void code_contractst::check_apply_loop_contracts( new_tmp_symbol( clause.type(), loop_head->source_location(), mode, symbol_table) .symbol_expr(); - havoc_code.add(goto_programt::make_decl( + generated_code.add(goto_programt::make_decl( old_decreases_var, loop_head->source_location())); old_decreases_vars.push_back(old_decreases_var); @@ -179,25 +231,51 @@ void code_contractst::check_apply_loop_contracts( new_tmp_symbol( clause.type(), loop_head->source_location(), mode, symbol_table) .symbol_expr(); - havoc_code.add(goto_programt::make_decl( + generated_code.add(goto_programt::make_decl( new_decreases_var, loop_head->source_location())); new_decreases_vars.push_back(new_decreases_var); } - // non-deterministically skip the loop if it is a do-while loop - if(!loop_head->is_goto()) + // TODO: Fix loop contract handling for do/while loops. + if(loop_end->is_goto() && !loop_end->get_condition().is_true()) { - havoc_code.add(goto_programt::make_goto( + log.error() << "Loop contracts are unsupported on do/while loops: " + << loop_head->source_location() << messaget::eom; + throw 0; + + // non-deterministically skip the loop if it is a do-while loop. + generated_code.add(goto_programt::make_goto( loop_end, side_effect_expr_nondett(bool_typet(), loop_head->source_location()))); } - // Now havoc at the loop head. + // Assume invariant & decl the variant temporaries (just before loop guard). // Use insert_before_swap to preserve jumps to loop head. - insert_before_swap_and_advance(goto_function.body, loop_head, havoc_code); + insert_before_swap_and_advance(goto_function.body, loop_head, generated_code); + + // Forward the loop_head iterator until the start of the body. + // This is necessary because complex C loop_head conditions could be + // converted to multiple GOTO instructions (e.g. temporaries are introduced). + // FIXME: This simple approach wouldn't work when + // the loop guard in the source file is split across multiple lines. + const auto head_loc = loop_head->source_location(); + while(loop_head->source_location() == head_loc) + loop_head++; + + // At this point, we are just past the loop head, + // so at the beginning of the loop body. + auto loop_body = loop_head; + loop_head--; + + // Perform write set instrumentation before adding anything else to loop body. + if(assigns.is_not_nil()) + { + check_frame_conditions( + function_name, goto_function.body, loop_body, loop_end, loop_assigns); + } // Generate: assignments to store the multidimensional decreases clause's - // value before the loop + // value just before the loop body (but just after the loop guard) if(!decreases_clause.is_nil()) { for(size_t i = 0; i < old_decreases_vars.size(); i++) @@ -206,10 +284,10 @@ void code_contractst::check_apply_loop_contracts( decreases_clause_exprs[i]}; old_decreases_assignment.add_source_location() = loop_head->source_location(); - converter.goto_convert(old_decreases_assignment, havoc_code, mode); + converter.goto_convert(old_decreases_assignment, generated_code, mode); } - goto_function.body.destructive_insert(std::next(loop_head), havoc_code); + goto_function.body.destructive_insert(loop_body, generated_code); } // Generate: assert(invariant) just after the loop exits @@ -218,8 +296,8 @@ void code_contractst::check_apply_loop_contracts( { code_assertt assertion{invariant_expr()}; assertion.add_source_location() = loop_end->source_location(); - converter.goto_convert(assertion, havoc_code, mode); - havoc_code.instructions.back().source_location_nonconst().set_comment( + converter.goto_convert(assertion, generated_code, mode); + generated_code.instructions.back().source_location_nonconst().set_comment( "Check that loop invariant is preserved"); } @@ -233,7 +311,7 @@ void code_contractst::check_apply_loop_contracts( decreases_clause_exprs[i]}; new_decreases_assignment.add_source_location() = loop_head->source_location(); - converter.goto_convert(new_decreases_assignment, havoc_code, mode); + converter.goto_convert(new_decreases_assignment, generated_code, mode); } // Generate: assertion that the multidimensional decreases clause's value @@ -244,29 +322,26 @@ void code_contractst::check_apply_loop_contracts( new_decreases_vars, old_decreases_vars)}; monotonic_decreasing_assertion.add_source_location() = loop_head->source_location(); - converter.goto_convert(monotonic_decreasing_assertion, havoc_code, mode); - havoc_code.instructions.back().source_location_nonconst().set_comment( + converter.goto_convert( + monotonic_decreasing_assertion, generated_code, mode); + generated_code.instructions.back().source_location_nonconst().set_comment( "Check decreases clause on loop iteration"); // Discard the temporary variables that store decreases clause's value for(size_t i = 0; i < old_decreases_vars.size(); i++) { - havoc_code.add(goto_programt::make_dead( + generated_code.add(goto_programt::make_dead( old_decreases_vars[i], loop_head->source_location())); - havoc_code.add(goto_programt::make_dead( + generated_code.add(goto_programt::make_dead( new_decreases_vars[i], loop_head->source_location())); } } - insert_before_swap_and_advance(goto_function.body, loop_end, havoc_code); + insert_before_swap_and_advance(goto_function.body, loop_end, generated_code); // change the back edge into assume(false) or assume(guard) loop_end->turn_into_assume(); - - if(loop_head->is_goto()) - loop_end->set_condition(false_exprt()); - else - loop_end->set_condition(boolean_negate(loop_end->get_condition())); + loop_end->set_condition(boolean_negate(loop_end->get_condition())); } void code_contractst::add_quantified_variable( @@ -572,8 +647,7 @@ bool code_contractst::apply_function_contract( // Havoc all targets in the write set modifiest modifies; - for(const auto &target : targets.operands()) - modifies.insert(target); + modifies.insert(targets.operands().cbegin(), targets.operands().cend()); goto_programt assigns_havoc; havoc_assigns_targetst havoc_gen(modifies, ns); @@ -598,22 +672,64 @@ bool code_contractst::apply_function_contract( } void code_contractst::apply_loop_contract( - const irep_idt &function, + const irep_idt &function_name, goto_functionst::goto_functiont &goto_function) { local_may_aliast local_may_alias(goto_function); natural_loops_mutablet natural_loops(goto_function.body); - // Iterate over the (natural) loops in the function, - // and apply any invariant annotations that we find. + // A graph node type that stores information about a loop. + // We create a DAG representing nesting of various loops in goto_function, + // sort them topologically, and instrument them in the top-sorted order. + // + // The goal here is not avoid explicit "subset checks" on nested write sets. + // When instrumenting in a top-sorted order, + // the outer loop would no longer observe the inner loop's write set, + // but only corresponding `havoc` statements, + // which can be instrumented in the usual way to achieve a "subset check". + + struct loop_graph_nodet : public graph_nodet + { + typedef const goto_programt::targett &targett; + typedef const typename natural_loops_mutablet::loopt &loopt; + + targett target; + loopt loop; + + loop_graph_nodet(targett t, loopt l) : target(t), loop(l) + { + } + }; + grapht loop_nesting_graph; + for(const auto &loop : natural_loops.loop_map) + loop_nesting_graph.add_node(loop.first, loop.second); + + for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer) { + for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner) + { + if(inner == outer) + continue; + + if(loop_nesting_graph[outer].loop.contains( + loop_nesting_graph[inner].target)) + loop_nesting_graph.add_edge(outer, inner); + } + } + + // Iterate over the (natural) loops in the function, in topo-sorted order, + // and apply any loop contracts that we find. + for(const auto &idx : loop_nesting_graph.topsort()) + { + const auto &loop_node = loop_nesting_graph[idx]; check_apply_loop_contracts( + function_name, goto_function, local_may_alias, - loop.first, - loop.second, - symbol_table.lookup_ref(function).mode); + loop_node.target, + loop_node.loop, + symbol_table.lookup_ref(function_name).mode); } } @@ -636,7 +752,6 @@ void code_contractst::instrument_assign_statement( instruction_it->is_assign(), "The first instruction of instrument_assign_statement should always be" " an assignment"); - add_inclusion_check( program, assigns_clause, instruction_it, instruction_it->assign_lhs()); } @@ -726,7 +841,9 @@ void code_contractst::instrument_call_statement( alias_checking_instructions.destructive_append(skip_program); insert_before_swap_and_advance( - body, instruction_it, alias_checking_instructions); + body, + instruction_it, + add_pragma_disable_assigns_check(alias_checking_instructions)); // move past the call and then insert the invalidation instructions instruction_it++; @@ -758,7 +875,9 @@ void code_contractst::instrument_call_statement( invalidation_instructions.destructive_append(skip_program); insert_before_swap_and_advance( - body, instruction_it, invalidation_instructions); + body, + instruction_it, + add_pragma_disable_assigns_check(invalidation_instructions)); instruction_it--; } @@ -875,7 +994,11 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) // Insert aliasing assertions check_frame_conditions( - function_obj->first, function_obj->second.body, instruction_it, assigns); + function_obj->first, + function_obj->second.body, + instruction_it, + function_obj->second.body.instructions.end(), + assigns); return false; } @@ -883,13 +1006,22 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function) void code_contractst::check_frame_conditions( const irep_idt &function, goto_programt &body, - goto_programt::targett &instruction_it, + goto_programt::targett instruction_it, + const goto_programt::targett &instruction_end, assigns_clauset &assigns) { goto_function_inline(goto_functions, function, ns, log.get_message_handler()); - for(; instruction_it != body.instructions.end(); ++instruction_it) + for(; instruction_it != instruction_end; ++instruction_it) { + const auto &pragmas = instruction_it->source_location().get_pragmas(); + if(pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end()) + continue; + + // Do not instrument this instruction again in the future, + // since we are going to instrument it now below. + add_pragma_disable_assigns_check(*instruction_it); + if(instruction_it->is_decl()) { // grab the declared symbol @@ -942,8 +1074,8 @@ void code_contractst::check_frame_conditions( instruction_it->is_other() && instruction_it->get_other().get_statement() == ID_havoc_object) { - const exprt &havoc_argument = dereference_exprt( - to_typecast_expr(instruction_it->get_other().operands().front()).op()); + const auto havoc_argument = + pointer_object(instruction_it->get_other().operands().front()); add_inclusion_check(body, assigns, instruction_it, havoc_argument); } } diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index bd79f6e3b7c..08cc0080571 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -98,6 +98,7 @@ class code_contractst void apply_loop_contracts(); void check_apply_loop_contracts( + const irep_idt &function_name, goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, goto_programt::targett loop_head, @@ -130,7 +131,8 @@ class code_contractst void check_frame_conditions( const irep_idt &, goto_programt &, - goto_programt::targett &, + goto_programt::targett, + const goto_programt::targett &, assigns_clauset &); /// Inserts an assertion into the goto program to ensure that diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index b1c199229d5..c39cf81da43 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -14,6 +14,21 @@ Date: September 2021 #include #include +goto_programt::instructiont & +add_pragma_disable_assigns_check(goto_programt::instructiont &instr) +{ + instr.source_location_nonconst().add_pragma( + CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK); + return instr; +} + +goto_programt &add_pragma_disable_assigns_check(goto_programt &prog) +{ + Forall_goto_program_instructions(it, prog) + add_pragma_disable_assigns_check(*it); + return prog; +} + static void append_safe_havoc_code_for_expr( const source_locationt location, const namespacet &ns, diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h index 3be8c8f965d..70b691aec66 100644 --- a/src/goto-instrument/contracts/utils.h +++ b/src/goto-instrument/contracts/utils.h @@ -17,6 +17,8 @@ Date: September 2021 #include +#define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check" + /// \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 @@ -42,6 +44,20 @@ class havoc_if_validt : public havoc_utilst const namespacet &ns; }; +/// \brief Adds a pragma on a GOTO instruction to disable inclusion checking. +/// +/// \param instr: A mutable reference to the GOTO instruction. +/// \return The same reference after mutation (i.e., adding the pragma). +goto_programt::instructiont & +add_pragma_disable_assigns_check(goto_programt::instructiont &instr); + +/// \brief Adds pragmas on all instructions in a GOTO program +/// to disable inclusion checking on them. +/// +/// \param prog: A mutable reference to the GOTO program. +/// \return The same reference after mutation (i.e., adding the pragmas). +goto_programt &add_pragma_disable_assigns_check(goto_programt &prog); + /// \brief Generate a validity check over all dereferences in an expression /// /// This function generates a formula: diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index 25a50e3cb34..a488c4ae738 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -51,6 +51,10 @@ void get_modifies_lhs( for(const auto &mod : local_may_alias.get(t, ptr.pointer)) { const typecast_exprt typed_mod{mod, ptr.pointer.type()}; + if(mod.id() == ID_unknown) + { + throw analysis_exceptiont("Alias analysis returned UNKNOWN!"); + } if(ptr.offset.is_nil()) modifies.insert(dereference_exprt{typed_mod}); else diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index dbbd5e226dc..d5ccf182cd9 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -863,11 +863,15 @@ void goto_convertt::convert_loop_contracts( goto_programt::targett loop, const irep_idt &mode) { - exprt invariant = - static_cast(code.find(ID_C_spec_loop_invariant)); - exprt decreases_clause = - static_cast(code.find(ID_C_spec_decreases)); + auto assigns = static_cast(code.find(ID_C_spec_assigns)); + if(assigns.is_not_nil()) + { + PRECONDITION(loop->is_goto()); + loop->guard.add(ID_C_spec_assigns).swap(assigns.op()); + } + auto invariant = + static_cast(code.find(ID_C_spec_loop_invariant)); if(!invariant.is_nil()) { if(has_subexpr(invariant, ID_side_effect)) @@ -880,6 +884,8 @@ void goto_convertt::convert_loop_contracts( loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant); } + auto decreases_clause = + static_cast(code.find(ID_C_spec_decreases)); if(!decreases_clause.is_nil()) { if(has_subexpr(decreases_clause, ID_side_effect)) @@ -972,7 +978,7 @@ void goto_convertt::convert_for( goto_programt::targett y = tmp_y.add( goto_programt::make_goto(u, true_exprt(), code.source_location())); - // loop invariant and decreases clause + // assigns clause, loop invariant and decreases clause convert_loop_contracts(code, y, mode); dest.destructive_append(sideeffects); @@ -1030,7 +1036,7 @@ void goto_convertt::convert_while( goto_programt tmp_x; convert(code.body(), tmp_x, mode); - // loop invariant and decreases clause + // assigns clause, loop invariant and decreases clause convert_loop_contracts(code, y, mode); dest.destructive_append(tmp_branch); @@ -1099,7 +1105,7 @@ void goto_convertt::convert_dowhile( // y: if(c) goto w; y->complete_goto(w); - // loop invariant and decreases clause + // assigns_clause, loop invariant and decreases clause convert_loop_contracts(code, y, mode); dest.destructive_append(tmp_w);