Skip to content

Commit 9c925b9

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 9c925b9

File tree

14 files changed

+279
-48
lines changed

14 files changed

+279
-48
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: 84 additions & 46 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>
@@ -149,7 +150,7 @@ static void check_apply_invariants(
149150

150151
// change the back edge into assume(false) or assume(guard)
151152
loop_end->targets.clear();
152-
loop_end->type=ASSUME;
153+
loop_end->type = ASSUME;
153154
if(loop_head->is_goto())
154155
loop_end->set_condition(false_exprt());
155156
else
@@ -168,23 +169,56 @@ 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)
173+
{
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(expression.id() == ID_notequal || expression.id() == ID_implies)
181+
{
182+
// For binary connectives, recursively check for
183+
// nested quantified formulae in the left and right terms
184+
binary_exprt binary_expression = to_binary_expr(expression);
185+
exprt left = binary_expression.operands().at(0);
186+
add_quantified_variable(left, replace, mode);
187+
exprt right = binary_expression.operands().at(1);
188+
add_quantified_variable(right, replace, mode);
189+
}
190+
if(expression.id() == ID_if)
191+
{
192+
// For ternary connectives, recursively check for
193+
// nested quantified formulae in all three terms
194+
if_exprt if_expression = to_if_expr(expression);
195+
exprt condition = if_expression.operands().at(0);
196+
add_quantified_variable(condition, replace, mode);
197+
exprt first = if_expression.operands().at(1);
198+
add_quantified_variable(first, replace, mode);
199+
exprt second = if_expression.operands().at(2);
200+
add_quantified_variable(second, replace, mode);
201+
}
202+
if(expression.id() == ID_and || expression.id() == ID_or)
203+
{
204+
// For multi-ary connectives, recursively check for
205+
// nested quantified formulae in all terms
206+
multi_ary_exprt multi_ary_expression = to_multi_ary_expr(expression);
207+
for(auto operand : multi_ary_expression.operands())
208+
{
209+
add_quantified_variable(operand, replace, mode);
210+
}
211+
}
212+
else if(expression.id() == ID_exists || expression.id() == ID_forall)
181213
{
182-
// get quantified symbol
183-
exprt tuple = expression.operands().front();
184-
exprt quantified_variable = tuple.operands().front();
214+
// When a quantifier expression is found,
215+
// 1. get quantified symbol
216+
quantifier_exprt quantifier_expression = to_quantifier_expr(expression);
217+
exprt tuple = quantifier_expression.operands().at(0);
218+
exprt quantified_variable = tuple.operands().at(0);
185219
symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable);
186220

187-
// create fresh symbol
221+
// 2. create fresh symbol
188222
symbolt new_symbol = get_fresh_aux_symbol(
189223
quantified_symbol.type(),
190224
id2string(quantified_symbol.get_identifier()),
@@ -193,10 +227,14 @@ void code_contractst::add_quantified_variable(
193227
mode,
194228
symbol_table);
195229

196-
// add created fresh symbol to expression map
230+
// 3. add created fresh symbol to expression map
197231
symbol_exprt q(
198232
quantified_symbol.get_identifier(), quantified_symbol.type());
199233
replace.insert(q, new_symbol.symbol_expr());
234+
235+
// 4. recursively check for nested quantified formulae
236+
exprt quantified_expression = quantifier_expression.operands().at(1);
237+
add_quantified_variable(quantified_expression, replace, mode);
200238
}
201239
}
202240

@@ -267,7 +305,7 @@ bool code_contractst::apply_function_contract(
267305
}
268306

269307
// Replace formal parameters
270-
code_function_callt::argumentst::const_iterator a_it=
308+
code_function_callt::argumentst::const_iterator a_it =
271309
call.arguments().begin();
272310
for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
273311
p_it != type.parameters().end() && a_it != call.arguments().end();
@@ -482,38 +520,38 @@ void code_contractst::instrument_call_statement(
482520

483521
return;
484522
}
485-
else // Called function has assigns clause
523+
else // Called function has assigns clause
524+
{
525+
replace_symbolt replace;
526+
// Replace formal parameters
527+
code_function_callt::argumentst::const_iterator a_it =
528+
call.arguments().begin();
529+
for(code_typet::parameterst::const_iterator p_it =
530+
called_type.parameters().begin();
531+
p_it != called_type.parameters().end() &&
532+
a_it != call.arguments().end();
533+
++p_it, ++a_it)
486534
{
487-
replace_symbolt replace;
488-
// Replace formal parameters
489-
code_function_callt::argumentst::const_iterator a_it =
490-
call.arguments().begin();
491-
for(code_typet::parameterst::const_iterator p_it =
492-
called_type.parameters().begin();
493-
p_it != called_type.parameters().end() &&
494-
a_it != call.arguments().end();
495-
++p_it, ++a_it)
535+
if(!p_it->get_identifier().empty())
496536
{
497-
if(!p_it->get_identifier().empty())
498-
{
499-
symbol_exprt p(p_it->get_identifier(), p_it->type());
500-
replace.insert(p, *a_it);
501-
}
537+
symbol_exprt p(p_it->get_identifier(), p_it->type());
538+
replace.insert(p, *a_it);
502539
}
503-
504-
replace(called_assigns);
505-
506-
// check compatibility of assigns clause with the called function
507-
assigns_clauset called_assigns_clause(
508-
called_assigns, *this, function_id, log);
509-
exprt compatible =
510-
assigns_clause.compatible_expression(called_assigns_clause);
511-
goto_programt alias_assertion;
512-
alias_assertion.add(goto_programt::make_assertion(
513-
compatible, instruction_iterator->source_location));
514-
program.insert_before_swap(instruction_iterator, alias_assertion);
515-
++instruction_iterator;
516540
}
541+
542+
replace(called_assigns);
543+
544+
// check compatibility of assigns clause with the called function
545+
assigns_clauset called_assigns_clause(
546+
called_assigns, *this, function_id, log);
547+
exprt compatible =
548+
assigns_clause.compatible_expression(called_assigns_clause);
549+
goto_programt alias_assertion;
550+
alias_assertion.add(goto_programt::make_assertion(
551+
compatible, instruction_iterator->source_location));
552+
program.insert_before_swap(instruction_iterator, alias_assertion);
553+
++instruction_iterator;
554+
}
517555
}
518556

519557
bool code_contractst::check_for_looped_mallocs(const goto_programt &program)
@@ -787,7 +825,7 @@ void code_contractst::add_contract_check(
787825
.symbol_expr();
788826
check.add(goto_programt::make_decl(r, skip->source_location));
789827

790-
call.lhs()=r;
828+
call.lhs() = r;
791829
return_stmt = code_returnt(r);
792830

793831
symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());

0 commit comments

Comments
 (0)