Skip to content

Commit 9e0058b

Browse files
kroeningkroening
authored
Merge pull request #1368 from diffblue/ltl_to_buechi_unsupported
better error reporting for Buechi conversion
2 parents f5276fe + 6c05d42 commit 9e0058b

14 files changed

+113
-112
lines changed

‎regression/ebmc-spot/sva-buechi/cover_sequence1.bmc.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
../../verilog/SVA/cover_sequence1.sv
33
--buechi --bound 10 --numbered-trace
4-
^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: not convertible to Buechi$
5-
^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
4+
^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 4\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
5+
^\[main\.p1\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
66
^EXIT=10$
77
^SIGNAL=0$
88
--

‎regression/ebmc-spot/sva-buechi/cover_sequence2.bmc.desc‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
CORE
22
../../verilog/SVA/cover_sequence2.sv
33
--buechi --bound 5
4-
^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$
5-
^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: not convertible to Buechi$
6-
^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
7-
^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: not convertible to Buechi$
4+
^\[main\.p0\] cover \(main\.x == 2 ##1 main\.x == 3 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
5+
^\[main\.p1\] cover \(main\.x == 98 ##1 main\.x == 99 ##1 main\.x == 100\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
6+
^\[main\.p2\] cover \(main\.x == 3 ##1 main\.x == 4 ##1 main\.x == 5\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
7+
^\[main\.p3\] cover \(main\.x == 4 ##1 main\.x == 5 ##1 main\.x == 6\): UNSUPPORTED: sva_implicit_strong not convertible to Buechi$
88
^EXIT=10$
99
^SIGNAL=0$
1010
--

‎regression/ebmc-spot/sva-buechi/sequence2.bmc.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
../../verilog/SVA/sequence2.sv
33
--buechi --bound 10
44
^\[main\.p0] weak\(##\[0:\$\] main\.x == 10\): PROVED up to bound 10$
5-
^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: not convertible to Buechi$
5+
^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: sva_strong not convertible to Buechi$
66
^EXIT=10$
77
^SIGNAL=0$
88
--

‎regression/ebmc-spot/sva-buechi/sequence_repetition1.bmc.desc‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,11 @@ CORE
22
../../verilog/SVA/sequence_repetition1.sv
33
--buechi --bound 10
44
^\[.*\] main\.half_x == 0 \[\*2\]: PROVED up to bound 10$
5-
^\[.*\] main\.half_x == 0 \[->2\]: UNSUPPORTED: not convertible to Buechi$
6-
^\[.*\] main\.half_x == 0 \[=2\]: UNSUPPORTED: not convertible to Buechi$
5+
^\[.*\] main\.half_x == 0 \[->2\]: UNSUPPORTED: sva_sequence_goto_repetition not convertible to Buechi$
6+
^\[.*\] main\.half_x == 0 \[=2\]: UNSUPPORTED: sva_sequence_non_consecutive_repetition not convertible to Buechi$
77
^\[.*\] main\.x == 0 \[\*2\]: REFUTED$
8-
^\[.*\] main\.x == 0 \[->2\]: UNSUPPORTED: not convertible to Buechi$
9-
^\[.*\] main\.x == 0 \[=2\]: UNSUPPORTED: not convertible to Buechi$
8+
^\[.*\] main\.x == 0 \[->2\]: UNSUPPORTED: sva_sequence_goto_repetition not convertible to Buechi$
9+
^\[.*\] main\.x == 0 \[=2\]: UNSUPPORTED: sva_sequence_non_consecutive_repetition not convertible to Buechi$
1010
^EXIT=10$
1111
^SIGNAL=0$
1212
--

‎regression/ebmc-spot/sva-buechi/sequence_throughout1.desc‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,11 @@
11
CORE
22
../../verilog/SVA/sequence_throughout1.sv
33
--buechi --bound 10
4-
^error: failed to convert sva_sequence_throughout$
5-
^EXIT=6$
4+
^\[main\.p0\] main\.x >= 0 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): UNSUPPORTED: sva_sequence_throughout not convertible to Buechi$
5+
^\[main\.p1\] main\.x <= 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): UNSUPPORTED: sva_sequence_throughout not convertible to Buechi$
6+
^\[main\.p2\] 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 3\): UNSUPPORTED: sva_sequence_throughout not convertible to Buechi$
7+
^EXIT=10$
68
^SIGNAL=0$
79
--
8-
^\[main\.p0\] main\.x >= 0 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): PROVED up to bound 10$
9-
^\[main\.p1\] main\.x <= 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 2\): REFUTED$
10-
^\[main\.p2\] 1 throughout \(main\.x == 0 ##1 main\.x == 1 ##1 main\.x == 3\): REFUTED$
1110
^warning: ignoring
1211
--

‎regression/ebmc-spot/sva-buechi/sequence_within1.desc‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,13 @@
11
CORE
22
../../verilog/SVA/sequence_within1.sv
33
--buechi --bound 20
4-
^error: failed to convert sva_sequence_within$
5-
^EXIT=6$
4+
^\[main\.p0\] main\.x == 0 within main\.x == 1: UNSUPPORTED: sva_sequence_within not convertible to Buechi$
5+
^\[main\.p1\] main\.x == 0 within \(##10 1\): UNSUPPORTED: sva_sequence_within not convertible to Buechi$
6+
^\[main\.p2\] main\.x == 5 within \(##10 1\): UNSUPPORTED: sva_sequence_within not convertible to Buechi$
7+
^\[main\.p3\] main\.x == 10 within \(##10 1\): UNSUPPORTED: sva_sequence_within not convertible to Buechi$
8+
^\[main\.p4\] main\.x == 11 within \(##10 1\): UNSUPPORTED: sva_sequence_within not convertible to Buechi$
9+
^EXIT=10$
610
^SIGNAL=0$
711
--
8-
^\[main\.p0\] main\.x == 0 within main\.x == 1: REFUTED$
9-
^\[main\.p1\] main\.x == 0 within \(##10 1\): PROVED up to bound 20$
10-
^\[main\.p2\] main\.x == 5 within \(##10 1\): PROVED up to bound 20$
11-
^\[main\.p3\] main\.x == 10 within \(##10 1\): PROVED up to bound 20$
12-
^\[main\.p4\] main\.x == 11 within \(##10 1\): REFUTED$
1312
^warning: ignoring
1413
--

‎regression/ebmc-spot/sva-buechi/strong1.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
../../verilog/SVA/strong1.sv
33
--buechi --bound 4
4-
^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
4+
^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: sva_strong not convertible to Buechi$
55
^EXIT=10$
66
^SIGNAL=0$
77
--

‎regression/ebmc-spot/sva-buechi/unbounded1.desc‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
../../verilog/SVA/unbounded1.sv
33
--buechi --module main --bound 1
4-
^error: failed to convert sva_cycle_delay$
5-
^EXIT=6$
4+
^\[.*\] always \(main\.a ##\[0:main\.upper\] main\.b\): UNSUPPORTED: sva_cycle_delay not convertible to Buechi$
5+
^EXIT=10$
66
^SIGNAL=0$
77
--

‎src/ebmc/instrument_buechi.cpp‎

Lines changed: 66 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,7 @@ void instrument_buechi(
2525
continue;
2626

2727
// This is for LTL and some fragment of SVA only.
28-
if(
29-
!is_LTL(property.normalized_expr) &&
30-
!is_Buechi_SVA(property.normalized_expr))
28+
if(!is_LTL(property.normalized_expr) && !is_SVA(property.normalized_expr))
3129
{
3230
property.unsupported("not convertible to Buechi");
3331
continue;
@@ -37,65 +35,74 @@ void instrument_buechi(
3735
message.debug() << "Translating " << property.description << " to Buechi"
3836
<< messaget::eom;
3937

40-
// make the automaton for the negation of the property
41-
auto buechi =
42-
ltl_to_buechi(not_exprt{property.normalized_expr}, message_handler);
43-
44-
// make a fresh symbol for the state of the automaton
45-
namespacet ns(transition_system.symbol_table);
46-
auto property_symbol = ns.lookup(property.identifier);
47-
48-
auxiliary_symbolt new_state_symbol{
49-
id2string(property_symbol.name) + "::buechi_state",
50-
buechi.state_symbol.type(),
51-
property_symbol.mode};
52-
new_state_symbol.is_state_var = true;
53-
new_state_symbol.module = property_symbol.module;
54-
55-
buechi.rename_state_symbol(new_state_symbol.symbol_expr());
56-
57-
// add the new symbol to the symbol table
58-
transition_system.symbol_table.add(std::move(new_state_symbol));
59-
60-
// add the automaton to the transition system
61-
transition_system.trans_expr.init() =
62-
and_exprt{transition_system.trans_expr.init(), buechi.init};
63-
64-
transition_system.trans_expr.trans() =
65-
and_exprt{transition_system.trans_expr.trans(), buechi.trans};
66-
67-
// Replace the normalized property expression
68-
// by the Buechi acceptance condition.
69-
exprt::operandst property_conjuncts;
70-
71-
bool have_liveness = false, have_safety = false;
72-
73-
if(!buechi.liveness_signal.is_false())
38+
try
7439
{
75-
// Note that we have negated the property,
76-
// so this is the negation of the Buechi acceptance condition.
77-
property_conjuncts.push_back(
78-
F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}});
79-
have_liveness = true;
40+
// make the automaton for the negation of the property
41+
auto buechi =
42+
ltl_to_buechi(not_exprt{property.normalized_expr}, message_handler);
43+
44+
// make a fresh symbol for the state of the automaton
45+
namespacet ns(transition_system.symbol_table);
46+
auto property_symbol = ns.lookup(property.identifier);
47+
48+
auxiliary_symbolt new_state_symbol{
49+
id2string(property_symbol.name) + "::buechi_state",
50+
buechi.state_symbol.type(),
51+
property_symbol.mode};
52+
new_state_symbol.is_state_var = true;
53+
new_state_symbol.module = property_symbol.module;
54+
55+
buechi.rename_state_symbol(new_state_symbol.symbol_expr());
56+
57+
// add the new symbol to the symbol table
58+
transition_system.symbol_table.add(std::move(new_state_symbol));
59+
60+
// add the automaton to the transition system
61+
transition_system.trans_expr.init() =
62+
and_exprt{transition_system.trans_expr.init(), buechi.init};
63+
64+
transition_system.trans_expr.trans() =
65+
and_exprt{transition_system.trans_expr.trans(), buechi.trans};
66+
67+
// Replace the normalized property expression
68+
// by the Buechi acceptance condition.
69+
exprt::operandst property_conjuncts;
70+
71+
bool have_liveness = false, have_safety = false;
72+
73+
if(!buechi.liveness_signal.is_false())
74+
{
75+
// Note that we have negated the property,
76+
// so this is the negation of the Buechi acceptance condition.
77+
property_conjuncts.push_back(
78+
F_exprt{G_exprt{not_exprt{buechi.liveness_signal}}});
79+
have_liveness = true;
80+
}
81+
82+
if(!buechi.error_signal.is_true())
83+
{
84+
property_conjuncts.push_back(G_exprt{not_exprt{buechi.error_signal}});
85+
have_safety = true;
86+
}
87+
88+
if(have_liveness && have_safety)
89+
message.debug() << "Buechi automaton has liveness and safety components"
90+
<< messaget::eom;
91+
else if(have_liveness)
92+
message.debug() << "Buechi automaton is liveness only" << messaget::eom;
93+
else if(have_safety)
94+
message.debug() << "Buechi automaton is safety only" << messaget::eom;
95+
96+
property.normalized_expr = conjunction(property_conjuncts);
97+
98+
message.debug() << "New property: " << format(property.normalized_expr)
99+
<< messaget::eom;
80100
}
81-
82-
if(!buechi.error_signal.is_true())
101+
catch(ltl_to_buechi_unsupportedt error)
83102
{
84-
property_conjuncts.push_back(G_exprt{not_exprt{buechi.error_signal}});
85-
have_safety = true;
103+
property.unsupported(
104+
error.expr.id_string() + " not convertible to Buechi");
105+
continue;
86106
}
87-
88-
if(have_liveness && have_safety)
89-
message.debug() << "Buechi automaton has liveness and safety components"
90-
<< messaget::eom;
91-
else if(have_liveness)
92-
message.debug() << "Buechi automaton is liveness only" << messaget::eom;
93-
else if(have_safety)
94-
message.debug() << "Buechi automaton is safety only" << messaget::eom;
95-
96-
property.normalized_expr = conjunction(property_conjuncts);
97-
98-
message.debug() << "New property: " << format(property.normalized_expr)
99-
<< messaget::eom;
100107
}
101108
}

‎src/temporal-logic/ltl_sva_to_string.cpp‎

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -297,9 +297,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
297297
auto new_expr = R_exprt{until_with.rhs(), until_with.lhs()}; // swapped
298298
return infix(" R ", new_expr, mode);
299299
}
300-
else if(
301-
expr.id() == ID_sva_weak || expr.id() == ID_sva_strong ||
302-
expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong)
300+
else if(expr.id() == ID_sva_weak || expr.id() == ID_sva_implicit_weak)
303301
{
304302
PRECONDITION(mode == PROPERTY);
305303
auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
@@ -308,6 +306,10 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
308306
// weak closure
309307
return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
310308
}
309+
else if(expr.id() == ID_sva_strong || expr.id() == ID_sva_implicit_strong)
310+
{
311+
throw ltl_sva_to_string_unsupportedt{expr};
312+
}
311313
else if(expr.id() == ID_sva_or)
312314
{
313315
// can be sequence or property
@@ -514,6 +516,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
514516
}
515517
else if(expr.id() == ID_sva_sequence_goto_repetition) // something[->n]
516518
{
519+
// ltl2tgba produces the wrong anser for [->n] and [=n]
520+
throw ltl_sva_to_string_unsupportedt{expr};
521+
517522
PRECONDITION(mode == SVA_SEQUENCE);
518523
auto &repetition = to_sva_sequence_goto_repetition_expr(expr);
519524
unary_exprt new_expr{ID_sva_sequence_goto_repetition, repetition.op()};
@@ -542,6 +547,9 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
542547
else if(
543548
expr.id() == ID_sva_sequence_non_consecutive_repetition) // something[=n]
544549
{
550+
// ltl2tgba produces the wrong anser for [->n] and [=n]
551+
throw ltl_sva_to_string_unsupportedt{expr};
552+
545553
PRECONDITION(mode == SVA_SEQUENCE);
546554
auto &repetition = to_sva_sequence_non_consecutive_repetition_expr(expr);
547555
unary_exprt new_expr{

0 commit comments

Comments
 (0)