Add validation of smt parse trees to construct smt_responset instances. #6458
Conversation
Codecov Report
@@ Coverage Diff @@
## develop #6458 +/- ##
===========================================
+ Coverage 75.98% 75.99% +0.01%
===========================================
Files 1542 1546 +4
Lines 165038 165240 +202
===========================================
+ Hits 125404 125579 +175
- Misses 39634 39661 +27
Continue to review full report at Codecov.
|
thomasspriggs
force-pushed
the
tas/type_check_smt_response
branch
2 times, most recently
from
2b91bf9 to
0e66013
Compare
| @@ -37,5 +37,14 @@ template class response_or_errort<smt_responset>; | |||
|
|
|||
| response_or_errort<smt_responset> validate_smt_response(const irept &parse_tree) | |||
| { | |||
| if(parse_tree.id() == "sat") | |||
There was a problem hiding this comment.
⛏️ Why not switch (parse_tree.id()) { case "sat": }. Might make it a bit more readable?
There was a problem hiding this comment.
Because you can't switch on a string in C++.
There was a problem hiding this comment.
But you can switch on a/the first character... so if you want a big nested tree of case statements... ;)
thomasspriggs
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
tautschnig and
TGWDB
as code owners
| return {response_or_errort<smt_responset>{ | ||
| "Error response has multiple error messages."}}; |
There was a problem hiding this comment.
Can we do something nicer here? Maybe gather all the error messages into a multiline string?
There was a problem hiding this comment.
I have done something nicer here. The original parse tree is now included in this error message, as instances where the messages are sub trees could also fall into this case.
| @@ -37,5 +37,14 @@ template class response_or_errort<smt_responset>; | |||
|
|
|||
| response_or_errort<smt_responset> validate_smt_response(const irept &parse_tree) | |||
| { | |||
| if(parse_tree.id() == "sat") | |||
There was a problem hiding this comment.
But you can switch on a/the first character... so if you want a big nested tree of case statements... ;)
The `response_or_errort` class is a template, so that it can be reused for smt_termt and `smt_sortt` sub trees of the SMT responses, whilst maintaining strong compile time type checking. The `UNIMPLEMENTED` macro in the `validate_smt_response` function will be replaced with an implementation in the following commits of this PR.
To facilitate debugging of tests and tracking down causes of test failures.
So they can be reused in multiple test `.cpp` files.
For each non-leaf node in the `smt_responset` tree, the same logic is required where the child nodes are validated and we construct the non-leaf node if there are no errors, or collect and propagate the errors upwards if there are errors validating the child nodes. The template in this commit abstracts this logic out, so that it doesn't need to be duplicated for each type of node we construct.
This is currently implemented using `pretty`, but this function is used forward to replace with an implementation specific to our use case which is more easily readable by users of CBMC.
The template parameter is specified for mapping to upper case characters to fix a warning compiling on Ubuntu 18. This warning was related to `std::toupper` being declared with the deprecated `throw ()` in the standard library and the meaning of this changing between C++ versions.
So that it is still possible to see the error message which was being reported.
thomasspriggs
force-pushed
the
tas/type_check_smt_response
branch
from
0e66013 to
6c3d1da
Compare
This PR adds validation of smt parse trees to construct smt_responset instances.