Skip to content

Commit 199dc18

Browse files
kroeningkroening
committed
better error reporting when Buechi conversion is given unsupported property
This improves the error reporting when the Buechi conversion is given an unsupported property.
1 parent eb37218 commit 199dc18

File tree

13 files changed

+109
-108
lines changed

13 files changed

+109
-108
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_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{

‎src/temporal-logic/ltl_to_buechi.cpp‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -264,6 +264,7 @@ ltl_to_buechi(const exprt &property, message_handlert &message_handler)
264264
}
265265
catch(ltl_sva_to_string_unsupportedt error)
266266
{
267-
throw ebmc_errort{} << "failed to convert " << error.expr.id();
267+
// re-throw
268+
throw ltl_to_buechi_unsupportedt{error.expr};
268269
}
269270
}

0 commit comments

Comments
 (0)