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

catch overflow in SVA delays during parsing

Browse source 
* spot/parsetl/scantl.ll: Diagnose delays (##n) larger than
unbounded().  Remove all checks for delays with 1 or 2 characters.
* tests/core/parseerr.test: Add a test case.
* NEWS: Mention this fix.
This commit is contained in:
Alexandre Duret-Lutz 2021-12-02 09:25:59 +01:00
parent 6b46401d36
commit 8ffd06e9a6
3 changed files with 28 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -8,6 +8,9 @@ New in spot 2.10.1.dev (not yet released)
- only use sched_getcpu() and pthread_setaffinity_np() when they are - only use sched_getcpu() and pthread_setaffinity_np() when they are
available. available.
- Using ##300 in a SERE will report that the repeatition exceeds the
allowed value using a parse error, not as an exception.
New in spot 2.10.1 (2021-11-19) New in spot 2.10.1 (2021-11-19)
Build: Build:

22
spot/parsetl/scantl.ll
View file

@ -1,6 +1,6 @@
/* -*- coding: utf-8 -*- /* -*- coding: utf-8 -*-
** Copyright (C) 2010-2015, 2017-2019, Laboratoire de Recherche et ** Copyright (C) 2010-2015, 2017-2019, 2021, Laboratoire de Recherche
** Développement de l'Epita (LRDE). ** et Développement de l'Epita (LRDE).
** Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 ** Copyright (C) 2003, 2004 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é
** Pierre et Marie Curie. ** Pierre et Marie Curie.
@ -35,6 +35,7 @@
#include <spot/parsetl/parsedecl.hh> #include <spot/parsetl/parsedecl.hh>
#include "spot/priv/trim.hh" #include "spot/priv/trim.hh"
#include "spot/tl/formula.hh"
#define YY_USER_ACTION \ #define YY_USER_ACTION \
yylloc->columns(yyleng); yylloc->columns(yyleng);
@ -221,7 +222,11 @@ eol2 (\n\r)+|(\r\n)+
"first_match" BEGIN(0); return token::OP_FIRST_MATCH; "first_match" BEGIN(0); return token::OP_FIRST_MATCH;
/* SVA operators */ /* SVA operators */
"##"[0-9]+ { "##"[0-9]{1,2} {
yylval->num = strtoul(yytext + 2, 0, 10);
return token::OP_DELAY_N;
}
"##"[0-9]{3,} {
errno = 0; errno = 0;
unsigned long n = strtoul(yytext + 2, 0, 10); unsigned long n = strtoul(yytext + 2, 0, 10);
yylval->num = n; yylval->num = n;
@ -232,6 +237,17 @@ eol2 (\n\r)+|(\r\n)+
"value too large ignored")); "value too large ignored"));
yylval->num = 1; yylval->num = 1;
} }
if (yylval->num >= spot::fnode::unbounded())
{
auto max = spot::fnode::unbounded() - 1;
std::ostringstream s;
s << yylval->num
<< (" exceeds maximum supported "
"repetition (")
<< max << ")";
error_list.emplace_back(*yylloc, s.str());
yylval->num = max;
}
return token::OP_DELAY_N; return token::OP_DELAY_N;
} }
"##[+]" BEGIN(0); return token::OP_DELAY_PLUS; "##[+]" BEGIN(0); return token::OP_DELAY_PLUS;

6
tests/core/parseerr.test
View file

@ -35,6 +35,7 @@ cat >input <<EOF
a - b a - b
{a[*9999999999]} {a[*9999999999]}
{a ##[1:255] b} {a ##[1:255] b}
{a ##255 b}
EOF EOF
run 1 ../ltl2text input | run 1 ../ltl2text input |
@ -80,6 +81,11 @@ Closure(@6 #0 [Star(@5 #0 0.. ["a"])])
255 exceeds maximum supported repetition (254) 255 exceeds maximum supported repetition (254)
Closure(@12 #0 [Concat(@11 #0 ["a", Star(@9 #0 0..253 [tt(@1 #0)]), "b"])]) Closure(@12 #0 [Concat(@11 #0 ["a", Star(@9 #0 0..253 [tt(@1 #0)]), "b"])])
>>> {a ##255 b}
^^^^^
255 exceeds maximum supported repetition (254)
Closure(@17 #0 [Concat(@16 #0 ["a", Star(@15 #0 253..253 [tt(@1 #0)]), "b"])])
EOF EOF
diff output expected diff output expected