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

fix "input buffer overflow, can't enlarge buffer..."

Browse source 
This occured when parsing the HOA automaton generated by Rabinizer3 for
a very long LTL formula with many nested U.  State labels could easily
be more than 40k characters.

* src/parseaut/scanaut.ll: Fix that.
* src/tests/parseaut.test: New test case.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2015-10-21 17:29:37 +02:00
parent 619b227eff
commit 64df4fbccc
3 changed files with 33 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -71,6 +71,9 @@ New in spot 1.99.4a (not yet released)
* unabbreviate could easily use forbidden operators. * unabbreviate could easily use forbidden operators.
* "autfilt --is-unambiguous" could fail to detect the nonambiguity * "autfilt --is-unambiguous" could fail to detect the nonambiguity
of some automata with empty languages. of some automata with empty languages.
* When parsing long tokens (e.g, state labels representing
very large strings) the automaton parser could die with
"input buffer overflow, can't enlarge buffer because scanner uses REJECT"
New in spot 1.99.4 (2015-10-01) New in spot 1.99.4 (2015-10-01)

16
src/parseaut/scanaut.ll
View file

@ -145,8 +145,8 @@ identifier [[:alpha:]_][[:alnum:]_-]*
"AP:" return token::AP; "AP:" return token::AP;
"v2" return token::V2; "v2" return token::V2;
"explicit" return token::EXPLICIT; "explicit" return token::EXPLICIT;
"Comment:".* continue; "Comment:".* yylloc->step();
"//".* continue; "//".* yylloc->step();
"Acceptance-Pairs:" return token::ACCPAIRS; "Acceptance-Pairs:" return token::ACCPAIRS;
"Acc-Sig:" return token::ACCSIG; "Acc-Sig:" return token::ACCSIG;
"---" return token::ENDOFHEADER; "---" return token::ENDOFHEADER;
@ -154,7 +154,9 @@ identifier [[:alpha:]_][[:alnum:]_-]*
/* The start of any automaton is the end of this one. /* The start of any automaton is the end of this one.
We do not try to detect LBTT automata, as that would We do not try to detect LBTT automata, as that would
be too hard to distinguish from state numbers. */ be too hard to distinguish from state numbers. */
""/{eols}("HOA:"|"never"|"DSA"|"DRA") { {eols}("HOA:"|"never"|"DSA"|"DRA") {
yylloc->end = yylloc->begin;
yyless(0);
BEGIN(INITIAL); BEGIN(INITIAL);
return token::ENDDSTAR; return token::ENDDSTAR;
} }
@ -281,7 +283,13 @@ identifier [[:alpha:]_][[:alnum:]_-]*
"*"+[^*/\n\r]* continue; "*"+[^*/\n\r]* continue;
{eol} yylloc->lines(yyleng); yylloc->end.column = 1; {eol} yylloc->lines(yyleng); yylloc->end.column = 1;
{eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1; {eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1;
"*"+"/" if (--comment_level == 0) BEGIN(orig_cond); "*"+"/" {
if (--comment_level == 0)
{
yylloc->step();
BEGIN(orig_cond);
}
}
<<EOF>> { <<EOF>> {
BEGIN(orig_cond); BEGIN(orig_cond);
error_list.push_back( error_list.push_back(

18
src/tests/parseaut.test
View file

@ -2365,3 +2365,21 @@ State: 3 "[{8}]"
[!1] 0 {0 1 2} [!1] 0 {0 1 2}
--END-- --END--
EOF EOF
# A 50000-char word
BIGLABEL=`yes y | sed 25000q | tr 'y\n' 'xx'`
cat >bigaut <<EOF
HOA: v1
States: 1
Start: 0
Acceptance: 1 Fin(0)
AP: 0
--BODY--
State: 0 "$BIGLABEL"
{0}
[t] 0
--END--
EOF
# At some point, this crashed with
# input buffer overflow, can't enlarge buffer because scanner uses REJECT
run 0 ../../bin/autfilt -q bigaut