Skip to content

Commit 97e1e19

Browse files
ArenBabikianSaswatPadhi
ArenBabikian
authored and
SaswatPadhi
committed
Add support for quantifiers in loop contracts
1 parent 69df960 commit 97e1e19

File tree

8 files changed

+215
-0
lines changed

8 files changed

+215
-0
lines changed

‎regression/contracts/quantifiers-loop-01/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
void main()
4+
{
5+
int N = 64, a[64];
6+
for(int i = 0; i < N; ++i)
7+
// clang-format off
8+
__CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
9+
int k;
10+
(0 <= k && k < N) ==> 1 == 1
11+
})
12+
// clang-format on
13+
{
14+
a[i] = 1;
15+
}
16+
}

‎regression/contracts/quantifiers-loop-01/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
This test case checks the handling of a forall expression within
11+
a loop invariant.
12+
This test case does not check correctness of the for loop.
13+
Instead, it is a trivial quantified expression to ensure that
14+
quantifiers can be handled in loop invariants.

‎regression/contracts/quantifiers-loop-02/main.c

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#include <assert.h>
2+
3+
#define N 8
4+
5+
void main()
6+
{
7+
int a[N];
8+
for(int i = 0; i < N; ++i)
9+
// clang-format off
10+
__CPROVER_loop_invariant(
11+
(0 <= i) && (i <= N) &&
12+
__CPROVER_forall {
13+
int k;
14+
(0 <= k && k < i) ==> a[k] == 1
15+
}
16+
)
17+
// clang-format on
18+
{
19+
a[i] = 1;
20+
}
21+
22+
// clang-format off
23+
assert(__CPROVER_forall {
24+
int k;
25+
(0 <= k && k < N) ==> a[k] == 1
26+
});
27+
// clang-format on
28+
}

‎regression/contracts/quantifiers-loop-02/main.enforced.gb.txt

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
Reading GOTO program from 'main.enforced.gb'
2+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
3+
4+
__CPROVER__start /* __CPROVER__start */
5+
// 37 no location
6+
// Labels: __CPROVER_HIDE
7+
SKIP
8+
// 38 no location
9+
__CPROVER_initialize();
10+
// 39 file main.c line 5
11+
main();
12+
// 40 no location
13+
END_FUNCTION
14+
15+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
16+
17+
__CPROVER_initialize /* __CPROVER_initialize */
18+
// 17 no location
19+
// Labels: __CPROVER_HIDE
20+
SKIP
21+
// 18 file <built-in-additions> line 20
22+
__CPROVER_alloca_object = NULL;
23+
// 19 file <built-in-additions> line 14
24+
__CPROVER_dead_object = NULL;
25+
// 20 file <built-in-additions> line 13
26+
__CPROVER_deallocated = NULL;
27+
// 21 file <built-in-additions> line 23
28+
__CPROVER_malloc_failure_mode_assert_then_assume = 2;
29+
// 22 file <built-in-additions> line 22
30+
__CPROVER_malloc_failure_mode_return_null = 1;
31+
// 23 file <built-in-additions> line 17
32+
__CPROVER_malloc_is_new_array = 0 != 0;
33+
// 24 file <built-in-additions> line 15
34+
__CPROVER_malloc_object = NULL;
35+
// 25 file <built-in-additions> line 16
36+
__CPROVER_malloc_size = 0ul;
37+
// 26 file <built-in-additions> line 24
38+
__CPROVER_max_malloc_size = (__CPROVER_size_t)36028797018963968l;
39+
// 27 file <built-in-additions> line 18
40+
__CPROVER_memory_leak = NULL;
41+
// 28 file <built-in-additions> line 8
42+
__CPROVER_next_thread_id = (unsigned long int)0;
43+
// 29 file <built-in-additions> line 11
44+
__CPROVER_next_thread_key = (unsigned long int)0;
45+
// 30 file <built-in-additions> line 38
46+
__CPROVER_pipe_count = (unsigned int)0;
47+
// 31 file <built-in-additions> line 29
48+
__CPROVER_rounding_mode = 0;
49+
// 32 file <built-in-additions> line 6
50+
__CPROVER_thread_id = (unsigned long int)0;
51+
// 33 file <built-in-additions> line 10
52+
__CPROVER_thread_key_dtors = ARRAY_OF(((void (*)(void *))NULL));
53+
// 34 file <built-in-additions> line 9
54+
__CPROVER_thread_keys = ARRAY_OF(NULL);
55+
// 35 file <built-in-additions> line 7
56+
__CPROVER_threads_exited = ARRAY_OF(FALSE);
57+
// 36 no location
58+
END_FUNCTION
59+
60+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
61+
62+
main /* main */
63+
// 0 file main.c line 7 function main
64+
signed int a[8l];
65+
// 1 file main.c line 8 function main
66+
signed int i;
67+
// 2 file main.c line 8 function main
68+
i = 0;
69+
// 3 file main.c line 8 function main
70+
ASSERT 0 <= i && i <= 8 && (forall { signed int tmp; 0 <= tmp && tmp < i ==> a[(signed long int)tmp] == 1 }) // Check loop invariant before entry
71+
// 4 file main.c line 8 function main
72+
irep("(\"code\" \"\" (\"address_of\" \"\" (\"index\" \"\" (\"symbol\" \"type\" (\"array\" \"\" (\"signedbv\" \"width\" (\"32\") \"#c_type\" (\"signed_int\")) \"#source_location\" (\"\" \"file\" (\"main.c\") \"line\" (\"7\") \"function\" (\"main\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip/regression/contracts/quantifiers-loop-02\")) \"size\" (\"constant\" \"type\" (\"signedbv\" \"width\" (\"64\") \"#c_type\" (\"signed_long_int\")) \"value\" (\"8\"))) \"#source_location\" (\"\" \"file\" (\"main.c\") \"line\" (\"19\") \"function\" (\"main\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip/regression/contracts/quantifiers-loop-02\")) \"identifier\" (\"main::1::a\") \"#lvalue\" (\"1\")) \"\" (\"typecast\" \"\" (\"symbol\" \"type\" (\"signedbv\" \"width\" (\"32\") \"#c_type\" (\"signed_int\")) \"#source_location\" (\"\" \"file\" (\"main.c\") \"line\" (\"19\") \"function\" (\"main\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip/regression/contracts/quantifiers-loop-02\")) \"identifier\" (\"main::1::1::i\") \"#lvalue\" (\"1\")) \"type\" (\"signedbv\" \"width\" (\"64\") \"#c_type\" (\"signed_long_int\"))) \"type\" (\"signedbv\" \"width\" (\"32\") \"#c_type\" (\"signed_int\")) \"#source_location\" (\"\" \"file\" (\"main.c\") \"line\" (\"19\") \"function\" (\"main\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip/regression/contracts/quantifiers-loop-02\")) \"#lvalue\" (\"1\")) \"type\" (\"pointer\" \"\" (\"signedbv\" \"width\" (\"32\") \"#c_type\" (\"signed_int\")) \"width\" (\"64\"))) \"type\" (\"empty\") \"#source_location\" (\"\" \"file\" (\"main.c\") \"line\" (\"8\") \"function\" (\"main\") \"working_directory\" (\"/Users/saspadhi/Repos/cbmc-wip/regression/contracts/quantifiers-loop-02\")) \"statement\" (\"havoc_object\"))")
73+
// 5 file main.c line 8 function main
74+
i = NONDET(signed int);
75+
// 6 file main.c line 8 function main
76+
ASSUME 0 <= i && i <= 8 && (forall { signed int tmp; 0 <= tmp && tmp < i ==> a[(signed long int)tmp] == 1 })
77+
// 7 file main.c line 8 function main
78+
IF !(i < 8) THEN GOTO 1
79+
// 8 file main.c line 19 function main
80+
a[(signed long int)i] = 1;
81+
// 9 file main.c line 8 function main
82+
i = i + 1;
83+
// 10 file main.c line 8 function main
84+
ASSERT 0 <= i && i <= 8 && (forall { signed int tmp; 0 <= tmp && tmp < i ==> a[(signed long int)tmp] == 1 }) // Check that loop invariant is preserved
85+
// 11 file main.c line 8 function main
86+
ASSUME FALSE
87+
// 12 file main.c line 8 function main
88+
1: SKIP
89+
// 13 file main.c line 20 function main
90+
dead i;
91+
// 14 file main.c line 23 function main
92+
ASSERT !((signed long int)(signed long int)!(forall { signed int k; 0 <= k && k < 8 ==> a[(signed long int)k] == 1 }) != 0l) // assertion __CPROVER_forall { int k; (0 <= k && k < N) ==> a[k] == 1 }
93+
// 15 file main.c line 28 function main
94+
dead a;
95+
// 16 file main.c line 28 function main
96+
END_FUNCTION
97+

‎regression/contracts/quantifiers-loop-02/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
KNOWNBUG
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
This test case checks the handling of a forall expression within
11+
a loop invariant.
12+
In this test, the quantified variable has a symbolic upper limit.
13+
14+
Known Bug:
15+
Currently, cbmc (using the SAT back-end) does not support quantified
16+
expressions where the quantified variable has a symbolic range.

‎regression/contracts/quantifiers-loop-03/main.c

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
#include <assert.h>
2+
void main()
3+
{
4+
int N, a[64];
5+
__CPROVER_assume(0 <= N && N < 64);
6+
for(int i = 0; i < N; ++i)
7+
// clang-format off
8+
__CPROVER_loop_invariant((0 <= i) && (i <= N) && __CPROVER_forall {
9+
int k;
10+
(0 <= k && k < i) ==> a[k] == 1
11+
})
12+
// clang-format on
13+
{
14+
a[i] = 1;
15+
}
16+
// clang-format off
17+
assert(__CPROVER_forall {
18+
int k;
19+
(0 <= k && k < N) ==> a[k] == 1
20+
});
21+
// clang-format on
22+
}

‎regression/contracts/quantifiers-loop-03/test.desc

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
KNOWNBUG
2+
main.c
3+
--enforce-all-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
This test case checks the handling of a forall expression within
11+
a loop invariant.
12+
In this test, the quantified variable has a symbolic upper limit.
13+
Additionally, the number of loop iterations is also defined by a
14+
symbolic value.
15+
16+
Known Bug:
17+
Currently, cbmc (using the SAT back-end) does not support quantified
18+
expressions where the quantified variable has a symbolic range.

‎src/goto-instrument/code_contracts.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,10 @@ void code_contractst::check_apply_invariants(
9494
if(invariant.is_nil())
9595
return;
9696

97+
replace_symbolt replace;
98+
code_contractst::add_quantified_variable(invariant, replace, mode);
99+
replace(invariant);
100+
97101
// change
98102
// H: loop;
99103
// E: ...

0 commit comments

Comments
 (0)