alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tl: diagnose repetitions that do not fit in uint_8

Browse source 
For issue #485.

* spot/parsetl/parsetl.yy: Add a diagnostic.
* tests/core/parseerr.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2021-11-17 17:10:38 +01:00
parent f82d26b625
commit 81375d7a93
2 changed files with 58 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

74
spot/parsetl/parsetl.yy
View file

@ -1,6 +1,6 @@
/* -*- coding: utf-8 -*- /* -*- coding: utf-8 -*-
** Copyright (C) 2009-2019 Laboratoire de Recherche et Développement ** Copyright (C) 2009-2019, 2021 Laboratoire de Recherche et Développement
** de l'Epita (LRDE). ** de l'Epita (LRDE).
** Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 ** Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
** (LIP6), département Systèmes Répartis Coopératifs (SRC), Université ** (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@ -279,6 +279,7 @@ using namespace spot;
%type <ltl> subformula atomprop booleanatom sere lbtformula boolformula %type <ltl> subformula atomprop booleanatom sere lbtformula boolformula
%type <ltl> bracedsere parenthesedsubformula %type <ltl> bracedsere parenthesedsubformula
%type <minmax> starargs fstarargs equalargs sqbracketargs gotoargs delayargs %type <minmax> starargs fstarargs equalargs sqbracketargs gotoargs delayargs
%type <num> sqbkt_num
%destructor { delete $$; } <str> %destructor { delete $$; } <str>
%destructor { $$->destroy(); } <ltl> %destructor { $$->destroy(); } <ltl>
@ -377,30 +378,47 @@ OP_SQBKT_SEP_opt: %empty
error_opt: %empty error_opt: %empty
| error | error
sqbkt_num: OP_SQBKT_NUM
{
if ($1 >= fnode::unbounded())
{
auto max = fnode::unbounded() - 1;
std::ostringstream s;
s << $1 << " exceeds maximum supported repetition ("
<< max << ")";
error_list.emplace_back(@1, s.str());
$$ = max;
}
else
{
$$ = $1;
}
}
/* for [*i..j] and [=i..j] */ /* for [*i..j] and [=i..j] */
sqbracketargs: OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE sqbracketargs: sqbkt_num OP_SQBKT_SEP sqbkt_num OP_SQBKT_CLOSE
{ $$.min = $1; $$.max = $3; } { $$.min = $1; $$.max = $3; }
| OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE | sqbkt_num OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
{ $$.min = $1; $$.max = fnode::unbounded(); } { $$.min = $1; $$.max = fnode::unbounded(); }
| OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE | OP_SQBKT_SEP sqbkt_num OP_SQBKT_CLOSE
{ $$.min = 0U; $$.max = $2; } { $$.min = 0U; $$.max = $2; }
| OP_SQBKT_SEP_opt OP_SQBKT_CLOSE | OP_SQBKT_SEP_opt OP_SQBKT_CLOSE
{ $$.min = 0U; $$.max = fnode::unbounded(); } { $$.min = 0U; $$.max = fnode::unbounded(); }
| OP_SQBKT_NUM OP_SQBKT_CLOSE | sqbkt_num OP_SQBKT_CLOSE
{ $$.min = $$.max = $1; } { $$.min = $$.max = $1; }
/* [->i..j] has default values that are different than [*] and [=]. */ /* [->i..j] has default values that are different than [*] and [=]. */
gotoargs: OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE gotoargs: OP_GOTO_OPEN sqbkt_num OP_SQBKT_SEP sqbkt_num OP_SQBKT_CLOSE
{ $$.min = $2; $$.max = $4; } { $$.min = $2; $$.max = $4; }
| OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE | OP_GOTO_OPEN sqbkt_num OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
{ $$.min = $2; $$.max = fnode::unbounded(); } { $$.min = $2; $$.max = fnode::unbounded(); }
| OP_GOTO_OPEN OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE | OP_GOTO_OPEN OP_SQBKT_SEP sqbkt_num OP_SQBKT_CLOSE
{ $$.min = 1U; $$.max = $3; } { $$.min = 1U; $$.max = $3; }
| OP_GOTO_OPEN OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE | OP_GOTO_OPEN OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
{ $$.min = 1U; $$.max = fnode::unbounded(); } { $$.min = 1U; $$.max = fnode::unbounded(); }
| OP_GOTO_OPEN OP_SQBKT_CLOSE | OP_GOTO_OPEN OP_SQBKT_CLOSE
{ $$.min = $$.max = 1U; } { $$.min = $$.max = 1U; }
| OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_CLOSE | OP_GOTO_OPEN sqbkt_num OP_SQBKT_CLOSE
{ $$.min = $$.max = $2; } { $$.min = $$.max = $2; }
| OP_GOTO_OPEN error OP_SQBKT_CLOSE | OP_GOTO_OPEN error OP_SQBKT_CLOSE
{ error_list.emplace_back(@$, "treating this goto block as [->]"); { error_list.emplace_back(@$, "treating this goto block as [->]");
@ -885,36 +903,36 @@ subformula: booleanatom
{ $$ = fnode::unop(op::F, $2); } { $$ = fnode::unop(op::F, $2); }
| OP_F error | OP_F error
{ missing_right_op($$, @1, "sometimes operator"); } { missing_right_op($$, @1, "sometimes operator"); }
| OP_FREP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_FREP | OP_FREP sqbkt_num OP_SQBKT_CLOSE subformula %prec OP_FREP
{ $$ = fnode::nested_unop_range(op::X, op::Or, $2, $2, $4); { $$ = fnode::nested_unop_range(op::X, op::Or, $2, $2, $4);
error_list.emplace_back(@1 + @3, error_list.emplace_back(@1 + @3,
"F[n:m] expects two parameters"); "F[n:m] expects two parameters");
} }
| OP_FREP OP_SQBKT_NUM OP_SQBKT_STRONG_CLOSE subformula | OP_FREP sqbkt_num OP_SQBKT_STRONG_CLOSE subformula
%prec OP_FREP %prec OP_FREP
{ $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2, $2, $4); { $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2, $2, $4);
error_list.emplace_back(@1 + @3, error_list.emplace_back(@1 + @3,
"F[n:m!] expects two parameters"); "F[n:m!] expects two parameters");
} }
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE | OP_FREP sqbkt_num OP_SQBKT_SEP sqbkt_num OP_SQBKT_CLOSE
subformula %prec OP_FREP subformula %prec OP_FREP
{ $$ = fnode::nested_unop_range(op::X, op::Or, $2, $4, $6); } { $$ = fnode::nested_unop_range(op::X, op::Or, $2, $4, $6); }
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM | OP_FREP sqbkt_num OP_SQBKT_SEP sqbkt_num
OP_SQBKT_STRONG_CLOSE subformula %prec OP_FREP OP_SQBKT_STRONG_CLOSE subformula %prec OP_FREP
{ $$ = fnode::nested_unop_range(op::strong_X, { $$ = fnode::nested_unop_range(op::strong_X,
op::Or, $2, $4, $6); } op::Or, $2, $4, $6); }
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE | OP_FREP sqbkt_num OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
subformula %prec OP_FREP subformula %prec OP_FREP
{ $$ = fnode::nested_unop_range(op::X, op::Or, $2, { $$ = fnode::nested_unop_range(op::X, op::Or, $2,
fnode::unbounded(), $5); } fnode::unbounded(), $5); }
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_STRONG_CLOSE | OP_FREP sqbkt_num OP_SQBKT_SEP_unbounded OP_SQBKT_STRONG_CLOSE
subformula %prec OP_FREP subformula %prec OP_FREP
{ $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2, { $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2,
fnode::unbounded(), $5); } fnode::unbounded(), $5); }
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE | OP_FREP sqbkt_num OP_SQBKT_SEP sqbkt_num OP_SQBKT_CLOSE
error error
{ missing_right_op($$, @1 + @5, "F[.] operator"); } { missing_right_op($$, @1 + @5, "F[.] operator"); }
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM | OP_FREP sqbkt_num OP_SQBKT_SEP sqbkt_num
OP_SQBKT_STRONG_CLOSE error OP_SQBKT_STRONG_CLOSE error
{ missing_right_op($$, @1 + @5, "F[.!] operator"); } { missing_right_op($$, @1 + @5, "F[.!] operator"); }
| OP_FREP error_opt END_OF_INPUT | OP_FREP error_opt END_OF_INPUT
@ -932,37 +950,37 @@ subformula: booleanatom
{ $$ = fnode::unop(op::G, $2); } { $$ = fnode::unop(op::G, $2); }
| OP_G error | OP_G error
{ missing_right_op($$, @1, "always operator"); } { missing_right_op($$, @1, "always operator"); }
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE | OP_GREP sqbkt_num OP_SQBKT_SEP sqbkt_num OP_SQBKT_CLOSE
subformula %prec OP_GREP subformula %prec OP_GREP
{ $$ = fnode::nested_unop_range(op::X, op::And, $2, $4, $6); } { $$ = fnode::nested_unop_range(op::X, op::And, $2, $4, $6); }
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM | OP_GREP sqbkt_num OP_SQBKT_SEP sqbkt_num
OP_SQBKT_STRONG_CLOSE subformula %prec OP_GREP OP_SQBKT_STRONG_CLOSE subformula %prec OP_GREP
{ $$ = fnode::nested_unop_range(op::strong_X, op::And, { $$ = fnode::nested_unop_range(op::strong_X, op::And,
$2, $4, $6); } $2, $4, $6); }
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE | OP_GREP sqbkt_num OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
subformula %prec OP_GREP subformula %prec OP_GREP
{ $$ = fnode::nested_unop_range(op::X, op::And, $2, { $$ = fnode::nested_unop_range(op::X, op::And, $2,
fnode::unbounded(), $5); } fnode::unbounded(), $5); }
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_STRONG_CLOSE | OP_GREP sqbkt_num OP_SQBKT_SEP_unbounded OP_SQBKT_STRONG_CLOSE
subformula %prec OP_GREP subformula %prec OP_GREP
{ $$ = fnode::nested_unop_range(op::strong_X, op::And, $2, { $$ = fnode::nested_unop_range(op::strong_X, op::And, $2,
fnode::unbounded(), $5); } fnode::unbounded(), $5); }
| OP_GREP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_GREP | OP_GREP sqbkt_num OP_SQBKT_CLOSE subformula %prec OP_GREP
{ $$ = fnode::nested_unop_range(op::X, op::And, $2, $2, $4); { $$ = fnode::nested_unop_range(op::X, op::And, $2, $2, $4);
error_list.emplace_back(@1 + @3, error_list.emplace_back(@1 + @3,
"G[n:m] expects two parameters"); "G[n:m] expects two parameters");
} }
| OP_GREP OP_SQBKT_NUM OP_SQBKT_STRONG_CLOSE subformula | OP_GREP sqbkt_num OP_SQBKT_STRONG_CLOSE subformula
%prec OP_GREP %prec OP_GREP
{ $$ = fnode::nested_unop_range(op::strong_X, op::And, { $$ = fnode::nested_unop_range(op::strong_X, op::And,
$2, $2, $4); $2, $2, $4);
error_list.emplace_back(@1 + @3, error_list.emplace_back(@1 + @3,
"G[n:m!] expects two parameters"); "G[n:m!] expects two parameters");
} }
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE | OP_GREP sqbkt_num OP_SQBKT_SEP sqbkt_num OP_SQBKT_CLOSE
error error
{ missing_right_op($$, @1 + @5, "G[.] operator"); } { missing_right_op($$, @1 + @5, "G[.] operator"); }
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM | OP_GREP sqbkt_num OP_SQBKT_SEP sqbkt_num
OP_SQBKT_STRONG_CLOSE error OP_SQBKT_STRONG_CLOSE error
{ missing_right_op($$, @1 + @5, "G[.!] operator"); } { missing_right_op($$, @1 + @5, "G[.!] operator"); }
| OP_GREP error_opt END_OF_INPUT | OP_GREP error_opt END_OF_INPUT
@ -984,16 +1002,16 @@ subformula: booleanatom
{ $$ = fnode::unop(op::strong_X, $2); } { $$ = fnode::unop(op::strong_X, $2); }
| OP_STRONG_X error | OP_STRONG_X error
{ missing_right_op($$, @1, "strong next operator"); } { missing_right_op($$, @1, "strong next operator"); }
| OP_XREP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_XREP | OP_XREP sqbkt_num OP_SQBKT_CLOSE subformula %prec OP_XREP
{ $$ = fnode::nested_unop_range(op::X, op::Or, $2, $2, $4); } { $$ = fnode::nested_unop_range(op::X, op::Or, $2, $2, $4); }
| OP_XREP OP_SQBKT_NUM OP_SQBKT_CLOSE error | OP_XREP sqbkt_num OP_SQBKT_CLOSE error
{ missing_right_op($$, @1 + @3, "X[.] operator"); } { missing_right_op($$, @1 + @3, "X[.] operator"); }
| OP_XREP error OP_SQBKT_CLOSE subformula %prec OP_XREP | OP_XREP error OP_SQBKT_CLOSE subformula %prec OP_XREP
{ error_list.emplace_back(@$, "treating this X[.] as a simple X"); { error_list.emplace_back(@$, "treating this X[.] as a simple X");
$$ = fnode::unop(op::X, $4); } $$ = fnode::unop(op::X, $4); }
| OP_XREP OP_SQBKT_STRONG_CLOSE subformula %prec OP_XREP | OP_XREP OP_SQBKT_STRONG_CLOSE subformula %prec OP_XREP
{ $$ = fnode::unop(op::strong_X, $3); } { $$ = fnode::unop(op::strong_X, $3); }
| OP_XREP OP_SQBKT_NUM OP_SQBKT_STRONG_CLOSE subformula | OP_XREP sqbkt_num OP_SQBKT_STRONG_CLOSE subformula
%prec OP_XREP %prec OP_XREP
{ $$ = fnode::nested_unop_range(op::strong_X, { $$ = fnode::nested_unop_range(op::strong_X,
op::Or, $2, $2, $4); } op::Or, $2, $2, $4); }

16
tests/core/parseerr.test
View file

@ -1,6 +1,6 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2009-2016, 2020 Laboratoire # Copyright (C) 2009-2016, 2020, 2021 Laboratoire
# de Recherche et Développement de l'Epita (LRDE). # de Recherche et Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -34,9 +34,11 @@ cat >input <<EOF
/2/3/4/5 a + b /6/7/8/ /2/3/4/5 a + b /6/7/8/
a - b a - b
{a[*9999999999]} {a[*9999999999]}
{a ##[1:255] b}
EOF EOF
run 1 ../ltl2text input | sed 's/[$]undefined/invalid token/g' > output run 1 ../ltl2text input |
sed 's/[$]undefined/invalid token/g;s/ap([^"]*\("[^"]*"\))/\1/g' > output
sed 's/$$//' >expected<<\EOF sed 's/$$//' >expected<<\EOF
>>> $ >>> $
@ -67,12 +69,17 @@ syntax error, unexpected invalid token
^^^ ^^^
ignoring trailing garbage ignoring trailing garbage
ap(@3 #0 "a") "a"
>>> {a[*9999999999]} >>> {a[*9999999999]}
^^^^^^^^^^ ^^^^^^^^^^
value too large ignored value too large ignored
Closure(@6 #0 [Star(@5 #0 0.. [ap(@4 #0 "a")])]) Closure(@6 #0 [Star(@5 #0 0.. ["a"])])
>>> {a ##[1:255] b}
^^^
255 exceeds maximum supported repetition (254)
Closure(@12 #0 [Concat(@11 #0 ["a", Star(@9 #0 0..253 [tt(@1 #0)]), "b"])])
EOF EOF
diff output expected diff output expected
@ -105,5 +112,6 @@ a & (, a & 0
{a[=8..1];b}, {a[=1..8];b} {a[=8..1];b}, {a[=1..8];b}
{a[->8..1];b}, {a[->1..8];b} {a[->8..1];b}, {a[->1..8];b}
{a[->..0];b}, {a[->0..1];b} {a[->..0];b}, {a[->0..1];b}
{a[->2..300];b}, {a[->2..254];b}
EOF EOF
run 0 ../equals -E recover.txt run 0 ../equals -E recover.txt