Skip to content

Commit 29c9935

Browse files
committed
Enable enumerating mode for checks other than pointer checks
1 parent 9f97bb2 commit 29c9935

File tree

4 files changed

+51
-11
lines changed

4 files changed

+51
-11
lines changed

regression/goto-synthesizer/loop_contracts_synthesis_assert_false/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
#include <stdlib.h>
21
#include <stdbool.h>
2+
#include <stdlib.h>
33

44
void main()
55
{
@@ -12,6 +12,6 @@ void main()
1212
x = 1;
1313
y = y - 1;
1414
}
15-
15+
1616
assert(false);
1717
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <stdlib.h>
2+
3+
void main()
4+
{
5+
long x = 0;
6+
long y;
7+
__CPROVER_assume(y > 1);
8+
9+
while(y > 0)
10+
{
11+
x = 1;
12+
y = y - 1;
13+
}
14+
assert(y == 0);
15+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
7+
^\[main.assigns.\d+\] .* Check that x is assignable: SUCCESS$
8+
^\[main.assigns.\d+\] .* Check that y is assignable: SUCCESS$
9+
^\[main.assertion.\d+\] .* assertion y \=\=
10+
^VERIFICATION SUCCESSFUL$
11+
--
12+
--
13+
Check whether loop invariant are synthesized for checks other than
14+
pointer checks.

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

Lines changed: 20 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -73,8 +73,8 @@ std::vector<exprt> construct_terminals(const std::set<symbol_exprt> &symbols)
7373
unary_exprt(ID_loop_entry, e, e.type()), size_type()));
7474
}
7575
}
76-
result.push_back(from_integer(1, unsigned_int_type()));
77-
result.push_back(from_integer(1, unsigned_long_int_type()));
76+
result.push_back(from_integer(1, signed_short_int_type()));
77+
result.push_back(from_integer(0, signed_short_int_type()));
7878
return result;
7979
}
8080

@@ -310,8 +310,11 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause(
310310
invariant_mapt new_in_clauses = invariant_mapt(in_invariant_clause_map);
311311
new_in_clauses[cause_loop_id] =
312312
and_exprt(new_in_clauses[cause_loop_id], strengthening_candidate);
313+
invariant_mapt new_pos_clauses = invariant_mapt(pos_invariant_clause_map);
314+
new_pos_clauses[cause_loop_id] =
315+
and_exprt(new_pos_clauses[cause_loop_id], strengthening_candidate);
313316
const auto &combined_invariant = combine_in_and_post_invariant_clauses(
314-
new_in_clauses, pos_invariant_clause_map, neg_guards);
317+
new_in_clauses, new_pos_clauses, neg_guards);
315318

316319
// The verifier we use to check current invariant candidates.
317320
cegis_verifiert verifier(
@@ -326,7 +329,9 @@ exprt enumerative_loop_contracts_synthesizert::synthesize_strengthening_clause(
326329
(verifier.properties.at(violation_id).status !=
327330
property_statust::FAIL &&
328331
return_cex->violation_type !=
329-
cext::violation_typet::cex_not_hold_upon_entry))
332+
cext::violation_typet::cex_not_hold_upon_entry &&
333+
return_cex->violation_type !=
334+
cext::violation_typet::cex_not_preserved))
330335
{
331336
return strengthening_candidate;
332337
}
@@ -374,6 +379,17 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
374379
synthesize_same_object_predicate(return_cex->checked_pointer);
375380
break;
376381

382+
case cext::violation_typet::cex_assignable:
383+
synthesize_assigns(
384+
return_cex->checked_pointer, return_cex->cause_loop_ids);
385+
break;
386+
387+
case cext::violation_typet::cex_other:
388+
// Update the dependent symbols.
389+
dependent_symbols = compute_dependent_symbols(
390+
return_cex->cause_loop_ids.front(),
391+
new_invariant_clause,
392+
return_cex->live_variables);
377393
case cext::violation_typet::cex_not_preserved:
378394
terminal_symbols = construct_terminals(dependent_symbols);
379395
new_invariant_clause = synthesize_strengthening_clause(
@@ -382,12 +398,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
382398
verifier.target_violation_id);
383399
break;
384400

385-
case cext::violation_typet::cex_assignable:
386-
synthesize_assigns(
387-
return_cex->checked_pointer, return_cex->cause_loop_ids);
388-
break;
389401
case cext::violation_typet::cex_not_hold_upon_entry:
390-
case cext::violation_typet::cex_other:
391402
INVARIANT(false, "unsupported violation type");
392403
break;
393404
}

0 commit comments

Comments
 (0)