From 81375d7a9320b030246a2e8f408295fab43e4858 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 17 Nov 2021 17:10:38 +0100 Subject: [PATCH] tl: diagnose repetitions that do not fit in uint_8 For issue #485. * spot/parsetl/parsetl.yy: Add a diagnostic. * tests/core/parseerr.test: Test it. --- spot/parsetl/parsetl.yy | 74 +++++++++++++++++++++++++--------------- tests/core/parseerr.test | 16 ++++++--- 2 files changed, 58 insertions(+), 32 deletions(-) diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index f3ea1164a..bbcdedcb5 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -1,6 +1,6 @@ /* -*- 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). ** Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 ** (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -279,6 +279,7 @@ using namespace spot; %type subformula atomprop booleanatom sere lbtformula boolformula %type bracedsere parenthesedsubformula %type starargs fstarargs equalargs sqbracketargs gotoargs delayargs +%type sqbkt_num %destructor { delete $$; } %destructor { $$->destroy(); } @@ -377,30 +378,47 @@ OP_SQBKT_SEP_opt: %empty error_opt: %empty | 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] */ -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; } - | OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE + | sqbkt_num OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE { $$.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; } | OP_SQBKT_SEP_opt OP_SQBKT_CLOSE { $$.min = 0U; $$.max = fnode::unbounded(); } - | OP_SQBKT_NUM OP_SQBKT_CLOSE + | sqbkt_num OP_SQBKT_CLOSE { $$.min = $$.max = $1; } /* [->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; } - | 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(); } - | 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; } | OP_GOTO_OPEN OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE { $$.min = 1U; $$.max = fnode::unbounded(); } | OP_GOTO_OPEN OP_SQBKT_CLOSE { $$.min = $$.max = 1U; } - | OP_GOTO_OPEN OP_SQBKT_NUM OP_SQBKT_CLOSE + | OP_GOTO_OPEN sqbkt_num OP_SQBKT_CLOSE { $$.min = $$.max = $2; } | OP_GOTO_OPEN error OP_SQBKT_CLOSE { error_list.emplace_back(@$, "treating this goto block as [->]"); @@ -885,36 +903,36 @@ subformula: booleanatom { $$ = fnode::unop(op::F, $2); } | OP_F error { 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); error_list.emplace_back(@1 + @3, "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 { $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2, $2, $4); error_list.emplace_back(@1 + @3, "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 { $$ = 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 { $$ = fnode::nested_unop_range(op::strong_X, 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 { $$ = fnode::nested_unop_range(op::X, op::Or, $2, 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 { $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2, 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 { 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 { missing_right_op($$, @1 + @5, "F[.!] operator"); } | OP_FREP error_opt END_OF_INPUT @@ -932,37 +950,37 @@ subformula: booleanatom { $$ = fnode::unop(op::G, $2); } | OP_G error { 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 { $$ = 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 { $$ = fnode::nested_unop_range(op::strong_X, op::And, $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 { $$ = fnode::nested_unop_range(op::X, op::And, $2, 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 { $$ = fnode::nested_unop_range(op::strong_X, op::And, $2, 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); error_list.emplace_back(@1 + @3, "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 { $$ = fnode::nested_unop_range(op::strong_X, op::And, $2, $2, $4); error_list.emplace_back(@1 + @3, "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 { 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 { missing_right_op($$, @1 + @5, "G[.!] operator"); } | OP_GREP error_opt END_OF_INPUT @@ -984,16 +1002,16 @@ subformula: booleanatom { $$ = fnode::unop(op::strong_X, $2); } | OP_STRONG_X error { 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); } - | OP_XREP OP_SQBKT_NUM OP_SQBKT_CLOSE error + | OP_XREP sqbkt_num OP_SQBKT_CLOSE error { missing_right_op($$, @1 + @3, "X[.] operator"); } | OP_XREP error OP_SQBKT_CLOSE subformula %prec OP_XREP { error_list.emplace_back(@$, "treating this X[.] as a simple X"); $$ = fnode::unop(op::X, $4); } | OP_XREP OP_SQBKT_STRONG_CLOSE subformula %prec OP_XREP { $$ = 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 { $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2, $2, $4); } diff --git a/tests/core/parseerr.test b/tests/core/parseerr.test index 5075d123d..479397b44 100755 --- a/tests/core/parseerr.test +++ b/tests/core/parseerr.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- 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). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -34,9 +34,11 @@ cat >input < output +run 1 ../ltl2text input | + sed 's/[$]undefined/invalid token/g;s/ap([^"]*\("[^"]*"\))/\1/g' > output sed 's/$$//' >expected<<\EOF >>> $ @@ -67,12 +69,17 @@ syntax error, unexpected invalid token ^^^ ignoring trailing garbage -ap(@3 #0 "a") +"a" >>> {a[*9999999999]} ^^^^^^^^^^ 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 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[->..0];b}, {a[->0..1];b} +{a[->2..300];b}, {a[->2..254];b} EOF run 0 ../equals -E recover.txt