From d49ea09721cb719fe74f87dd0804debc08ef3c26 Mon Sep 17 00:00:00 2001 From: klaas Date: Tue, 5 Jun 2018 16:40:31 -0400 Subject: [PATCH] Added an initial set of tests for contracts, which (expectedly) either fail or will need to be redone once the new flags are added in. Fixed test descriptions to put comments in the correct place and updated some stylistic issues with test cases. Enabled tests that work (if with different flag name) in the current state to give a better sense of the initial state. --- regression/Makefile | 3 +- regression/contracts/CMakeLists.txt | 9 ++ regression/contracts/Makefile | 35 ++++++ regression/contracts/chain.sh | 38 ++++++ regression/contracts/function_apply_01/main.c | 20 ++++ .../contracts/function_apply_01/test.desc | 9 ++ regression/contracts/function_check_01/main.c | 31 +++++ .../contracts/function_check_01/test.desc | 11 ++ regression/contracts/function_check_02/main.c | 24 ++++ .../contracts/function_check_02/test.desc | 10 ++ regression/contracts/function_check_03/main.c | 26 ++++ .../contracts/function_check_03/test.desc | 10 ++ regression/contracts/function_check_04/main.c | 19 +++ .../contracts/function_check_04/test.desc | 11 ++ regression/contracts/function_check_05/main.c | 26 ++++ .../contracts/function_check_05/test.desc | 10 ++ .../contracts/function_check_mem_01/main.c | 45 +++++++ .../contracts/function_check_mem_01/test.desc | 10 ++ regression/contracts/invar_check_01/main.c | 20 ++++ regression/contracts/invar_check_01/test.desc | 11 ++ regression/contracts/invar_check_02/main.c | 29 +++++ regression/contracts/invar_check_02/test.desc | 11 ++ regression/contracts/invar_check_03/main.c | 85 +++++++++++++ regression/contracts/invar_check_03/test.desc | 11 ++ regression/contracts/invar_check_04/main.c | 30 +++++ regression/contracts/invar_check_04/test.desc | 12 ++ .../contracts/invar_loop_constant/main.c | 25 ++++ .../contracts/invar_loop_constant/test.desc | 9 ++ .../contracts/quicksort_contracts_01/main.c | 112 ++++++++++++++++++ .../quicksort_contracts_01/test.desc | 9 ++ 30 files changed, 710 insertions(+), 1 deletion(-) create mode 100644 regression/contracts/CMakeLists.txt create mode 100644 regression/contracts/Makefile create mode 100755 regression/contracts/chain.sh create mode 100644 regression/contracts/function_apply_01/main.c create mode 100644 regression/contracts/function_apply_01/test.desc create mode 100644 regression/contracts/function_check_01/main.c create mode 100644 regression/contracts/function_check_01/test.desc create mode 100644 regression/contracts/function_check_02/main.c create mode 100644 regression/contracts/function_check_02/test.desc create mode 100644 regression/contracts/function_check_03/main.c create mode 100644 regression/contracts/function_check_03/test.desc create mode 100644 regression/contracts/function_check_04/main.c create mode 100644 regression/contracts/function_check_04/test.desc create mode 100644 regression/contracts/function_check_05/main.c create mode 100644 regression/contracts/function_check_05/test.desc create mode 100644 regression/contracts/function_check_mem_01/main.c create mode 100644 regression/contracts/function_check_mem_01/test.desc create mode 100644 regression/contracts/invar_check_01/main.c create mode 100644 regression/contracts/invar_check_01/test.desc create mode 100644 regression/contracts/invar_check_02/main.c create mode 100644 regression/contracts/invar_check_02/test.desc create mode 100644 regression/contracts/invar_check_03/main.c create mode 100644 regression/contracts/invar_check_03/test.desc create mode 100644 regression/contracts/invar_check_04/main.c create mode 100644 regression/contracts/invar_check_04/test.desc create mode 100644 regression/contracts/invar_loop_constant/main.c create mode 100644 regression/contracts/invar_loop_constant/test.desc create mode 100644 regression/contracts/quicksort_contracts_01/main.c create mode 100644 regression/contracts/quicksort_contracts_01/test.desc diff --git a/regression/Makefile b/regression/Makefile index c41b1080e89..9d38a19e234 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -18,7 +18,8 @@ DIRS = cbmc \ goto-cc-cbmc \ cbmc-cpp \ goto-cc-goto-analyzer \ - systemc + systemc \ + contracts \ # Empty last line # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks diff --git a/regression/contracts/CMakeLists.txt b/regression/contracts/CMakeLists.txt new file mode 100644 index 00000000000..f7f08694f6a --- /dev/null +++ b/regression/contracts/CMakeLists.txt @@ -0,0 +1,9 @@ +if(WIN32) + set(is_windows true) +else() + set(is_windows false) +endif() + +add_test_pl_tests( + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $ $ ${is_windows}" +) diff --git a/regression/contracts/Makefile b/regression/contracts/Makefile new file mode 100644 index 00000000000..8d53e0b2656 --- /dev/null +++ b/regression/contracts/Makefile @@ -0,0 +1,35 @@ +default: tests.log + +include ../../src/config.inc +include ../../src/common + +ifeq ($(BUILD_ENV_),MSVC) + exe=../../../src/goto-cc/goto-cl + is_windows=true +else + exe=../../../src/goto-cc/goto-cc + is_windows=false +endif + +test: + @../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' + +tests.log: + @../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + @for dir in *; do \ + $(RM) tests.log; \ + if [ -d "$$dir" ]; then \ + cd "$$dir"; \ + $(RM) *.out *.gb; \ + cd ..; \ + fi \ + done diff --git a/regression/contracts/chain.sh b/regression/contracts/chain.sh new file mode 100755 index 00000000000..2656ea4488f --- /dev/null +++ b/regression/contracts/chain.sh @@ -0,0 +1,38 @@ +#!/bin/bash + +set -e + +goto_cc=$1 +goto_instrument=$2 +cbmc=$3 +is_windows=$4 + +name=${*:$#} +name=${name%.c} + +args=${*:5:$#-5} + +if [[ "${is_windows}" == "true" ]]; then + $goto_cc "${name}.c" + mv "${name}.exe" "${name}.gb" +else + $goto_cc -o "${name}.gb" "${name}.c" +fi + +$goto_instrument ${args} "${name}.gb" "${name}-mod.gb" +if [ ! -e "${name}-mod.gb" ] ; then + cp "$name.gb" "${name}-mod.gb" +elif echo $args | grep -q -- "--dump-c" ; then + mv "${name}-mod.gb" "${name}-mod.c" + + if [[ "${is_windows}" == "true" ]]; then + $goto_cc "${name}-mod.c" + mv "${name}-mod.exe" "${name}-mod.gb" + else + $goto_cc -o "${name}-mod.gb" "${name}-mod.c" + fi + + rm "${name}-mod.c" +fi +$goto_instrument --show-goto-functions "${name}-mod.gb" +$cbmc "${name}-mod.gb" diff --git a/regression/contracts/function_apply_01/main.c b/regression/contracts/function_apply_01/main.c new file mode 100644 index 00000000000..3112343940f --- /dev/null +++ b/regression/contracts/function_apply_01/main.c @@ -0,0 +1,20 @@ +// function_apply_01 + +// Note that this test is supposed to have an incorrect contract. +// We verify that applying (without checking) the contract yields success, +// and that checking the contract yields failure. + +#include + +int foo() + __CPROVER_ensures(__CPROVER_return_value == 0) +{ + return 1; +} + +int main() +{ + int x = foo(); + assert(x == 0); + return 0; +} diff --git a/regression/contracts/function_apply_01/test.desc b/regression/contracts/function_apply_01/test.desc new file mode 100644 index 00000000000..abc8686ad8e --- /dev/null +++ b/regression/contracts/function_apply_01/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +main.c +--apply-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Applying code contracts currently also checks them. diff --git a/regression/contracts/function_check_01/main.c b/regression/contracts/function_check_01/main.c new file mode 100644 index 00000000000..27bc259c58b --- /dev/null +++ b/regression/contracts/function_check_01/main.c @@ -0,0 +1,31 @@ +// function_check_01 + +// This tests a simple example of a function with requires and +// ensures which should both be satisfied. + +#include + +int min(int a, int b) + __CPROVER_requires(a >= 0 && b >= 0) + __CPROVER_ensures(__CPROVER_return_value <= a && + __CPROVER_return_value <= b && + (__CPROVER_return_value == a || __CPROVER_return_value == b) + ) +{ + if(a <= b) + { + return a; + } + else + { + return b; + } +} + +int main() +{ + int x, y, z; + __CPROVER_assume(x >= 0 && y >= 0); + z = min(x, y); + assert(z <= x); +} diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc new file mode 100644 index 00000000000..d9a2ec0a8ca --- /dev/null +++ b/regression/contracts/function_check_01/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +--check-code-contracts not implemented yet. +--apply-code-contracts is the current name for the flag. This should be +updated as the flag changes. diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c new file mode 100644 index 00000000000..020113bd1d5 --- /dev/null +++ b/regression/contracts/function_check_02/main.c @@ -0,0 +1,24 @@ +// function_check_02 + +// This test checks the use of quantifiers in ensures clauses. +// A known bug (resolved in PR #2278) causes the use of quantifiers +// in ensures to fail. + +int initialize(int *arr) + __CPROVER_ensures( + __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i} + ) +{ + for(int i = 0; i < 10; i++) + { + arr[i] = i; + } + + return 0; +} + +int main() +{ + int arr[10]; + initialize(arr); +} diff --git a/regression/contracts/function_check_02/test.desc b/regression/contracts/function_check_02/test.desc new file mode 100644 index 00000000000..9c4d3556c69 --- /dev/null +++ b/regression/contracts/function_check_02/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c +--check-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Ensures statements currently do not allow quantified predicates unless the +function has void return type. diff --git a/regression/contracts/function_check_03/main.c b/regression/contracts/function_check_03/main.c new file mode 100644 index 00000000000..2e2e9af0d9f --- /dev/null +++ b/regression/contracts/function_check_03/main.c @@ -0,0 +1,26 @@ +// function_check_03 + +// This extends function_check_02's test of quantifiers in ensures +// and adds in a loop invariant which can be used to prove the ensures. +// This currently fails because side-effect checking in loop invariants is +// incorrect. + +void initialize(int *arr, int len) + __CPROVER_ensures( + __CPROVER_forall {int i; (0 <= i && i < len) ==> arr[i] == i} + ) +{ + for(int i = 0; i < len; i++) + __CPROVER_loop_invariant( + __CPROVER_forall {int j; (0 <= j && j < i) ==> arr[j] == j} + ) + { + arr[i] = i; + } +} + +int main() +{ + int arr[10]; + initialize(arr, 10); +} diff --git a/regression/contracts/function_check_03/test.desc b/regression/contracts/function_check_03/test.desc new file mode 100644 index 00000000000..14848623f06 --- /dev/null +++ b/regression/contracts/function_check_03/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c +--check-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Loop invariants currently do not support memory reads in at least some +circumstances. diff --git a/regression/contracts/function_check_04/main.c b/regression/contracts/function_check_04/main.c new file mode 100644 index 00000000000..acf0122c5e4 --- /dev/null +++ b/regression/contracts/function_check_04/main.c @@ -0,0 +1,19 @@ +// function_check_04 + +// Note that this test is supposed to have an incorrect contract. +// We verify that checking this faulty contract (correctly) yields a failure. + +#include + +int foo() + __CPROVER_ensures(__CPROVER_return_value == 0) +{ + return 1; +} + +int main() +{ + int x = foo(); + assert(x == 0); + return 0; +} diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc new file mode 100644 index 00000000000..db7ee5aa32a --- /dev/null +++ b/regression/contracts/function_check_04/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-code-contracts +^\[main.assertion.1\] assertion x == 0: SUCCESS$ +^\[foo.1\] : FAILURE$ +^VERIFICATION FAILED$ +-- +-- +--check-code-contracts not implemented yet. +--apply-code-contracts is the current name for the flag. This should be +updated as the flag changes. diff --git a/regression/contracts/function_check_05/main.c b/regression/contracts/function_check_05/main.c new file mode 100644 index 00000000000..14f85546506 --- /dev/null +++ b/regression/contracts/function_check_05/main.c @@ -0,0 +1,26 @@ +// function_check_05 + +// This test checks that when a function call is replaced by an invariant, +// it adequately havocs the locations modified by the function. +// This test currently fails because the analysis of what is modified by +// a function is flawed. + +#include + +int foo(int *x) + __CPROVER_ensures(__CPROVER_return_value == 1) +{ + *x = 1; + return 1; +} + +int main() +{ + int y = 0; + int z = foo(&y); + // This assert should fail. + assert(y == 0); + // This one should succeed. + assert(z == 1); + return 0; +} diff --git a/regression/contracts/function_check_05/test.desc b/regression/contracts/function_check_05/test.desc new file mode 100644 index 00000000000..77e210f10d8 --- /dev/null +++ b/regression/contracts/function_check_05/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c +--check-code-contracts +^\[main.assertion.1\] assertion y == 0: FAILURE$ +^\[main.assertion.2\] assertion z == 1: SUCCESS$ +^\[foo.1\] : SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Contract checking does not properly havoc function calls. diff --git a/regression/contracts/function_check_mem_01/main.c b/regression/contracts/function_check_mem_01/main.c new file mode 100644 index 00000000000..b63364f4d57 --- /dev/null +++ b/regression/contracts/function_check_mem_01/main.c @@ -0,0 +1,45 @@ +// function_check_mem_01 + +// This test checks the use of pointer-related predicates in assumptions and +// requires. +// This test currently fails because of the lack of support for assuming +// pointer predicates. + +#include + +#define __CPROVER_VALID_MEM(ptr, size) \ + __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) && \ + !__CPROVER_invalid_pointer((ptr)) && \ + __CPROVER_POINTER_OBJECT((ptr)) != \ + __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \ + __CPROVER_POINTER_OBJECT((ptr)) != \ + __CPROVER_POINTER_OBJECT(__CPROVER_dead_object) && \ + (__builtin_object_size((ptr), 1) >= (size) && \ + __CPROVER_POINTER_OFFSET((ptr)) >= 0l || \ + __CPROVER_DYNAMIC_OBJECT((ptr))) && \ + (__CPROVER_POINTER_OFFSET((ptr)) >= 0 && \ + __CPROVER_malloc_size >= (size) + __CPROVER_POINTER_OFFSET((ptr)) || \ + __CPROVER_POINTER_OBJECT((ptr)) != \ + __CPROVER_POINTER_OBJECT(__CPROVER_malloc_object)) + +typedef struct bar +{ + int x; + int y; + int z; +} bar; + +void foo(bar *x) + __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar))) +{ + x->x += 1; + return +} + +int main() +{ + bar *y; + __CPROVER_assume(__CPROVER_VALID_MEM(y, sizeof(bar))); + y->x = 0; + return 0; +} diff --git a/regression/contracts/function_check_mem_01/test.desc b/regression/contracts/function_check_mem_01/test.desc new file mode 100644 index 00000000000..b46799f781b --- /dev/null +++ b/regression/contracts/function_check_mem_01/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +main.c +--check-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +CBMC currently does not support assumptions about pointers in the general way +that other assumptions are supported. diff --git a/regression/contracts/invar_check_01/main.c b/regression/contracts/invar_check_01/main.c new file mode 100644 index 00000000000..d23252ebd6b --- /dev/null +++ b/regression/contracts/invar_check_01/main.c @@ -0,0 +1,20 @@ +// invar_check_01 + +// This test checks that a basic loop invariant can be proven and used in +// combination with the negation of the loop guard to get a result. + +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + while(r > 0) + __CPROVER_loop_invariant(r >= 0) + { + --r; + } + assert(r == 0); + + return 0; +} diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc new file mode 100644 index 00000000000..d9a2ec0a8ca --- /dev/null +++ b/regression/contracts/invar_check_01/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +--check-code-contracts not implemented yet. +--apply-code-contracts is the current name for the flag. This should be +updated as the flag changes. diff --git a/regression/contracts/invar_check_02/main.c b/regression/contracts/invar_check_02/main.c new file mode 100644 index 00000000000..fee261011ea --- /dev/null +++ b/regression/contracts/invar_check_02/main.c @@ -0,0 +1,29 @@ +// invar_check_02 + +// This test checks that loop invariants adequately handle continues. + +#include + +int main() +{ + int r; + __CPROVER_assume(r >= 0); + + while(r > 0) + __CPROVER_loop_invariant(r >= 0) + { + --r; + if (r < 5) + { + continue; + } + else + { + --r; + } + } + + assert(r == 0); + + return 0; +} diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc new file mode 100644 index 00000000000..d9a2ec0a8ca --- /dev/null +++ b/regression/contracts/invar_check_02/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +--check-code-contracts not implemented yet. +--apply-code-contracts is the current name for the flag. This should be +updated as the flag changes. diff --git a/regression/contracts/invar_check_03/main.c b/regression/contracts/invar_check_03/main.c new file mode 100644 index 00000000000..253e5a951d6 --- /dev/null +++ b/regression/contracts/invar_check_03/main.c @@ -0,0 +1,85 @@ +// invar_check_03 + +// This test checks the use of loop invariants on a larger problem --- in this +// case, the partition portion 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. + +#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) + __CPROVER_loop_invariant( + 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) + ) + { + 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 if(*(arr[h]) <= pivot) { + l++; + } + else { + h--; + } + } + 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); + return r; +} diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc new file mode 100644 index 00000000000..d9a2ec0a8ca --- /dev/null +++ b/regression/contracts/invar_check_03/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--apply-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +--check-code-contracts not implemented yet. +--apply-code-contracts is the current name for the flag. This should be +updated as the flag changes. diff --git a/regression/contracts/invar_check_04/main.c b/regression/contracts/invar_check_04/main.c new file mode 100644 index 00000000000..68c2fa4ceea --- /dev/null +++ b/regression/contracts/invar_check_04/main.c @@ -0,0 +1,30 @@ +// invar_check_04 + +// This test checks the handling of break by loop invariants. +// This test is expected to fail along the code path where r is even before +// entering the loop. + +#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/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc new file mode 100644 index 00000000000..7414b7f58a6 --- /dev/null +++ b/regression/contracts/invar_check_04/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--apply-code-contracts +^\[main.1\] Loop invariant violated before entry: SUCCESS$ +^\[main.2\] Loop invariant not preserved: SUCCESS$ +^\[main.assertion.1\] assertion r == 0: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +--check-code-contracts not implemented yet. +--apply-code-contracts is the current name for the flag. This should be +updated as the flag changes. diff --git a/regression/contracts/invar_loop_constant/main.c b/regression/contracts/invar_loop_constant/main.c new file mode 100644 index 00000000000..34eb0575d53 --- /dev/null +++ b/regression/contracts/invar_loop_constant/main.c @@ -0,0 +1,25 @@ +// invar_loop_constant + +// This test checks to see whether loop invariant checking discards sufficiently +// little information to be aware after the loop that s is necessarily 1. +// This test currently fails due to excessive havocking in checking loop +// invariants, but is not an obstacle to soundness of contract checking. + +#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/invar_loop_constant/test.desc b/regression/contracts/invar_loop_constant/test.desc new file mode 100644 index 00000000000..a27604a79fd --- /dev/null +++ b/regression/contracts/invar_loop_constant/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +main.c +--check-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Loop invariant checking throws away more information than needed. diff --git a/regression/contracts/quicksort_contracts_01/main.c b/regression/contracts/quicksort_contracts_01/main.c new file mode 100644 index 00000000000..3b846a927d3 --- /dev/null +++ b/regression/contracts/quicksort_contracts_01/main.c @@ -0,0 +1,112 @@ +// 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/quicksort_contracts_01/test.desc b/regression/contracts/quicksort_contracts_01/test.desc new file mode 100644 index 00000000000..683f54a5b7a --- /dev/null +++ b/regression/contracts/quicksort_contracts_01/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +main.c +--check-code-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Loop invariants are overzealous in deciding what counts as side effects.