From 3d3baf449ec6fcb636a4c724328d58d448d9e994 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 14 Mar 2017 17:13:59 +0100 Subject: [PATCH] parsetl: improve coverage * spot/parsetl/parsetl.yy: Adjust one diagnostic. * spot/parsetl/scantl.ll: Fix recovering of missing closing brace in lenient mode. * tests/python/declenv.py: Move some tests... * tests/python/ltlparse.py: ... here, and add many more. * NEWS: Mention the lenient mode bug. --- NEWS | 5 ++ spot/parsetl/parsetl.yy | 2 +- spot/parsetl/scantl.ll | 8 +- tests/python/declenv.py | 18 ----- tests/python/ltlparse.py | 155 ++++++++++++++++++++++++++++++++++++++- 5 files changed, 162 insertions(+), 26 deletions(-) diff --git a/NEWS b/NEWS index b45fe07ec..14a2912d8 100644 --- a/NEWS +++ b/NEWS @@ -10,6 +10,11 @@ New in spot 2.3.2.dev (not yet released) - spot::sum() and spot::sum_and() implements the union and the intersection of two automatons, respectively. + Bug fixes: + + - In "lenient" mode the parser would fail to recover from + a missing closing brace. + Backward-incompatible changes: - spot::acc_cond::mark_t::operator bool() has been marked as diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index 319ccbcdb..69b619252 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -427,7 +427,7 @@ fstarargs: OP_BFSTAR equalargs: OP_EQUAL_OPEN sqbracketargs { $$ = $2; } | OP_EQUAL_OPEN error OP_SQBKT_CLOSE - { error_list.emplace_back(@$, "treating this equal block as [*]"); + { error_list.emplace_back(@$, "treating this equal block as [=]"); $$.min = 0U; $$.max = fnode::unbounded(); } | OP_EQUAL_OPEN error_opt END_OF_INPUT { error_list. diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll index fc40db1b8..256543726 100644 --- a/spot/parsetl/scantl.ll +++ b/spot/parsetl/scantl.ll @@ -1,6 +1,6 @@ /* -*- coding: utf-8 -*- -** Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, Laboratoire de -** Recherche et Développement de l'Epita (LRDE). +** Copyright (C) 2010-2015, 2017, Laboratoire de Recherche et +** Développement de l'Epita (LRDE). ** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ** département Systèmes Répartis Coopératifs (SRC), Université Pierre ** et Marie Curie. @@ -142,7 +142,7 @@ eol2 (\n\r)+|(\r\n)+ if (!missing_parent) error_list.push_back( spot::one_parse_error(*yylloc, - "missing closing parenthese")); + "missing closing parenthesis")); missing_parent = true; } } @@ -192,7 +192,7 @@ eol2 (\n\r)+|(\r\n)+ } [^{}]+ yylval->str->append(yytext, yyleng); <> { - unput(')'); + unput('}'); if (!missing_parent) error_list.push_back( spot::one_parse_error(*yylloc, diff --git a/tests/python/declenv.py b/tests/python/declenv.py index 647f4d5e1..868f6ca1d 100644 --- a/tests/python/declenv.py +++ b/tests/python/declenv.py @@ -51,21 +51,3 @@ assert "unknown atomic proposition `d'" in err f4 = spot.parse_prefix_ltl("R a b", env) assert not f4.errors - -for (x, op) in [('a* <-> b*', "`<->'"), - ('a* -> b', "`->'"), - ('a ^ b*', "`^'"), - ('!(b*)', "`!'"), - ('a*[=2]', "[=...]"), - ('a*[->2]', "[->...]")]: - f5 = spot.parse_infix_sere(x) - assert f5.errors - ostr = spot.ostringstream() - f5.format_errors(ostr) - err = ostr.str() - assert "not a Boolean expression" in err - assert op in err - assert "SERE" in err - -f6 = spot.parse_infix_sere('(a <-> b -> c ^ b)[=2] & c[->2]') -assert not f6.errors diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py index de4bff9d6..96b05c58c 100755 --- a/tests/python/ltlparse.py +++ b/tests/python/ltlparse.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche et +# Copyright (C) 2009-2012, 2014-2017 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -33,12 +33,161 @@ for str1 in l: sys.exit(1) str2 = str(pf.f) del pf - sys.stdout.write(str2 + "\n") # Try to reparse the stringified formula pf = spot.parse_infix_psl(str2, e) if pf.format_errors(spot.get_cout()): sys.exit(1) - sys.stdout.write(str(pf.f) + "\n") del pf +for str1 in ['a * b', 'a xor b', 'a <-> b']: + pf = spot.parse_infix_boolean(str1, e, False) + if pf.format_errors(spot.get_cout()): + sys.exit(1) + str2 = str(pf.f) + del pf + # Try to reparse the stringified formula + pf = spot.parse_infix_boolean(str2, e) + if pf.format_errors(spot.get_cout()): + sys.exit(1) + del pf + +for (x, op) in [('a* <-> b*', "`<->'"), + ('a* -> b', "`->'"), + ('a ^ b*', "`^'"), + ('!(b*)', "`!'"), + ('a*[=2]', "[=...]"), + ('a*[->2]', "[->...]")]: + f5 = spot.parse_infix_sere(x) + assert f5.errors + ostr = spot.ostringstream() + f5.format_errors(ostr) + err = ostr.str() + assert "not a Boolean expression" in err + assert op in err + assert "SERE" in err + del f5 + +f6 = spot.parse_infix_sere('(a <-> b -> c ^ "b\n\n\rc")[=2] & c[->2]') +assert not f6.errors +del f6 + +f6 = spot.parse_infix_sere('-') +assert f6.errors +del f6 + +for (x, msg) in [('{foo[->bug]}', "treating this goto block as [->]"), + ('{foo[->', 'missing closing bracket for goto operator'), + ('{foo[->3..1]}', "reversed range"), + ('{foo[*bug]}', "treating this star block as [*]"), + ('{foo[*bug', "missing closing bracket for star"), + ('{foo[*3..1]}', "reversed range"), + ('{[*3..1]}', "reversed range"), + ('{foo[:*bug]}', "treating this fusion-star block as [:*]"), + ('{foo[:*3..1]}', "reversed range"), + ('{foo[:*bug', "missing closing bracket for fusion-star"), + ('{foo[=bug]}', "treating this equal block as [=]"), + ('{foo[=bug', "missing closing bracket for equal operator"), + ('{foo[=3..1]}', "reversed range"), + ('{()}', "treating this brace block as false"), + ('{(a b)}', "treating this parenthetical block as false"), + ('{(a*}', "missing closing parenthesis"), + ('{(a*&)}', "missing right operand for " + + "\"non-length-matching and operator\""), + ('{(a*&&)}', "missing right operand for " + + "\"length-matching and operator\""), + ('{(a*|)}', "missing right operand for \"or operator\""), + ('{a*;}', "missing right operand for \"concat operator\""), + ('{a*::b}', "missing right operand for \"fusion operator\""), + ('{a* xor }', "missing right operand for \"xor operator\""), + ('{a* -> }', "missing right operand for " + + "\"implication operator\""), + ('{a <-> <-> b }', + "missing right operand for \"equivalent operator\""), + ('{a;b b}', "ignoring this"), + ('{*', "missing closing brace"), + ('{(a', "missing closing parenthesis"), + ('{* a', "ignoring trailing garbage and missing closing brace"), + ('F(a b)', "ignoring this"), + ('F(-)', "treating this parenthetical block as false"), + ('F(', "missing closing parenthesis"), + ('F(a b', "ignoring trailing garbage and " + + "missing closing parenthesis"), + ('F(-', "missing closing parenthesis"), + ('F(-', "parenthetical block as false"), + ('a&', "missing right operand for \"and operator\""), + ('a*', "missing right operand for \"and operator\""), + ('a|', "missing right operand for \"or operator\""), + ('a^', "missing right operand for \"xor operator\""), + ('a->', "missing right operand for \"implication operator\""), + ('a<->', "missing right operand for \"equivalent operator\""), + ('!', "missing right operand for \"not operator\""), + ('a W', "missing right operand for \"weak until operator\""), + ('a U', "missing right operand for \"until operator\""), + ('a R', "missing right operand for \"release operator\""), + ('a M', "missing right operand for " + + "\"strong release operator\""), + ('{a}[]->', "missing right operand for " + + "\"universal overlapping concat operator\""), + ('{a}[]=>', "missing right operand for " + + "\"universal non-overlapping concat operator\""), + ('{a}<>->', "missing right operand for " + + "\"existential overlapping concat operator\""), + ('{a}<>=>', "missing right operand for " + + "\"existential non-overlapping concat operator\""), + ('(X)', "missing right operand for \"next operator\""), + ('("X)', "unclosed string"), + ('("X)', "missing closing parenthesis"), + ('{"X', "unclosed string"), + ('{"X}', "missing closing brace"), + ]: + f7 = spot.parse_infix_psl(x) + assert f7.errors + ostr = spot.ostringstream() + f7.format_errors(ostr) + err = ostr.str() + print(err) + assert msg in err + del f7 + +for (x, msg) in [('a&', "missing right operand for \"and operator\""), + ('a*', "missing right operand for \"and operator\""), + ('a|', "missing right operand for \"or operator\""), + ('a^', "missing right operand for \"xor operator\""), + ('a->', "missing right operand for \"implication operator\""), + ('a<->', "missing right operand for \"equivalent operator\""), + ('(-', "parenthetical block as false"), + ('(-', "missing closing parenthesis"), + ('(-)', "treating this parenthetical block as false"), + ('(a', "missing closing parenthesis"), + ('(a b)', "ignoring this"), + ('(a b', "ignoring trailing garbage and " + + "missing closing parenthesis"), + ('!', "missing right operand for \"not operator\""), + ]: + f8 = spot.parse_infix_boolean(x) + assert f8.errors + ostr = spot.ostringstream() + f8.format_errors(ostr) + err = ostr.str() + print(err) + assert msg in err + del f8 + +for (x, msg) in [('a->', "missing right operand for \"implication operator\""), + ('a<->', "missing right operand for \"equivalent operator\""), + ('(aa', "missing closing parenthesis"), + ('("aa', "missing closing parenthesis"), + ('"(aa', "unclosed string"), + ('{aa', "missing closing brace"), + ]: + f9 = spot.parse_infix_psl(x, spot.default_environment.instance(), + False, True) + assert f9.errors + ostr = spot.ostringstream() + f9.format_errors(ostr) + err = ostr.str() + print(err) + assert msg in err + del f9 + assert spot.fnode_instances_check()