Skip to content

Commit 47c1c7e

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #6399 from NlightNFotis/fix_6231
Allow checks to be performed inside quantifier statements.
2 parents 73fbad9 + bc772e4 commit 47c1c7e

29 files changed

+507
-50
lines changed

‎regression/cbmc-primitives/CMakeLists.txt

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,11 @@
1-
add_test_pl_tests(
2-
"$<TARGET_FILE:cbmc>"
3-
)
1+
find_program(Z3_EXISTS "z3")
2+
message(${Z3_EXISTS})
3+
if(Z3_EXISTS)
4+
add_test_pl_tests(
5+
"$<TARGET_FILE:cbmc>"
6+
)
7+
else()
8+
add_test_pl_tests(
9+
"$<TARGET_FILE:cbmc>" -X smt-backend
10+
)
11+
endif()

‎regression/cbmc-primitives/alternating_quantifiers_6231/exists_in_forall.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <stdlib.h>
2+
3+
// clang-format off
4+
int main(int argc, char **argv)
5+
{
6+
int *i = malloc(sizeof(int));
7+
*i = 1;
8+
9+
__CPROVER_assert(
10+
__CPROVER_forall { int z; (0 < z && z < 10) ==>
11+
__CPROVER_exists { int y; ( 10 < y && y < 20) && y == z + 10 && y > *i } },
12+
"for all z, there exists a y so that y = z + 10 and y > 1");
13+
}
14+
// clang-format on

‎regression/cbmc-primitives/alternating_quantifiers_6231/exists_in_forall.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
exists_in_forall.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.1\] line \d* for all z, there exists a y so that y = z \+ 10 and y > 1: SUCCESS
7+
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in \*i: SUCCESS
8+
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in \*i: SUCCESS
9+
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in \*i: SUCCESS
10+
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in \*i: SUCCESS
11+
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in \*i: SUCCESS
12+
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in \*i: SUCCESS
13+
--
14+
--
15+
The assertion reference number here is present so that we make sure
16+
we always match the properties of the dereference inside the exists.

‎regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <stdlib.h>
2+
3+
// clang-format off
4+
int main(int argc, char **argv)
5+
{
6+
int *i = malloc(sizeof(int));
7+
*i = 1;
8+
9+
__CPROVER_assert(
10+
__CPROVER_exists { int z; (0 < z && z < 2) &&
11+
__CPROVER_forall { int o; (10 < o && o < 20) ==> o > z && z == * i }},
12+
"there exists a z between 0 and 2 so that for all o between 10 and 20, o > z and z = 1");
13+
}
14+
// clang-format on

‎regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
forall_in_exists.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.1\] line \d* there exists a z between 0 and 2 so that for all o between 10 and 20, o > z and z = 1: SUCCESS
7+
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in \*i: SUCCESS
8+
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in \*i: SUCCESS
9+
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in \*i: SUCCESS
10+
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in \*i: SUCCESS
11+
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in \*i: SUCCESS
12+
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in \*i: SUCCESS
13+
--
14+
--

‎regression/cbmc-primitives/exists_assume_6231/test.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <stdlib.h>
2+
3+
// clang-format off
4+
int main(int argc, char **argv)
5+
{
6+
int *i = malloc(sizeof(int));
7+
*i = 1;
8+
9+
// The exists inside the assume will evaluate to true,
10+
// and be flipped by the negation in front of it, resulting
11+
// to assume(false), which will allow the assertion to evaluate
12+
// to true.
13+
__CPROVER_assume(
14+
!__CPROVER_exists{int z; (z > 1 && z < 10) && z > *i}
15+
);
16+
__CPROVER_assert(0, "this assertion should be satified");
17+
}
18+
// clang-format on

‎regression/cbmc-primitives/exists_assume_6231/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.1\] line \d+ this assertion should be satified: SUCCESS
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
^warning: ignoring forall
10+
--

‎regression/cbmc-primitives/exists_assume_6231/test2.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <stdlib.h>
2+
3+
// clang-format off
4+
int main(int argc, char **argv)
5+
{
6+
int *i = malloc(sizeof(int));
7+
*i = 1;
8+
9+
// The exists inside the assume will evaluate to true,
10+
// and as such, the assertion below will fail as expected.
11+
__CPROVER_assume(
12+
__CPROVER_exists{int z; (z > 1 && z < 10) && z > *i}
13+
);
14+
__CPROVER_assert(0, "this should come out as failure");
15+
}
16+
// clang-format on

‎regression/cbmc-primitives/exists_assume_6231/test2.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test2.c
3+
--pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
\[main\.assertion\.1\] line \d+ this should come out as failure: FAILURE
7+
^VERIFICATION FAILED$
8+
--
9+
^warning: ignoring forall
10+
--

‎regression/cbmc-primitives/exists_memory_checks/invalid_index_range.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
int main()
5+
{
6+
int *a = calloc(10, sizeof(int));
7+
a[5] = 25;
8+
9+
assert(__CPROVER_exists {
10+
int i;
11+
(0 <= i && i < 20) && a[i] == i *i
12+
});
13+
}

‎regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
invalid_index_range.c
3+
--pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 20\) && a\[i\] == i \*i \}: SUCCESS
8+
line 9 dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
9+
--
10+
--
11+
Check that memory checks fail for pointer dereferences inside an existential
12+
qualifier, for out of bounds memory access.

‎regression/cbmc-primitives/exists_memory_checks/negated_exists.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
int main()
5+
{
6+
int *a = calloc(10, sizeof(int));
7+
a[5] = 25;
8+
9+
assert(!__CPROVER_exists {
10+
int i;
11+
(0 <= i && i < 10) && a[i] == 42
12+
});
13+
}

‎regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
negated_exists.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
\[main\.assertion\.1\] line 9 assertion !__CPROVER_exists \{ int i; \(0 <= i && i < 10\) && a\[i\] == 42 \}: SUCCESS
8+
\[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
9+
\[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
10+
\[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11+
\[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
12+
\[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
13+
\[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
14+
--
15+
--
16+
Check that memory checks pass for valid pointer dereferences inside a negated
17+
existential qualifier.

‎regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
int main()
5+
{
6+
int *a = calloc(10, sizeof(int));
7+
a[5] = 25;
8+
9+
assert(__CPROVER_exists {
10+
int i;
11+
a[i] == i *i
12+
});
13+
}

‎regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE smt-backend
2+
smt_missing_range_check.c
3+
--pointer-check -z3
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: SUCCESS
8+
\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
9+
--
10+
--
11+
Check that memory checks fail for pointer dereferences inside an existential
12+
qualifier, for out of bounds memory access, when using the smt backend and
13+
the range of the index is unbound. Note that this test is not expected to work
14+
with the SAT backend at the time of writing, as the SAT backend does not support
15+
qualifiers in this form.

‎regression/cbmc-primitives/exists_memory_checks/valid_index_range.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
int main()
5+
{
6+
int *a = calloc(10, sizeof(int));
7+
a[5] = 25;
8+
9+
assert(__CPROVER_exists {
10+
int i;
11+
(0 <= i && i < 10) && a[i] == i *i
12+
});
13+
}

‎regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
valid_index_range.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 10\) && a\[i\] == i \*i \}: SUCCESS
8+
\[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
9+
\[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
10+
\[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11+
\[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
12+
\[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
13+
\[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
14+
--
15+
--
16+
Check that memory checks pass for valid pointer dereferences inside an
17+
existential qualifier.

‎regression/cbmc-primitives/forall_6231_1/test.c

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
// clang-format off
5+
int main() {
6+
char *a = malloc(1);
7+
8+
assert(*a == *a);
9+
10+
// BUG: In https://github.com/diffblue/cbmc/issues/6231, it was reported that
11+
// no checks would be performed on the derefence inside the quantified statement,
12+
// even when explicitly requested via for instance `--pointer-check`, because
13+
// we would simply skip over these quantified statements in goto-check.
14+
assert(
15+
__CPROVER_forall {
16+
int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)
17+
}
18+
);
19+
}
20+
// clang-format on

‎regression/cbmc-primitives/forall_6231_1/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
test.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
7+
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
8+
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
9+
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
10+
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11+
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
12+
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
13+
^VERIFICATION SUCCESSFUL$
14+
--
15+
--
16+
This is fixing an issue first reported in https://github.com/diffblue/cbmc/issues/6231

‎regression/cbmc-primitives/forall_6231_2/test.c

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
// clang-format off
5+
int main() {
6+
char *a = malloc(128);
7+
8+
// BUG: In https://github.com/diffblue/cbmc/issues/6231, it was reported that
9+
// no checks would be performed on the derefence inside the quantified statement,
10+
// even when explicitly requested via for instance `--pointer-check`, because
11+
// we would simply skip over these quantified statements in goto-check.
12+
assert(
13+
__CPROVER_forall {
14+
int i ; (0 <= i && i < 1) ==> *(a+i) == *(a+i)
15+
}
16+
);
17+
18+
assert(
19+
__CPROVER_forall {
20+
int j; !(0 <= j && j < 1) || (j == 0 && *(a+j) == *(a+j))
21+
});
22+
}
23+
// clang-format on

‎regression/cbmc-primitives/forall_6231_2/test.desc

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
CORE
2+
test.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.1\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
7+
\[main\.pointer_dereference\.1\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
8+
\[main\.pointer_dereference\.2\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
9+
\[main\.pointer_dereference\.3\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
10+
\[main\.pointer_dereference\.4\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11+
\[main\.pointer_dereference\.5\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
12+
\[main\.pointer_dereference\.6\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
13+
\[main\.assertion.2] line \d+ assertion __CPROVER_forall \{ int j; \!\(0 <= j && j < 1\) || \(j == 0 && \*\(a\+j\) == \*\(a+j\)\) \}: SUCCESS
14+
\[main\.pointer_dereference\.7] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)j\]: SUCCESS
15+
\[main\.pointer_dereference\.8] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)j\]: SUCCESS
16+
\[main\.pointer_dereference\.9] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)j\]: SUCCESS
17+
\[main\.pointer_dereference\.10] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)j\]: SUCCESS
18+
\[main\.pointer_dereference\.11] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)j\]: SUCCESS
19+
\[main\.pointer_dereference\.12] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)j\]: SUCCESS
20+
^VERIFICATION SUCCESSFUL$
21+
--
22+
--
23+
This is fixing an issue first reported in https://github.com/diffblue/cbmc/issues/6231

‎regression/cbmc-primitives/forall_6231_3/test.c

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
// This is essentially the same file as in test `forall_6231_1`, with the difference
5+
// being that the forall statement contains a bigger bound, so that we are to have
6+
// more concrete instantiations of the bound variable.
7+
8+
// clang-format off
9+
int main() {
10+
char *a = malloc(10);
11+
12+
assert(*a == *a);
13+
14+
// BUG: In https://github.com/diffblue/cbmc/issues/6231, it was reported that
15+
// no checks would be performed on the derefence inside the quantified statement,
16+
// even when explicitly requested via for instance `--pointer-check`, because
17+
// we would simply skip over these quantified statements in goto-check.
18+
assert(
19+
__CPROVER_forall {
20+
int i ; (0 <= i && i < 10) ==> *(a+i) == *(a+i)
21+
}
22+
);
23+
}
24+
// clang-format on

‎regression/cbmc-primitives/forall_6231_3/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
test.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
7+
\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
8+
\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
9+
\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
10+
\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11+
\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
12+
\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
13+
^VERIFICATION SUCCESSFUL$
14+
--
15+
--
16+
This is fixing an issue first reported in https://github.com/diffblue/cbmc/issues/6231

0 commit comments

Comments
 (0)