SMT2 parser errors #3441
SMT2 parser errors #3441
Conversation
kroening
commented
Nov 18, 2018
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
requested review from
martin-cs,
peterschrammel and
tautschnig
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 726babc).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91800481
src/solvers/smt2/smt2_tokenizer.h
Outdated
| /// this is a dummy -- errors are reported via the error() stream | ||
| std::string what() const override | ||
| { | ||
| return ""; |
There was a problem hiding this comment.
This is a bit of non-standard use of exceptions. The error message should be attached to it so that the fatal error handling and printing can be done by the caller. It's the decision of the caller what to do when an error happens (ignore, log and carry on, abort,...). Moreover, the message handler dependency could be removed here.
There was a problem hiding this comment.
Ok, now with error message in the exception.
| } | ||
| } | ||
| catch(smt2_errort) | ||
| { | ||
| return true; |
There was a problem hiding this comment.
I don't think translating exceptions to 'error codes' at internal interfaces is a good thing.
There was a problem hiding this comment.
I'm with @peterschrammel - I think this is exceptions-as-return-values, which is the one thing we teach people not to use exceptions for. Also both commits lack a commit message body explaining why any of these changes are being made. Such messages might help understand why introducing state into the lexer is a good idea.
| @@ -56,6 +56,10 @@ class smt2_tokenizert:public parsert | |||
| return messaget::error(); | |||
| } | |||
|
|
|||
| /// skip any tokens until all parentheses are closed | |||
| /// or the end of file is reached | |||
| void skip_to_end_of_list(); | |||
There was a problem hiding this comment.
This is being added, but never invoked. (And I find it rather weird to have an a lexical analyzer.)
There was a problem hiding this comment.
Ok, now moved one level up to parser.
src/solvers/smt2/smt2_parser.cpp
Outdated
| error() << "expected end of command" << eom; | ||
| return; | ||
| // consume any tokens till the end of the command | ||
| skip_to_end_of_list(); |
There was a problem hiding this comment.
This is to recover cleanly from parse errors.
kroening
force-pushed
the
smt2_parser_errors
branch
from
726babc to
b97d3a1
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: b97d3a1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92465647
src/solvers/smt2/smt2irep.cpp
Outdated
| } | ||
| } | ||
| catch(smt2_errort) |
There was a problem hiding this comment.
This will now just eat the error message.
kroening
force-pushed
the
smt2_parser_errors
branch
from
b97d3a1 to
e8382a2
Compare
kroening
force-pushed
the
smt2_parser_errors
branch
2 times, most recently
from
a0444cd to
5f79032
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 5f79032).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92913553
|
This (now) needs a rebase, but is otherwise good to go. |
The tokenizer is changed to split reading tokens and consuming them; the parser counts the parentheses.
kroening
force-pushed
the
smt2_parser_errors
branch
from
5f79032 to
e6049e1
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: e6049e1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92942542
