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

LTL parser: better error recovery.

Browse source 
* src/ltlparse/ltlparse.yy: Keep the left operand of binary operator,
if the right one is erroneous.  Also keep the sane beginning of
parenthesized blocks.
* src/ltltest/parseerr.test: Adjust test cases.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2012-06-19 23:43:36 +02:00
parent ac41825efd
commit 0c1fec1259
3 changed files with 55 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

1
NEWS
View file

@ -22,6 +22,7 @@ New in spot 0.9.1a:
automata.
- The Makefile.am of BuDDy, LBTT, and Spot have been adjusted to
accomodate Automake 1.12 (while still working with 1.11).
- Better error recovery when parsing broken LTL formulae.
New in spot 0.9.1 (2012-05-23):

61
src/ltlparse/ltlparse.yy
View file

@ -58,23 +58,36 @@
#include "parsedecl.hh"
using namespace spot::ltl;
#define missing_right_op(res, op, str) \
do \
{ \
error_list.push_back(parse_error(op, \
"missing right operand for \"" str "\"")); \
res = constant::false_instance(); \
} \
#define missing_right_op_msg(op, str) \
error_list.push_back(parse_error(op, \
"missing right operand for \"" str "\""));
#define missing_right_op(res, op, str) \
do \
{ \
missing_right_op_msg(op, str); \
res = constant::false_instance(); \
} \
while (0);
// right is missing, so complain and use left.
#define missing_right_binop(res, left, op, str) \
do \
{ \
left->destroy(); \
missing_right_op(res, op, str); \
missing_right_op_msg(op, str); \
res = left; \
} \
while (0);
// right is missing, so complain and use false.
#define missing_right_binop_hard(res, left, op, str) \
do \
{ \
left->destroy(); \
missing_right_op(res, op, str); \
} \
while (0);
}
@ -362,8 +375,8 @@ sere: booleanatom
| sere OP_AND sere
{ $$ = multop::instance(multop::AndRat, $1, $3); }
| sere OP_AND error
{ missing_right_binop($$, $1, @2,
"length-matching and operator"); }
{ missing_right_binop($$, $1, @2,
"length-matching and operator"); }
| sere OP_SHORT_AND sere
{ $$ = multop::instance(multop::AndNLM, $1, $3); }
| sere OP_SHORT_AND error
@ -528,6 +541,10 @@ sere: booleanatom
bracedsere: BRACE_OPEN sere BRACE_CLOSE
{ $$ = $2; }
| BRACE_OPEN sere error BRACE_CLOSE
{ error_list.push_back(parse_error(@3, "ignoring this"));
$$ = $2;
}
| BRACE_OPEN error BRACE_CLOSE
{ error_list.push_back(parse_error(@$,
"treating this brace block as false"));
@ -538,6 +555,11 @@ bracedsere: BRACE_OPEN sere BRACE_CLOSE
"missing closing brace"));
$$ = $2;
}
| BRACE_OPEN sere error END_OF_INPUT
{ error_list.push_back(parse_error(@3,
"ignoring trailing garbage and missing closing brace"));
$$ = $2;
}
| BRACE_OPEN error END_OF_INPUT
{ error_list.push_back(parse_error(@$,
"missing closing brace, "
@ -547,6 +569,10 @@ bracedsere: BRACE_OPEN sere BRACE_CLOSE
parenthesedsubformula: PAR_OPEN subformula PAR_CLOSE
{ $$ = $2; }
| PAR_OPEN subformula error PAR_CLOSE
{ error_list.push_back(parse_error(@3, "ignoring this"));
$$ = $2;
}
| PAR_OPEN error PAR_CLOSE
{ error_list.push_back(parse_error(@$,
"treating this parenthetical block as false"));
@ -557,6 +583,11 @@ parenthesedsubformula: PAR_OPEN subformula PAR_CLOSE
"missing closing parenthesis"));
$$ = $2;
}
| PAR_OPEN subformula error END_OF_INPUT
{ error_list.push_back(parse_error(@3,
"ignoring trailing garbage and missing closing parenthesis"));
$$ = $2;
}
| PAR_OPEN error END_OF_INPUT
{ error_list.push_back(parse_error(@$,
"missing closing parenthesis, "
@ -630,12 +661,12 @@ subformula: booleanatom
| bracedsere parenthesedsubformula
{ $$ = binop::instance(binop::UConcat, $1, $2); }
| bracedsere OP_UCONCAT error
{ missing_right_binop($$, $1, @2,
{ missing_right_binop_hard($$, $1, @2,
"universal overlapping concat operator"); }
| bracedsere OP_ECONCAT subformula
{ $$ = binop::instance(binop::EConcat, $1, $3); }
| bracedsere OP_ECONCAT error
{ missing_right_binop($$, $1, @2,
{ missing_right_binop_hard($$, $1, @2,
"existential overlapping concat operator");
}
| bracedsere OP_UCONCAT_NONO subformula
@ -645,7 +676,7 @@ subformula: booleanatom
constant::true_instance()), $3);
}
| bracedsere OP_UCONCAT_NONO error
{ missing_right_binop($$, $1, @2,
{ missing_right_binop_hard($$, $1, @2,
"universal non-overlapping concat operator");
}
| bracedsere OP_ECONCAT_NONO subformula
@ -655,7 +686,7 @@ subformula: booleanatom
constant::true_instance()), $3);
}
| bracedsere OP_ECONCAT_NONO error
{ missing_right_binop($$, $1, @2,
{ missing_right_binop_hard($$, $1, @2,
"existential non-overlapping concat operator");
}
| BRACE_OPEN sere BRACE_BANG_CLOSE

15
src/ltltest/parseerr.test
View file

@ -67,23 +67,24 @@ check '/2/3/4/5 a + b /6/7/8/' ''
# leading and trailing garbage are skipped
run 0 ../equals -E 'a U b c' 'a U b'
run 0 ../equals -E 'a &&& b' '0 && b'
# (check multop merging while we are at it)
run 0 ../equals -E 'a & b & c & d e' 'a & b & c & d'
run 0 ../equals -E 'a & (b | c) & d should work' 'a & (b | c) & d'
# Binop recovery
run 0 ../equals -E 'a U' 0
run 0 ../equals -E 'a U b V c R' 0
run 0 ../equals -E 'a U' a
run 0 ../equals -E 'a U b V c R' 'a U b V c'
run 0 ../equals -E 'a &&& b' 'a & b'
run 0 ../equals -E 'a &&| b' 'a | b'
# Recovery inside parentheses
run 0 ../equals -E 'a U (b c) U e R (f g <=> h)' 'a U (0) U e R (0)'
run 0 ../equals -E 'a U (b c) U e R (f g <=> h)' 'a U b U e R f'
run 0 ../equals -E 'a U ((c) U e) R (<=> f g)' 'a U ((c) U e) R (0)'
# Missing parentheses
run 0 ../equals -E 'a & (a + b' 'a & (a + b)'
run 0 ../equals -E 'a & (a + b c' 'a & (0)'
run 0 ../equals -E 'a & (+' 'a & (0)'
run 0 ../equals -E 'a & (' 'a & (0)'
run 0 ../equals -E 'a & (a + b c' 'a & (a + b)'
run 0 ../equals -E 'a & (+' 'a & 0'
run 0 ../equals -E 'a & (' 'a & 0'
# Invalid ranges
run 0 ../equals -E '{a[*8..1];b}' '{a[*1..8];b}'