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+
}

0 commit comments

Comments
 (0)