Add initial struct support for incremental SMT2 decision procedure #7740
Conversation
Codecov ReportPatch coverage:
Additional details and impacted files@@ Coverage Diff @@
## develop #7740 +/- ##
===========================================
+ Coverage 78.54% 78.55% +0.01%
===========================================
Files 1688 1691 +3
Lines 193001 193111 +110
===========================================
+ Hits 151596 151702 +106
- Misses 41405 41409 +4
☔ View full report in Codecov by Sentry. |
thomasspriggs
force-pushed
the
tas/smt2_structs
branch
2 times, most recently
from
5e99bd8 to
f966107
Compare
As some of the setup is the same for each test, the tests can be sections in a single test which share the same setup instead of copying it.
So that multiple lowering transformations can be added and maintained in a single location in a single order.
So that we have initial struct support in place.
To make it easier to debug the changes made by lowering operations.
thomasspriggs
force-pushed
the
tas/smt2_structs
branch
from
f966107 to
a06d62f
Compare
thomasspriggs
requested review from
kroening,
tautschnig,
peterschrammel,
NlightNFotis and
TGWDB
as code owners
I wasn't entirely certain reviewers would prefer the code before or after the refactor, hence I left it in, in case of requests to drop it.
I have merged the PR as is, but I will take a look to see if more regression tests can be switched on for a follow-up PR. |
| @@ -41,6 +42,11 @@ typet struct_encodingt::encode(typet type) const | |||
| return type; | |||
| } | |||
|
|
|||
| static exprt encode(const struct_exprt &struct_expr) | |||
| { | |||
| return concatenation_exprt{struct_expr.operands(), struct_expr.type()}; | |||
There was a problem hiding this comment.
With apologies for being (too) late on this: I think this isn't correct as concatenation expressions have the most-significant bits/bytes first. So IMHO you are now getting the byte order wrong.
There was a problem hiding this comment.
Thanks for letting me know. Do you think reversing the order of the operands is sufficient to fix this and is there a regression test (without unions) which would be sufficient to demonstrate the problem?
There was a problem hiding this comment.
I think there is more to it: you will also need to (recursively?) convert the struct expression's operands to bit vectors, unless that will be handled elsewhere?
Do you have any test that exercises this code at all? I would expect that byte-operator lowering produces such struct expressions at times, but then this might involve unions. Why do unions give you grief? I'd expect all operations on unions to use byte operators, which in turn are lowered.
There was a problem hiding this comment.
Unions in combination with structs are not known to cause any grief to us yet. As the PR title suggests, only initial struct support is in place. All further combinations of structs + other feature are yet to be tested / implemented. It may be as you say that the unions will all disappear in the byte-operator lowering. We need to test to confirm the current status for this.
The deep (recursive style) processing of the operands is handled by the struct_encodingt::encode(exprt expr) function. I have avoided actual recursion in order avoid overflowing the stack in the case of deeply nested expressions. There are unit tests for this function in general which can be found in unit/solvers/smt2_incremental/struct_encoding.cpp.
I will add further tests along with other remaining pieces of struct related functionality in follow-up PRs.
| Test that we support struct values and traces for a trivial example. At the | ||
| time of adding the regression test, this exercised the conversion code specific | ||
| to struct_tag_typet and struct_exprt. Field sensitivity is expected to eliminate | ||
| many of the struct specific expressions before they can reach the decision |
There was a problem hiding this comment.
So .. do you actually exercise the newly added code at all? I'm inclined to think that field sensitivity will completely eliminate any use of structs in this example.
There was a problem hiding this comment.
Yes, the newly added code is exercised. Before this PR an invariant violation would have been encountered, due to the type to sort conversion not understanding a struct_tag_type. The added type conversion pass is sufficient to support non-det struct typed symbols. After field sensitivity has done its thing with the separate symbols/expressions for each field, they are reassembled back into a struct using a struct_exprt at some stage. This is why support for this type of expression was included in this PR.
The kinds of expressions which are eliminated by field sensitivity in this example are member_exprt and with_exprt applied to structs. I have an example C input file which avoids this, with the aid of a sufficiently large array. So next on my list is support for these two kinds of expression.
My apologies if I hadn't explained this sufficiently clearly in the test description.
This PR adds initial
structsupport for the incremental SMT2 decision procedure. Further refinements of this and support for other kinds of expression will be handled in follow-up PRs.