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

how: fix multi-line incomplete strings

Browse source 
Location tracking was incorrect for multi-line
strings/comments/parentheses.  This also fixes and tests recovery on
inclosed strings/comments/parentheses.

* src/hoaparse/hoaparse.yy: Abort on expected EOF.
* src/hoaparse/hoascan.ll: Track newlines inside strings and comments.
Do not use unput() to close incomplete parentheses.
* src/tgbatest/neverclaimread.test, src/tgbatest/hoaparse.test: Add
more tests.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-04 09:55:00 +01:00
parent ebc3d64927
commit ad77145496
4 changed files with 82 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/hoaparse/hoaparse.yy
View file

@ -203,8 +203,11 @@
%% %%
aut: aut-1 { res.h->loc = @$; YYACCEPT; } aut: aut-1 { res.h->loc = @$; YYACCEPT; }
| ENDOFFILE { YYABORT; } | ENDOFFILE { YYABORT; }
| error ENDOFFILE { YYABORT; }
aut-1: hoa
| never
aut-1: hoa | never
/**********************************************************************/ /**********************************************************************/
/* Rules for HOA */ /* Rules for HOA */
@ -212,7 +215,6 @@ aut-1: hoa | never
hoa: header "--BODY--" body "--END--" hoa: header "--BODY--" body "--END--"
hoa: error "--END--" hoa: error "--END--"
hoa: error ENDOFFILE
string_opt: | STRING string_opt: | STRING
BOOLEAN: 't' | 'f' BOOLEAN: 't' | 'f'

51
src/hoaparse/hoascan.ll
View file

@ -149,9 +149,11 @@ identifier [[:alpha:]_][[:alnum:]_-]*
[^*/\n]* continue; [^*/\n]* continue;
"/"[^*\n]* continue; "/"[^*\n]* continue;
"*"+[^*/\n]* continue; "*"+[^*/\n]* continue;
"\n"+ yylloc->end.column = 1; yylloc->lines(yyleng); {eol} yylloc->lines(yyleng); yylloc->end.column = 1;
{eol2} yylloc->lines(yyleng / 2); yylloc->end.column = 1;
"*"+"/" if (--comment_level == 0) BEGIN(orig_cond); "*"+"/" if (--comment_level == 0) BEGIN(orig_cond);
<<EOF>> { <<EOF>> {
BEGIN(orig_cond);
error_list.push_back( error_list.push_back(
spot::hoa_parse_error(*yylloc, spot::hoa_parse_error(*yylloc,
"unclosed comment")); "unclosed comment"));
@ -165,26 +167,36 @@ identifier [[:alpha:]_][[:alnum:]_-]*
yylval->str = new std::string(s); yylval->str = new std::string(s);
return token::STRING; return token::STRING;
} }
{eol} {
s.append(yytext, yyleng);
yylloc->lines(yyleng); yylloc->end.column = 1;
}
{eol2} {
s.append(yytext, yyleng);
yylloc->lines(yyleng / 2); yylloc->end.column = 1;
}
\\. s += yytext[1]; \\. s += yytext[1];
[^\\\"]+ s.append(yytext, yyleng); [^\\\"\n\r]+ s.append(yytext, yyleng);
<<EOF>> { <<EOF>> {
error_list.push_back( error_list.push_back(
spot::hoa_parse_error(*yylloc, spot::hoa_parse_error(*yylloc,
"unclosed string")); "unclosed string"));
return 0; BEGIN(orig_cond);
yylval->str = new std::string(s);
return token::STRING;
} }
} }
<in_NEVER_PAR>{ <in_NEVER_PAR>{
"(" { "(" {
++parent_level; ++parent_level;
yylval->str->append(yytext, yyleng); yylval->str->append(yytext, yyleng);
} }
/* if we match ")&&(" or ")||(", stay in <in_NEVER_PAR> mode */ /* if we match ")&&(" or ")||(", stay in <in_NEVER_PAR> mode */
")"[ \t]*("&&"|"||")[ \t!]*"(" { ")"[ \t]*("&&"|"||")[ \t!]*"(" {
yylval->str->append(yytext, yyleng); yylval->str->append(yytext, yyleng);
} }
")" { ")" {
yylval->str->append(yytext, yyleng); yylval->str->append(yytext, yyleng);
if (!--parent_level) if (!--parent_level)
{ {
@ -193,14 +205,23 @@ identifier [[:alpha:]_][[:alnum:]_-]*
return token::FORMULA; return token::FORMULA;
} }
} }
[^()]+ yylval->str->append(yytext, yyleng); {eol} {
<<EOF>> { yylval->str->append(yytext, yyleng);
unput(')'); yylloc->lines(yyleng); yylloc->end.column = 1;
if (!missing_parent) }
error_list.push_back( {eol2} {
spot::hoa_parse_error(*yylloc, yylval->str->append(yytext, yyleng);
"missing closing parenthese")); yylloc->lines(yyleng / 2); yylloc->end.column = 1;
missing_parent = true; }
[^()\n\r]+ yylval->str->append(yytext, yyleng);
<<EOF>> {
error_list.push_back(
spot::hoa_parse_error(*yylloc,
"missing closing parenthese"));
yylval->str->append(parent_level, ')');
BEGIN(in_NEVER);
spot::trim(*yylval->str);
return token::FORMULA;
} }
} }

33
src/tgbatest/hoaparse.test
View file

@ -603,7 +603,9 @@ cat >input <<EOF
HOA: v1 HOA: v1
States: 3 States: 3
Start: 0 Start: 0
AP: 2 "a" "b" AP: 2 "a" "b"/* multi
line
comment */
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
--BODY-- --BODY--
State: [1] 0 {0} State: [1] 0 {0}
@ -620,18 +622,21 @@ State: 2
EOF EOF
expecterr input <<EOF expecterr input <<EOF
input:8.1-4: cannot label this edge because... input:10.1-4: cannot label this edge because...
input:7.8-10: ... the state is already labeled. input:9.8-10: ... the state is already labeled.
input:12.6: missing label for this edge (previous edge is labeled) input:14.6: missing label for this edge (previous edge is labeled)
input:15.1-3: ignoring this label, because previous edge has no label input:17.1-3: ignoring this label, because previous edge has no label
EOF EOF
cat >input <<EOF cat >input <<EOF
HOA: v1 HOA: v1
States: 2 States: /* multi-line
comment
*/2
Start: 0 Start: 0
Important: 4 very important "!" Important: 4 very important "with multi-line
string!"
AP: 0 AP: 0
Acceptance: 1 Inf(0) Acceptance: 1 Inf(0)
--BODY-- --BODY--
@ -641,7 +646,7 @@ State: 1 0
EOF EOF
expecterr input <<EOF expecterr input <<EOF
input:4.1-31: ignoring unsupported header "Important:" input:6.1-7.8: ignoring unsupported header "Important:"
(but the capital indicates information that should not be ignored) (but the capital indicates information that should not be ignored)
EOF EOF
@ -663,6 +668,13 @@ EOF
diff expected input.out diff expected input.out
# DOS-style new lines should have the same output.
sed 's/$/\r/g' input > input.dos
mv input.dos input
../../bin/autfilt --hoa input 2>stderr && exit 1
cat stderr
diff stderr input.exp
diff expected input.out
# Error recovery # Error recovery
@ -719,6 +731,7 @@ input:25.1: $se \$undefined, expecting end of file or HOA: or never
input:25.1-12: ignoring leading garbage input:25.1-12: ignoring leading garbage
input:32.1-5: $se header name, expecting --END-- or State: input:32.1-5: $se header name, expecting --END-- or State:
input:37.1: $se 't', expecting end of file or HOA: or never input:37.1: $se 't', expecting end of file or HOA: or never
autfilt: failed to read automaton from input
EOF EOF
# A comment can contain --BODY-- or --END--, so we do not want to be # A comment can contain --BODY-- or --END--, so we do not want to be
@ -786,8 +799,8 @@ State: 1
EOF EOF
expecterr input <<EOF expecterr input <<EOF
input:4.7-242: unclosed string input:4.7-26.1: unclosed string
input:4.7-242: syntax error, unexpected end of file, expecting string input:26.1: syntax error, unexpected end of file
autfilt: failed to read automaton from input autfilt: failed to read automaton from input
EOF EOF

22
src/tgbatest/neverclaimread.test
View file

@ -312,10 +312,17 @@ T0_init:
accept_all: accept_all:
skip skip
} }
never { /* a U b */
T0_init:
if
:: ((b)) -> goto accept_all
:: ((b) -> goto T0_init
fi;
accept_all:
skip
}
EOF EOF
run 2 ../../bin/autfilt --dot <input >stdout 2>stderr ../../bin/autfilt --dot <input >stdout 2>stderr && exit 1
grep '5.6-8: unexpected empty block' stderr
cat >expected <<EOF cat >expected <<EOF
digraph G { digraph G {
0 [label="", style=invis, height=0] 0 [label="", style=invis, height=0]
@ -328,6 +335,15 @@ digraph G {
} }
EOF EOF
diff stdout expected diff stdout expected
# FIXME: the "ignoring trailing garbage" is unwanted
cat >expected.err <<EOF
5.6-8: unexpected empty block
5.6-8: ignoring trailing garbage
14.6-19.1: missing closing parenthese
19.1: syntax error, unexpected end of file, expecting fi or ':'
autfilt: failed to read automaton from -
EOF
diff stderr expected.err
cat >formulae<<EOF cat >formulae<<EOF