Skip to content

Commit d79e5f0

Browse files
SaswatPadhiSaswatPadhi
authored
Merge pull request #5968 from ArenBabikian/contracts-quantifiers-nested
Support nested quantifiers within function contracts
2 parents 99f1a2e + 33b412b commit d79e5f0

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)