Skip to content

Commit fbeef9e

Browse files
ArenBabikianArenBabikian
committed
Add support for nested quantifiers in function contracts
This adds support for nested quantifiers in funtion contracts. We recusrively handle quantifiers that are nested within other quantifiers or within and/or/implies statements.
1 parent d98b56b commit fbeef9e

File tree

14 files changed

+240
-17
lines changed

14 files changed

+240
-17
lines changed

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

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
3+
int i;
4+
__CPROVER_forall
5+
{
6+
int j;
7+
(0 <= i && i < 10 && i <= j && j < 10) ==> arr[i] <= arr[j]
8+
}
9+
})
10+
// clang-format on
11+
{
12+
for(int i = 0; i < 10; i++)
13+
{
14+
arr[i] = i;
15+
}
16+
17+
return 0;
18+
}
19+
20+
int main()
21+
{
22+
int arr[10];
23+
f1(arr);
24+
}

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
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
11+
nested within another forall expression.

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
3+
int i;
4+
0 <= i && i < 9 ==> __CPROVER_forall
5+
{
6+
int j;
7+
(i <= j && j < 10) ==> arr[i] <= arr[j]
8+
}
9+
}) __CPROVER_ensures(__CPROVER_return_value == 0)
10+
// clang-format on
11+
{
12+
return 0;
13+
}
14+
15+
int main()
16+
{
17+
int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
18+
f1(arr);
19+
}

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-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
11+
nested within an implication.

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int f1(int *arr)
2+
__CPROVER_ensures(__CPROVER_return_value == 0 && __CPROVER_exists {
3+
int i;
4+
(0 <= i && i < 10) && arr[i] == i
5+
})
6+
{
7+
for(int i = 0; i < 10; i++)
8+
{
9+
arr[i] = i;
10+
}
11+
12+
return 0;
13+
}
14+
15+
int main()
16+
{
17+
int arr[10];
18+
f1(arr);
19+
}

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
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 an exists expression
11+
nested within a conjunction.

‎regression/contracts/quantifiers-nested-04/main.c

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_requires(
3+
__CPROVER_forall {
4+
int i;
5+
(0 <= i && i < 10) ==> arr[i] == 0
6+
} ||
7+
arr[9] == -1 ||
8+
__CPROVER_exists {
9+
int i;
10+
(0 <= i && i < 10) && arr[i] == i
11+
}) __CPROVER_ensures(__CPROVER_return_value == 0)
12+
// clang-format on
13+
{
14+
return 0;
15+
}
16+
17+
int main()
18+
{
19+
int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
20+
f1(arr);
21+
}

‎regression/contracts/quantifiers-nested-04/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
This test case checks the handling of both a forall expression
11+
and an exists expression nested within a disjunction.

‎regression/contracts/quantifiers-nested-05/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_requires(!__CPROVER_forall {
3+
int i;
4+
(0 <= i && i < 10) ==> arr[i] == 0
5+
}) __CPROVER_ensures(__CPROVER_return_value == 0)
6+
// clang-format on
7+
{
8+
return 0;
9+
}
10+
11+
int main()
12+
{
13+
int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
14+
f1(arr);
15+
}

‎regression/contracts/quantifiers-nested-05/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-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
11+
nested within a negation.

‎regression/contracts/quantifiers-nested-06/main.c

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// clang-format off
2+
int f1(int *arr) __CPROVER_requires(
3+
(__CPROVER_forall {
4+
int i;
5+
(0 <= i && i < 10) ==> arr[i] == 0
6+
} ? __CPROVER_exists {
7+
int i;
8+
(0 <= i && i < 10) ==> arr[i] == 0
9+
} : 1 == 0) &&
10+
(__CPROVER_forall {
11+
int i;
12+
(0 <= i && i < 10) ==> arr[i] == i
13+
} ? 1 == 0 :
14+
__CPROVER_forall {
15+
int i;
16+
(0 <= i && i < 10) ==> arr[i] == 0
17+
})) __CPROVER_ensures(__CPROVER_return_value == 0)
18+
// clang-format on
19+
{
20+
return 0;
21+
}
22+
23+
int main()
24+
{
25+
int arr[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
26+
f1(arr);
27+
}

‎regression/contracts/quantifiers-nested-06/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--replace-all-calls-with-contracts
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
Verification:
10+
This test case checks the handling of forall and exists expressions
11+
nested within ternary ITE expressions (condition ? true : false).

‎src/goto-instrument/code_contracts.cpp

Lines changed: 45 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ Date: February 2016
2626
#include <util/expr_util.h>
2727
#include <util/format_type.h>
2828
#include <util/fresh_symbol.h>
29+
#include <util/mathematical_expr.h>
2930
#include <util/mathematical_types.h>
3031
#include <util/message.h>
3132
#include <util/pointer_offset_size.h>
@@ -168,23 +169,48 @@ void code_contractst::add_quantified_variable(
168169
replace_symbolt &replace,
169170
irep_idt mode)
170171
{
171-
// If the expression is a quantified expression, this function adds
172-
// the quantified variable to the symbol table and to the expression map
173-
174-
// TODO Currently only works if the contract contains only a single
175-
// quantified formula
176-
// i.e. (1) the top-level element is a quantifier formula
177-
// and (2) there are no inner quantifier formulae
178-
// This TODO is handled in PR #5968
179-
180-
if(expression.id() == ID_exists || expression.id() == ID_forall)
172+
if(expression.id() == ID_not || expression.id() == ID_typecast)
181173
{
182-
// get quantified symbol
183-
exprt tuple = expression.operands().front();
184-
exprt quantified_variable = tuple.operands().front();
174+
// For unary connectives, recursively check for
175+
// nested quantified formulae in the term
176+
unary_exprt unary_expression = to_unary_expr(expression);
177+
exprt term = unary_expression.operands().at(0);
178+
add_quantified_variable(term, replace, mode);
179+
}
180+
if(
181+
expression.id() == ID_and || expression.id() == ID_or ||
182+
expression.id() == ID_notequal || expression.id() == ID_implies)
183+
{
184+
// For binary connectives, recursively check for
185+
// nested quantified formulae in the left and right terms
186+
binary_exprt binary_expression = to_binary_expr(expression);
187+
exprt left = binary_expression.operands().at(0);
188+
add_quantified_variable(left, replace, mode);
189+
exprt right = binary_expression.operands().at(1);
190+
add_quantified_variable(right, replace, mode);
191+
}
192+
if(expression.id() == ID_if)
193+
{
194+
// For ternary connectives, recursively check for
195+
// nested quantified formulae in all three terms
196+
if_exprt if_expression = to_if_expr(expression);
197+
exprt condition = if_expression.operands().at(0);
198+
add_quantified_variable(condition, replace, mode);
199+
exprt first = if_expression.operands().at(1);
200+
add_quantified_variable(first, replace, mode);
201+
exprt second = if_expression.operands().at(2);
202+
add_quantified_variable(second, replace, mode);
203+
}
204+
else if(expression.id() == ID_exists || expression.id() == ID_forall)
205+
{
206+
// When a quantifier expression is found,
207+
// 1. get quantified symbol
208+
quantifier_exprt quantifier_expression = to_quantifier_expr(expression);
209+
exprt tuple = quantifier_expression.operands().at(0);
210+
exprt quantified_variable = tuple.operands().at(0);
185211
symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable);
186212

187-
// create fresh symbol
213+
// 2. create fresh symbol
188214
symbolt new_symbol = get_fresh_aux_symbol(
189215
quantified_symbol.type(),
190216
id2string(quantified_symbol.get_identifier()),
@@ -193,10 +219,14 @@ void code_contractst::add_quantified_variable(
193219
mode,
194220
symbol_table);
195221

196-
// add created fresh symbol to expression map
222+
// 3. add created fresh symbol to expression map
197223
symbol_exprt q(
198224
quantified_symbol.get_identifier(), quantified_symbol.type());
199225
replace.insert(q, new_symbol.symbol_expr());
226+
227+
// 4. recursively check for nested quantified formulae
228+
exprt quantified_expression = quantifier_expression.operands().at(1);
229+
add_quantified_variable(quantified_expression, replace, mode);
200230
}
201231
}
202232

‎src/goto-instrument/code_contracts.h

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -167,8 +167,10 @@ class code_contractst
167167
void
168168
add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest);
169169

170-
/// If the expression is a quantified expression, this function adds
171-
/// the quantified variable to the symbol table and to the expression map
170+
// This function recursively searches the expression to find nested or
171+
// non-nested quantified expressions. When a quantified expression is found,
172+
// the quantified variable is added to the symbol table
173+
// and to the expression map.
172174
void add_quantified_variable(
173175
exprt expression,
174176
replace_symbolt &replace,

0 commit comments

Comments
 (0)