Skip to content

Commit 6224332

Browse files
ArenBabikianSaswatPadhi
ArenBabikian
authored and
SaswatPadhi
committed
Add support for quantifiers in loop contracts
1 parent ef9e076 commit 6224332

File tree

8 files changed

+234
-5
lines changed

8 files changed

+234
-5
lines changed

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
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(
9+
(0 <= i) && (i <= N) &&
10+
__CPROVER_forall {
11+
int k;
12+
(0 <= k && k < N) ==> 1 == 1
13+
}
14+
)
15+
// clang-format on
16+
{
17+
a[i] = 1;
18+
}
19+
}

‎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; 0 <= tmp$0 && tmp$0 < i ==> a[(signed long int)tmp$0] == 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$1; 0 <= tmp$1 && tmp$1 < i ==> a[(signed long int)tmp$1] == 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: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
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(
9+
(0 <= i) && (i <= N) &&
10+
__CPROVER_forall {
11+
int k;
12+
(0 <= k && k < i) ==> a[k] == 1
13+
}
14+
)
15+
// clang-format on
16+
{
17+
a[i] = 1;
18+
}
19+
// clang-format off
20+
assert(__CPROVER_forall {
21+
int k;
22+
(0 <= k && k < N) ==> a[k] == 1
23+
});
24+
// clang-format on
25+
}

‎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: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -114,9 +114,19 @@ void code_contractst::check_apply_invariants(
114114
// build the havocking code
115115
goto_programt havoc_code;
116116

117+
// process quantified variables correctly (introduce a fresh temporary)
118+
// and return a copy of the invariant
119+
const auto &invariant_expr = [&]() {
120+
auto invariant_copy = invariant;
121+
replace_symbolt replace;
122+
code_contractst::add_quantified_variable(invariant_copy, replace, mode);
123+
replace(invariant_copy);
124+
return invariant_copy;
125+
};
126+
117127
// assert the invariant
118128
{
119-
code_assertt assertion{invariant};
129+
code_assertt assertion{invariant_expr()};
120130
assertion.add_source_location() = loop_head->source_location;
121131
converter.goto_convert(assertion, havoc_code, mode);
122132
havoc_code.instructions.back().source_location.set_comment(
@@ -127,9 +137,11 @@ void code_contractst::check_apply_invariants(
127137
build_havoc_code(loop_head, modifies, havoc_code);
128138

129139
// assume the invariant
130-
code_assumet assumption{invariant};
131-
assumption.add_source_location() = loop_head->source_location;
132-
converter.goto_convert(assumption, havoc_code, mode);
140+
{
141+
code_assumet assumption{invariant_expr()};
142+
assumption.add_source_location() = loop_head->source_location;
143+
converter.goto_convert(assumption, havoc_code, mode);
144+
}
133145

134146
// non-deterministically skip the loop if it is a do-while loop
135147
if(!loop_head->is_goto())
@@ -145,7 +157,7 @@ void code_contractst::check_apply_invariants(
145157

146158
// assert the invariant at the end of the loop body
147159
{
148-
code_assertt assertion{invariant};
160+
code_assertt assertion{invariant_expr()};
149161
assertion.add_source_location() = loop_end->source_location;
150162
converter.goto_convert(assertion, havoc_code, mode);
151163
havoc_code.instructions.back().source_location.set_comment(

0 commit comments

Comments
 (0)