Skip to content

Commit 33b412b

Browse files
ArenBabikianArenBabikian
committed
Add support for nested quantifiers in function contracts
This adds support for nested quantifiers in funtion contracts. We recursively handle quantifiers that are nested within other quantifiers or within Boolean connectives.
1 parent d98b56b commit 33b412b

File tree

14 files changed

+258
-31
lines changed

14 files changed

+258
-31
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: 63 additions & 29 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,35 +169,68 @@ 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)
181-
{
182-
// get quantified symbol
183-
exprt tuple = expression.operands().front();
184-
exprt quantified_variable = tuple.operands().front();
185-
symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable);
186-
187-
// create fresh symbol
188-
symbolt new_symbol = get_fresh_aux_symbol(
189-
quantified_symbol.type(),
190-
id2string(quantified_symbol.get_identifier()),
191-
"tmp",
192-
quantified_symbol.source_location(),
193-
mode,
194-
symbol_table);
195-
196-
// add created fresh symbol to expression map
197-
symbol_exprt q(
198-
quantified_symbol.get_identifier(), quantified_symbol.type());
199-
replace.insert(q, new_symbol.symbol_expr());
172+
if(expression.id() == ID_not || expression.id() == ID_typecast)
173+
{
174+
// For unary connectives, recursively check for
175+
// nested quantified formulae in the term
176+
const auto &unary_expression = to_unary_expr(expression);
177+
add_quantified_variable(unary_expression.op(), replace, mode);
178+
}
179+
if(expression.id() == ID_notequal || expression.id() == ID_implies)
180+
{
181+
// For binary connectives, recursively check for
182+
// nested quantified formulae in the left and right terms
183+
const auto &binary_expression = to_binary_expr(expression);
184+
add_quantified_variable(binary_expression.lhs(), replace, mode);
185+
add_quantified_variable(binary_expression.rhs(), replace, mode);
186+
}
187+
if(expression.id() == ID_if)
188+
{
189+
// For ternary connectives, recursively check for
190+
// nested quantified formulae in all three terms
191+
const auto &if_expression = to_if_expr(expression);
192+
add_quantified_variable(if_expression.cond(), replace, mode);
193+
add_quantified_variable(if_expression.true_case(), replace, mode);
194+
add_quantified_variable(if_expression.false_case(), replace, mode);
195+
}
196+
if(expression.id() == ID_and || expression.id() == ID_or)
197+
{
198+
// For multi-ary connectives, recursively check for
199+
// nested quantified formulae in all terms
200+
const auto &multi_ary_expression = to_multi_ary_expr(expression);
201+
for(const auto &operand : multi_ary_expression.operands())
202+
{
203+
add_quantified_variable(operand, replace, mode);
204+
}
205+
}
206+
else if(expression.id() == ID_exists || expression.id() == ID_forall)
207+
{
208+
// When a quantifier expression is found,
209+
// 1. get quantified variables
210+
const auto &quantifier_expression = to_quantifier_expr(expression);
211+
const auto &quantified_variables = quantifier_expression.variables();
212+
for(const auto &quantified_variable : quantified_variables)
213+
{
214+
// for each quantified variable...
215+
const auto &quantified_symbol = to_symbol_expr(quantified_variable);
216+
217+
// 1.1 create fresh symbol
218+
symbolt new_symbol = get_fresh_aux_symbol(
219+
quantified_symbol.type(),
220+
id2string(quantified_symbol.get_identifier()),
221+
"tmp",
222+
quantified_symbol.source_location(),
223+
mode,
224+
symbol_table);
225+
226+
// 1.2 add created fresh symbol to expression map
227+
symbol_exprt q(
228+
quantified_symbol.get_identifier(), quantified_symbol.type());
229+
replace.insert(q, new_symbol.symbol_expr());
230+
231+
// 1.3 recursively check for nested quantified formulae
232+
add_quantified_variable(quantifier_expression.where(), replace, mode);
233+
}
200234
}
201235
}
202236

‎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)