diff --git a/regression/contracts-dfcc/detect_loop_locals/main.c b/regression/contracts-dfcc/detect_loop_locals/main.c new file mode 100644 index 00000000000..602df7f5db9 --- /dev/null +++ b/regression/contracts-dfcc/detect_loop_locals/main.c @@ -0,0 +1,12 @@ +#include + +int main() +{ + unsigned char *i = malloc(5); + + while(i != i + 5) + __CPROVER_loop_invariant(1 == 1) + { + const char lower = *i++; + } +} diff --git a/regression/contracts-dfcc/detect_loop_locals/test.desc b/regression/contracts-dfcc/detect_loop_locals/test.desc new file mode 100644 index 00000000000..b21adc093b0 --- /dev/null +++ b/regression/contracts-dfcc/detect_loop_locals/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.assigns.\d+\].*line 10 Check that i is assignable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks that loop local variables do not cause explicit checks. diff --git a/regression/contracts-dfcc/detect_loop_locals2/main.c b/regression/contracts-dfcc/detect_loop_locals2/main.c new file mode 100644 index 00000000000..fb37cf3442a --- /dev/null +++ b/regression/contracts-dfcc/detect_loop_locals2/main.c @@ -0,0 +1,28 @@ +static void foo() +{ + unsigned i; + + for(i = 0; i < 16; i++) + __CPROVER_loop_invariant(1 == 1) + { + int v = 1; + } +} + +static void bar() +{ + unsigned i; + + for(i = 0; i < 16; i++) + __CPROVER_loop_invariant(1 == 1) + { + int v = 1; + } +} + +int main() +{ + bar(); + foo(); + foo(); +} diff --git a/regression/contracts-dfcc/detect_loop_locals2/test.desc b/regression/contracts-dfcc/detect_loop_locals2/test.desc new file mode 100644 index 00000000000..fb410beef89 --- /dev/null +++ b/regression/contracts-dfcc/detect_loop_locals2/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[bar.assigns.\d+\].*Check that i is assignable: SUCCESS$ +^\[foo.assigns.\d+\].*Check that i is assignable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks that loop local variables do not cause explicit checks diff --git a/regression/contracts-dfcc/github_6168_infinite_unwinding_bug/main.c b/regression/contracts-dfcc/github_6168_infinite_unwinding_bug/main.c new file mode 100644 index 00000000000..c24c4aff133 --- /dev/null +++ b/regression/contracts-dfcc/github_6168_infinite_unwinding_bug/main.c @@ -0,0 +1,21 @@ +#include +#include + +static int adder(const int *a, const int *b) +{ + return (*a + *b); +} + +int main() +{ + int x = 1024; + + int (*local_adder)(const int *, const int *) = adder; + + while(x > 0) + __CPROVER_loop_invariant(1 == 1) + { + x += local_adder(&x, &x); // loop detection fails + //x += adder(&x, &x); // works fine + } +} diff --git a/regression/contracts-dfcc/github_6168_infinite_unwinding_bug/test.desc b/regression/contracts-dfcc/github_6168_infinite_unwinding_bug/test.desc new file mode 100644 index 00000000000..aeeb4d28589 --- /dev/null +++ b/regression/contracts-dfcc/github_6168_infinite_unwinding_bug/test.desc @@ -0,0 +1,13 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +^\[main.loop_assigns.\d+\] line 15 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 15 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 15 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 15 Check step was unwound for loop .*: SUCCESS$ +-- +-- +This is guarding against an issue described in https://github.com/diffblue/cbmc/issues/6168. diff --git a/regression/contracts-dfcc/history-index/main.c b/regression/contracts-dfcc/history-index/main.c new file mode 100644 index 00000000000..9fed4fd6868 --- /dev/null +++ b/regression/contracts-dfcc/history-index/main.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int i, n, x[10]; + __CPROVER_assume(x[0] == x[9]); + while(i < n) + __CPROVER_loop_invariant(x[0] == __CPROVER_loop_entry(x[0])) + { + x[0] = x[9] - 1; + x[0]++; + } + assert(x[0] == x[9]); +} diff --git a/regression/contracts-dfcc/history-index/test.desc b/regression/contracts-dfcc/history-index/test.desc new file mode 100644 index 00000000000..60d8e545ce3 --- /dev/null +++ b/regression/contracts-dfcc/history-index/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^Tracking history of index expressions is not supported yet\. +-- +This test checks that `ID_index` expressions are allowed within history variables. diff --git a/regression/contracts-dfcc/history-invalid/main.c b/regression/contracts-dfcc/history-invalid/main.c new file mode 100644 index 00000000000..77cd920c20f --- /dev/null +++ b/regression/contracts-dfcc/history-invalid/main.c @@ -0,0 +1,19 @@ +#include + +int foo(int x) +{ + return x; +} + +int main() +{ + int i, n, x[10]; + __CPROVER_assume(x[0] == x[9]); + while(i < n) + __CPROVER_loop_invariant(x[0] == __CPROVER_loop_entry(foo(x[0]))) + { + x[0] = x[9] - 1; + x[0]++; + } + assert(x[0] == x[9]); +} diff --git a/regression/contracts-dfcc/history-invalid/test.desc b/regression/contracts-dfcc/history-invalid/test.desc new file mode 100644 index 00000000000..ab2aceea1df --- /dev/null +++ b/regression/contracts-dfcc/history-invalid/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc --apply-loop-contracts +^main.c.* error: Tracking history of side_effect expressions is not supported yet.$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test ensures that expressions with side effect, such as function calls, +may not be used in history variables. diff --git a/regression/contracts-dfcc/invar_assigns_empty/main.c b/regression/contracts-dfcc/invar_assigns_empty/main.c new file mode 100644 index 00000000000..4a41b2ea796 --- /dev/null +++ b/regression/contracts-dfcc/invar_assigns_empty/main.c @@ -0,0 +1,9 @@ +#include + +int main() +{ + while(1 == 1) + __CPROVER_assigns() __CPROVER_loop_invariant(1 == 1) + { + } +} diff --git a/regression/contracts-dfcc/invar_assigns_empty/test.desc b/regression/contracts-dfcc/invar_assigns_empty/test.desc new file mode 100644 index 00000000000..d727a4b9573 --- /dev/null +++ b/regression/contracts-dfcc/invar_assigns_empty/test.desc @@ -0,0 +1,14 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 5 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 5 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 5 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 5 Check step was unwound for loop .*: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that empty assigns clause is supported +in loop contracts. diff --git a/regression/contracts-dfcc/invar_assigns_opt/main.c b/regression/contracts-dfcc/invar_assigns_opt/main.c new file mode 100644 index 00000000000..f58b52a7091 --- /dev/null +++ b/regression/contracts-dfcc/invar_assigns_opt/main.c @@ -0,0 +1,31 @@ +#include + +int main() +{ + foo(); +} + +int foo() +{ + int r1, s1 = 1; + __CPROVER_assume(r1 >= 0); + while(r1 > 0) + __CPROVER_loop_invariant(r1 >= 0 && s1 == 1) __CPROVER_decreases(r1) + { + s1 = 1; + r1--; + } + assert(r1 == 0); + + int r2, s2 = 1; + __CPROVER_assume(r2 >= 0); + while(r2 > 0) + __CPROVER_assigns(r2, s2) __CPROVER_loop_invariant(r2 >= 0 && s2 == 1) + __CPROVER_decreases(r2) + { + s2 = 1; + r2--; + } + assert(r2 == 0); + return 0; +} diff --git a/regression/contracts-dfcc/invar_assigns_opt/test.desc b/regression/contracts-dfcc/invar_assigns_opt/test.desc new file mode 100644 index 00000000000..cff1c82dbc4 --- /dev/null +++ b/regression/contracts-dfcc/invar_assigns_opt/test.desc @@ -0,0 +1,28 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[foo.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[foo.loop_invariant_base.\d+\] line 12 Check invariant before entry for loop .*: SUCCESS$ +^\[foo.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$ +^\[foo.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$ +^\[foo.loop_decreases.\d+\] line 12 Check variant decreases after step for loop .*: SUCCESS$ +^\[foo.loop_assigns.\d+\] line 22 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[foo.loop_assigns.\d+\] line 22 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[foo.loop_invariant_base.\d+\] line 22 Check invariant before entry for loop .*: SUCCESS$ +^\[foo.loop_invariant_base.\d+\] line 22 Check invariant before entry for loop .*: SUCCESS$ +^\[foo.loop_invariant_step.\d+\] line 22 Check invariant after step for loop .*: SUCCESS$ +^\[foo.loop_step_unwinding.\d+\] line 22 Check step was unwound for loop .*: SUCCESS$ +^\[foo.loop_decreases.\d+\] line 22 Check variant decreases after step for loop .*: SUCCESS$ +^\[foo.assertion.\d+\] .* assertion r1 == 0: SUCCESS$ +^\[foo.assigns.\d+\] .* Check that s2 is assignable: SUCCESS$ +^\[foo.assigns.\d+\] .* Check that r2 is assignable: SUCCESS$ +^\[foo.assertion.\d+\] .* assertion r2 == 0: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that adding assigns clause is optional +and that if a proof does not require it, then adding an +appropriate assigns clause does not lead to any +unexpected behavior. diff --git a/regression/contracts-dfcc/invar_check_break_fail/main.c b/regression/contracts-dfcc/invar_check_break_fail/main.c new file mode 100644 index 00000000000..938877b2788 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_break_fail/main.c @@ -0,0 +1,25 @@ +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + + while(r > 0) + __CPROVER_loop_invariant(r >= 0) + { + --r; + if(r <= 1) + { + break; + } + else + { + --r; + } + } + + assert(r == 0); + + return 0; +} diff --git a/regression/contracts-dfcc/invar_check_break_fail/test.desc b/regression/contracts-dfcc/invar_check_break_fail/test.desc new file mode 100644 index 00000000000..fc631b16d94 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_break_fail/test.desc @@ -0,0 +1,16 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion r == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +This test is expected to fail along the code path where r is an even integer +before entering the loop. +The program is simply incompatible with the desired property in this case -- +there is no loop invariant that can establish the required assertion. diff --git a/regression/contracts-dfcc/invar_check_break_pass/main.c b/regression/contracts-dfcc/invar_check_break_pass/main.c new file mode 100644 index 00000000000..c8eeb27e513 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_break_pass/main.c @@ -0,0 +1,28 @@ +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + + while(r > 0) + // clang-format off + __CPROVER_loop_invariant(r >= 0) + __CPROVER_decreases(r) + // clang-format on + { + --r; + if(r <= 1) + { + break; + } + else + { + --r; + } + } + + assert(r == 0 || r == 1); + + return 0; +} diff --git a/regression/contracts-dfcc/invar_check_break_pass/test.desc b/regression/contracts-dfcc/invar_check_break_pass/test.desc new file mode 100644 index 00000000000..296d3790c62 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_break_pass/test.desc @@ -0,0 +1,14 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion r == 0 || r == 1: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that conditionals and `break` are correctly handled. diff --git a/regression/contracts-dfcc/invar_check_continue/main.c b/regression/contracts-dfcc/invar_check_continue/main.c new file mode 100644 index 00000000000..c60b5233082 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_continue/main.c @@ -0,0 +1,28 @@ +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + + while(r > 0) + // clang-format off + __CPROVER_loop_invariant(r >= 0) + __CPROVER_decreases(r) + // clang-format on + { + --r; + if(r < 5) + { + continue; + } + else + { + --r; + } + } + + assert(r == 0); + + return 0; +} diff --git a/regression/contracts-dfcc/invar_check_continue/test.desc b/regression/contracts-dfcc/invar_check_continue/test.desc new file mode 100644 index 00000000000..d001a45151d --- /dev/null +++ b/regression/contracts-dfcc/invar_check_continue/test.desc @@ -0,0 +1,15 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that conditionals and `continue` are correctly handled. diff --git a/regression/contracts-dfcc/invar_check_large/main.c b/regression/contracts-dfcc/invar_check_large/main.c new file mode 100644 index 00000000000..8f817a3a8cb --- /dev/null +++ b/regression/contracts-dfcc/invar_check_large/main.c @@ -0,0 +1,98 @@ +#include + +void swap(int *a, int *b) +{ + *a ^= *b; + *b ^= *a; + *a ^= *b; +} + +int main() +{ + int arr0, arr1, arr2, arr3, arr4; + arr0 = 1; + arr1 = 2; + arr2 = 0; + arr3 = 4; + arr4 = 3; + int *arr[5] = {&arr0, &arr1, &arr2, &arr3, &arr4}; + int pivot = 2; + + int h = 5 - 1; + int l = 0; + int r = 1; + while(h > l) + // clang-format off + __CPROVER_assigns(arr0, arr1, arr2, arr3, arr4, h, l, r) + __CPROVER_loop_invariant( + // Turn off `clang-format` because it breaks the `==>` operator. + h >= l && + 0 <= l && l < 5 && + 0 <= h && h < 5 && + l <= r && r <= h && + (r == 0 ==> arr0 == pivot) && + (r == 1 ==> arr1 == pivot) && + (r == 2 ==> arr2 == pivot) && + (r == 3 ==> arr3 == pivot) && + (r == 4 ==> arr4 == pivot) && + (0 < l ==> arr0 <= pivot) && + (1 < l ==> arr1 <= pivot) && + (2 < l ==> arr2 <= pivot) && + (3 < l ==> arr3 <= pivot) && + (4 < l ==> arr4 <= pivot) && + (0 > h ==> arr0 >= pivot) && + (1 > h ==> arr1 >= pivot) && + (2 > h ==> arr2 >= pivot) && + (3 > h ==> arr3 >= pivot) && + (4 > h ==> arr4 >= pivot) + ) + __CPROVER_decreases(h - l) + // clang-format on + { + if(*(arr[h]) <= pivot && *(arr[l]) >= pivot) + { + swap(arr[h], arr[l]); + if(r == h) + { + r = l; + h--; + } + else if(r == l) + { + r = h; + l++; + } + else + { + h--; + l++; + } + } + else if(*(arr[h]) <= pivot) + { + l++; + } + else + { + h--; + } + } + + // Turn off `clang-format` because it breaks the `==>` operator. + /* clang-format off */ + assert(0 <= r && r < 5); + assert(*(arr[r]) == pivot); + assert(0 < r ==> arr0 <= pivot); + assert(1 < r ==> arr1 <= pivot); + assert(2 < r ==> arr2 <= pivot); + assert(3 < r ==> arr3 <= pivot); + assert(4 < r ==> arr4 <= pivot); + assert(0 > r ==> arr0 >= pivot); + assert(1 > r ==> arr1 >= pivot); + assert(2 > r ==> arr2 >= pivot); + assert(3 > r ==> arr3 >= pivot); + assert(4 > r ==> arr4 >= pivot); + /* clang-format on */ + + return r; +} diff --git a/regression/contracts-dfcc/invar_check_large/test.desc b/regression/contracts-dfcc/invar_check_large/test.desc new file mode 100644 index 00000000000..3ec6cea6e39 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_large/test.desc @@ -0,0 +1,28 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 24 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 24 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 24 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 24 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 24 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assertion.1\] .* assertion 0 <= r && r < 5: SUCCESS$ +^\[main.assertion.2\] .* assertion \*\(arr\[r\]\) == pivot: SUCCESS$ +^\[main.assertion.3\] .* assertion 0 < r ==> arr0 <= pivot: SUCCESS$ +^\[main.assertion.4\] .* assertion 1 < r ==> arr1 <= pivot: SUCCESS$ +^\[main.assertion.5\] .* assertion 2 < r ==> arr2 <= pivot: SUCCESS$ +^\[main.assertion.6\] .* assertion 3 < r ==> arr3 <= pivot: SUCCESS$ +^\[main.assertion.7\] .* assertion 4 < r ==> arr4 <= pivot: SUCCESS$ +^\[main.assertion.8\] .* assertion 0 > r ==> arr0 >= pivot: SUCCESS$ +^\[main.assertion.9\] .* assertion 1 > r ==> arr1 >= pivot: SUCCESS$ +^\[main.assertion.10\] .* assertion 2 > r ==> arr2 >= pivot: SUCCESS$ +^\[main.assertion.11\] .* assertion 3 > r ==> arr3 >= pivot: SUCCESS$ +^\[main.assertion.12\] .* assertion 4 > r ==> arr4 >= pivot: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks the invariant contracts on a larger problem --- in this case, +the partition function of quicksort, applied to a fixed-length array. +This serves as a stop-gap test until issues to do with quantifiers and +side-effects in loop invariants are fixed. diff --git a/regression/contracts-dfcc/invar_check_multiple_loops/main.c b/regression/contracts-dfcc/invar_check_multiple_loops/main.c new file mode 100644 index 00000000000..dea8557dd6e --- /dev/null +++ b/regression/contracts-dfcc/invar_check_multiple_loops/main.c @@ -0,0 +1,30 @@ +#include + +int main() +{ + int r, n, x, y; + __CPROVER_assume(n > 0 && x == y); + + for(r = 0; r < n; ++r) + // clang-format off + __CPROVER_loop_invariant(0 <= r && r <= n) + __CPROVER_loop_invariant(x == y + r) + __CPROVER_decreases(n - r) + // clang-format on + { + x++; + } + while(r > 0) + // clang-format off + __CPROVER_loop_invariant(r >= 0 && x == y + n + (n - r)) + __CPROVER_decreases(r) + // clang-format on + { + y--; + r--; + } + + assert(x == y + 2 * n); + + return 0; +} diff --git a/regression/contracts-dfcc/invar_check_multiple_loops/test.desc b/regression/contracts-dfcc/invar_check_multiple_loops/test.desc new file mode 100644 index 00000000000..a22224b1c4e --- /dev/null +++ b/regression/contracts-dfcc/invar_check_multiple_loops/test.desc @@ -0,0 +1,23 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+\] line 17 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 17 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 17 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 17 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 17 Check variant decreases after step for loop .*: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion x == y \+ 2 \* n: SUCCESS$ +^\[main.assigns.\d+\] line 8 Check that r is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 15 Check that x is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 23 Check that y is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 24 Check that r is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that multiple loops and `for` loops are correctly handled. diff --git a/regression/contracts-dfcc/invar_check_nested_loops/main.c b/regression/contracts-dfcc/invar_check_nested_loops/main.c new file mode 100644 index 00000000000..8ea27e7bd99 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_nested_loops/main.c @@ -0,0 +1,33 @@ +#include + +int main() +{ + int n, s = 0; + __CPROVER_assume(n >= 0); + + for(int i = 0; i < n; ++i) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= n && s == i) + __CPROVER_decreases(n - i) + // clang-format on + { + int a, b; + __CPROVER_assume(b >= 0 && a == b); + + while(a > 0) + // clang-format off + __CPROVER_loop_invariant(a >= 0 && s == i + (b - a)) + __CPROVER_decreases(a) + // clang-format on + { + s++; + a--; + } + + s -= (b - 1); + } + + assert(s == n); + + return 0; +} diff --git a/regression/contracts-dfcc/invar_check_nested_loops/test.desc b/regression/contracts-dfcc/invar_check_nested_loops/test.desc new file mode 100644 index 00000000000..f034a5efda6 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_nested_loops/test.desc @@ -0,0 +1,23 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+\] line 17 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 17 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 17 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 17 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 17 Check variant decreases after step for loop .*: SUCCESS$ +^\[main\.assigns\.\d+\].*line 23 Check that s is assignable: SUCCESS$ +^\[main\.assigns\.\d+\].*line 24 Check that a is assignable: SUCCESS$ +^\[main\.assigns\.\d+\].*line 27 Check that s is assignable: SUCCESS$ +^\[main\.assertion.\d+\] .* assertion s == n: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that nested loops, `for` loops, +and loop-local declarations of the index variable are correctly handled. diff --git a/regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c b/regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c new file mode 100644 index 00000000000..c6034daab31 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c @@ -0,0 +1,21 @@ +#include +#include + +void main() +{ + char *data = malloc(1); + *data = 42; + + unsigned i; + while(i > 0) + // clang-format off + __CPROVER_loop_invariant(*data == 42) + __CPROVER_decreases(i) + // clang-format on + { + *data = 42; + i--; + } + + assert(*data = 42); +} diff --git a/regression/contracts-dfcc/invar_check_pointer_modifies-01/test.desc b/regression/contracts-dfcc/invar_check_pointer_modifies-01/test.desc new file mode 100644 index 00000000000..859bc6b1006 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_pointer_modifies-01/test.desc @@ -0,0 +1,19 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts --pointer-check +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 10 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 10 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 10 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 10 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 10 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+] .* Check that \*data is assignable: SUCCESS$ +^\[main.assigns.\d+] .* Check that i is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion \*data = 42: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE +-- +This test checks that modifications to deref-ed pointers are correctly handled. +In such cases, pointers should not be havoc'ed, only the value should be. diff --git a/regression/contracts-dfcc/invar_check_pointer_modifies-02/main.c b/regression/contracts-dfcc/invar_check_pointer_modifies-02/main.c new file mode 100644 index 00000000000..03ae679af71 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_pointer_modifies-02/main.c @@ -0,0 +1,24 @@ +#include +#include + +void main() +{ + char *copy, *data = malloc(1); + + copy = data; + *data = 42; + + unsigned i; + while(i > 0) + // clang-format off + __CPROVER_loop_invariant(*data == 42) + __CPROVER_decreases(i) + // clang-format on + { + *data = 42; + i--; + } + + assert(data == copy); + assert(*copy = 42); +} diff --git a/regression/contracts-dfcc/invar_check_pointer_modifies-02/test.desc b/regression/contracts-dfcc/invar_check_pointer_modifies-02/test.desc new file mode 100644 index 00000000000..18c9d31cff2 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_pointer_modifies-02/test.desc @@ -0,0 +1,19 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts --pointer-check +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 12 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 12 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*data is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion data == copy: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion \*copy = 42: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE +-- +This test checks that modifications to aliased pointers are correctly handled. diff --git a/regression/contracts-dfcc/invar_check_sufficiency/main.c b/regression/contracts-dfcc/invar_check_sufficiency/main.c new file mode 100644 index 00000000000..667d3bdfd9e --- /dev/null +++ b/regression/contracts-dfcc/invar_check_sufficiency/main.c @@ -0,0 +1,20 @@ +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + + while(r > 0) + // clang-format off + __CPROVER_loop_invariant(r >= 0) + __CPROVER_decreases(r) + // clang-format on + { + --r; + } + + assert(r == 0); + + return 0; +} diff --git a/regression/contracts-dfcc/invar_check_sufficiency/test.desc b/regression/contracts-dfcc/invar_check_sufficiency/test.desc new file mode 100644 index 00000000000..df74671d0a1 --- /dev/null +++ b/regression/contracts-dfcc/invar_check_sufficiency/test.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main\.assertion\.1\] .* assertion r == 0: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that a loop invariant can be proven to be inductive, +and is used in conjunction with the negation of the loop guard +to establish the postcondition. diff --git a/regression/contracts-dfcc/invar_dynamic_struct_member/main.c b/regression/contracts-dfcc/invar_dynamic_struct_member/main.c new file mode 100644 index 00000000000..71af535f801 --- /dev/null +++ b/regression/contracts-dfcc/invar_dynamic_struct_member/main.c @@ -0,0 +1,30 @@ +typedef struct test +{ + int x; +} test; + +void main() +{ + struct test *t = malloc(sizeof(test)); + t->x = 0; + + unsigned n; + for(unsigned i = 0; i < n; ++i) + __CPROVER_loop_invariant(i <= n) + { + switch(i % 4) + { + case 0: + break; + + case 1: + case 2: + t->x += 1; + + default: + t->x += 2; + } + } + + assert(t->x == 0 || t->x == 1 || t->x == 2); +} diff --git a/regression/contracts-dfcc/invar_dynamic_struct_member/test.desc b/regression/contracts-dfcc/invar_dynamic_struct_member/test.desc new file mode 100644 index 00000000000..5346bc358b7 --- /dev/null +++ b/regression/contracts-dfcc/invar_dynamic_struct_member/test.desc @@ -0,0 +1,23 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 12 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 22 Check that t->x is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 25 Check that t->x is assignable: SUCCESS$ +^\[main.assertion.\d+\] line 29 assertion .*: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test checks that members of typedef'd and dynamically allocated structs +are correctly havoced when enforcing loop invariants. +The assertion is expected to fail when `t->x` is correctly havoced (so would be +set to a nondet value). +However, it `t->x` is not havoced then it stays at value `0` and would satisfy +the assertion when the loop is replaced by a single nondet iteration. + diff --git a/regression/contracts/invar_function-old_fail/main.c b/regression/contracts-dfcc/invar_function-old_fail/main.c similarity index 100% rename from regression/contracts/invar_function-old_fail/main.c rename to regression/contracts-dfcc/invar_function-old_fail/main.c diff --git a/regression/contracts/invar_function-old_fail/test.desc b/regression/contracts-dfcc/invar_function-old_fail/test.desc similarity index 85% rename from regression/contracts/invar_function-old_fail/test.desc rename to regression/contracts-dfcc/invar_function-old_fail/test.desc index 07f2ce0de84..17202031cdd 100644 --- a/regression/contracts/invar_function-old_fail/test.desc +++ b/regression/contracts-dfcc/invar_function-old_fail/test.desc @@ -1,6 +1,6 @@ CORE main.c ---apply-loop-contracts +--dfcc main --apply-loop-contracts ^main.c.* error: __CPROVER_old is not allowed in loop invariants.$ ^CONVERSION ERROR$ ^EXIT=(1|64)$ diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_array/main.c b/regression/contracts-dfcc/invar_havoc_dynamic_array/main.c new file mode 100644 index 00000000000..0aed03906df --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_array/main.c @@ -0,0 +1,22 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char *data = malloc(SIZE * sizeof(char)); + data[5] = 0; + + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_whole(data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + data[i] = 1; + } + + assert(data[5] == 0); + assert(data[5] == 1); +} diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_array/test.desc b/regression/contracts-dfcc/invar_havoc_dynamic_array/test.desc new file mode 100644 index 00000000000..e0d6bbf766c --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_array/test.desc @@ -0,0 +1,21 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 11 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 11 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 11 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 11 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$ +^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that dynamically allocated arrays +are correctly havoced when enforcing loop invariant contracts. +The `data[5] == 0` assertion is expected to fail since `data` is havoced. +The `data[5] == 1` assertion is also expected to fail since the invariant does +not reestablish the value for `data[5]`. diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c b/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c new file mode 100644 index 00000000000..10d2c7a1904 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/main.c @@ -0,0 +1,20 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char *data = malloc(SIZE * sizeof(char)); + data[1] = 0; + data[4] = 0; + + for(unsigned i = 0; i < SIZE; i++) + __CPROVER_loop_invariant(i <= SIZE) + { + data[1] = i; + } + + assert(data[1] == 0 || data[1] == 1); + assert(data[4] == 0); +} diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/test.desc new file mode 100644 index 00000000000..45c7baa0489 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/test.desc @@ -0,0 +1,22 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 12 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$ +^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that dynamically allocated arrays +are correctly havoced when enforcing loop invariant contracts. +The `data[1] == 0 || data[1] == 1` assertion is expected to fail since `data[1]` +is havoced and the invariant does not reestablish the value of `data[1]`. +However, the `data[4] == 0` assertion is expected to pass -- we should not havoc +the entire `data` array, if only a constant index if being modified. diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array/main.c b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array/main.c new file mode 100644 index 00000000000..6f047330589 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array/main.c @@ -0,0 +1,27 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char ***data = malloc(SIZE * sizeof(char **)); + for(unsigned i = 0; i < SIZE; i++) + { + data[i] = malloc(SIZE * sizeof(char *)); + for(unsigned j = 0; j < SIZE; j++) + data[i][j] = malloc(SIZE * sizeof(char)); + } + + data[1][2][3] = 0; + char *old_data123 = &(data[1][2][3]); + + for(unsigned i = 0; i < SIZE; i++) + __CPROVER_loop_invariant(i <= SIZE) + { + data[i][(i + 1) % SIZE][(i + 2) % SIZE] = 1; + } + + assert(__CPROVER_same_object(old_data123, &(data[1][2][3]))); + assert(data[1][2][3] == 0); +} diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array/test.desc b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array/test.desc new file mode 100644 index 00000000000..5efb01b6ead --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array/test.desc @@ -0,0 +1,26 @@ +KNOWNBUG +main.c +--dfcc main --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 __CPROVER_same_object(old_data123, &(data\[1\]\[2\]\[3\])): SUCCESS$ +^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that dynamically allocated multi +dimensional arrays are correctly havoced when enforcing invariant contracts. + +The `__CPROVER_same_object(old_data123, &(data[1][2][3]))` assertion is expected +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 #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-dfcc/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c new file mode 100644 index 00000000000..02f03ffa58f --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c @@ -0,0 +1,30 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char ***data = malloc(SIZE * sizeof(char **)); + for(unsigned i = 0; i < SIZE; i++) + { + data[i] = malloc(SIZE * sizeof(char *)); + for(unsigned j = 0; j < SIZE; j++) + data[i][j] = malloc(SIZE * sizeof(char)); + } + + data[1][2][3] = 0; + 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; + } + + assert(data[4][5][6] == 0); + assert(data[1][2][3] == 0); +} diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc new file mode 100644 index 00000000000..7ac33db5165 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc @@ -0,0 +1,23 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 19 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 19 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 19 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 19 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(.*)4\]\[(.*)5\]\[(.*)6\] is assignable: SUCCESS$ +^\[main.assertion.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ +^\[main.assertion.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that dynamically allocated multi +dimensional arrays are correctly havoced when enforcing invariant contracts. + +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. diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_partial_const_idx/main.c b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_partial_const_idx/main.c new file mode 100644 index 00000000000..16357fb74af --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_partial_const_idx/main.c @@ -0,0 +1,27 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char ***data = malloc(SIZE * sizeof(char **)); + for(unsigned i = 0; i < SIZE; i++) + { + data[i] = malloc(SIZE * sizeof(char *)); + for(unsigned j = 0; j < SIZE; j++) + data[i][j] = malloc(SIZE * sizeof(char)); + } + + data[1][2][3] = 0; + data[4][5][6] = 0; + + for(unsigned i = 0; i < SIZE; i++) + __CPROVER_loop_invariant(i <= SIZE) + { + data[4][i][6] = 1; + } + + assert(data[1][2][3] == 0); + assert(data[4][5][6] == 0); +} diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc new file mode 100644 index 00000000000..735d226142a --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc @@ -0,0 +1,27 @@ +KNOWNBUG +main.c +--dfcc main --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\[1\]\[2\]\[3\] == 0: FAILURE$ +^\[main.assertion.2\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that dynamically allocated multi +dimensional arrays are correctly havoced when enforcing invariant contracts. + +Here, both assertions are expected to fail -- the entire `data` array should +be havoced since we are assigning to a non-constant index. +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 #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-dfcc/invar_havoc_static_array/main.c b/regression/contracts-dfcc/invar_havoc_static_array/main.c new file mode 100644 index 00000000000..a1b3762bfc2 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_array/main.c @@ -0,0 +1,22 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char data[SIZE]; + data[5] = 0; + + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_whole(data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + data[i] = 1; + } + + assert(data[5] == 0); + assert(data[5] == 1); +} diff --git a/regression/contracts-dfcc/invar_havoc_static_array/test.desc b/regression/contracts-dfcc/invar_havoc_static_array/test.desc new file mode 100644 index 00000000000..4f49c1e7f5e --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_array/test.desc @@ -0,0 +1,21 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 11 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 11 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 11 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 11 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$ +^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that arrays are correctly havoced +when enforcing loop invariant contracts. +The `data[5] == 0` assertion is expected to fail since `data` is havoced. +The `data[5] == 1` assertion is also expected to fail since the invariant does +not reestablish the value for `data[5]`. diff --git a/regression/contracts-dfcc/invar_havoc_static_array_const_idx/main.c b/regression/contracts-dfcc/invar_havoc_static_array_const_idx/main.c new file mode 100644 index 00000000000..59c808555e4 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_array_const_idx/main.c @@ -0,0 +1,20 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char data[SIZE]; + data[1] = 0; + data[4] = 0; + + for(unsigned i = 0; i < SIZE; i++) + __CPROVER_loop_invariant(i <= SIZE) + { + data[1] = i; + } + + assert(data[1] == 0 || data[1] == 1); + assert(data[4] == 0); +} diff --git a/regression/contracts-dfcc/invar_havoc_static_array_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_static_array_const_idx/test.desc new file mode 100644 index 00000000000..303ea1596e1 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_array_const_idx/test.desc @@ -0,0 +1,22 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 12 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$ +^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that arrays are correctly havoced +when enforcing loop invariant contracts. +The `data[1] == 0 || data[1] == 1` assertion is expected to fail since `data[1]` +is havoced and the invariant does not reestablish the value of `data[1]`. +However, the `data[4] == 0` assertion is expected to pass -- we should not havoc +the entire `data` array, if only a constant index if being modified. diff --git a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array/main.c b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array/main.c new file mode 100644 index 00000000000..40064627023 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array/main.c @@ -0,0 +1,21 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char data[SIZE][SIZE][SIZE]; + + data[1][2][3] = 0; + char *old_data123 = &(data[1][2][3]); + + for(unsigned i = 0; i < SIZE; i++) + __CPROVER_loop_invariant(i <= SIZE) + { + data[i][(i + 1) % SIZE][(i + 2) % SIZE] = 1; + } + + assert(__CPROVER_same_object(old_data123, &(data[1][2][3]))); + assert(data[1][2][3] == 0); +} diff --git a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array/test.desc b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array/test.desc new file mode 100644 index 00000000000..ae30f637cc0 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array/test.desc @@ -0,0 +1,21 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion __CPROVER_same_object\(old_data123, &\(data\[1\]\[2\]\[3\]\)\): SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that multi dimensional arrays +are correctly havoced when enforcing invariant contracts. + +The `__CPROVER_same_object(old_data123, &(data[1][2][3]))` assertion is expected +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. diff --git a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/main.c b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/main.c new file mode 100644 index 00000000000..f07392269b7 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/main.c @@ -0,0 +1,21 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char data[SIZE][SIZE][SIZE]; + + data[1][2][3] = 0; + data[4][5][6] = 0; + + for(unsigned i = 0; i < SIZE; i++) + __CPROVER_loop_invariant(i <= SIZE) + { + data[4][5][6] = 1; + } + + assert(data[4][5][6] == 0); + assert(data[1][2][3] == 0); +} diff --git a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/test.desc new file mode 100644 index 00000000000..a94daab6908 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/test.desc @@ -0,0 +1,22 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)5\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ +^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that multi dimensional arrays +are correctly havoced when enforcing invariant contracts. + +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. diff --git a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/main.c b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/main.c new file mode 100644 index 00000000000..004d3c22ecc --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/main.c @@ -0,0 +1,22 @@ +#include +#include + +#define SIZE 8 + +void main() +{ + char data[SIZE][SIZE][SIZE]; + + data[1][2][3] = 0; + data[4][5][6] = 0; + + for(unsigned i = 0; i < SIZE; i++) + __CPROVER_assigns(i, __CPROVER_object_whole(data)) + __CPROVER_loop_invariant(i <= SIZE) + { + data[4][i][6] = 1; + } + + assert(data[1][2][3] == 0); + assert(data[4][5][6] == 0); +} diff --git a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc new file mode 100644 index 00000000000..96a251f3471 --- /dev/null +++ b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc @@ -0,0 +1,24 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)i\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$ +^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Test case related to issue #6020: it checks that multi dimensional arrays +are correctly havoced when enforcing invariant contracts. + +Here, both assertions are expected to fail -- the entire `data` array should +be havoced since we are assigning to a non-constant index. +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. diff --git a/regression/contracts-dfcc/invar_loop-entry_check/main.c b/regression/contracts-dfcc/invar_loop-entry_check/main.c new file mode 100644 index 00000000000..5e8b4bb5a00 --- /dev/null +++ b/regression/contracts-dfcc/invar_loop-entry_check/main.c @@ -0,0 +1,49 @@ +#include +#include + +typedef struct +{ + int *n; +} s; + +void main() +{ + int *x1, y1, z1; + x1 = &z1; + + while(y1 > 0) + __CPROVER_loop_invariant(*x1 == __CPROVER_loop_entry(*x1)) + { + --y1; + *x1 = *x1 + 1; + *x1 = *x1 - 1; + } + assert(*x1 == z1); + + int x2, y2, z2; + x2 = z2; + + while(y2 > 0) + __CPROVER_loop_invariant(x2 == __CPROVER_loop_entry(x2)) + { + --y2; + x2 = x2 + 1; + x2 = x2 - 1; + } + assert(x2 == z2); + + int y3; + s s0, s1, *s2 = &s0; + s2->n = malloc(sizeof(int)); + s1.n = s2->n; + + while(y3 > 0) + __CPROVER_loop_invariant(s2->n == __CPROVER_loop_entry(s2->n)) + { + --y3; + s0.n = s0.n + 1; + s2->n = s2->n - 1; + } + + assert(*(s1.n) == *(s2->n)); +} diff --git a/regression/contracts-dfcc/invar_loop-entry_check/test.desc b/regression/contracts-dfcc/invar_loop-entry_check/test.desc new file mode 100644 index 00000000000..80e2e4cc57a --- /dev/null +++ b/regression/contracts-dfcc/invar_loop-entry_check/test.desc @@ -0,0 +1,33 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts _ --pointer-primitive-check +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+] line 14 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+] line 14 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+] line 14 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+] line 14 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+] line 26 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+] line 26 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+] line 26 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+] line 26 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+] line 40 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+] line 40 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+] line 40 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+] line 40 Check step was unwound for loop .*: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion \*x1 == z1: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$ +^\[main.assigns.\d+\] .* Check that y1 is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 18 Check that \*x1 is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 19 Check that \*x1 is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that y2 is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 30 Check that x2 is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 31 Check that x2 is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that y3 is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s0\.n is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s2->n is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that __CPROVER_loop_entry is supported. diff --git a/regression/contracts-dfcc/invar_loop-entry_fail/main.c b/regression/contracts-dfcc/invar_loop-entry_fail/main.c new file mode 100644 index 00000000000..e902c8ab841 --- /dev/null +++ b/regression/contracts-dfcc/invar_loop-entry_fail/main.c @@ -0,0 +1,15 @@ +#include + +void main() +{ + int x, y, z; + x = z; + + while(y > 0) + __CPROVER_loop_invariant(x == __CPROVER_loop_entry(x)) + { + --y; + x = x + 1; + x = x - 2; + } +} diff --git a/regression/contracts-dfcc/invar_loop-entry_fail/test.desc b/regression/contracts-dfcc/invar_loop-entry_fail/test.desc new file mode 100644 index 00000000000..f3ef3571ce5 --- /dev/null +++ b/regression/contracts-dfcc/invar_loop-entry_fail/test.desc @@ -0,0 +1,16 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=(10|6)$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+] line 8 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+] line 8 Check invariant after step for loop .*: FAILURE$ +^\[main.loop_step_unwinding.\d+] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] line 11 Check that y is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 12 Check that x is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 13 Check that x is assignable: SUCCESS$ +^VERIFICATION FAILED$ +-- +-- +This test ensures that __CPROVER_loop_entry violations are checked. diff --git a/regression/contracts-dfcc/invar_loop_constant_fail/main.c b/regression/contracts-dfcc/invar_loop_constant_fail/main.c new file mode 100644 index 00000000000..c2085486cb6 --- /dev/null +++ b/regression/contracts-dfcc/invar_loop_constant_fail/main.c @@ -0,0 +1,18 @@ +#include + +int main() +{ + int r; + int s = 1; + __CPROVER_assume(r >= 0); + while(r > 0) + __CPROVER_loop_invariant(r >= 0) + { + s = 1; + r--; + } + assert(r == 0); + assert(s == 1); + + return 0; +} diff --git a/regression/contracts-dfcc/invar_loop_constant_fail/test.desc b/regression/contracts-dfcc/invar_loop_constant_fail/test.desc new file mode 100644 index 00000000000..ab42969a76d --- /dev/null +++ b/regression/contracts-dfcc/invar_loop_constant_fail/test.desc @@ -0,0 +1,24 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion s == 1: FAILURE$ +^VERIFICATION FAILED$ +-- +This test is expected to fail because it modifies a variable within a loop, +but attempts to check that it is "effectively constant" without asserting so +within the loop invariant. +The current implementation of `check_apply_invariant` correctly havocs all +variables that are modified within the loop. +The fact that a variable is "effectively constant" within a loop must be +established using an appropriate clause in the invariant. diff --git a/regression/contracts-dfcc/invar_loop_constant_no_modify/main.c b/regression/contracts-dfcc/invar_loop_constant_no_modify/main.c new file mode 100644 index 00000000000..3b03c7777d2 --- /dev/null +++ b/regression/contracts-dfcc/invar_loop_constant_no_modify/main.c @@ -0,0 +1,20 @@ +#include + +int main() +{ + int r; + int s = 1; + __CPROVER_assume(r >= 0); + while(r > 0) + // clang-format off + __CPROVER_loop_invariant(r >= 0) + __CPROVER_decreases(r) + // clang-format on + { + r--; + } + assert(r == 0); + assert(s == 1); + + return 0; +} diff --git a/regression/contracts-dfcc/invar_loop_constant_no_modify/test.desc b/regression/contracts-dfcc/invar_loop_constant_no_modify/test.desc new file mode 100644 index 00000000000..b5fe62eb1f7 --- /dev/null +++ b/regression/contracts-dfcc/invar_loop_constant_no_modify/test.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that variables that are not modified within the loop +are not unnecessarily havoced by `check_apply_invariant`. diff --git a/regression/contracts-dfcc/invar_loop_constant_pass/main.c b/regression/contracts-dfcc/invar_loop_constant_pass/main.c new file mode 100644 index 00000000000..fbb5cb3d88a --- /dev/null +++ b/regression/contracts-dfcc/invar_loop_constant_pass/main.c @@ -0,0 +1,20 @@ +#include + +int main() +{ + int r, s = 1; + __CPROVER_assume(r >= 0); + while(r > 0) + // clang-format off + __CPROVER_loop_invariant(r >= 0 && s == 1) + __CPROVER_decreases(r) + // clang-format on + { + s = 1; + r--; + } + assert(r == 0); + assert(s == 1); + + return 0; +} diff --git a/regression/contracts-dfcc/invar_loop_constant_pass/test.desc b/regression/contracts-dfcc/invar_loop_constant_pass/test.desc new file mode 100644 index 00000000000..a3e553eb30f --- /dev/null +++ b/regression/contracts-dfcc/invar_loop_constant_pass/test.desc @@ -0,0 +1,18 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 7 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 7 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 7 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 7 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 7 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that the invariant is correctly used to satisfy +all assertions that follow a loop. diff --git a/regression/contracts-dfcc/invar_loop_constant_pass/test_unwind.desc b/regression/contracts-dfcc/invar_loop_constant_pass/test_unwind.desc new file mode 100644 index 00000000000..b97a6be241a --- /dev/null +++ b/regression/contracts-dfcc/invar_loop_constant_pass/test_unwind.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts --unwind 1 --unwinding-assertions +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 7 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 7 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 7 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 7 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 7 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that s is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that there is no loop after contract transformation. diff --git a/regression/contracts-dfcc/invar_struct_member/main.c b/regression/contracts-dfcc/invar_struct_member/main.c new file mode 100644 index 00000000000..dc585980b22 --- /dev/null +++ b/regression/contracts-dfcc/invar_struct_member/main.c @@ -0,0 +1,19 @@ +struct test +{ + int x; +}; + +void main() +{ + struct test t; + t.x = 0; + + unsigned n; + for(unsigned i = 0; i < n; ++i) + __CPROVER_loop_invariant(i <= n) + { + t.x += 2; + } + + assert(t.x == 0 || t.x == 2); +} diff --git a/regression/contracts-dfcc/invar_struct_member/test.desc b/regression/contracts-dfcc/invar_struct_member/test.desc new file mode 100644 index 00000000000..e1fa9d91acc --- /dev/null +++ b/regression/contracts-dfcc/invar_struct_member/test.desc @@ -0,0 +1,21 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 12 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\].* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\].* Check that t\.x is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion t.x == 0 || t.x == 2: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test checks that members of statically allocated are correctly havoced +when enforcing loop invariants. +The `t.x == 0 || t.x == 2` assertion is expected to fail when `t.x` is correctly +havoced (so would be set to a nondet value). +However, it `t.x` is not havoced then it stays at value `0` and would satisfy +the assertion when the loop is replaced by a single nondet iteration. diff --git a/regression/contracts-dfcc/invariant_side_effects/main.c b/regression/contracts-dfcc/invariant_side_effects/main.c new file mode 100644 index 00000000000..b2000c05c06 --- /dev/null +++ b/regression/contracts-dfcc/invariant_side_effects/main.c @@ -0,0 +1,19 @@ +#include +#include + +int main() +{ + unsigned N, *a = malloc(sizeof(unsigned int)); + + *a = 0; + while(*a < N) + // clang-format off + __CPROVER_loop_invariant((0 <= *a) && (*a <= N)) + __CPROVER_decreases(N - *a) + // clang-format on + { + ++(*a); + } + + assert(*a == N); +} diff --git a/regression/contracts-dfcc/invariant_side_effects/test.desc b/regression/contracts-dfcc/invariant_side_effects/test.desc new file mode 100644 index 00000000000..342ce99c74e --- /dev/null +++ b/regression/contracts-dfcc/invariant_side_effects/test.desc @@ -0,0 +1,16 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 9 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 9 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 9 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*a is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion \*a == N: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +This test checks that C expressions are correctly converted to logic +when enforcing loop invariant annotations. diff --git a/regression/contracts-dfcc/labeled_loop_head/main.c b/regression/contracts-dfcc/labeled_loop_head/main.c new file mode 100644 index 00000000000..89e236870fb --- /dev/null +++ b/regression/contracts-dfcc/labeled_loop_head/main.c @@ -0,0 +1,12 @@ +int main() +{ + int x; + goto label; + x = 2; +label: + while(x < 5) + __CPROVER_loop_invariant(x <= 5) + { + x++; + } +} diff --git a/regression/contracts-dfcc/labeled_loop_head/test.desc b/regression/contracts-dfcc/labeled_loop_head/test.desc new file mode 100644 index 00000000000..d11b4fef1c7 --- /dev/null +++ b/regression/contracts-dfcc/labeled_loop_head/test.desc @@ -0,0 +1,14 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 7 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 7 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 7 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 7 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that x is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks transformed loop won't be skipped by a jump to the loop head. diff --git a/regression/contracts-dfcc/loop_assigns-01/main.c b/regression/contracts-dfcc/loop_assigns-01/main.c new file mode 100644 index 00000000000..1a515bcc350 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-01/main.c @@ -0,0 +1,32 @@ +#include +#include + +#define SIZE 8 + +struct blob +{ + char *data; +}; + +void main() +{ + foo(); +} + +void foo() +{ + 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_object_whole(b->data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts-dfcc/loop_assigns-01/test.desc b/regression/contracts-dfcc/loop_assigns-01/test.desc new file mode 100644 index 00000000000..df3c852612c --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-01/test.desc @@ -0,0 +1,18 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[foo.loop_assigns.\d+\] line 22 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[foo.loop_invariant_base.\d+\] line 22 Check invariant before entry for loop .*: SUCCESS$ +^\[foo.loop_invariant_step.\d+\] line 22 Check invariant after step for loop .*: SUCCESS$ +^\[foo.loop_step_unwinding.\d+\] line 22 Check step was unwound for loop .*: SUCCESS$ +^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[foo.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$ +^\[foo.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-dfcc/loop_assigns-02/main.c b/regression/contracts-dfcc/loop_assigns-02/main.c new file mode 100644 index 00000000000..d4b45140be3 --- /dev/null +++ b/regression/contracts-dfcc/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-dfcc/loop_assigns-02/test.desc b/regression/contracts-dfcc/loop_assigns-02/test.desc new file mode 100644 index 00000000000..100dfcb2dc7 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-02/test.desc @@ -0,0 +1,22 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 17 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 17 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 17 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 17 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] 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 us 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 so we expect +this to fail. diff --git a/regression/contracts-dfcc/loop_assigns-03/main.c b/regression/contracts-dfcc/loop_assigns-03/main.c new file mode 100644 index 00000000000..5f64342902d --- /dev/null +++ b/regression/contracts-dfcc/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_object_whole(b->data)) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } + + assert(b->data[5] == 0); +} diff --git a/regression/contracts-dfcc/loop_assigns-03/test.desc b/regression/contracts-dfcc/loop_assigns-03/test.desc new file mode 100644 index 00000000000..dcc78e2687a --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-03/test.desc @@ -0,0 +1,20 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 17 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 17 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 17 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 17 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: FAILURE$ +^\[main.assigns.\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-dfcc/loop_assigns-04/main.c b/regression/contracts-dfcc/loop_assigns-04/main.c new file mode 100644 index 00000000000..255d7aed40e --- /dev/null +++ b/regression/contracts-dfcc/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_object_whole(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-dfcc/loop_assigns-04/test.desc b/regression/contracts-dfcc/loop_assigns-04/test.desc new file mode 100644 index 00000000000..4c171095b11 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-04/test.desc @@ -0,0 +1,25 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 18 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 18 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 18 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 18 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+\] line 27 Check assigns clause inclusion for loop .*: FAILURE$ +^\[main.loop_invariant_base.\d+\] line 27 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 27 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 27 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[main.assigns.\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 `y` is also assigned in the loop and should be marked as assignable. diff --git a/regression/contracts-dfcc/loop_assigns-05/main.c b/regression/contracts-dfcc/loop_assigns-05/main.c new file mode 100644 index 00000000000..454aa2e4117 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-05/main.c @@ -0,0 +1,59 @@ +#include + +int j; + +int lowerbound() +{ + return 0; +} + +int upperbound() +{ + return 10; +} + +void incr(int *i) +{ + (*i)++; +} + +void body_1(int i) +{ + j = i; +} + +void body_2(int *i) +{ + (*i)++; + (*i)--; +} + +int body_3(int *i) +{ + (*i)++; + if(*i == 4) + return 1; + + (*i)--; + return 0; +} + +int main() +{ + for(int i = lowerbound(); i < upperbound(); incr(&i)) + // clang-format off + __CPROVER_assigns(i, j) + __CPROVER_loop_invariant(0 <= i && i <= 10) + __CPROVER_loop_invariant(i != 0 ==> j + 1 == i) + // clang-format on + { + body_1(i); + + if(body_3(&i)) + return 1; + + body_2(&i); + } + + assert(j == 9); +} diff --git a/regression/contracts-dfcc/loop_assigns-05/test.desc b/regression/contracts-dfcc/loop_assigns-05/test.desc new file mode 100644 index 00000000000..2b6b90eeb8e --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-05/test.desc @@ -0,0 +1,20 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.loop_assigns.\d+\] line 43 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 43 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 43 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 43 Check step was unwound for loop .*: SUCCESS$ +^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks write set inclusion checks in presence of function calls, +which are inlined, and also checks that DEAD instructions introduced during +inlining is correctly handled. diff --git a/regression/contracts-dfcc/loop_assigns-fail/main.c b/regression/contracts-dfcc/loop_assigns-fail/main.c new file mode 100644 index 00000000000..3f9ce1de467 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-fail/main.c @@ -0,0 +1,22 @@ +#include +#include + +#define SIZE 8 + +struct blob +{ + char *data; +}; + +void main() +{ + struct blob *b = malloc(sizeof(struct blob)); + b->data = malloc(SIZE); + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b->data[i] = 1; + } +} diff --git a/regression/contracts-dfcc/loop_assigns-fail/test.desc b/regression/contracts-dfcc/loop_assigns-fail/test.desc new file mode 100644 index 00000000000..069cdf5ae5c --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-fail/test.desc @@ -0,0 +1,13 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.assigns.\d+\] line 20 Check that b->data\[\(.*\)i\] is assignable: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test shows the need for assigns clauses on loops. The assigns the local may +alias analysis cannot identify the target of `b->data\[\(.*\)i\]` and assigns +clause inference computes an incomplete set of targets, +which makes the analysis fail with an assigns clause violation. diff --git a/regression/contracts-dfcc/loop_assigns-slice-assignable-ptr/main.c b/regression/contracts-dfcc/loop_assigns-slice-assignable-ptr/main.c new file mode 100644 index 00000000000..279ebc99de0 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-slice-assignable-ptr/main.c @@ -0,0 +1,43 @@ +#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 && + b->data == __CPROVER_loop_entry(b->data)) + // 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-dfcc/loop_assigns-slice-assignable-ptr/test.desc b/regression/contracts-dfcc/loop_assigns-slice-assignable-ptr/test.desc new file mode 100644 index 00000000000..039c33a6e20 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-slice-assignable-ptr/test.desc @@ -0,0 +1,20 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 24 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 24 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 24 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 24 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: 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: SUCCESS$ +^\[main.assertion.\d+\] .* assertion start <= b->data && b->data <= end: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +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-dfcc/loop_assigns-slice-assignable-scalar/main.c b/regression/contracts-dfcc/loop_assigns-slice-assignable-scalar/main.c new file mode 100644 index 00000000000..e3ec6910f8f --- /dev/null +++ b/regression/contracts-dfcc/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-dfcc/loop_assigns-slice-assignable-scalar/test.desc b/regression/contracts-dfcc/loop_assigns-slice-assignable-scalar/test.desc new file mode 100644 index 00000000000..65b6121277f --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-slice-assignable-scalar/test.desc @@ -0,0 +1,24 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 21 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 21 Check step was unwound for loop .*: 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.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-dfcc/loop_assigns-slice-from/main.c b/regression/contracts-dfcc/loop_assigns-slice-from/main.c new file mode 100644 index 00000000000..d75deef74cb --- /dev/null +++ b/regression/contracts-dfcc/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-dfcc/loop_assigns-slice-from/test.desc b/regression/contracts-dfcc/loop_assigns-slice-from/test.desc new file mode 100644 index 00000000000..7bd1ec33507 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-slice-from/test.desc @@ -0,0 +1,21 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 21 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 21 Check step was unwound for loop .*: 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: 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-dfcc/loop_assigns-slice-upto-fail/main.c b/regression/contracts-dfcc/loop_assigns-slice-upto-fail/main.c new file mode 100644 index 00000000000..2e59fe38975 --- /dev/null +++ b/regression/contracts-dfcc/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-dfcc/loop_assigns-slice-upto-fail/test.desc b/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc new file mode 100644 index 00000000000..06cd5cef0e7 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc @@ -0,0 +1,23 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 21 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 21 Check step was unwound for loop .*: 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-dfcc/loop_assigns-slice-upto-pass/main.c b/regression/contracts-dfcc/loop_assigns-slice-upto-pass/main.c new file mode 100644 index 00000000000..3922020407e --- /dev/null +++ b/regression/contracts-dfcc/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-dfcc/loop_assigns-slice-upto-pass/test.desc b/regression/contracts-dfcc/loop_assigns-slice-upto-pass/test.desc new file mode 100644 index 00000000000..413a2cb96c1 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns-slice-upto-pass/test.desc @@ -0,0 +1,20 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 21 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 21 Check step was unwound for loop .*: 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-dfcc/loop_assigns_inference-01/main.c b/regression/contracts-dfcc/loop_assigns_inference-01/main.c new file mode 100644 index 00000000000..88e8263aa59 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_inference-01/main.c @@ -0,0 +1,58 @@ +#include + +int j; + +int lowerbound() +{ + return 0; +} + +int upperbound() +{ + return 10; +} + +void incr(int *i) +{ + (*i)++; +} + +void body_1(int i) +{ + j = i; +} + +void body_2(int *i) +{ + (*i)++; + (*i)--; +} + +int body_3(int *i) +{ + (*i)++; + if(*i == 4) + return 1; + + (*i)--; + return 0; +} + +int main() +{ + for(int i = lowerbound(); i < upperbound(); incr(&i)) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= 10) + __CPROVER_loop_invariant(i != 0 ==> j + 1 == i) + // clang-format on + { + body_1(i); + + if(body_3(&i)) + return 1; + + body_2(&i); + } + + assert(j == 9); +} diff --git a/regression/contracts-dfcc/loop_assigns_inference-01/test.desc b/regression/contracts-dfcc/loop_assigns_inference-01/test.desc new file mode 100644 index 00000000000..da609994d99 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_inference-01/test.desc @@ -0,0 +1,18 @@ +KNOWNBUG +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ +^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ +^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks loop locals are correctly removed during assigns inference so +that the assign clause is correctly inferred. +This test failed when using dfcc for loop contracts. diff --git a/regression/contracts-dfcc/loop_assigns_inference-02/main.c b/regression/contracts-dfcc/loop_assigns_inference-02/main.c new file mode 100644 index 00000000000..063b47929ee --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_inference-02/main.c @@ -0,0 +1,20 @@ +#include + +#define SIZE 8 + +void main() +{ + foo(); +} + +void foo() +{ + int *b = malloc(SIZE * sizeof(int)); + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b[i] = 1; + } +} diff --git a/regression/contracts-dfcc/loop_assigns_inference-02/test.desc b/regression/contracts-dfcc/loop_assigns_inference-02/test.desc new file mode 100644 index 00000000000..50481eefadc --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_inference-02/test.desc @@ -0,0 +1,18 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$ +^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$ +^\[foo.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$ +^\[foo.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$ +^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[foo.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks assigns clauses (i, __CPROVER_object_whole(b)) is inferred, +and widened correctly. diff --git a/regression/contracts-dfcc/loop_assigns_inference-03/main.c b/regression/contracts-dfcc/loop_assigns_inference-03/main.c new file mode 100644 index 00000000000..c969cde10a0 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_inference-03/main.c @@ -0,0 +1,15 @@ +#include + +#define SIZE 8 + +void main() +{ + int b[SIZE]; + for(unsigned i = 0; i < SIZE; i++) + // clang-format off + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + b[i] = 1; + } +} diff --git a/regression/contracts-dfcc/loop_assigns_inference-03/test.desc b/regression/contracts-dfcc/loop_assigns_inference-03/test.desc new file mode 100644 index 00000000000..28b2c296deb --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_inference-03/test.desc @@ -0,0 +1,15 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that the assigns clause (i, __CPROVER_object_whole(b)) is inferred. diff --git a/regression/contracts-dfcc/loop_assigns_scoped_local_statics/main.c b/regression/contracts-dfcc/loop_assigns_scoped_local_statics/main.c new file mode 100644 index 00000000000..f8f93005f21 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_scoped_local_statics/main.c @@ -0,0 +1,91 @@ +#include + +int j; + +int before_loop() +{ + static int __static_local; + __static_local = 0; + return __static_local; +} + +int after_loop() +{ + static int __static_local; + __static_local = 0; + return __static_local; +} + +int lowerbound() +{ + static int __static_local; + __static_local = 0; + return 0; +} + +int upperbound() +{ + static int __static_local; + __static_local = 0; + return 10; +} + +void incr(int *i) +{ + static int __static_local; + __static_local = 0; + (*i)++; +} + +int body_1(int i) +{ + static int __static_local; + __static_local = 0; + j = i; + return __static_local; +} + +int body_2(int *i) +{ + static int __static_local; + __static_local = 0; + (*i)++; + (*i)--; + return __static_local; +} + +int body_3(int *i) +{ + static int __static_local; + __static_local = 0; + (*i)++; + if(*i == 4) + return 1; + + (*i)--; + return 0; +} + +int main() +{ + assert(before_loop() == 0); + + for(int i = lowerbound(); i < upperbound(); incr(&i)) + // clang-format off + __CPROVER_assigns(i, j) + __CPROVER_loop_invariant(0 <= i && i <= 10) + __CPROVER_loop_invariant(i != 0 ==> j + 1 == i) + // clang-format on + { + body_1(i); + + if(body_3(&i)) + return 1; + + body_2(&i); + } + + assert(j == 9); + assert(before_loop() == 0); + assert(after_loop() == 0); +} diff --git a/regression/contracts-dfcc/loop_assigns_scoped_local_statics/test.desc b/regression/contracts-dfcc/loop_assigns_scoped_local_statics/test.desc new file mode 100644 index 00000000000..88cece512ab --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_scoped_local_statics/test.desc @@ -0,0 +1,29 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$ +^\[body_1.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^\[body_2.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^\[body_3.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^\[incr.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^\[main.loop_assigns.\d+\] line 73 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 73 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 73 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 73 Check step was unwound for loop .*: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion after_loop\(\) == 0: SUCCESS$ +^\[upperbound.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks assigns clause checking presence of locally declared static +variables. +We observe that the local static variables declared within the loop's +scope are correctly gathered and added to the write set, +and are havoced (body_1 and body_2 do not return 0 anymore after the loop). diff --git a/regression/contracts-dfcc/loop_assigns_scoped_local_statics_propagate/main.c b/regression/contracts-dfcc/loop_assigns_scoped_local_statics_propagate/main.c new file mode 100644 index 00000000000..43098f62238 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_scoped_local_statics_propagate/main.c @@ -0,0 +1,46 @@ +#include +#include + +int j; + +int before_loop() +{ + static int __static_local; + __static_local = 0; + return __static_local; +} + +int after_loop() +{ + static int __static_local; + __static_local = 0; + return __static_local; +} + +int bar(int i) __CPROVER_requires(true) __CPROVER_ensures(j == i) + __CPROVER_assigns(j) +{ + static int __static_local; + __static_local = 0; + j = i; + return __static_local; +} + +int main() +{ + assert(before_loop() == 0); + + for(int i = 0; i < 10; i++) + // clang-format off + __CPROVER_assigns(i, j) + __CPROVER_loop_invariant(0 <= i && i <= 10) + __CPROVER_loop_invariant(i != 0 ==> j + 1 == i) + // clang-format on + { + bar(i); + } + + assert(j == 9); + assert(before_loop() == 0); + assert(after_loop() == 0); +} diff --git a/regression/contracts-dfcc/loop_assigns_scoped_local_statics_propagate/test.desc b/regression/contracts-dfcc/loop_assigns_scoped_local_statics_propagate/test.desc new file mode 100644 index 00000000000..722c4c15be1 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_scoped_local_statics_propagate/test.desc @@ -0,0 +1,22 @@ +CORE dfcc-only +main.c +--dfcc main --replace-call-with-contract bar --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 33 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 33 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 33 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 33 Check step was unwound for loop .*: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$ +^\[main.assigns.\d+\] line \d+ Check that i is assignable: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion j == 9: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$ +^\[main.assertion.\d+\] line \d+ assertion after_loop\(\) == 0: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks assigns clause checking presence of locally declared static +variables and loops. +We observe that the local static variables declared within the loop's +scope are correctly gathered and added to the write set, +and are havoced (body_1 and body_2 do not return 0 anymore after the loop). diff --git a/regression/contracts-dfcc/loop_assigns_target_base_idents/main.c b/regression/contracts-dfcc/loop_assigns_target_base_idents/main.c new file mode 100644 index 00000000000..a785111100b --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_target_base_idents/main.c @@ -0,0 +1,40 @@ +#include + +#define SIZE 32 +int foo() __CPROVER_assigns() +{ + char buf1[SIZE]; + char buf2[SIZE]; + char buf3[SIZE]; + size_t i = 0; + while(i < SIZE) + // clang-format off + __CPROVER_assigns( + i, + __CPROVER_object_whole(buf1), + __CPROVER_object_from(&buf2[10]), + *&buf3[10]) + __CPROVER_loop_invariant(i <= SIZE) + // clang-format on + { + buf1[i] = 0; // pass + buf1[SIZE - 1] = 0; // pass + + buf2[0] = 0; // fail + buf2[10] = 0; // pass + buf2[11] = 0; // pass + buf1[SIZE - 1] = 0; // pass + + buf3[0] = 0; // fail + buf3[9] = 0; // fail + buf3[10] = 0; // pass + buf3[11] = 0; // fail + buf3[SIZE - 1] = 0; // fail + i++; + } +} + +void main() +{ + foo(); +} diff --git a/regression/contracts-dfcc/loop_assigns_target_base_idents/test.desc b/regression/contracts-dfcc/loop_assigns_target_base_idents/test.desc new file mode 100644 index 00000000000..682eb3bd093 --- /dev/null +++ b/regression/contracts-dfcc/loop_assigns_target_base_idents/test.desc @@ -0,0 +1,33 @@ +CORE dfcc-only +main.c +--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo --apply-loop-contracts +^\[foo.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ +^\[foo.loop_assigns.\d+\] line .* Check assigns clause inclusion for loop foo.0: SUCCESS$ +^\[foo.loop_invariant_base.\d+\] line .* Check invariant before entry for loop foo.0: SUCCESS$ +^\[foo.loop_invariant_step.\d+\] line .* Check invariant after step for loop foo.0: SUCCESS$ +^\[foo.loop_step_unwinding.\d+\] line .* Check step was unwound for loop foo.0: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf1\[\(.*\)i\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf1\[\(.*\)\(32 - 1\)\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf2\[\(.*\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that buf2\[\(.*\)10\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf2\[\(.*\)11\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf1\[\(.*\)\(32 - 1\)\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)9\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)10\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)11\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)\(32 - 1\)\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that the optimisation that consists in not tracking locally +declared array symbols in the write set *not* kick in when said symbols are +assigned by a loop. This specifically tests the pattern matchin logic that is +used to identify the set of base symbols touched by an assigns clause target. +In particular the succesfull check +`[foo.assigns.*] Check assigns clause inclusion for loop foo.0` +shows that the targets listed in the loop's assigns clause are also found in the +function write set and hence explicitly tracked. diff --git a/regression/contracts-dfcc/loop_body_with_hole/main.c b/regression/contracts-dfcc/loop_body_with_hole/main.c new file mode 100644 index 00000000000..1ff6d65bbc3 --- /dev/null +++ b/regression/contracts-dfcc/loop_body_with_hole/main.c @@ -0,0 +1,22 @@ +#include +#include + +int main() +{ + unsigned n, k, sum_to_k = 0; + bool flag = false; + + for(unsigned i = 0; i < n; ++i) + // clang-format off + __CPROVER_assigns(i, sum_to_k) + __CPROVER_loop_invariant(0 <= i && i <= n) + // clang-format on + { + if(i == k) + { + flag = true; + break; + } + sum_to_k += i; + } +} diff --git a/regression/contracts-dfcc/loop_body_with_hole/test.desc b/regression/contracts-dfcc/loop_body_with_hole/test.desc new file mode 100644 index 00000000000..f737506492b --- /dev/null +++ b/regression/contracts-dfcc/loop_body_with_hole/test.desc @@ -0,0 +1,24 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.assigns.\d+\] line 6 Check that sum_to_k is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 7 Check that flag is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 9 Check that i is assignable: SUCCESS$ +^\[main.loop_assigns.\d+\] line 9 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 9 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 9 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] line 17 Check that flag is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 20 Check that sum_to_k is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test checks that we only instrument instructions contained in natural loops +against loop write sets. +The variable `flag` is not listed in the assigns clause of the loop. +The statement `flag = true;` is not part of the natural loop since it is only +executed once when breaking out of the loop. In the goto program this assignment +it is found between the loop head instruction and the loop latch instructions +it should not cause an loop assigns clause violation. diff --git a/regression/contracts-dfcc/loop_contracts_binary_search/main.c b/regression/contracts-dfcc/loop_contracts_binary_search/main.c new file mode 100644 index 00000000000..18a3cd67ff3 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_binary_search/main.c @@ -0,0 +1,41 @@ +#include +#include +#include + +#define NOT_FOUND (-1) + +int binary_search(int val, int *buf, int size) +{ + if(size <= 0 || buf == NULL) + return NOT_FOUND; + + int lb = 0, ub = size - 1; + int mid = ((unsigned int)lb + (unsigned int)ub) >> 1; + + while(lb <= ub) + // clang-format off + __CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size) + __CPROVER_loop_invariant(mid == ((unsigned int)lb + (unsigned int)ub) >> 1) + __CPROVER_decreases(ub - lb) + // clang-format on + { + if(buf[mid] == val) + break; + if(buf[mid] < val) + lb = mid + 1; + else + ub = mid - 1; + mid = ((unsigned int)lb + (unsigned int)ub) >> 1; + } + return lb > ub ? NOT_FOUND : mid; +} + +int main() +{ + int val, size; + int *buf = size >= 0 ? malloc(size * sizeof(int)) : NULL; + + int idx = binary_search(val, buf, size); + if(idx != NOT_FOUND) + assert(buf[idx] == val); +} diff --git a/regression/contracts-dfcc/loop_contracts_binary_search/test.desc b/regression/contracts-dfcc/loop_contracts_binary_search/test.desc new file mode 100644 index 00000000000..64b7be882dc --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_binary_search/test.desc @@ -0,0 +1,18 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts _ --pointer-check --bounds-check --signed-overflow-check +^EXIT=0$ +^SIGNAL=0$ +^\[binary_search.loop_assigns.\d+\] line 15 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[binary_search.loop_invariant_base.\d+\] line 15 Check invariant before entry for loop .*: SUCCESS$ +^\[binary_search.loop_invariant_step.\d+\] line 15 Check invariant after step for loop .*: SUCCESS$ +^\[binary_search.loop_step_unwinding.\d+\] line 15 Check step was unwound for loop .*: SUCCESS$ +^\[binary_search.loop_decreases.\d+\] line 15 Check variant decreases after step for loop .*: SUCCESS$ +^\[binary_search.assigns.\d+\] .* Check that lb is assignable: SUCCESS$ +^\[binary_search.assigns.\d+\] .* Check that ub is assignable: SUCCESS$ +^\[binary_search.assigns.\d+\] .* Check that mid is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] .* assertion buf\[idx\] == val: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test case verifies memory safety and termination of a binary search implementation. diff --git a/regression/contracts-dfcc/loop_contracts_do_while/main.c b/regression/contracts-dfcc/loop_contracts_do_while/main.c new file mode 100644 index 00000000000..88477df7fc2 --- /dev/null +++ b/regression/contracts-dfcc/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-dfcc/loop_contracts_do_while/test.desc b/regression/contracts-dfcc/loop_contracts_do_while/test.desc new file mode 100644 index 00000000000..dbe8bafe65d --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_do_while/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +main.c +--dfcc main --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-dfcc/loop_contracts_no_unwind/main.c b/regression/contracts-dfcc/loop_contracts_no_unwind/main.c new file mode 100644 index 00000000000..bff5fa3c56d --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_no_unwind/main.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int x = 0; + + while(x < 10) + __CPROVER_loop_invariant(0 <= x && x <= 10); + { + x++; + } + + assert(x == 10); +} diff --git a/regression/contracts-dfcc/loop_contracts_no_unwind/test.desc b/regression/contracts-dfcc/loop_contracts_no_unwind/test.desc new file mode 100644 index 00000000000..52a194a6c86 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_no_unwind/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts --loop-contracts-no-unwind _ --unwind 1 --unwinding-assertions +^EXIT=10$ +^SIGNAL=0$ +\[main.unwind.\d+\] line \d+ unwinding assertion loop 0: FAILURE +^VERIFICATION FAILED$ +-- +-- +Check that transformed loop will not be unwound with flag --loop-contracts-no-unwind. diff --git a/regression/contracts-dfcc/loop_contracts_reject_inner_loops_without_contracts/main.c b/regression/contracts-dfcc/loop_contracts_reject_inner_loops_without_contracts/main.c new file mode 100644 index 00000000000..05eb1b0d040 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_reject_inner_loops_without_contracts/main.c @@ -0,0 +1,17 @@ +int main() +{ + int i = 0, j = 0, k = 0; + + while(j < 10) + { + while(k < 10) + __CPROVER_loop_invariant(1 == 1) + { + while(i < 10) + { + i++; + } + } + j++; + } +} diff --git a/regression/contracts-dfcc/loop_contracts_reject_inner_loops_without_contracts/test.desc b/regression/contracts-dfcc/loop_contracts_reject_inner_loops_without_contracts/test.desc new file mode 100644 index 00000000000..4565f26d98f --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_reject_inner_loops_without_contracts/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^file main.c line 10 function main: Found loop without contract nested in a loop with a contract.$ +^Please provide a contract or unwind this loop before applying loop contracts.$ +^EXIT=(6|10)$ +^SIGNAL=0$ +-- +-- +This test checks that our loop contract instrumentation verifies that loops +nested in loops with contracts also have contracts. diff --git a/regression/contracts-dfcc/loop_contracts_reject_loops_instruction_not_in_head_latch/main.c b/regression/contracts-dfcc/loop_contracts_reject_loops_instruction_not_in_head_latch/main.c new file mode 100644 index 00000000000..91c12d62aa1 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_reject_loops_instruction_not_in_head_latch/main.c @@ -0,0 +1,18 @@ +void main() +{ + int i = 0; + +HEAD: + if(i > 5) + goto EXIT; + goto BODY; + +LATCH: + goto HEAD; + +BODY: + i++; + goto LATCH; + +EXIT:; +} diff --git a/regression/contracts-dfcc/loop_contracts_reject_loops_instruction_not_in_head_latch/test.desc b/regression/contracts-dfcc/loop_contracts_reject_loops_instruction_not_in_head_latch/test.desc new file mode 100644 index 00000000000..976633bb168 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_reject_loops_instruction_not_in_head_latch/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^Found loop body instruction outside of the \[head, latch\] instruction span$ +^EXIT=(6|10)$ +^SIGNAL=0$ +-- +-- +This test checks that our loop contract instrumentation verifies that loops +nested in loops with contracts also have contracts. diff --git a/regression/contracts-dfcc/loop_contracts_reject_loops_overlapping_spans/main.c b/regression/contracts-dfcc/loop_contracts_reject_loops_overlapping_spans/main.c new file mode 100644 index 00000000000..a059d7b1996 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_reject_loops_overlapping_spans/main.c @@ -0,0 +1,25 @@ +void main() +{ + int i = 0; + int j = 0; + +HEAD1: + if(i > 5) + goto EXIT1; + goto BODY1; + +EXIT1:; +HEAD2: + if(j > 5) + goto EXIT2; + goto BODY2; + +BODY1: + i++; + goto HEAD1; + +BODY2: + j++; + goto HEAD2; +EXIT2:; +} diff --git a/regression/contracts-dfcc/loop_contracts_reject_loops_overlapping_spans/test.desc b/regression/contracts-dfcc/loop_contracts_reject_loops_overlapping_spans/test.desc new file mode 100644 index 00000000000..4a1d8d5f70f --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_reject_loops_overlapping_spans/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^Found loops with overlapping instruction spans$ +^EXIT=(6|10)$ +^SIGNAL=0$ +-- +-- +This test checks that our loop contract instrumentation verifies that loops +nested in loops with contracts also have contracts. diff --git a/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/main.c b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/main.c new file mode 100644 index 00000000000..247b4ed32d6 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/main.c @@ -0,0 +1,19 @@ +#include + +void main() +{ + int i = 0; + int j = 0; + +HEAD: + if(i > 5) + goto EXIT1; + i++; + goto HEAD; +EXIT1:; + if(j > 5) + goto EXIT2; + j++; + goto HEAD; +EXIT2:; +} diff --git a/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc new file mode 100644 index 00000000000..0c2a66a7b05 --- /dev/null +++ b/regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc @@ -0,0 +1,10 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^Found loop with more than one latch instruction$ +^EXIT=(6|10)$ +^SIGNAL=0$ +-- +-- +This test checks that our loop contract instrumentation verifies that loops +nested in loops with contracts also have contracts. diff --git a/regression/contracts-dfcc/loop_guard_with_side_effects/main.c b/regression/contracts-dfcc/loop_guard_with_side_effects/main.c new file mode 100644 index 00000000000..868e83cd1c7 --- /dev/null +++ b/regression/contracts-dfcc/loop_guard_with_side_effects/main.c @@ -0,0 +1,29 @@ +#include +#include +#include + +bool check(unsigned *i, unsigned *j, unsigned *k) +{ + (*j)++; + return *i < *k; +} + +int main() +{ + unsigned i, j, k; + __CPROVER_assume(k < UINT_MAX); + + i = j = 0; + + while(check(&i, &j, &k)) + // clang-format off + __CPROVER_assigns(i, j) + __CPROVER_loop_invariant(0 <= i && i == j && i <= k) + // clang-format on + { + i++; + } + + assert(i == k); + assert(j == k + 1); +} diff --git a/regression/contracts-dfcc/loop_guard_with_side_effects/test.desc b/regression/contracts-dfcc/loop_guard_with_side_effects/test.desc new file mode 100644 index 00000000000..a469501d623 --- /dev/null +++ b/regression/contracts-dfcc/loop_guard_with_side_effects/test.desc @@ -0,0 +1,23 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts _ --unsigned-overflow-check +\[main.loop_assigns.\d+\] line 18 Check assigns clause inclusion for loop .*: SUCCESS$ +\[main.loop_invariant_base.\d+\] line 18 Check invariant before entry for loop .*: SUCCESS$ +\[main.loop_invariant_step.\d+\] line 18 Check invariant after step for loop .*: SUCCESS$ +\[main.loop_step_unwinding.\d+\] line 18 Check step was unwound for loop .*: SUCCESS$ +\[check.assigns.\d+\] line \d+ Check that \*j is assignable: SUCCESS$ +\[check.overflow.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS +\[check.overflow.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS +\[main.assigns.\d+\] line \d+ Check that i is assignable: SUCCESS$ +\[main.overflow.\d+\] line \d+ arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS +\[main.assertion.\d+\] line \d+ assertion i == k: SUCCESS$ +\[main.overflow.\d+\] line \d+ arithmetic overflow on unsigned \+ in k \+ \(unsigned int\)1: SUCCESS +\[main.assertion.\d+\] line \d+ assertion j == k \+ 1: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test demonstrates a case where the loop guard has side effects. +The loop contracts must specify the state of all modified variables, +including those in the loop guard. diff --git a/regression/contracts-dfcc/loop_guard_with_side_effects_fail/main.c b/regression/contracts-dfcc/loop_guard_with_side_effects_fail/main.c new file mode 100644 index 00000000000..7af53a31386 --- /dev/null +++ b/regression/contracts-dfcc/loop_guard_with_side_effects_fail/main.c @@ -0,0 +1,26 @@ +#include +#include + +bool check(unsigned *i, unsigned *j, unsigned *k) +{ + (*j)++; + return *i < *k; +} + +int main() +{ + unsigned i, j, k; + + i = j = 0; + + while(check(&i, &j, &k)) + // clang-format off + __CPROVER_assigns(i) + __CPROVER_loop_invariant(0 <= i && i <= k) + // clang-format on + { + i++; + } + + assert(i == k); +} diff --git a/regression/contracts-dfcc/loop_guard_with_side_effects_fail/test.desc b/regression/contracts-dfcc/loop_guard_with_side_effects_fail/test.desc new file mode 100644 index 00000000000..f3e8811d8ef --- /dev/null +++ b/regression/contracts-dfcc/loop_guard_with_side_effects_fail/test.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts _ --unsigned-overflow-check +\[main.loop_assigns.\d+\] line 16 Check assigns clause inclusion for loop .*: SUCCESS$ +\[main.loop_invariant_base.\d+\] line 16 Check invariant before entry for loop .*: SUCCESS$ +\[main.loop_invariant_step.\d+\] line 16 Check invariant after step for loop .*: SUCCESS$ +\[main.loop_step_unwinding.\d+\] line 16 Check step was unwound for loop .*: SUCCESS$ +\[check.assigns.\d+\] line \d+ Check that \*j is assignable: FAILURE$ +\[main.assigns.\d+\] line \d+ Check that i is assignable: SUCCESS$ +\[main.assertion.\d+\] line \d+ assertion i == k: SUCCESS$ +^EXIT=(6|10)$ +^SIGNAL=0$ +-- +-- +This test demonstrates a case where the loop guard has side effects. +The writes performed in the guard must also be specified +in the assigns clause of the loop. diff --git a/regression/contracts-dfcc/nonvacuous_loop_contracts/main.c b/regression/contracts-dfcc/nonvacuous_loop_contracts/main.c new file mode 100644 index 00000000000..876845e399f --- /dev/null +++ b/regression/contracts-dfcc/nonvacuous_loop_contracts/main.c @@ -0,0 +1,33 @@ +#include +#include + +int main() +{ + size_t size; + + char *buf = malloc(size); + char c; + + size_t start; + size_t end = start; + + while(end < size) + // clang-format off + __CPROVER_loop_invariant(start <= end && end <= size) + __CPROVER_decreases(size - end) + // clang-format on + { + if(buf[end] != c) + break; + end++; + } + + if(start > size) + { + assert(end == start); + } + else + { + assert(start <= end && end <= size); + } +} diff --git a/regression/contracts-dfcc/nonvacuous_loop_contracts/test.desc b/regression/contracts-dfcc/nonvacuous_loop_contracts/test.desc new file mode 100644 index 00000000000..d4c3ef6d197 --- /dev/null +++ b/regression/contracts-dfcc/nonvacuous_loop_contracts/test.desc @@ -0,0 +1,28 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts _ --signed-overflow-check --unsigned-overflow-check +^\[main.loop_assigns.\d+\] line 14 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 14 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 14 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 14 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 14 Check variant decreases after step for loop .*: SUCCESS$ +\[main.assigns.\d+\] line \d+ Check that end is assignable: SUCCESS$ +\[main.assertion.\d+\] line \d+ assertion end == start: SUCCESS$ +\[main.assertion.\d+\] line \d+ assertion start <= end && end <= size: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test demonstrates a simplification that is now possible on loop contracts. + +Prior to this commit, loop contracts were unconditionally applied on loops, +and thus had to also consider the case when the loop doesn't run even once. + +The contracts that were previously necessary were: + __CPROVER_loop_invariant( + (start > size && end == start) || (start <= end && end <= size) + ) + __CPROVER_decreases( + max(start, size) - end + ) diff --git a/regression/contracts-dfcc/quantifiers-loop-01/main.c b/regression/contracts-dfcc/quantifiers-loop-01/main.c new file mode 100644 index 00000000000..67287a83167 --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loop-01/main.c @@ -0,0 +1,30 @@ +#include + +#define N 16 + +void main() +{ + int a[N]; + a[10] = 0; + + for(int i = 0; i < N; ++i) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_whole(a)) + __CPROVER_loop_invariant( + (0 <= i) && (i <= N) && + __CPROVER_forall { + int k; + // constant bounds for explicit unrolling with SAT backend + (0 <= k && k <= N) ==> ( + // the actual symbolic bound for `k` + k < i ==> a[k] == 1 + ) + } + ) + // clang-format on + { + a[i] = 1; + } + + assert(a[10] == 1); +} diff --git a/regression/contracts-dfcc/quantifiers-loop-01/test.desc b/regression/contracts-dfcc/quantifiers-loop-01/test.desc new file mode 100644 index 00000000000..29c882f55b1 --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loop-01/test.desc @@ -0,0 +1,20 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 10 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 10 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 10 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 10 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] line .* assertion a\[10\] == 1: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +This test case checks the handling of a `forall` quantifier within a loop invariant. + +This test case uses explicit constant bounds on the quantified variable, +so that it can be unrolled (to conjunctions) with the SAT backend. diff --git a/regression/contracts-dfcc/quantifiers-loop-02/main.c b/regression/contracts-dfcc/quantifiers-loop-02/main.c new file mode 100644 index 00000000000..ca7b41d0ec5 --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loop-02/main.c @@ -0,0 +1,34 @@ +#include + +#define MAX_ARRAY_SIZE 3 +void main() +{ + int N, a[MAX_ARRAY_SIZE]; + __CPROVER_assume(0 <= N && N < MAX_ARRAY_SIZE); + + for(int i = 0; i < N; ++i) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_whole(a)) + __CPROVER_loop_invariant( + (0 <= i) && (i <= N) && + __CPROVER_forall { + int k; + (0 <= k && k < i) ==> a[k] == 1 + } + ) + // clang-format on + { + a[i] = 1; + } + + // clang-format off + assert(__CPROVER_forall { + int k; + (0 <= k && k < N) ==> a[k] == 1 + }); + // clang-format on + + int k; + __CPROVER_assume(0 <= k && k < N); + assert(a[k] == 1); +} diff --git a/regression/contracts-dfcc/quantifiers-loop-02/test.desc b/regression/contracts-dfcc/quantifiers-loop-02/test.desc new file mode 100644 index 00000000000..57e027c8708 --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loop-02/test.desc @@ -0,0 +1,24 @@ +CORE smt-backend broken-cprover-smt-backend thorough-smt-backend dfcc-only +main.c +--dfcc main --apply-loop-contracts _ --z3 +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 9 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_assigns.\d+\] line 9 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 9 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 9 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assertion.\d+\] line .* assertion .*: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This test case checks the handling of a universal quantifier, with a symbolic +upper bound, within a loop invariant. + +TODO: This test should: +- not use the `_ --z3` parameters: + once SMT-related tags are supported by the `Makefile`. diff --git a/regression/contracts-dfcc/quantifiers-loop-03/main.c b/regression/contracts-dfcc/quantifiers-loop-03/main.c new file mode 100644 index 00000000000..efd006cda80 --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loop-03/main.c @@ -0,0 +1,43 @@ +#include +#include + +#define MAX_SIZE 64 + +void main() +{ + unsigned N; + __CPROVER_assume(0 < N && N <= MAX_SIZE); + + int *a = malloc(N * sizeof(int)); + + for(int i = 0; i < N; ++i) + // clang-format off + __CPROVER_assigns(i, __CPROVER_object_whole(a)) + __CPROVER_loop_invariant( + (0 <= i) && (i <= N) && + (i != 0 ==> __CPROVER_exists { + int k; + // constant bounds for explicit unrolling with SAT backend + (0 <= k && k <= MAX_SIZE) && ( + // the actual symbolic bound for `k` + k < i && a[k] == 1 + ) + }) + ) + // clang-format on + { + a[i] = 1; + } + + // clang-format off + assert( + N != 0 ==> __CPROVER_exists { + int k; + // constant bounds for explicit unrolling with SAT backend + (0 <= k && k <= MAX_SIZE) && ( + // the actual symbolic bound for `k` + k < N && a[k] == 1 + ) + }); + // clang-format on +} diff --git a/regression/contracts-dfcc/quantifiers-loop-03/test.desc b/regression/contracts-dfcc/quantifiers-loop-03/test.desc new file mode 100644 index 00000000000..e71da9dd258 --- /dev/null +++ b/regression/contracts-dfcc/quantifiers-loop-03/test.desc @@ -0,0 +1,21 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^\[main.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main\.assertion\.\d+\] line .* assertion .*: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This test case checks the handling of an existential quantifier, with a symbolic +upper bound, within a loop invariant. + +This test case uses explicit constant bounds on the quantified variable, +so that it can be unrolled (to conjunctions) with the SAT backend. diff --git a/regression/contracts-dfcc/quicksort_contracts_01/main.c b/regression/contracts-dfcc/quicksort_contracts_01/main.c new file mode 100644 index 00000000000..1b0c3d6dbbb --- /dev/null +++ b/regression/contracts-dfcc/quicksort_contracts_01/main.c @@ -0,0 +1,157 @@ +// quicksort_contracts_01 + +// This test checks the correctness of a quicksort implementation using explicit +// ghost state. + +// This test currently fails for a variety of reasons, including: +// (1) Lack of support for quantifiers in ensures statements. +// (2) Lack of support for reading from memory in loop invariants (under some +// circumstances) + +#include +#include +#include + +void swap(int *a, int *b) +{ + *a ^= *b; + *b ^= *a; + *a ^= *b; +} + +int partition(int arr_ghost[], int arr[], int len) + __CPROVER_requires(__CPROVER_forall { + int i; + (0 <= i && i < len) == > arr_ghost[i] == arr[i] + } && len > 0 && 1 == 1) + __CPROVER_ensures( + __CPROVER_forall { + int i; + (0 <= i && i < len) == > __CPROVER_exists + { + int j; + 0 <= j &&j < len &&arr_ghost[i] == arr[j] + } + } && + __CPROVER_forall { + int i; + (0 <= i && i < len) == > __CPROVER_exists + { + int j; + 0 <= j &&j < len &&arr[i] == arr_ghost[j] + } + } && + 0 <= __CPROVER_return_value && __CPROVER_return_value < len && + __CPROVER_forall { + int i; + (0 <= i && i <= __CPROVER_return_value) == + > arr[i] <= arr[__CPROVER_return_value] + } && + __CPROVER_forall { + int i; + (__CPROVER_return_value <= i && i < len) == + > arr[__CPROVER_return_value] <= arr[i] + } && + 1 == 1) +{ + int h = len - 1; + int l = 0; + + int pivot_idx = len / 2; + int pivot = arr[pivot_idx]; + + while(h > l) + __CPROVER_loop_invariant( + 0 <= l && l <= pivot_idx && pivot_idx <= h && h < len && + arr[pivot_idx] == pivot && + __CPROVER_forall { + int i; + (0 <= i && i < l) == > arr[i] <= pivot + } && + __CPROVER_forall { + int i; + (h < i && i < len) == > pivot <= arr[i] + } && + 1 == 1) + { + if(arr[h] <= pivot && arr[l] >= pivot) + { + swap(arr + h, arr + l); + if(pivot_idx == h) + { + pivot_idx = l; + h--; + } + if(pivot_idx == l) + { + pivot_idx = h; + l++; + } + } + else if(arr[h] <= pivot) + { + l++; + } + else + { + h--; + } + } + return pivot_idx; +} + +void quicksort(int arr_ghost[], int arr[], int len) + __CPROVER_requires(__CPROVER_forall { + int i; + (0 <= i && i < len) == > arr_ghost[i] == arr[i] + } && 1 == 1) + __CPROVER_ensures( + __CPROVER_forall { + int i; + (0 <= i && i < len) == > __CPROVER_exists + { + int j; + 0 <= j &&j < len &&arr_ghost[i] == arr[j] + } + } && + __CPROVER_forall { + int i; + (0 <= i && i < len) == > __CPROVER_exists + { + int j; + 0 <= j &&j < len &&arr[i] == arr_ghost[j] + } + } && + __CPROVER_forall { + int i; + (0 <= i && i < len) == > __CPROVER_forall + { + int j; + (i <= j && j < len) == > arr[i] <= arr[j] + } + } && + 1 == 1) +{ + if(len <= 1) + { + return; + } + int *new_ghost = malloc(len * sizeof(int)); + memcpy(new_ghost, arr, len * sizeof(int)); + + int pivot_idx = partition(new_ghost, arr, len); + + memcpy(new_ghost, arr, len * sizeof(int)); + + quicksort(new_ghost, arr, pivot_idx); + quicksort(new_ghost, arr + pivot_idx + 1, len - pivot_idx - 1); + + free(new_ghost); +} + +int main() +{ + int arr[5] = {1, 2, 3, 0, 4}; + int arr_ghost[5] = {1, 2, 3, 0, 4}; + quicksort(arr_ghost, arr, 5); +} diff --git a/regression/contracts-dfcc/quicksort_contracts_01/test.desc b/regression/contracts-dfcc/quicksort_contracts_01/test.desc new file mode 100644 index 00000000000..c603af9274b --- /dev/null +++ b/regression/contracts-dfcc/quicksort_contracts_01/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c +--dfcc main --enforce-contract quicksort --enforce-contract partition --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Loop invariants are overzealous in deciding what counts as side effects. +Recursion is not supported for function contracts. diff --git a/regression/contracts-dfcc/recursive-function-and-loop-contracts/main.c b/regression/contracts-dfcc/recursive-function-and-loop-contracts/main.c new file mode 100644 index 00000000000..3e43e3333c7 --- /dev/null +++ b/regression/contracts-dfcc/recursive-function-and-loop-contracts/main.c @@ -0,0 +1,68 @@ +#include +#include +#include + +bool nondet_bool(); + +int foo(char *arr, const size_t size, size_t offset) + // clang-format off +__CPROVER_requires( 0 < size && offset <= size && __CPROVER_is_fresh(arr, size)) +__CPROVER_assigns(__CPROVER_object_whole(arr)) +// clang-format on +{ + if(offset == 0) + return 0; + + // recursive call + foo(arr, size, offset - 1); + + size_t i1 = offset; + while(i1 < size) + // clang-format off + __CPROVER_assigns(i1, __CPROVER_object_whole(arr)) + __CPROVER_loop_invariant(i1 <= size) + __CPROVER_decreases(size - i1) + // clang-format on + { + static int local_static = 0; + local_static = 1; + arr[i1] = 1; + size_t i2 = offset; + while(i2 < size) + //clang-format off + __CPROVER_assigns(i2, __CPROVER_object_whole(arr)) + __CPROVER_loop_invariant(i2 <= size) __CPROVER_decreases(size - i2) + //clang-format on + { + local_static = 2; + arr[i2] = 2; + i2++; + } + bool must_break = nondet_bool(); + if(must_break) + { + size_t i3 = offset; + while(i3 < size) + // clang-format off + __CPROVER_assigns(i3, __CPROVER_object_whole(arr)) + __CPROVER_loop_invariant(i3 <= size) + __CPROVER_decreases(size - i3) + // clang-format on + { + local_static = 3; + arr[i3] = 3; + i3++; + } + break; + } + i1++; + } +} + +int main() +{ + char *arr; + size_t size; + size_t offset; + foo(arr, size, offset); +} diff --git a/regression/contracts-dfcc/recursive-function-and-loop-contracts/test.desc b/regression/contracts-dfcc/recursive-function-and-loop-contracts/test.desc new file mode 100644 index 00000000000..0a595f0018c --- /dev/null +++ b/regression/contracts-dfcc/recursive-function-and-loop-contracts/test.desc @@ -0,0 +1,19 @@ +THOROUGH dfcc-only +main.c +--dfcc main --enforce-contract-rec foo --apply-loop-contracts --malloc-may-fail --malloc-fail-null _ --bounds-check --pointer-check --signed-overflow-check --unsigned-overflow-check --conversion-check --sat-solver cadical +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test illustrates the analysis of a function with a combination of features: +- the function is recursive +- the function contains loops +- the function assigns local static variables + +The following write set checks are performed: +- the write set of the recursive call is included in the caller'set +- the write set of each loop is included in the outer write set, either the + function's write set or some loop's write set) +- local statics are automatically detected and added to each write set +- the instructions are checked against their respective write sets diff --git a/regression/contracts-dfcc/ternary-lhs-loop-contract/main.c b/regression/contracts-dfcc/ternary-lhs-loop-contract/main.c new file mode 100644 index 00000000000..d1d40996523 --- /dev/null +++ b/regression/contracts-dfcc/ternary-lhs-loop-contract/main.c @@ -0,0 +1,25 @@ +#include +#include + +void foo(int a, int b) +{ + char arr1[10]; + char arr2[10]; + char arr3[10]; + int i = 0; + + while(i < 10) + __CPROVER_loop_invariant(0 <= i && i <= 10) + { + ((a > 0) ? arr1 : b > 0 ? arr2 : arr3)[i] = 0; + i++; + } +} + +int main() +{ + int a; + int b; + foo(a, b); + return 0; +} diff --git a/regression/contracts-dfcc/ternary-lhs-loop-contract/test.desc b/regression/contracts-dfcc/ternary-lhs-loop-contract/test.desc new file mode 100644 index 00000000000..3ff3417d81e --- /dev/null +++ b/regression/contracts-dfcc/ternary-lhs-loop-contract/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo --apply-loop-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +checks that when assignment lhs expressions have ternary expressions, +loop assigns clause checking correctly infers what gets assigned and +automatically tracks targets in the both the top level and the loop write sets. diff --git a/regression/contracts/variant_function_call_fail/main.c b/regression/contracts-dfcc/variant_function_call_fail/main.c similarity index 100% rename from regression/contracts/variant_function_call_fail/main.c rename to regression/contracts-dfcc/variant_function_call_fail/main.c diff --git a/regression/contracts/variant_function_call_fail/test.desc b/regression/contracts-dfcc/variant_function_call_fail/test.desc similarity index 85% rename from regression/contracts/variant_function_call_fail/test.desc rename to regression/contracts-dfcc/variant_function_call_fail/test.desc index 2fdfb1f8405..d1bff78a41a 100644 --- a/regression/contracts/variant_function_call_fail/test.desc +++ b/regression/contracts-dfcc/variant_function_call_fail/test.desc @@ -1,6 +1,6 @@ CORE main.c ---apply-loop-contracts +--dfcc main --apply-loop-contracts ^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$ ^EXIT=70$ ^SIGNAL=0$ @@ -8,7 +8,7 @@ main.c -- This test fails because the decreases clause contains a function call. Decreases clauses must not contain loops, since we want to ensure that the -calculation of decreases clauses will terminate. To enforce this requirement, -for now, we simply ban decreases clauses from containing function calls. +calculation of decreases clauses will terminate. To enforce this requirement, +for now, we simply ban decreases clauses from containing function calls. In the future, we may allow function calls (but definitely not loops) to appear -inside decreases clauses. +inside decreases clauses. diff --git a/regression/contracts-dfcc/variant_init_inside_loop/main.c b/regression/contracts-dfcc/variant_init_inside_loop/main.c new file mode 100644 index 00000000000..01c2e565ae3 --- /dev/null +++ b/regression/contracts-dfcc/variant_init_inside_loop/main.c @@ -0,0 +1,19 @@ +int main() +{ + unsigned start, max; + unsigned i = start; + + while(i < max) + // clang-format off + __CPROVER_loop_invariant( + (start > max && i == start) || + (start <= i && i <= max) + ) + __CPROVER_decreases(max - i) + // clang-format on + { + i++; + } + + return 0; +} diff --git a/regression/contracts-dfcc/variant_init_inside_loop/test.desc b/regression/contracts-dfcc/variant_init_inside_loop/test.desc new file mode 100644 index 00000000000..c18f5a4dfc5 --- /dev/null +++ b/regression/contracts-dfcc/variant_init_inside_loop/test.desc @@ -0,0 +1,22 @@ +CORE new-smt-backend dfcc-only +main.c +--dfcc main --apply-loop-contracts _ --unsigned-overflow-check +^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$ +^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$ +^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test checks that the decreases clause is evaluated only within the loop iteration, +not outside of it (before the loop guard). +The `main.overflow.1` check would fail if the decreases clause `(max - i)` is evaluated +before the loop guard is satisfied. This would occur when `start > max` and therefore +`i > max` after assuming the invariant. diff --git a/regression/contracts-dfcc/variant_missing_invariant_warning/main.c b/regression/contracts-dfcc/variant_missing_invariant_warning/main.c new file mode 100644 index 00000000000..2fa5b695d24 --- /dev/null +++ b/regression/contracts-dfcc/variant_missing_invariant_warning/main.c @@ -0,0 +1,13 @@ +int main() +{ + unsigned i = 10; + while(i != 0) + // clang-format off + __CPROVER_decreases(i) + // clang-format on + { + i--; + } + + return 0; +} diff --git a/regression/contracts-dfcc/variant_missing_invariant_warning/test.desc b/regression/contracts-dfcc/variant_missing_invariant_warning/test.desc new file mode 100644 index 00000000000..59de9351780 --- /dev/null +++ b/regression/contracts-dfcc/variant_missing_invariant_warning/test.desc @@ -0,0 +1,18 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +activate-multi-line-match +^No invariant provided for loop main.0 at file main.c line 4 function main. +^\[main.loop_assigns.\d+\] line 4 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 4 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 4 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 4 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 4 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test succeeds, but it gives a warning that the user has not provided a loop +invariant. Hence, a default loop invariant (i.e. true) will be used. diff --git a/regression/contracts-dfcc/variant_multi_instruction_loop_head/main.c b/regression/contracts-dfcc/variant_multi_instruction_loop_head/main.c new file mode 100644 index 00000000000..e20ca0d9402 --- /dev/null +++ b/regression/contracts-dfcc/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(0 <= *y && *y <= 10) + __CPROVER_decreases(10 - x) + // clang-format on + { + x++; + } +} diff --git a/regression/contracts-dfcc/variant_multi_instruction_loop_head/test.desc b/regression/contracts-dfcc/variant_multi_instruction_loop_head/test.desc new file mode 100644 index 00000000000..c692c7f3ffc --- /dev/null +++ b/regression/contracts-dfcc/variant_multi_instruction_loop_head/test.desc @@ -0,0 +1,16 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] line \d+ Check that x is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test checks that decreases clause is properly initialized +when the loop head and loop invariant compilation emit several goto instructions. diff --git a/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c b/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c new file mode 100644 index 00000000000..7f7e5c1be1f --- /dev/null +++ b/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c @@ -0,0 +1,39 @@ +#include + +int ackermann(int m, int n); + +int main() +{ + int m = 3; + int n = 5; + int result = ackermann(m, n); + + printf("Result of the Ackermann function: %d\n", result); + return 0; +} + +int ackermann(int m, int n) + // clang-format off +__CPROVER_requires(0 <= m && 0 <= n) +__CPROVER_ensures(__CPROVER_return_value >= 0) +// clang-format on +{ + while(m > 0) + // clang-format off + __CPROVER_loop_invariant(0 <= m && 0 <= n) + __CPROVER_decreases(m, n) + // clang-format on + { + if(n == 0) + { + m--; + n = 1; + } + else + { + n = ackermann(m, n - 1); + m--; + } + } + return n + 1; +} diff --git a/regression/contracts-dfcc/variant_multidimensional_ackermann/test.desc b/regression/contracts-dfcc/variant_multidimensional_ackermann/test.desc new file mode 100644 index 00000000000..ff5e6fa3ba2 --- /dev/null +++ b/regression/contracts-dfcc/variant_multidimensional_ackermann/test.desc @@ -0,0 +1,31 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts --replace-call-with-contract ackermann +^\[ackermann.precondition\.\d+\] line \d+ Check requires clause of contract contract\:\:ackermann for function ackermann: SUCCESS$ +^\[ackermann.assigns.\d+\] line \d+ Check that the assigns clause of contract\:\:ackermann is included in the caller\'s assigns clause: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +It tests whether we can prove (only partially) the termination of the Ackermann +function using a multidimensional decreases clause. + +Note that this particular implementation of the Ackermann function contains +both a while-loop and recursion. Therefore, to fully prove the termination of +the Ackermann function, we must prove both +(i) the termination of the while-loop and +(ii) the termination of the recursion. +Because CBMC does not support termination proofs of recursions (yet), we cannot +prove the latter, but the former. Hence, the termination proof in the code is +only "partial." + +Furthermore, the Ackermann function has a function contract that the result +is always non-negative. This post-condition is necessary for establishing +the loop invariant. However, in this test, we do not enforce the function +contract. Instead, we assume that the function contract is correct and use it +(i.e. replace a recursive call of the Ackermann function with its contract). + +We cannot verify/enforce the function contract of the Ackermann function, since +CBMC does not support function contracts for recursively defined functions. +As of now, CBMC only supports function contracts for non-recursive functions. diff --git a/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail1/main.c b/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail1/main.c new file mode 100644 index 00000000000..0bee402c26b --- /dev/null +++ b/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail1/main.c @@ -0,0 +1,22 @@ +int main() +{ + int i = 0; + int j = 0; + int N = 10; + while(i < N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N) + __CPROVER_decreases(N - i, j) + // clang-format on + { + if(j < N) + { + j++; + } + else + { + i++; + j = 0; + } + } +} diff --git a/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail1/test.desc b/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail1/test.desc new file mode 100644 index 00000000000..e464991bebe --- /dev/null +++ b/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail1/test.desc @@ -0,0 +1,19 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: FAILURE$ +^\[main.assigns.\d+\] line 14 Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 18 Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 19 Check that j is assignable: SUCCESS$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails because the given multidimensional decreases clause does not +monotonically decrease. A mistake is in the second component of the +decreases clause: j. It should instead be N - j. diff --git a/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail2/main.c b/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail2/main.c new file mode 100644 index 00000000000..bef032c8e4d --- /dev/null +++ b/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail2/main.c @@ -0,0 +1,22 @@ +int main() +{ + int i = 0; + int j = 0; + int N = 10; + while(i < N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N) + __CPROVER_decreases(i, N - j) + // clang-format on + { + if(j < N) + { + j++; + } + else + { + i++; + j = 0; + } + } +} diff --git a/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail2/test.desc b/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail2/test.desc new file mode 100644 index 00000000000..b2932da52cf --- /dev/null +++ b/regression/contracts-dfcc/variant_multidimensional_not_decreasing_fail2/test.desc @@ -0,0 +1,19 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: FAILURE$ +^\[main.assigns.\d+\] line 14 Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 18 Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 19 Check that j is assignable: SUCCESS$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails because the given multidimensional decreases clause does not +monotonically decrease. A mistake is in the first component of the +decreases clause: i. It should instead be N - i. diff --git a/regression/contracts-dfcc/variant_multidimensional_two_index_variables/main.c b/regression/contracts-dfcc/variant_multidimensional_two_index_variables/main.c new file mode 100644 index 00000000000..a4b889a03b4 --- /dev/null +++ b/regression/contracts-dfcc/variant_multidimensional_two_index_variables/main.c @@ -0,0 +1,22 @@ +int main() +{ + int i = 0; + int j = 0; + int N = 10; + while(i < N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N && 0 <= j && j <= N) + __CPROVER_decreases(N - i, N - j) + // clang-format on + { + if(j < N) + { + j++; + } + else + { + i++; + j = 0; + } + } +} diff --git a/regression/contracts-dfcc/variant_multidimensional_two_index_variables/test.desc b/regression/contracts-dfcc/variant_multidimensional_two_index_variables/test.desc new file mode 100644 index 00000000000..a96aefa4847 --- /dev/null +++ b/regression/contracts-dfcc/variant_multidimensional_two_index_variables/test.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] line 14 Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 18 Check that i is assignable: SUCCESS$ +^\[main.assigns.\d+\] line 19 Check that j is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +It tests whether a multidimensional decreases clause works properly. diff --git a/regression/contracts-dfcc/variant_not_decreasing_fail/main.c b/regression/contracts-dfcc/variant_not_decreasing_fail/main.c new file mode 100644 index 00000000000..a2913e961ac --- /dev/null +++ b/regression/contracts-dfcc/variant_not_decreasing_fail/main.c @@ -0,0 +1,16 @@ + +int main() +{ + int i = 0; + int N = 10; + while(i != N) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N) + __CPROVER_decreases(i) + // clang-format on + { + i++; + } + + return 0; +} diff --git a/regression/contracts-dfcc/variant_not_decreasing_fail/test.desc b/regression/contracts-dfcc/variant_not_decreasing_fail/test.desc new file mode 100644 index 00000000000..ac996f6baf6 --- /dev/null +++ b/regression/contracts-dfcc/variant_not_decreasing_fail/test.desc @@ -0,0 +1,15 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: FAILURE$ +^\[main.assigns.\d+] .* Check that i is assignable: SUCCESS$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails because the decreases clause is not monotinically decreasing. diff --git a/regression/contracts/variant_parsing_multiple_clauses_fail/main.c b/regression/contracts-dfcc/variant_parsing_multiple_clauses_fail/main.c similarity index 100% rename from regression/contracts/variant_parsing_multiple_clauses_fail/main.c rename to regression/contracts-dfcc/variant_parsing_multiple_clauses_fail/main.c diff --git a/regression/contracts/variant_parsing_multiple_clauses_fail/test.desc b/regression/contracts-dfcc/variant_parsing_multiple_clauses_fail/test.desc similarity index 85% rename from regression/contracts/variant_parsing_multiple_clauses_fail/test.desc rename to regression/contracts-dfcc/variant_parsing_multiple_clauses_fail/test.desc index 33fd4093a26..a4b414c242a 100644 --- a/regression/contracts/variant_parsing_multiple_clauses_fail/test.desc +++ b/regression/contracts-dfcc/variant_parsing_multiple_clauses_fail/test.desc @@ -1,6 +1,6 @@ CORE main.c ---apply-loop-contracts +--dfcc main --apply-loop-contracts activate-multi-line-match ^main.c.*error: syntax error before '__CPROVER_decreases'\n.*__CPROVER_decreases\(42\)$ ^PARSING ERROR$ @@ -12,5 +12,5 @@ This test fails because we have multiple decreases clauses. CBMC only admits one decreases clause for each loop. If one wants to write a multidimensional decreases clause, it should be placed inside a single __CPROVER_decreases(...), where each component of the multidimensional decreases clause is separated by a -comma. Hence, in this test, the correct syntax is +comma. Hence, in this test, the correct syntax is __CPROVER_decreases(N - i, 42). diff --git a/regression/contracts/variant_parsing_statement_fail/main.c b/regression/contracts-dfcc/variant_parsing_statement_fail/main.c similarity index 100% rename from regression/contracts/variant_parsing_statement_fail/main.c rename to regression/contracts-dfcc/variant_parsing_statement_fail/main.c diff --git a/regression/contracts/variant_parsing_statement_fail/test.desc b/regression/contracts-dfcc/variant_parsing_statement_fail/test.desc similarity index 86% rename from regression/contracts/variant_parsing_statement_fail/test.desc rename to regression/contracts-dfcc/variant_parsing_statement_fail/test.desc index 84fbc0df122..dedd24d0b5e 100644 --- a/regression/contracts/variant_parsing_statement_fail/test.desc +++ b/regression/contracts-dfcc/variant_parsing_statement_fail/test.desc @@ -1,6 +1,6 @@ CORE main.c ---apply-loop-contracts +--dfcc main --apply-loop-contracts activate-multi-line-match ^main.c.*error: syntax error before 'int'\n.*__CPROVER_decreases\(int x = 0\)$ ^PARSING ERROR$ @@ -8,6 +8,6 @@ activate-multi-line-match ^SIGNAL=0$ -- -- -This test fails because the decreases clause is a statement (more precisely, +This test fails because the decreases clause is a statement (more precisely, an assignment) rather than an expression (more precisely, an ACSL binding expression). diff --git a/regression/contracts/variant_side_effects_fail/main.c b/regression/contracts-dfcc/variant_side_effects_fail/main.c similarity index 100% rename from regression/contracts/variant_side_effects_fail/main.c rename to regression/contracts-dfcc/variant_side_effects_fail/main.c diff --git a/regression/contracts/variant_side_effects_fail/test.desc b/regression/contracts-dfcc/variant_side_effects_fail/test.desc similarity index 86% rename from regression/contracts/variant_side_effects_fail/test.desc rename to regression/contracts-dfcc/variant_side_effects_fail/test.desc index 6f6c47d36a6..7ce5cab0ce1 100644 --- a/regression/contracts/variant_side_effects_fail/test.desc +++ b/regression/contracts-dfcc/variant_side_effects_fail/test.desc @@ -1,6 +1,6 @@ CORE main.c ---apply-loop-contracts +--dfcc main --apply-loop-contracts ^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$ ^EXIT=70$ ^SIGNAL=0$ @@ -8,6 +8,6 @@ main.c -- This test fails because the decreases clause contains a side effect, namely incrementing variable N by zero. In this case, although the value of N -remains unchanged after the increment operation, we read from and write to N. -So this constitues a side effect. Decreases clauses are banned from containing -side effects, since decreases clauses should not modify program states. +remains unchanged after the increment operation, we read from and write to N. +So this constitues a side effect. Decreases clauses are banned from containing +side effects, since decreases clauses should not modify program states. diff --git a/regression/contracts-dfcc/variant_weak_invariant_fail/main.c b/regression/contracts-dfcc/variant_weak_invariant_fail/main.c new file mode 100644 index 00000000000..c9ab28d2403 --- /dev/null +++ b/regression/contracts-dfcc/variant_weak_invariant_fail/main.c @@ -0,0 +1,16 @@ + +int main() +{ + int i = 0; + int N = 10; + while(i != N) + // clang-format off + __CPROVER_loop_invariant(i <= N) + __CPROVER_decreases(N - i) + // clang-format on + { + i++; + } + + return 0; +} diff --git a/regression/contracts-dfcc/variant_weak_invariant_fail/test.desc b/regression/contracts-dfcc/variant_weak_invariant_fail/test.desc new file mode 100644 index 00000000000..bc34e845bae --- /dev/null +++ b/regression/contracts-dfcc/variant_weak_invariant_fail/test.desc @@ -0,0 +1,16 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: FAILURE$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This test fails because the loop invariant is not strong enough for the +termination proof. We must add 0 <= i to the loop invariant. diff --git a/regression/contracts-dfcc/variant_while_true_pass/main.c b/regression/contracts-dfcc/variant_while_true_pass/main.c new file mode 100644 index 00000000000..2684f85f885 --- /dev/null +++ b/regression/contracts-dfcc/variant_while_true_pass/main.c @@ -0,0 +1,20 @@ + +int main() +{ + int i = 0; + int N = 10; + while(1 == 1) + // clang-format off + __CPROVER_loop_invariant(0 <= i && i <= N) + __CPROVER_decreases(N - i) + // clang-format on + { + if(i == 10) + { + break; + } + i++; + } + + return 0; +} diff --git a/regression/contracts-dfcc/variant_while_true_pass/test.desc b/regression/contracts-dfcc/variant_while_true_pass/test.desc new file mode 100644 index 00000000000..949fe4e6362 --- /dev/null +++ b/regression/contracts-dfcc/variant_while_true_pass/test.desc @@ -0,0 +1,17 @@ +CORE dfcc-only +main.c +--dfcc main --apply-loop-contracts +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$ +^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$ +^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$ +^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$ +^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +The purpose of this test is to check whether a decreases clause can +successfully prove the termination of a loop (i) whose exit condition is +1 == 1 (i.e. true) and (ii) that will eventually exit via a break statement. diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index 15339efd454..e8407519334 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -38,7 +38,6 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include #include -#include #include #include #include @@ -122,6 +121,7 @@ void dfcc( const bool allow_recursive_calls, const std::set &to_replace, const bool apply_loop_contracts, + const bool unwind_transformed_loops, const std::set &to_exclude_from_nondet_static, message_handlert &message_handler) { @@ -138,6 +138,7 @@ void dfcc( allow_recursive_calls, to_replace_map, apply_loop_contracts, + unwind_transformed_loops, to_exclude_from_nondet_static, message_handler); } @@ -150,6 +151,7 @@ void dfcc( const bool allow_recursive_calls, const std::map &to_replace, const bool apply_loop_contracts, + const bool unwind_transformed_loops, const std::set &to_exclude_from_nondet_static, message_handlert &message_handler) { @@ -160,7 +162,8 @@ void dfcc( to_check, allow_recursive_calls, to_replace, - apply_loop_contracts, + dfcc_loop_contract_mode_from_bools( + apply_loop_contracts, unwind_transformed_loops), message_handler, to_exclude_from_nondet_static}; } @@ -172,7 +175,7 @@ dfcct::dfcct( const optionalt> &to_check, const bool allow_recursive_calls, const std::map &to_replace, - const bool apply_loop_contracts, + const dfcc_loop_contract_modet loop_contract_mode, message_handlert &message_handler, const std::set &to_exclude_from_nondet_static) : options(options), @@ -181,22 +184,23 @@ dfcct::dfcct( to_check(to_check), allow_recursive_calls(allow_recursive_calls), to_replace(to_replace), - apply_loop_contracts(apply_loop_contracts), + loop_contract_mode(loop_contract_mode), to_exclude_from_nondet_static(to_exclude_from_nondet_static), message_handler(message_handler), log(message_handler), utils(goto_model, message_handler), library(goto_model, utils, message_handler), ns(goto_model.symbol_table), - instrument(goto_model, message_handler, utils, library), - memory_predicates(goto_model, utils, library, instrument, message_handler), - spec_functions(goto_model, message_handler, utils, library, instrument), - contract_clauses_codegen( + spec_functions(goto_model, message_handler, utils, library), + contract_clauses_codegen(goto_model, message_handler, utils, library), + instrument( goto_model, message_handler, utils, library, - spec_functions), + spec_functions, + contract_clauses_codegen), + memory_predicates(goto_model, utils, library, instrument, message_handler), contract_handler( goto_model, message_handler, @@ -340,7 +344,7 @@ void dfcct::instrument_harness_function() << messaget::eom; instrument.instrument_harness_function( - harness_id, function_pointer_contracts); + harness_id, loop_contract_mode, function_pointer_contracts); other_symbols.erase(harness_id); } @@ -369,6 +373,7 @@ void dfcct::wrap_checked_function() << contract_id << "' in CHECK mode" << messaget::eom; swap_and_wrap.swap_and_wrap_check( + loop_contract_mode, wrapper_id, contract_id, function_pointer_contracts, @@ -377,7 +382,7 @@ void dfcct::wrap_checked_function() if(other_symbols.find(wrapper_id) != other_symbols.end()) other_symbols.erase(wrapper_id); - // upate max contract size + // update max contract size const std::size_t assigns_clause_size = contract_handler.get_assigns_clause_size(contract_id); if(assigns_clause_size > max_assigns_clause_size) @@ -485,20 +490,11 @@ void dfcct::instrument_other_functions() log.status() << "Instrumenting '" << function_id << "'" << messaget::eom; - instrument.instrument_function(function_id, function_pointer_contracts); + instrument.instrument_function( + function_id, loop_contract_mode, function_pointer_contracts); } goto_model.goto_functions.update(); - - // TODO specialise the library functions for the max size of - // loop and function contracts - if(to_check.has_value()) - { - log.status() << "Specializing cprover_contracts functions for assigns " - "clauses of at most " - << max_assigns_clause_size << " targets" << messaget::eom; - library.specialize(max_assigns_clause_size); - } } void dfcct::transform_goto_model() @@ -511,6 +507,17 @@ void dfcct::transform_goto_model() wrap_replaced_functions(); wrap_discovered_function_pointer_contracts(); instrument_other_functions(); + + // take the max of function of loop contracts assigns clauses + auto assigns_clause_size = instrument.get_max_assigns_clause_size(); + if(assigns_clause_size > max_assigns_clause_size) + max_assigns_clause_size = assigns_clause_size; + + log.status() << "Specializing cprover_contracts functions for assigns " + "clauses of at most " + << max_assigns_clause_size << " targets" << messaget::eom; + library.specialize(max_assigns_clause_size); + library.inhibit_front_end_builtins(); // TODO implement a means to inhibit unreachable functions (possibly via the diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.h b/src/goto-instrument/contracts/dynamic-frames/dfcc.h index 93c45dcb1b3..83ff4b8a2b7 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.h @@ -38,6 +38,7 @@ Author: Remi Delmas, delmasrd@amazon.com #include "dfcc_instrument.h" #include "dfcc_library.h" #include "dfcc_lift_memory_predicates.h" +#include "dfcc_loop_contract_mode.h" #include "dfcc_spec_functions.h" #include "dfcc_swap_and_wrap.h" #include "dfcc_utils.h" @@ -50,7 +51,6 @@ class messaget; class message_handlert; class symbolt; class conditional_target_group_exprt; -class cfg_infot; class optionst; #define FLAG_DFCC "dfcc" @@ -58,9 +58,9 @@ class optionst; // clang-format off #define HELP_DFCC \ - " --dfcc activate dynamic frame condition checking\n"\ - " for function contracts using the given\n"\ - " harness as entry point\n" + " --dfcc activate dynamic frame condition checking\n" \ + " for contracts using the given harness as\n" \ + " entry point\n" #define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec" #define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):" @@ -100,6 +100,8 @@ class invalid_function_contract_pair_exceptiont : public cprover_exception_baset /// \param allow_recursive_calls Allow the checked function to be recursive /// \param to_replace set of functions to replace with their contract /// \param apply_loop_contracts apply loop contract transformations iff true +/// \param unwind_transformed_loops unwind transformed loops after applying loop +/// contracts. /// \param to_exclude_from_nondet_static set of symbols to exclude when havocing /// static program symbols. /// \param message_handler used for debug/warning/error messages @@ -111,6 +113,7 @@ void dfcc( const bool allow_recursive_calls, const std::set &to_replace, const bool apply_loop_contracts, + const bool unwind_transformed_loops, const std::set &to_exclude_from_nondet_static, message_handlert &message_handler); @@ -129,7 +132,9 @@ void dfcc( /// \param to_check (function,contract) pair for contract checking /// \param allow_recursive_calls Allow the checked function to be recursive /// \param to_replace Functions-to-contract mapping for replacement -/// \param apply_loop_contracts Spply loop contract transformations iff true +/// \param apply_loop_contracts Apply loop contract transformations iff true +/// \param unwind_transformed_loops unwind transformed loops after applying loop +/// contracts. /// \param to_exclude_from_nondet_static Set of symbols to exclude when havocing /// static program symbols. /// \param message_handler used for debug/warning/error messages @@ -141,6 +146,7 @@ void dfcc( const bool allow_recursive_calls, const std::map &to_replace, const bool apply_loop_contracts, + const bool unwind_transformed_loops, const std::set &to_exclude_from_nondet_static, message_handlert &message_handler); @@ -157,8 +163,7 @@ class dfcct /// \param to_check (function,contract) pair for contract checking /// \param allow_recursive_calls Allow the checked function to be recursive /// \param to_replace functions-to-contract mapping for replacement - /// \param apply_loop_contracts apply loop contract transformations iff true - /// havocing static program symbols. + /// \param loop_contract_mode mode to use for loop contracts /// \param message_handler used for debug/warning/error messages /// \param to_exclude_from_nondet_static set of symbols to exclude when dfcct( @@ -168,7 +173,7 @@ class dfcct const optionalt> &to_check, const bool allow_recursive_calls, const std::map &to_replace, - const bool apply_loop_contracts, + const dfcc_loop_contract_modet loop_contract_mode, message_handlert &message_handler, const std::set &to_exclude_from_nondet_static); @@ -194,7 +199,7 @@ class dfcct /// (replacement mode) /// - instrument all remaining functions GOTO model /// - (this includes standard library functions). - /// - specialise the instrumentation functions by unwiding loops they contain + /// - specialise the instrumentation functions by unwinding loops they contain /// to the maximum size of any assigns clause involved in the model. void transform_goto_model(); @@ -205,7 +210,7 @@ class dfcct const optionalt> &to_check; const bool allow_recursive_calls; const std::map &to_replace; - const bool apply_loop_contracts; + const dfcc_loop_contract_modet loop_contract_mode; const std::set &to_exclude_from_nondet_static; message_handlert &message_handler; messaget log; @@ -215,10 +220,10 @@ class dfcct dfcc_utilst utils; dfcc_libraryt library; namespacet ns; - dfcc_instrumentt instrument; - dfcc_lift_memory_predicatest memory_predicates; dfcc_spec_functionst spec_functions; dfcc_contract_clauses_codegent contract_clauses_codegen; + dfcc_instrumentt instrument; + dfcc_lift_memory_predicatest memory_predicates; dfcc_contract_handlert contract_handler; dfcc_swap_and_wrapt swap_and_wrap; @@ -277,7 +282,7 @@ class dfcct /// for each instrumented function /// /// A call to `nondet_static` will re-generate the initialize function with - /// nondet values. The intrumentation statics will not get nondet initialised + /// nondet values. The instrumentation statics will not get nondet initialised /// by virtue of being tagged with ID_C_no_nondet_initialization. /// /// However, nondet_static expects instructions to be either function calls diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp index 2a961778dbe..e18b949ed3c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp @@ -8,11 +8,13 @@ Date: February 2023 \*******************************************************************/ #include "dfcc_contract_clauses_codegen.h" +#include #include #include #include #include #include +#include #include #include @@ -23,21 +25,18 @@ Date: February 2023 #include #include "dfcc_library.h" -#include "dfcc_spec_functions.h" #include "dfcc_utils.h" dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent( goto_modelt &goto_model, message_handlert &message_handler, dfcc_utilst &utils, - dfcc_libraryt &library, - dfcc_spec_functionst &spec_functions) + dfcc_libraryt &library) : goto_model(goto_model), message_handler(message_handler), log(message_handler), utils(utils), library(library), - spec_functions(spec_functions), ns(goto_model.symbol_table) { } @@ -63,6 +62,7 @@ void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions( // inline resulting program and check for loops inline_and_check_warnings(dest); + dest.update(); PRECONDITION_WITH_DIAGNOSTICS( is_loop_free(dest, ns, log), "loops in assigns clause specification functions must be unwound before " diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h index c3a8b2709dd..4609569a1d6 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h @@ -29,25 +29,23 @@ class goto_modelt; class message_handlert; class dfcc_libraryt; class dfcc_utilst; -class dfcc_spec_functionst; class code_with_contract_typet; class conditional_target_group_exprt; +/// Translates assigns and frees clauses of a function contract or +/// loop contract into GOTO programs that build write sets or havoc write sets. class dfcc_contract_clauses_codegent { public: - /// \param goto_model goto model being transformed - /// \param message_handler used debug/warning/error messages - /// \param utils utility class for dynamic frames - /// \param library the contracts instrumentation library - /// \param spec_functions provides translation methods for assignable set - /// or freeable set specification functions. + /// \param goto_model GOTO model being transformed + /// \param message_handler Used debug/warning/error messages + /// \param utils Utility class for dynamic frames + /// \param library The contracts instrumentation library dfcc_contract_clauses_codegent( goto_modelt &goto_model, message_handlert &message_handler, dfcc_utilst &utils, - dfcc_libraryt &library, - dfcc_spec_functionst &spec_functions); + dfcc_libraryt &library); /// \brief Generates instructions encoding the \p assigns_clause targets and /// adds them to \p dest. @@ -85,7 +83,6 @@ class dfcc_contract_clauses_codegent messaget log; dfcc_utilst &utils; dfcc_libraryt &library; - dfcc_spec_functionst &spec_functions; namespacet ns; /// Generates GOTO instructions to build the representation of the given diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp index 33fcbe59b64..957c50fcae4 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp @@ -23,6 +23,7 @@ Date: August 2022 #include #include "dfcc_contract_clauses_codegen.h" +#include "dfcc_instrument.h" #include "dfcc_library.h" #include "dfcc_spec_functions.h" #include "dfcc_utils.h" @@ -34,7 +35,8 @@ dfcc_contract_functionst::dfcc_contract_functionst( dfcc_utilst &utils, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, - dfcc_contract_clauses_codegent &contract_clauses_codegen) + dfcc_contract_clauses_codegent &contract_clauses_codegen, + dfcc_instrumentt &instrument) : pure_contract_symbol(pure_contract_symbol), code_with_contract(to_code_with_contract_type(pure_contract_symbol.type)), spec_assigns_function_id( @@ -50,6 +52,7 @@ dfcc_contract_functionst::dfcc_contract_functionst( library(library), spec_functions(spec_functions), contract_clauses_codegen(contract_clauses_codegen), + instrument(instrument), ns(goto_model.symbol_table) { gen_spec_assigns_function(); @@ -66,6 +69,28 @@ dfcc_contract_functionst::dfcc_contract_functionst( spec_functions.to_spec_frees_function( spec_frees_function_id, nof_frees_targets); + + instrument_without_loop_contracts_check_no_pointer_contracts( + spec_assigns_function_id); + + instrument_without_loop_contracts_check_no_pointer_contracts( + spec_frees_function_id); +} + +void dfcc_contract_functionst:: + instrument_without_loop_contracts_check_no_pointer_contracts( + const irep_idt &spec_function_id) +{ + std::set function_pointer_contracts; + instrument.instrument_function( + spec_function_id, + dfcc_loop_contract_modet::NONE, + function_pointer_contracts); + + INVARIANT( + function_pointer_contracts.empty(), + id2string(spec_function_id) + " shall not contain calls to " CPROVER_PREFIX + "obeys_contract"); } const symbolt & diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h index 32e27a9742f..7511f6fcd21 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h @@ -29,6 +29,7 @@ class goto_modelt; class message_handlert; class dfcc_libraryt; class dfcc_utilst; +class dfcc_instrumentt; class dfcc_spec_functionst; class dfcc_contract_clauses_codegent; class code_with_contract_typet; @@ -36,24 +37,26 @@ class conditional_target_group_exprt; /// Generates GOTO functions modelling a contract assigns and frees clauses. /// -/// The generated functions are the following. +/// The generated functions are the following: /// -/// Populates write_set_to_fill with targets of the assigns clause -/// checks its own body against write_set_to_check: /// ```c +/// // Populates write_set_to_fill with targets of the assigns clause +/// // checks its own body against write_set_to_check: /// void contract_id::assigns( /// function-params, /// write_set_to_fill, /// write_set_to_check); /// ``` -/// Havocs the targets specified in the assigns clause, assuming -/// write_set_to_havoc is a snapshot created using contract_id::assigns: +/// /// ```c +/// // Havocs the targets specified in the assigns clause, assuming +/// // write_set_to_havoc is a snapshot created using contract_id::assigns /// void contract_id::assigns::havoc(write_set_to_havoc); /// ``` -/// Populates write_set_to_fill with targets of the frees clause -/// checks its own body against write_set_to_check: +/// /// ```c +/// // Populates write_set_to_fill with targets of the frees clause +/// // checks its own body against write_set_to_check: /// void contract_id::frees( /// function-params, /// write_set_to_fill, @@ -70,6 +73,7 @@ class dfcc_contract_functionst /// \param spec_functions provides translation methods for assignable set /// \param contract_clauses_codegen provides GOTO code generation methods /// for assigns and free clauses. + /// \param instrument Used to instrument generated functions for side effects dfcc_contract_functionst( const symbolt &pure_contract_symbol, goto_modelt &goto_model, @@ -77,7 +81,13 @@ class dfcc_contract_functionst dfcc_utilst &utils, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, - dfcc_contract_clauses_codegent &contract_clauses_codegen); + dfcc_contract_clauses_codegent &contract_clauses_codegen, + dfcc_instrumentt &instrument); + + /// Instruments the given function without loop contracts and checks that no + /// function pointer contracts were discovered. + void instrument_without_loop_contracts_check_no_pointer_contracts( + const irep_idt &spec_function_id); /// Returns the contract::assigns function symbol const symbolt &get_spec_assigns_function_symbol() const; @@ -120,6 +130,7 @@ class dfcc_contract_functionst dfcc_libraryt &library; dfcc_spec_functionst &spec_functions; dfcc_contract_clauses_codegent &contract_clauses_codegen; + dfcc_instrumentt &instrument; namespacet ns; std::size_t nof_assigns_targets; std::size_t nof_frees_targets; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp index be6ca1db972..91096acb576 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp @@ -24,7 +24,6 @@ Date: August 2022 #include #include -#include #include #include @@ -79,7 +78,8 @@ dfcc_contract_handlert::get_contract_functions(const irep_idt &contract_id) utils, library, spec_functions, - contract_clauses_codegen)}) + contract_clauses_codegen, + instrument)}) .first->second; } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index e9d2e03685b..fe3bc6b1a19 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -23,17 +23,22 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include -#include -#include #include #include +#include +#include #include +#include "dfcc_cfg_info.h" +#include "dfcc_contract_clauses_codegen.h" +#include "dfcc_instrument_loop.h" +#include "dfcc_is_cprover_symbol.h" #include "dfcc_is_freeable.h" #include "dfcc_is_fresh.h" #include "dfcc_library.h" #include "dfcc_obeys_contract.h" #include "dfcc_pointer_in_range.h" +#include "dfcc_spec_functions.h" #include "dfcc_utils.h" #include @@ -44,12 +49,23 @@ dfcc_instrumentt::dfcc_instrumentt( goto_modelt &goto_model, message_handlert &message_handler, dfcc_utilst &utils, - dfcc_libraryt &library) + dfcc_libraryt &library, + dfcc_spec_functionst &spec_functions, + dfcc_contract_clauses_codegent &contract_clauses_codegen) : goto_model(goto_model), message_handler(message_handler), log(message_handler), utils(utils), library(library), + spec_functions(spec_functions), + contract_clauses_codegen(contract_clauses_codegen), + instrument_loop( + goto_model, + message_handler, + utils, + library, + spec_functions, + contract_clauses_codegen), ns(goto_model.symbol_table) { // these come from different assert.h implementation on different systems @@ -93,6 +109,11 @@ void dfcc_instrumentt::get_instrumented_functions( dfcc_instrumentt::function_cache.end()); } +std::size_t dfcc_instrumentt::get_max_assigns_clause_size() const +{ + return instrument_loop.get_max_assigns_clause_size(); +} + /* A word on built-ins: @@ -133,7 +154,7 @@ void dfcc_instrumentt::get_instrumented_functions( are allowed for deallocation by the write set. There is also a number of CPROVER global static symbols that are used to - suport memory safety property instrumentation, and assignments to these + support memory safety property instrumentation, and assignments to these statics should always be allowed (i.e not instrumented): - __CPROVER_alloca_object, - __CPROVER_dead_object, @@ -211,57 +232,71 @@ bool dfcc_instrumentt::is_internal_symbol(const irep_idt &id) const return internal_symbols.find(id) != internal_symbols.end(); } -/// True if id has `CPROVER_PREFIX` or `__VERIFIER` or `nondet` prefix, -/// or an `&object` suffix (cf system_library_symbols.cpp) -bool dfcc_instrumentt::is_cprover_symbol(const irep_idt &id) const -{ - std::string str = id2string(id); - return has_prefix(str, CPROVER_PREFIX) || has_prefix(str, "__VERIFIER") || - has_prefix(str, "nondet") || has_suffix(str, "$object"); -} - bool dfcc_instrumentt::do_not_instrument(const irep_idt &id) const { return !has_prefix(id2string(id), CPROVER_PREFIX "file_local") && - (is_cprover_symbol(id) || is_internal_symbol(id)); + (dfcc_is_cprover_symbol(id) || is_internal_symbol(id)); } void dfcc_instrumentt::instrument_harness_function( const irep_idt &function_id, + const dfcc_loop_contract_modet loop_contract_mode, std::set &function_pointer_contracts) { + // never instrument a function twice bool inserted = dfcc_instrumentt::function_cache.insert(function_id).second; if(!inserted) return; + auto found = goto_model.goto_functions.function_map.find(function_id); + PRECONDITION_WITH_DIAGNOSTICS( + found != goto_model.goto_functions.function_map.end(), + "Function '" + id2string(function_id) + "' must exist in the model."); + const null_pointer_exprt null_expr( to_pointer_type(library.dfcc_type[dfcc_typet::WRITE_SET_PTR])); - auto &goto_function = goto_model.goto_functions.function_map.at(function_id); - auto &body = goto_function.body; + // create a local write set symbol + const auto &function_symbol = utils.get_function_symbol(function_id); + const auto &write_set = utils + .create_symbol( + library.dfcc_type[dfcc_typet::WRITE_SET_PTR], + function_id, + "__write_set_to_check", + function_symbol.location, + function_symbol.mode, + function_symbol.module, + false) + .symbol_expr(); - // rewrite pointer_in_range calls - dfcc_pointer_in_ranget pointer_in_range(library, message_handler); - pointer_in_range.rewrite_calls(body, null_expr); + std::set local_statics = get_local_statics(function_id); - // rewrite is_fresh_calls - dfcc_is_fresht is_fresh(library, message_handler); - is_fresh.rewrite_calls(body, null_expr); + goto_functiont &goto_function = found->second; - // rewrite is_freeable/was_freed calls - dfcc_is_freeablet is_freeable(library, message_handler); - is_freeable.rewrite_calls(body, null_expr); + instrument_goto_function( + function_id, + goto_function, + write_set, + local_statics, + loop_contract_mode, + function_pointer_contracts); - // rewrite obeys_contract calls - dfcc_obeys_contractt obeys_contract(library, message_handler); - obeys_contract.rewrite_calls(body, null_expr, function_pointer_contracts); + auto &body = goto_function.body; - // rewrite calls - Forall_goto_program_instructions(it, body) - { - if(it->is_function_call()) - instrument_call_instruction(null_expr, it, body); - } + // add write set definitions at the top of the function + // DECL write_set_harness + // ASSIGN write_set_harness := NULL + auto first_instr = body.instructions.begin(); + + body.insert_before( + first_instr, + goto_programt::make_decl(write_set, first_instr->source_location())); + body.update(); + + body.insert_before( + first_instr, + goto_programt::make_assignment( + write_set, null_expr, first_instr->source_location())); goto_model.goto_functions.update(); } @@ -287,66 +322,123 @@ dfcc_instrumentt::get_local_statics(const irep_idt &function_id) void dfcc_instrumentt::instrument_function( const irep_idt &function_id, + const dfcc_loop_contract_modet loop_contract_mode, std::set &function_pointer_contracts) { - // use same name for local static search - instrument_function(function_id, function_id, function_pointer_contracts); + // never instrument a function twice + bool inserted = dfcc_instrumentt::function_cache.insert(function_id).second; + if(!inserted) + return; + + auto found = goto_model.goto_functions.function_map.find(function_id); + PRECONDITION_WITH_DIAGNOSTICS( + found != goto_model.goto_functions.function_map.end(), + "Function '" + id2string(function_id) + "' must exist in the model."); + + const auto &write_set = utils + .add_parameter( + function_id, + "__write_set_to_check", + library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) + .symbol_expr(); + + std::set local_statics = get_local_statics(function_id); + + goto_functiont &goto_function = found->second; + + instrument_goto_function( + function_id, + goto_function, + write_set, + local_statics, + loop_contract_mode, + function_pointer_contracts); } void dfcc_instrumentt::instrument_wrapped_function( const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, - std::set &function_pointer_contracts) -{ - // use the initial name name for local static search - instrument_function( - wrapped_function_id, initial_function_id, function_pointer_contracts); -} - -void dfcc_instrumentt::instrument_function( - const irep_idt &function_id, - const irep_idt &function_id_for_local_static_search, + const dfcc_loop_contract_modet loop_contract_mode, std::set &function_pointer_contracts) { // never instrument a function twice - bool inserted = dfcc_instrumentt::function_cache.insert(function_id).second; + bool inserted = + dfcc_instrumentt::function_cache.insert(wrapped_function_id).second; if(!inserted) return; - auto found = goto_model.goto_functions.function_map.find(function_id); + auto found = goto_model.goto_functions.function_map.find(wrapped_function_id); PRECONDITION_WITH_DIAGNOSTICS( found != goto_model.goto_functions.function_map.end(), - "Function '" + id2string(function_id) + "' must exist in the model."); + "Function '" + id2string(wrapped_function_id) + + "' must exist in the model."); - auto &goto_function = found->second; + const auto &write_set = utils + .add_parameter( + wrapped_function_id, + "__write_set_to_check", + library.dfcc_type[dfcc_typet::WRITE_SET_PTR]) + .symbol_expr(); - function_cfg_infot cfg_info(goto_function); + std::set local_statics = get_local_statics(initial_function_id); - const auto &write_set = utils.add_parameter( - function_id, - "__write_set_to_check", - library.dfcc_type[dfcc_typet::WRITE_SET_PTR]); + goto_functiont &goto_function = found->second; + + instrument_goto_function( + wrapped_function_id, + goto_function, + write_set, + local_statics, + loop_contract_mode, + function_pointer_contracts); +} - std::set local_statics = - get_local_statics(function_id_for_local_static_search); +void dfcc_instrumentt::instrument_goto_program( + const irep_idt &function_id, + goto_programt &goto_program, + const exprt &write_set, + std::set &function_pointer_contracts) +{ + // create a dummy goto function with empty parameters + goto_functiont goto_function; + goto_function.body.copy_from(goto_program); - instrument_function_body( + // build control flow graph information + dfcc_cfg_infot cfg_info( + function_id, + goto_function, + write_set, + dfcc_loop_contract_modet::NONE, + goto_model.symbol_table, + message_handler, + utils, + library); + + // instrument instructions + goto_programt &body = goto_function.body; + instrument_instructions( function_id, - write_set.symbol_expr(), + body, + body.instructions.begin(), + body.instructions.end(), cfg_info, - local_statics, function_pointer_contracts); + + // cleanup + goto_program.clear(); + goto_program.copy_from(goto_function.body); + remove_skip(goto_program); + goto_model.goto_functions.update(); } -void dfcc_instrumentt::instrument_function_body( +void dfcc_instrumentt::instrument_goto_function( const irep_idt &function_id, + goto_functiont &goto_function, const exprt &write_set, - cfg_infot &cfg_info, const std::set &local_statics, + const dfcc_loop_contract_modet loop_contract_mode, std::set &function_pointer_contracts) { - auto &goto_function = goto_model.goto_functions.function_map.at(function_id); - if(!goto_function.body_available()) { // generate a default body `assert(false);assume(false);` @@ -361,88 +453,79 @@ void dfcc_instrumentt::instrument_function_body( auto &body = goto_function.body; - // instrument the whole body - instrument_instructions( + // build control flow graph information + dfcc_cfg_infot cfg_info( function_id, + goto_function, write_set, + loop_contract_mode, + goto_model.symbol_table, + message_handler, + utils, + library); + + // instrument instructions + instrument_instructions( + function_id, body, body.instructions.begin(), body.instructions.end(), cfg_info, - // don't skip any instructions - {}, function_pointer_contracts); - // insert add/remove instructions for local statics + // recalculate numbers, etc. + goto_model.goto_functions.update(); + + if(loop_contract_mode != dfcc_loop_contract_modet::NONE) + { + apply_loop_contracts( + function_id, + goto_function, + cfg_info, + loop_contract_mode, + local_statics, + function_pointer_contracts); + } + + // insert add/remove instructions for local statics in the top level write set auto begin = body.instructions.begin(); auto end = std::prev(body.instructions.end()); + // automatically add/remove local statics from the top level write set for(const auto &local_static : local_statics) { - // automatically add local statics to the write set insert_add_decl_call(function_id, write_set, local_static, begin, body); - - // automatically remove local statics to the write set insert_record_dead_call(function_id, write_set, local_static, end, body); } - // cleanup remove_skip(body); // recalculate numbers, etc. goto_model.goto_functions.update(); - - // add loop ids - goto_model.goto_functions.compute_loop_numbers(); -} - -void dfcc_instrumentt::instrument_goto_program( - const irep_idt &function_id, - goto_programt &goto_program, - const exprt &write_set, - std::set &function_pointer_contracts) -{ - goto_program_cfg_infot cfg_info(goto_program); - - instrument_instructions( - function_id, - write_set, - goto_program, - goto_program.instructions.begin(), - goto_program.instructions.end(), - cfg_info, - // no pred, don't skip any instructions - {}, - function_pointer_contracts); - - // cleanup - remove_skip(goto_program); } void dfcc_instrumentt::instrument_instructions( const irep_idt &function_id, - const exprt &write_set, goto_programt &goto_program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, - cfg_infot &cfg_info, - const std::function &pred, + dfcc_cfg_infot &cfg_info, std::set &function_pointer_contracts) { // rewrite pointer_in_range calls dfcc_pointer_in_ranget pointer_in_range(library, message_handler); pointer_in_range.rewrite_calls( - goto_program, first_instruction, last_instruction, write_set); + goto_program, first_instruction, last_instruction, cfg_info); // rewrite is_fresh calls dfcc_is_fresht is_fresh(library, message_handler); is_fresh.rewrite_calls( - goto_program, first_instruction, last_instruction, write_set); + goto_program, first_instruction, last_instruction, cfg_info); // rewrite is_freeable/was_freed calls dfcc_is_freeablet is_freeable(library, message_handler); is_freeable.rewrite_calls( - goto_program, first_instruction, last_instruction, write_set); + goto_program, first_instruction, last_instruction, cfg_info); // rewrite obeys_contract calls dfcc_obeys_contractt obeys_contract(library, message_handler); @@ -450,7 +533,7 @@ void dfcc_instrumentt::instrument_instructions( goto_program, first_instruction, last_instruction, - write_set, + cfg_info, function_pointer_contracts); const namespacet ns(goto_model.symbol_table); @@ -459,56 +542,31 @@ void dfcc_instrumentt::instrument_instructions( // excluding the last while(target != last_instruction) { - // Skip instructions marked as disabled for assigns clause checking - // or rejected by the predicate - if(pred && !pred(target)) - { - target++; - continue; - } - if(target->is_decl()) { - instrument_decl(function_id, write_set, target, goto_program, cfg_info); + instrument_decl(function_id, target, goto_program, cfg_info); } if(target->is_dead()) { - instrument_dead(function_id, write_set, target, goto_program, cfg_info); + instrument_dead(function_id, target, goto_program, cfg_info); } else if(target->is_assign()) { - instrument_assign(function_id, write_set, target, goto_program, cfg_info); + instrument_assign(function_id, target, goto_program, cfg_info); } else if(target->is_function_call()) { - instrument_function_call( - function_id, write_set, target, goto_program, cfg_info); + instrument_function_call(function_id, target, goto_program, cfg_info); } else if(target->is_other()) { - instrument_other(function_id, write_set, target, goto_program, cfg_info); + instrument_other(function_id, target, goto_program, cfg_info); } // else do nothing target++; } } -bool dfcc_instrumentt::must_track_decl_or_dead( - const goto_programt::targett &target, - const cfg_infot &cfg_info) const -{ - INVARIANT( - target->is_decl() || target->is_dead(), - "Target must be a DECL or DEAD instruction"); - - const auto &ident = target->is_decl() - ? target->decl_symbol().get_identifier() - : target->dead_symbol().get_identifier(); - bool retval = cfg_info.is_not_local_or_dirty_local(ident); - - return retval; -} - void dfcc_instrumentt::insert_add_decl_call( const irep_idt &function_id, const exprt &write_set, @@ -517,16 +575,17 @@ void dfcc_instrumentt::insert_add_decl_call( goto_programt &goto_program) { goto_programt payload; + const auto &target_location = target->source_location(); auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target->source_location())); + utils.make_null_check_expr(write_set), target_location)); payload.add(goto_programt::make_function_call( library.write_set_add_decl_call( - write_set, address_of_exprt(symbol_expr), target->source_location()), - target->source_location())); + write_set, address_of_exprt(symbol_expr), target_location), + target_location)); auto label_instruction = - payload.add(goto_programt::make_skip(target->source_location())); + payload.add(goto_programt::make_skip(target_location)); goto_instruction->complete_goto(label_instruction); insert_before_swap_and_advance(goto_program, target, payload); @@ -540,15 +599,15 @@ void dfcc_instrumentt::insert_add_decl_call( /// ``` void dfcc_instrumentt::instrument_decl( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info) + dfcc_cfg_infot &cfg_info) { - if(!must_track_decl_or_dead(target, cfg_info)) + if(!cfg_info.must_track_decl_or_dead(target)) return; - const auto &decl_symbol = target->decl_symbol(); + auto &write_set = cfg_info.get_write_set(target); + target++; insert_add_decl_call( function_id, write_set, decl_symbol, target, goto_program); @@ -563,17 +622,17 @@ void dfcc_instrumentt::insert_record_dead_call( goto_programt &goto_program) { goto_programt payload; - + const auto &target_location = target->source_location(); auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set), target->source_location())); + utils.make_null_check_expr(write_set), target_location)); payload.add(goto_programt::make_function_call( library.write_set_record_dead_call( - write_set, address_of_exprt(symbol_expr), target->source_location()), - target->source_location())); + write_set, address_of_exprt(symbol_expr), target_location), + target_location)); auto label_instruction = - payload.add(goto_programt::make_skip(target->source_location())); + payload.add(goto_programt::make_skip(target_location)); goto_instruction->complete_goto(label_instruction); @@ -588,96 +647,32 @@ void dfcc_instrumentt::insert_record_dead_call( /// ``` void dfcc_instrumentt::instrument_dead( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info) + dfcc_cfg_infot &cfg_info) { - if(!must_track_decl_or_dead(target, cfg_info)) + if(!cfg_info.must_track_decl_or_dead(target)) return; const auto &decl_symbol = target->dead_symbol(); + auto &write_set = cfg_info.get_write_set(target); insert_record_dead_call( function_id, write_set, decl_symbol, target, goto_program); } -bool dfcc_instrumentt::must_check_lhs( - const source_locationt &lhs_source_location, - source_locationt &check_source_location, - const irep_idt &language_mode, - const exprt &lhs, - const cfg_infot &cfg_info) -{ - if(can_cast_expr(lhs)) - { - const auto &symbol_expr = to_symbol_expr(lhs); - const auto &id = symbol_expr.get_identifier(); - - check_source_location.set_comment( - "Check that " + from_expr_using_mode(ns, language_mode, lhs) + - " is assignable"); - - if(cfg_info.is_local(id)) - return false; - - // this is a global symbol. Ignore if it is one of the CPROVER globals - if(is_cprover_symbol(id)) - { - check_source_location.set_comment( - "Check that " + from_expr_using_mode(ns, language_mode, lhs) + - " is assignable"); - - return false; - } - - return true; - } - else - { - // This is a more complex expression. - // Since non-dirty locals are not tracked explicitly in the write set, - // we need to skip the check if we can verify that the expression describes - // an access to a non-dirty local symbol or an function parameter, - // otherwise the check will necessarily fail. - // If the expression contains address_of operator, - // the assignment gets checked. If the base object of the expression - // is a local or a function parameter, it will also be flagged as dirty and - // will be tracked explicitly, and the check will pass. - // If the expression contains a dereference operation, the assignment gets - // checked. If the dereferenced address was computed from a local object, - // from a function parameter or returned by a local malloc, - // then the object will also be tracked explicitly for being dirty, - // and the check will pass. - // In all other cases (address of a non-local object, or dereference of - // a non-locally computed address) the location must be given explicitly - // in the assigns clause to be allowed for assignment and we must check - // the assignment. - if(cfg_info.is_local_composite_access(lhs)) - { - check_source_location.set_comment( - "Check that " + from_expr_using_mode(ns, language_mode, lhs) + - " is assignable"); - - return false; - } - - return true; - } -} - void dfcc_instrumentt::instrument_lhs( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, const exprt &lhs, goto_programt &goto_program, - cfg_infot &cfg_info) + dfcc_cfg_infot &cfg_info) { const auto &mode = utils.get_function_symbol(function_id).mode; goto_programt payload; const auto &lhs_source_location = target->source_location(); + auto &write_set = cfg_info.get_write_set(target); auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( utils.make_null_check_expr(write_set), lhs_source_location)); @@ -686,8 +681,7 @@ void dfcc_instrumentt::instrument_lhs( check_source_location.set_comment( "Check that " + from_expr_using_mode(ns, mode, lhs) + " is assignable"); - if(must_check_lhs( - target->source_location(), check_source_location, mode, lhs, cfg_info)) + if(cfg_info.must_check_lhs(target)) { // ``` // IF !write_set GOTO skip_target; @@ -725,7 +719,7 @@ void dfcc_instrumentt::instrument_lhs( payload.add( goto_programt::make_assertion(check_var, check_source_location)); - payload.add(goto_programt::make_dead(check_var)); + payload.add(goto_programt::make_dead(check_var, check_source_location)); } else { @@ -772,17 +766,17 @@ dfcc_instrumentt::is_dead_object_update(const exprt &lhs, const exprt &rhs) void dfcc_instrumentt::instrument_assign( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info) + dfcc_cfg_infot &cfg_info) { const auto &lhs = target->assign_lhs(); const auto &rhs = target->assign_rhs(); const auto &target_location = target->source_location(); + auto &write_set = cfg_info.get_write_set(target); // check the lhs - instrument_lhs(function_id, write_set, target, lhs, goto_program, cfg_info); + instrument_lhs(function_id, target, lhs, goto_program, cfg_info); // handle dead_object updates (created by __builtin_alloca for instance) // Remark: we do not really need to track this deallocation since the default @@ -825,7 +819,7 @@ void dfcc_instrumentt::instrument_assign( if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_allocate) { // ``` - // CALL lhs := side_effect(statemet = ID_allocate, args = {size, clear}); + // CALL lhs := side_effect(statement = ID_allocate, args = {size, clear}); // ---- // IF !write_set GOTO skip_target; // CALL add_allocated(write_set, lhs); @@ -836,7 +830,6 @@ void dfcc_instrumentt::instrument_assign( target++; goto_programt payload; - auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( utils.make_null_check_expr(write_set), target_location)); @@ -1006,25 +999,21 @@ void dfcc_instrumentt::instrument_deallocate_call( void dfcc_instrumentt::instrument_function_call( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info) + dfcc_cfg_infot &cfg_info) { INVARIANT( target->is_function_call(), "the target must be a function call instruction"); + auto &write_set = cfg_info.get_write_set(target); + // Instrument the lhs if any. if(target->call_lhs().is_not_nil()) { instrument_lhs( - function_id, - write_set, - target, - target->call_lhs(), - goto_program, - cfg_info); + function_id, target, target->call_lhs(), goto_program, cfg_info); } const auto &call_function = target->call_function(); @@ -1044,13 +1033,13 @@ void dfcc_instrumentt::instrument_function_call( void dfcc_instrumentt::instrument_other( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info) + dfcc_cfg_infot &cfg_info) { const auto &target_location = target->source_location(); auto &statement = target->get_other().get_statement(); + auto &write_set = cfg_info.get_write_set(target); if(statement == ID_array_set || statement == ID_array_copy) { @@ -1063,7 +1052,7 @@ void dfcc_instrumentt::instrument_other( // DEAD check_array_set; // skip_target: SKIP; // ---- - // OTHER {statemet = array_set, args = {dest, value}}; + // OTHER {statement = array_set, args = {dest, value}}; // ``` const auto &mode = utils.get_function_symbol(function_id).mode; goto_programt payload; @@ -1104,7 +1093,7 @@ void dfcc_instrumentt::instrument_other( check_location.set_comment(comment); payload.add(goto_programt::make_assertion(check_var, check_location)); - payload.add(goto_programt::make_dead(check_var)); + payload.add(goto_programt::make_dead(check_var, target_location)); auto label_instruction = payload.add(goto_programt::make_skip(target_location)); @@ -1122,13 +1111,13 @@ void dfcc_instrumentt::instrument_other( // DEAD check_array_replace; // skip_target: SKIP; // ---- - // OTHER {statemet = array_replace, args = {dest, src}}; + // OTHER {statement = array_replace, args = {dest, src}}; // ``` const auto &mode = utils.get_function_symbol(function_id).mode; goto_programt payload; auto goto_instruction = payload.add(goto_programt::make_incomplete_goto( - utils.make_null_check_expr(write_set))); + utils.make_null_check_expr(write_set), target_location)); auto &check_sym = get_fresh_aux_symbol( bool_typet(), @@ -1140,7 +1129,7 @@ void dfcc_instrumentt::instrument_other( const auto &check_var = check_sym.symbol_expr(); - payload.add(goto_programt::make_decl(check_var)); + payload.add(goto_programt::make_decl(check_var, target_location)); const auto &dest = target->get_other().operands().at(0); const auto &src = target->get_other().operands().at(1); @@ -1193,7 +1182,7 @@ void dfcc_instrumentt::instrument_other( const auto &check_var = check_sym.symbol_expr(); - payload.add(goto_programt::make_decl(check_var)); + payload.add(goto_programt::make_decl(check_var, target_location)); const auto &ptr = target->get_other().operands().at(0); @@ -1249,3 +1238,52 @@ void dfcc_instrumentt::instrument_other( << messaget::eom; } } + +void dfcc_instrumentt::apply_loop_contracts( + const irep_idt &function_id, + goto_functiont &goto_function, + dfcc_cfg_infot &cfg_info, + const dfcc_loop_contract_modet loop_contract_mode, + const std::set &local_statics, + std::set &function_pointer_contracts) +{ + PRECONDITION(loop_contract_mode != dfcc_loop_contract_modet::NONE); + cfg_info.get_loops_toposorted(); + + std::list to_unwind; + + // Apply loop contract transformations in topological order + for(const auto &loop_id : cfg_info.get_loops_toposorted()) + { + const auto &loop = cfg_info.get_loop_info(loop_id); + if(loop.invariant.is_nil() && loop.decreases.empty()) + { + // skip loops that do not have contracts + log.warning() << "loop " << function_id << "." << loop.cbmc_loop_id + << " does not have a contract, skipping instrumentation" + << messaget::eom; + continue; + } + + instrument_loop( + loop_id, + function_id, + goto_function, + cfg_info, + local_statics, + function_pointer_contracts); + to_unwind.push_back( + id2string(function_id) + "." + std::to_string(loop.cbmc_loop_id) + ":2"); + } + + // If required, unwind all transformed loops to yield base and step cases + if(loop_contract_mode == dfcc_loop_contract_modet::APPLY_UNWIND) + { + unwindsett unwindset{goto_model}; + unwindset.parse_unwindset(to_unwind, log.get_message_handler()); + goto_unwindt goto_unwind; + goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME); + } + + remove_skip(goto_function.body); +} diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h index 0c7ec972d1a..c02f1e6a55c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h @@ -22,6 +22,8 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include "dfcc_contract_mode.h" +#include "dfcc_instrument_loop.h" +#include "dfcc_loop_contract_mode.h" #include #include @@ -30,12 +32,16 @@ class goto_modelt; class message_handlert; class symbolt; class conditional_target_group_exprt; -class cfg_infot; class dfcc_libraryt; +class dfcc_spec_functionst; +class dfcc_contract_clauses_codegent; class dfcc_utilst; +class dfcc_loop_utilst; +class dirtyt; +class dfcc_cfg_infot; /// This class instruments GOTO functions or instruction sequences -/// for frame condition checking. +/// for frame condition checking and loop contracts. class dfcc_instrumentt { public: @@ -43,11 +49,9 @@ class dfcc_instrumentt goto_modelt &goto_model, message_handlert &message_handler, dfcc_utilst &utils, - dfcc_libraryt &library); - - /// True if id has `CPROVER_PREFIX` or `__VERIFIER` or `nondet` prefix, - /// or an `&object` - bool is_cprover_symbol(const irep_idt &function_id) const; + dfcc_libraryt &library, + dfcc_spec_functionst &spec_functions, + dfcc_contract_clauses_codegent &contract_clauses_codegen); /// True iff the symbol an internal symbol bool is_internal_symbol(const irep_idt &id) const; @@ -56,47 +60,52 @@ class dfcc_instrumentt /// symbol or a CPROVER symbol bool do_not_instrument(const irep_idt &id) const; - /// Instruments a function as a proof harness. - /// - /// Instrumenting a harness function just consists in passing a NULL value - /// for the write_set parameter to all function and function pointer calls - /// it contains. + /// Instruments a GOTO function used as a proof harness. Proof harnesses + /// are closed functions without parameters, so we declare a local write set + /// pointer and initialise it to NULL, and check body instructions against + /// that NULL write set. /// - /// This will result in no write_set updates or checks being performed in - /// the harness or in the functions called directly from the harness - /// (and transitively in functions they call). + /// By using a NULL write set pointer we ensure that no checks are being + /// performed in the harness or in the functions called from the harness, + /// except in the following cases: + /// 1. One of the functions called directly (or indirectly) by the harness + /// is a verification wrapper function that checks some contract against some + /// function. This wrapper will ignore the NULL write set it received from the + /// harness and will instantiate its own write set from the contract and pass + /// it to the function under analysis. + /// 2. The harness function contains loops that have contracts. + /// A write set is created for each loop and loop instructions instrumented + /// against that write set. The write set is propagated to all functions + /// called from the loop. /// - /// One of the functions called directly (or indirectly) by the harness - /// is eventually going to be a wrapper function that checks the contract - /// against the function of interest. This wrapper will ignore the NULL - /// write set it received from the harness and instantiate its own local - /// write set from the contract and pass it to the function under analysis. - /// This will trigger cascading checks in all functions called from the - /// checked function thanks to the propagation of the write set through - /// function calls and function pointer calls. - /// - /// \param function_id function to instrument - /// \param function_pointer_contracts contracts discovered in calls to - /// the obeys_contract predicate are added to this set. + /// \param function_id Function to instrument + /// \param loop_contract_mode Mode to use for loop contracts + /// \param function_pointer_contracts Contract names discovered in calls to + /// the `obeys_contract` predicate are added to this set. void instrument_harness_function( const irep_idt &function_id, + const dfcc_loop_contract_modet loop_contract_mode, std::set &function_pointer_contracts); /// \brief Instruments a GOTO function by adding an extra write set parameter - /// and inserting frame condition checks in its GOTO program, as well as - /// instructions to automatically insert and remove locally declared static - /// variables in the write set. + /// and instrumenting its body instructions against the write set. Adds ghost + /// instructions that automatically insert locally declared static variables + /// to the write set when entering the function and removing them upon exit. + /// + /// \pre The function must *not* be one of the functions checked against a + /// contract or replaced by a contract. The method + /// \ref instrument_wrapped_function must be used to instrument check/replaced + /// functions instead. /// - /// \pre The function must *not* be one of the checked or replaced functions. - /// For checked/replaced functions \ref instrument_wrapped_function must be - /// used instead. /// \param function_id The name of the function, used to retrieve the function /// to instrument and used as prefix when generating new symbols during /// instrumentation. - /// \param function_pointer_contracts contracts discovered in calls to + /// \param loop_contract_mode Mode to use for loop contracts + /// \param function_pointer_contracts Contracts discovered in calls to /// the obeys_contract predicate are added to this set. void instrument_function( const irep_idt &function_id, + const dfcc_loop_contract_modet loop_contract_mode, std::set &function_pointer_contracts); /// \brief Instruments a GOTO function by adding an extra write set parameter @@ -105,8 +114,10 @@ class dfcc_instrumentt /// variables in the write set. /// /// \pre The function must be a function wrapped for contract checking or - /// replacemend. For other functions \ref instrument_function must be used - /// instead. + /// replacement checking. For other functions \ref instrument_function must + /// be used instead. The difference is that checked or replaced functions have + /// their name mangled, so the the search for local statics uses a possibly + /// different function identifier as base name for static symbols. /// /// \param wrapped_function_id The name of the function, used to retrieve the /// function to instrument and used as prefix when generating new symbols @@ -114,27 +125,30 @@ class dfcc_instrumentt /// \param initial_function_id The initial name of the function, /// before mangling. This is the name used to identify statics symbols in the /// symbol table that were locally declared in the function. + /// \param loop_contract_mode Mode to use for loop contracts /// \param function_pointer_contracts contracts discovered in calls to /// the obeys_contract predicate are added to this set. void instrument_wrapped_function( const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, + const dfcc_loop_contract_modet loop_contract_mode, std::set &function_pointer_contracts); /// \brief Instruments a GOTO program against a given write set variable. /// - /// \remark Only variables declared within the instruction sequence are - /// considered local and automatically assignable. In particular, occurrences - /// of symbols with the `is_parameter` which represent parameters of the - /// enclosing function are not considered as local to the program. - /// \remark Local statics declared in the program are *not* searched for and - /// are *not* added automatically to the write set. - /// \remark This function is meant to instrument instruction sequences that - /// were generated from contract clauses. + /// \remark This function is meant to instrument instruction + /// sequences generated from contract clauses. + /// \remark Only variables declared within the instruction sequence are + /// considered local and implicitly assignable. In particular, occurrences + /// of symbols with the `is_parameter` flag set to true, which represent + /// parameters of the enclosing function, are not considered implicitly + /// assignable. + /// \remark Loop contracts are never applied. + /// \remark Local statics are *not* collected and added to the write set. /// /// \param function_id Name used as prefix when creating new symbols during /// instrumentation. - /// \param goto_program Goto program to instrument. + /// \param goto_program GOTO program to instrument. /// \param write_set Write set variable to use for instrumentation. /// \param function_pointer_contracts Discovered function pointer contracts void instrument_goto_program( @@ -147,12 +161,19 @@ class dfcc_instrumentt /// The names are kept track of in the \ref function_cache field. void get_instrumented_functions(std::set &dest) const; + /// \return The maximum assigns clause size discovered when instrumenting + /// loop contracts + std::size_t get_max_assigns_clause_size() const; + protected: goto_modelt &goto_model; message_handlert &message_handler; messaget log; dfcc_utilst &utils; dfcc_libraryt &library; + dfcc_spec_functionst &spec_functions; + dfcc_contract_clauses_codegent &contract_clauses_codegen; + dfcc_instrument_loopt instrument_loop; namespacet ns; /// \brief Keeps track of instrumented functions, so that no function gets @@ -210,23 +231,15 @@ class dfcc_instrumentt goto_programt::targett &target, goto_programt &goto_program); - /// Instruments a GOTO function by adding an extra write set parameter and - /// inserting frame condition checks in its goto program. - /// Uses \p function_id_for_local_static_search to search for local statics - /// and automatically to add/remove to the write set. - void instrument_function( - const irep_idt &function_id, - const irep_idt &function_id_for_local_static_search, - std::set &function_pointer_contracts); - /// Instruments the body of a GOTO function against a given write set. /// Adds the given local statics to the write set in pre and removes them /// post. - void instrument_function_body( + void instrument_goto_function( const irep_idt &function_id, + goto_functiont &goto_function, const exprt &write_set, - cfg_infot &cfg_info, const std::set &local_statics, + const dfcc_loop_contract_modet loop_contract_mode, std::set &function_pointer_contracts); /// \brief Instruments the instructions found between \p first_instruction and @@ -235,71 +248,44 @@ class dfcc_instrumentt /// /// \param function_id Name of the enclosing function used as prefix for new /// variables generated during instrumentation. - /// \param write_set Write set variable to instrument against /// \param goto_program Program to instrument the instructions of /// \param first_instruction First instruction to instrument in the program /// \param last_instruction Last instruction to instrument (excluded !!!) /// \param cfg_info Computes local and dirty variables to discard some checks - /// \param pred filter predicate for instructions. If \p pred is not provided, - /// all instructions are instrumented. If \p pred is provided, only - /// instructions satisfying \p pred are instrumented. - /// \param function_pointer_contracts contracts discovered in calls to + /// \param function_pointer_contracts Contracts discovered in calls to /// the obeys_contract predicate are added to this set. void instrument_instructions( const irep_idt &function_id, - const exprt &write_set, goto_programt &goto_program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, // excluding the last - cfg_infot &cfg_info, - const std::function &pred, + dfcc_cfg_infot &cfg_info, std::set &function_pointer_contracts); - /// Returns `true` if the symbol `x` in `DECL x` or `DEAD x` must be added - /// explicitly to the write set. Returns `false` when assignments to `x` must - /// be implicitly allowed. - bool must_track_decl_or_dead( - const goto_programt::targett &target, - const cfg_infot &cfg_info) const; - /// Instruments a `DECL x` instruction. /// \pre \p target points to a `DECL` instruction void instrument_decl( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info); + dfcc_cfg_infot &cfg_info); /// Instruments a `DEAD x` instruction. /// \pre \p target points to a `DEAD` instruction void instrument_dead( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info); - - /// Returns true iff the lhs of a `ASSIGN lhs := ...` instruction or - /// `CALL lhs := ...` must be checked against the write set. - /// Returns false if the assignment must be implicitly allowed. - /// Works in tandem with \ref must_track_decl_or_dead - bool must_check_lhs( - const source_locationt &lhs_source_location, - source_locationt &check_source_location, - const irep_idt &language_mode, - const exprt &lhs, - const cfg_infot &cfg_info); + dfcc_cfg_infot &cfg_info); /// \brief Instruments the LHS of an assignment instruction instruction by /// adding an inclusion check of \p lhs in \p write_set. void instrument_lhs( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, const exprt &lhs, goto_programt &goto_program, - cfg_infot &cfg_info); + dfcc_cfg_infot &cfg_info); /// Checks if \p lhs is the `dead_object`, and if \p rhs /// is an `if_exprt(nondet, ptr, dead_object)` expression. @@ -309,17 +295,16 @@ class dfcc_instrumentt /// Instrument the \p lhs of an `ASSIGN lhs := rhs` instruction by /// adding an inclusion check of \p lhs in \p write_set. - /// If \ref is_dead_object_update returns a successfull match, the matched + /// If \ref is_dead_object_update returns a successful match, the matched /// pointer expression is removed from \p write_set. /// If \p rhs is a `side_effect_expr(ID_allocate)`, the allocated pointer gets /// added to the \p write_set. /// \pre \p target points to an `ASSIGN` instruction. void instrument_assign( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info); + dfcc_cfg_infot &cfg_info); /// Adds the \p write_set as extra argument to a function of function pointer /// call instruction. @@ -332,7 +317,7 @@ class dfcc_instrumentt /// Before calling a function pointer, performs a dynamic lookup into /// the map of instrumented function provided by /// \ref dfcc_libraryt.get_instrumented_functions_map_symbol, - /// and passes the write_set parameter to the funciton pointer only if + /// and passes the write_set parameter to the function pointer only if /// it points to a function known to be instrumented and hence able to accept /// this parameter. /// \pre \p target points to a `CALL` instruction where the function @@ -357,10 +342,9 @@ class dfcc_instrumentt /// \pre \p target points to a `CALL` instruction. void instrument_function_call( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info); + dfcc_cfg_infot &cfg_info); /// Instruments a `OTHER statement;` instruction. /// OTHER instructions can be an array_set, array_copy, array_replace or @@ -368,10 +352,22 @@ class dfcc_instrumentt /// \pre \p target points to an `OTHER` instruction. void instrument_other( const irep_idt &function_id, - const exprt &write_set, goto_programt::targett &target, goto_programt &goto_program, - cfg_infot &cfg_info); + dfcc_cfg_infot &cfg_info); + + /// \brief Applies loop contracts transformations to the given GOTO function, + /// using the given cfg_info instance to drive the transformation. + /// + /// \pre Instructions of the function must already have been instrumented for + /// DFCC using the same cfg_info. + void apply_loop_contracts( + const irep_idt &function_id, + goto_functiont &goto_function, + dfcc_cfg_infot &cfg_info, + const dfcc_loop_contract_modet loop_contract_mode, + const std::set &local_statics, + std::set &function_pointer_contracts); }; #endif diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp index b4500cf4d13..8626d153409 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.cpp @@ -12,6 +12,7 @@ Date: August 2022 #include #include +#include "dfcc_cfg_info.h" #include "dfcc_library.h" dfcc_is_freeablet::dfcc_is_freeablet( @@ -23,20 +24,20 @@ dfcc_is_freeablet::dfcc_is_freeablet( void dfcc_is_freeablet::rewrite_calls( goto_programt &program, - const exprt &write_set) + dfcc_cfg_infot &cfg_info) { rewrite_calls( program, program.instructions.begin(), program.instructions.end(), - write_set); + cfg_info); } void dfcc_is_freeablet::rewrite_calls( goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, - const exprt &write_set) + dfcc_cfg_infot &cfg_info) { auto target = first_instruction; while(target != last_instruction) @@ -54,7 +55,7 @@ void dfcc_is_freeablet::rewrite_calls( // redirect call to library implementation to_symbol_expr(target->call_function()) .set_identifier(library.get_dfcc_fun_name(dfcc_funt::IS_FREEABLE)); - target->call_arguments().push_back(write_set); + target->call_arguments().push_back(cfg_info.get_write_set(target)); } else if(fun_name == CPROVER_PREFIX "was_freed") { @@ -62,7 +63,7 @@ void dfcc_is_freeablet::rewrite_calls( auto inst = goto_programt::make_function_call( library.check_replace_ensures_was_freed_preconditions_call( target->call_arguments().at(0), - write_set, + cfg_info.get_write_set(target), target->source_location()), target->source_location()); program.insert_before_swap(target, inst); @@ -71,7 +72,7 @@ void dfcc_is_freeablet::rewrite_calls( // redirect call to library implementation to_symbol_expr(target->call_function()) .set_identifier(library.get_dfcc_fun_name(dfcc_funt::WAS_FREED)); - target->call_arguments().push_back(write_set); + target->call_arguments().push_back(cfg_info.get_write_set(target)); } } } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.h index 8c5a1ab4c8c..986cf2b6abd 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_freeable.h @@ -21,6 +21,7 @@ Date: August 2022 class goto_modelt; class message_handlert; class dfcc_libraryt; +class dfcc_cfg_infot; class exprt; /// Rewrites calls to is_freeable and was_freed predicates in goto programs @@ -35,7 +36,7 @@ class dfcc_is_freeablet /// Rewrites calls to is_freeable and was_freed predicates into calls /// to the library implementation in the given program, passing the /// given write_set expression as parameter to the library function. - void rewrite_calls(goto_programt &program, const exprt &write_set); + void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info); /// Rewrites calls to is_fresh predicates into calls /// to the library implementation in the given program between @@ -45,7 +46,7 @@ class dfcc_is_freeablet goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, // excluding the last - const exprt &write_set); + dfcc_cfg_infot &cfg_info); protected: dfcc_libraryt &library; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp index 9ce1b7d69df..10a8ee97f95 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.cpp @@ -13,6 +13,7 @@ Date: August 2022 #include #include +#include "dfcc_cfg_info.h" #include "dfcc_library.h" dfcc_is_fresht::dfcc_is_fresht( @@ -24,20 +25,20 @@ dfcc_is_fresht::dfcc_is_fresht( void dfcc_is_fresht::rewrite_calls( goto_programt &program, - const exprt &write_set) + dfcc_cfg_infot &cfg_info) { rewrite_calls( program, program.instructions.begin(), program.instructions.end(), - write_set); + cfg_info); } void dfcc_is_fresht::rewrite_calls( goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, - const exprt &write_set) + dfcc_cfg_infot &cfg_info) { auto &target = first_instruction; while(target != last_instruction) @@ -61,7 +62,7 @@ void dfcc_is_fresht::rewrite_calls( .set_identifier(library.dfcc_fun_symbol[dfcc_funt::IS_FRESH].name); // pass the write_set - target->call_arguments().push_back(write_set); + target->call_arguments().push_back(cfg_info.get_write_set(target)); } } } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.h index dfe2394a9ec..c7b6ee1151b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_is_fresh.h @@ -21,6 +21,7 @@ Date: August 2022 class goto_modelt; class message_handlert; class dfcc_libraryt; +class dfcc_cfg_infot; class exprt; /// Rewrites calls to is_fresh predicates into calls @@ -35,7 +36,7 @@ class dfcc_is_fresht /// Rewrites calls to is_fresh predicates into calls /// to the library implementation in the given program, passing the /// given write_set expression as parameter to the library function. - void rewrite_calls(goto_programt &program, const exprt &write_set); + void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info); /// Rewrites calls to is_fresh predicates into calls /// to the library implementation in the given program between @@ -45,7 +46,7 @@ class dfcc_is_fresht goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, - const exprt &write_set); + dfcc_cfg_infot &cfg_info); protected: dfcc_libraryt &library; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp index 68495294bd1..afe413858dd 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -386,7 +386,9 @@ void dfcc_lift_memory_predicatest::lift_predicate( // instrument the function for side effects: adds the write_set parameter, // adds checks for side effects, maps core predicates to their implementation. instrument.instrument_function( - function_id, discovered_function_pointer_contracts); + function_id, + dfcc_loop_contract_modet::NONE, + discovered_function_pointer_contracts); } void dfcc_lift_memory_predicatest::fix_calls(goto_programt &program) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp index 42cc92ddfc3..da69a217332 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.cpp @@ -16,6 +16,7 @@ Date: August 2022 #include +#include "dfcc_cfg_info.h" #include "dfcc_library.h" dfcc_obeys_contractt::dfcc_obeys_contractt( @@ -27,14 +28,14 @@ dfcc_obeys_contractt::dfcc_obeys_contractt( void dfcc_obeys_contractt::rewrite_calls( goto_programt &program, - const exprt &write_set, + dfcc_cfg_infot &cfg_info, std::set &function_pointer_contracts) { rewrite_calls( program, program.instructions.begin(), program.instructions.end(), - write_set, + cfg_info, function_pointer_contracts); } @@ -62,7 +63,7 @@ void dfcc_obeys_contractt::rewrite_calls( goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, - const exprt &write_set, + dfcc_cfg_infot &cfg_info, std::set &function_pointer_contracts) { for(auto &target = first_instruction; target != last_instruction; target++) @@ -87,7 +88,7 @@ void dfcc_obeys_contractt::rewrite_calls( library.dfcc_fun_symbol[dfcc_funt::OBEYS_CONTRACT].name); // pass the write_set - target->call_arguments().push_back(write_set); + target->call_arguments().push_back(cfg_info.get_write_set(target)); // record discovered function contract get_contract_name( diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h index a24c6bde562..5116a7fcd22 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_obeys_contract.h @@ -21,6 +21,7 @@ Date: August 2022 class goto_modelt; class message_handlert; class dfcc_libraryt; +class dfcc_cfg_infot; class exprt; /// Rewrites calls to obeys_contract predicates into calls @@ -39,7 +40,7 @@ class dfcc_obeys_contractt /// given write_set expression as parameter to the library function. void rewrite_calls( goto_programt &program, - const exprt &write_set, + dfcc_cfg_infot &cfg_info, std::set &function_pointer_contracts); /// Rewrites calls to obeys_contract predicates into calls @@ -50,7 +51,7 @@ class dfcc_obeys_contractt goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, - const exprt &write_set, + dfcc_cfg_infot &cfg_info, std::set &function_pointer_contracts); protected: diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp index 00d4579f5a4..76cb565fd67 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.cpp @@ -15,6 +15,7 @@ Date: August 2022 #include #include +#include "dfcc_cfg_info.h" #include "dfcc_library.h" dfcc_pointer_in_ranget::dfcc_pointer_in_ranget( @@ -26,20 +27,20 @@ dfcc_pointer_in_ranget::dfcc_pointer_in_ranget( void dfcc_pointer_in_ranget::rewrite_calls( goto_programt &program, - const exprt &write_set) + dfcc_cfg_infot cfg_info) { rewrite_calls( program, program.instructions.begin(), program.instructions.end(), - write_set); + cfg_info); } void dfcc_pointer_in_ranget::rewrite_calls( goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, - const exprt &write_set) + dfcc_cfg_infot cfg_info) { auto &target = first_instruction; while(target != last_instruction) @@ -64,7 +65,7 @@ void dfcc_pointer_in_ranget::rewrite_calls( library.dfcc_fun_symbol[dfcc_funt::POINTER_IN_RANGE_DFCC].name); // pass the write_set - target->call_arguments().push_back(write_set); + target->call_arguments().push_back(cfg_info.get_write_set(target)); } } } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h index 0a368f8cc9a..6086ee0db7d 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_pointer_in_range.h @@ -21,6 +21,7 @@ Date: August 2022 class goto_modelt; class message_handlert; class dfcc_libraryt; +class dfcc_cfg_infot; class exprt; /// Rewrites calls to pointer_in_range predicates into calls @@ -37,7 +38,7 @@ class dfcc_pointer_in_ranget /// Rewrites calls to pointer_in_range predicates into calls /// to the library implementation in the given program, passing the /// given write_set expression as parameter to the library function. - void rewrite_calls(goto_programt &program, const exprt &write_set); + void rewrite_calls(goto_programt &program, dfcc_cfg_infot cfg_info); /// Rewrites calls to pointer_in_range predicates into calls /// to the library implementation in the given program between @@ -47,7 +48,7 @@ class dfcc_pointer_in_ranget goto_programt &program, goto_programt::targett first_instruction, const goto_programt::targett &last_instruction, - const exprt &write_set); + dfcc_cfg_infot cfg_info); protected: dfcc_libraryt &library; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp index d9103bc5cfd..eb1ddd428dd 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.cpp @@ -17,20 +17,19 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include "dfcc_library.h" +#include "dfcc_loop_contract_mode.h" #include "dfcc_utils.h" dfcc_spec_functionst::dfcc_spec_functionst( goto_modelt &goto_model, message_handlert &message_handler, dfcc_utilst &utils, - dfcc_libraryt &library, - dfcc_instrumentt &instrument) + dfcc_libraryt &library) : goto_model(goto_model), message_handler(message_handler), log(message_handler), utils(utils), library(library), - instrument(instrument), ns(goto_model.symbol_table) { } @@ -111,6 +110,8 @@ void dfcc_spec_functionst::generate_havoc_function( havoc_program, nof_targets); + havoc_program.add(goto_programt::make_end_function()); + goto_model.goto_functions.update(); std::set no_body; @@ -246,7 +247,6 @@ void dfcc_spec_functionst::generate_havoc_instructions( } } nof_targets = next_idx; - havoc_program.add(goto_programt::make_end_function()); } void dfcc_spec_functionst::to_spec_assigns_function( @@ -272,13 +272,6 @@ void dfcc_spec_functionst::to_spec_assigns_function( goto_model.goto_functions.update(); - // instrument for side-effects checking - std::set function_pointer_contracts; - instrument.instrument_function(function_id, function_pointer_contracts); - INVARIANT( - function_pointer_contracts.empty(), - "discovered function pointer contracts unexpectedly"); - goto_model.goto_functions.function_map.at(function_id).make_hidden(); } @@ -362,13 +355,6 @@ void dfcc_spec_functionst::to_spec_frees_function( goto_model.goto_functions.update(); - // instrument for side-effects checking - std::set function_pointer_contracts; - instrument.instrument_function(function_id, function_pointer_contracts); - INVARIANT( - function_pointer_contracts.empty(), - "discovered function pointer contracts unexpectedly"); - goto_model.goto_functions.function_map.at(function_id).make_hidden(); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h index 6e12be814d0..42d188cb762 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_spec_functions.h @@ -21,7 +21,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include -#include "dfcc_instrument.h" #include "dfcc_library.h" #include "dfcc_utils.h" @@ -32,19 +31,15 @@ class goto_modelt; class message_handlert; class symbolt; class conditional_target_group_exprt; -class cfg_infot; -/// This class transforms (in place) declarative assigns clause and frees clause -/// specification functions expressed in terms of the builtins: +/// This class rewrites GOTO functions that use the built-ins: /// - `__CPROVER_assignable`, /// - `__CPROVER_object_whole`, /// - `__CRPOVER_object_from`, /// - `__CPROVER_object_upto`, /// - `__CPROVER_freeable` -/// into active functions by transforming the builtin calls into calls to -/// dfcc library functions that actually built frame descriptions. -/// The resulting function is then itself instrumented for frame condition -/// checking to be able to prove the absence of side effects. +/// into GOTO functions that populate a write set instance or havoc a write set +/// by calling the library implementation of these built-ins. class dfcc_spec_functionst { public: @@ -52,8 +47,7 @@ class dfcc_spec_functionst goto_modelt &goto_model, message_handlert &message_handler, dfcc_utilst &utils, - dfcc_libraryt &library, - dfcc_instrumentt &instrument); + dfcc_libraryt &library); /// From a function: /// @@ -122,13 +116,11 @@ class dfcc_spec_functionst /// void function_id( /// params, /// __CPROVER_assignable_set_t write_set_to_fill, - /// __CPROVER_assignable_set_t write_set_to_check /// ) /// ``` /// /// Where: /// - `write_set_to_fill` is the write set to populate. - /// - `write_set_to_check` is the write set to use for checking side effects. /// /// \param function_id function to transform in place /// \param nof_targets receives the estimated size of the write set @@ -174,13 +166,11 @@ class dfcc_spec_functionst /// void function_id( /// params, /// __CPROVER_assignable_set_t write_set_to_fill, - /// __CPROVER_assignable_set_t write_set_to_check /// ) /// ``` /// /// Where: /// - `write_set_to_fill` is the write set to populate. - /// - `write_set_to_check` is the write set to use for checking side effects. /// /// The function must be fully inlined and loop free. /// @@ -219,7 +209,6 @@ class dfcc_spec_functionst messaget log; dfcc_utilst &utils; dfcc_libraryt &library; - dfcc_instrumentt &instrument; namespacet ns; /// Extracts the type of an assigns clause target expression diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp index 5ac421f0ba5..e2a9f22cd7f 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp @@ -32,7 +32,6 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include #include -#include #include #include @@ -57,38 +56,45 @@ dfcc_swap_and_wrapt::dfcc_swap_and_wrapt( } // static map -std::map> +std::map< + irep_idt, + std::pair>> dfcc_swap_and_wrapt::cache; void dfcc_swap_and_wrapt::swap_and_wrap( const dfcc_contract_modet contract_mode, + const dfcc_loop_contract_modet loop_contract_mode, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, bool allow_recursive_calls) { - auto pair = cache.insert({function_id, {contract_id, contract_mode}}); + auto pair = cache.insert( + {function_id, {contract_id, {contract_mode, loop_contract_mode}}}); auto inserted = pair.second; if(!inserted) { - auto old_contract_id = pair.first->second.first; - auto old_contract_mode = pair.first->second.second; - - // different swapp already performed, abort - if(old_contract_id != contract_id || old_contract_mode != contract_mode) + irep_idt old_contract_id = pair.first->second.first; + dfcc_contract_modet old_contract_mode = pair.first->second.second.first; + dfcc_loop_contract_modet old_loop_contract_mode = + pair.first->second.second.second; + + // different swap already performed, abort (should be unreachable) + if( + old_contract_id != contract_id || old_contract_mode != contract_mode || + old_loop_contract_mode != loop_contract_mode) { - auto mode1 = (old_contract_mode == dfcc_contract_modet::REPLACE) - ? "REPLACE" - : "CHECK"; - auto mode2 = - (contract_mode == dfcc_contract_modet::REPLACE) ? "REPLACE" : "CHECK)"; - std::ostringstream err_msg; err_msg << "DFCC: multiple attempts to swap and wrap function '" << function_id << "':\n"; - err_msg << "- with '" << old_contract_id << "' in mode " << mode1 << "\n"; - err_msg << "- with '" << contract_id << "' in mode " << mode2 << "\n"; + err_msg << "- with '" << old_contract_id << "' in " + << dfcc_contract_mode_to_string(old_contract_mode) << " " + << dfcc_loop_contract_mode_to_string(old_loop_contract_mode) + << "\n"; + err_msg << "- with '" << contract_id << "' in " + << dfcc_contract_mode_to_string(contract_mode) << " " + << dfcc_loop_contract_mode_to_string(loop_contract_mode) << "\n"; throw invalid_input_exceptiont(err_msg.str()); } // same swap already performed @@ -101,6 +107,7 @@ void dfcc_swap_and_wrapt::swap_and_wrap( case dfcc_contract_modet::CHECK: { check_contract( + loop_contract_mode, function_id, contract_id, function_pointer_contracts, @@ -148,6 +155,7 @@ void dfcc_swap_and_wrapt::get_swapped_functions(std::set &dest) const /// END_FUNCTION; /// ``` void dfcc_swap_and_wrapt::check_contract( + const dfcc_loop_contract_modet loop_contract_mode, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, @@ -271,7 +279,7 @@ void dfcc_swap_and_wrapt::check_contract( // instrument the wrapped function instrument.instrument_wrapped_function( - wrapped_id, wrapper_id, function_pointer_contracts); + wrapped_id, wrapper_id, loop_contract_mode, function_pointer_contracts); goto_model.goto_functions.update(); } diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h index c3a6eefa385..06987fbcf7e 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.h @@ -38,7 +38,6 @@ class messaget; class message_handlert; class symbolt; class conditional_target_group_exprt; -class cfg_infot; class dfcc_swap_and_wrapt { @@ -53,6 +52,7 @@ class dfcc_swap_and_wrapt dfcc_contract_handlert &contract_handler); void swap_and_wrap_check( + const dfcc_loop_contract_modet loop_contract_mode, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, @@ -60,6 +60,7 @@ class dfcc_swap_and_wrapt { swap_and_wrap( dfcc_contract_modet::CHECK, + loop_contract_mode, function_id, contract_id, function_pointer_contracts, @@ -73,6 +74,7 @@ class dfcc_swap_and_wrapt { swap_and_wrap( dfcc_contract_modet::REPLACE, + dfcc_loop_contract_modet::NONE, function_id, contract_id, function_pointer_contracts, @@ -94,10 +96,15 @@ class dfcc_swap_and_wrapt namespacet ns; /// remember all functions that were swapped/wrapped and in which mode - static std::map> cache; + static std::map< + irep_idt, + std:: + pair>> + cache; void swap_and_wrap( const dfcc_contract_modet contract_mode, + const dfcc_loop_contract_modet loop_contract_mode, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, @@ -106,6 +113,7 @@ class dfcc_swap_and_wrapt /// Swaps-and-wraps the given `function_id` in a wrapper function that /// checks the given `contract_id`. void check_contract( + const dfcc_loop_contract_modet loop_contract_mode, const irep_idt &function_id, const irep_idt &contract_id, std::set &function_pointer_contracts, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp index 22c40279d03..3155088a398 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp @@ -797,7 +797,8 @@ void dfcc_wrapper_programt::encode_havoced_function_call() write_set_checks.add(goto_programt::make_dead(check_var, wrapper_sl)); } - auto label_instruction = write_set_checks.add(goto_programt::make_skip()); + auto label_instruction = + write_set_checks.add(goto_programt::make_skip(wrapper_sl)); goto_instruction->complete_goto(label_instruction); code_function_callt havoc_call( diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 79c269b14fe..3d3995631e2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1168,14 +1168,6 @@ void goto_instrument_parse_optionst::instrument_goto_program() "Use a single " FLAG_DFCC " option"); } - if(cmdline.isset(FLAG_LOOP_CONTRACTS)) - { - throw invalid_command_line_argument_exceptiont( - "Incompatible options detected", - "--" FLAG_DFCC " and --" FLAG_LOOP_CONTRACTS, - "Use either --" FLAG_DFCC " or --" FLAG_LOOP_CONTRACTS); - } - do_indirect_call_and_rtti_removal(); const irep_idt harness_id(cmdline.get_value(FLAG_DFCC)); @@ -1206,6 +1198,22 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.get_values("nondet-static-exclude").begin(), cmdline.get_values("nondet-static-exclude").end()); + if( + cmdline.isset(FLAG_LOOP_CONTRACTS) && + cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND)) + { + // When the model is produced by Kani, we must not automatically unwind + // the backjump introduced by the loop transformation. + // Automatic unwinding duplicates assertions found in the loop body, and + // since Kani expects property identifiers to remain unique. Having + // duplicate instances of the assertions makes Kani fail to handle the + // analysis results. + log.warning() << "**** WARNING: transformed loops will not be unwound " + << "after applying loop contracts. Remember to unwind " + << "them at least twice to pass unwinding-assertions." + << messaget::eom; + } + dfcc( options, goto_model, @@ -1214,7 +1222,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() : optionalt{to_enforce.front()}, allow_recursive_calls, to_replace, - false, + cmdline.isset(FLAG_LOOP_CONTRACTS), + !cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND), to_exclude_from_nondet_static, log.get_message_handler()); } @@ -1239,7 +1248,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() cmdline.get_values("nondet-static-exclude").begin(), cmdline.get_values("nondet-static-exclude").end()); - // It’s important to keep the order of contracts instrumentation, i.e., + // It's important to keep the order of contracts instrumentation, i.e., // first replacement then enforcement. We rely on contract replacement // and inlining of sub-function calls to properly annotate all // assignments. @@ -1251,6 +1260,12 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND)) { contracts.unwind_transformed_loops = false; + // When the model is produced by Kani, we must not automatically unwind + // the backjump introduced by the loop transformation. + // Automatic unwinding duplicates assertions found in the loop body, and + // since Kani expects property identifiers to remain unique. Having + // duplicate instances of the assertions makes Kani fail to handle the + // analysis results. log.warning() << "**** WARNING: transformed loops will not be unwound " << "after applying loop contracts. Remember to unwind " << "them at least twice to pass unwinding-assertions."