crucible-mir: use real element sizes in arrays
#1704
Conversation
spernsteiner
left a comment
spernsteiner
left a comment
There was a problem hiding this comment.
Just reviewed Intrinsics.hs so far
spernsteiner
left a comment
spernsteiner
left a comment
There was a problem hiding this comment.
Reviewed the rest of it
| [Crux] Total: 9 | ||
| [Crux] Proved: 9 |
There was a problem hiding this comment.
Why is this test producing extra subgoals? It would be good to know if we can eliminate those, to reduce the chances of introducing a new performance regression
There was a problem hiding this comment.
The excess goals come from checking the validity of an offset into an aggregate, arising in this case from indexing the 1-length slice. The statement to be proved is that the index (if c { 1 } else { 0 }) is valid, and in this case, that means checking it for equality against the only valid offset, 0. So, this ended up in what4 as roughly if c then 1 else 0 == 0, and what4 then recognized that this could reduce to not c. (I learned this from printing out several intermediate expressions within Mir.Intrinsics.offsetInSpans.) I surmise that not c was simple enough not to show up as a proved goal. With my changes, we're still checking for equality with 0, but because the offset needs to account for the elements' width, the goal statement looks more like 4 * (if c then 1 else 0) == 0, which what4 doesn't seem able to simplify.
I don't know that there's much we can do about this (though perhaps we could to try to patch what4 to recognize and simplify expressions like the one we're producing here). On the bright side, these goals shouldn't grow in size with the number of array elements, because with any length above 1 we should be generating validity expressions using the "run" recognition functionality of #1625 instead.
| subindexMirRefSim sym tpr ref idx elemSize = do | ||
| modifyRefMuxSim (\ref' -> subindexMirRefLeaf sym tpr ref' idx elemSize) ref |
There was a problem hiding this comment.
As an FYI, adding a sym argument will require some minor changes on the SAW and crucible-mir-comp side to accommodate.
There was a problem hiding this comment.
Ah, indeed. I see two calls in crucible-mir-comp's Mir.Compositional.Override to subindexMirRefSim, and both appear to have the necessary sym parameter in scope at the call site already, so this should be fine.
There was a problem hiding this comment.
Indeed, I don't expect it to be difficult to adapt to these changes. This is more of a "please hold off on merging this until the Crux/SAW releases are done" warning.
There was a problem hiding this comment.
Right, I certainly will.
Avoid substantial ad-hoc evaluation effort for slices at the cost of supporting evaluation of entire symbolic arrays, which should be pretty uncommon in the first place.
NFCI - the element type size is still hardcoded as 1, but this is appropriate, since we know we're working with `[u8]` slices.
Note that this causes the `indexing.rs` test to fail, though by generating excess goals to check rather than by failing to verify entirely, making the issue one of performance rather than correctness. The next commit will address this.
Addresses the performance regression introduced and mentioned in the previous commit.
Also add a test case to demonstrate the code pattern this enables.
samcowger
force-pushed
the
sc/array-type-sizes
branch
from
7a5d34c to
d2e58da
Compare
Towards #1666, this makes
crucible-mirconstruct and eliminateMirAggregates representing Rust arrays with offsets and sizes that match those used in Rust, rather than hardcoding all element sizes as 1. (This does not change that same hardcoding in structs or tuples.)The first two commits in this essentially supersede #1700. A major motivation of that PR was to give access to slice element types in order to be able to provide their proper width when accessing them, but it turns out that we can avoid accessing individual slice elements in a way that requires their width.