Fix two bugs in SAWCore's handing of infinite streams #1773
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This was referenced Dec 5, 2022
RyanGlScott
added
the
PR: ready to merge
When calling `atWithDefault n d v i`, `d` should be returned if `i` is greater than or equal to `n`. `atWithDefault` is implemented as a primitive, so we must ensure that this is done in `saw-core`'s `atWithDefaultOp` function. While `atWithDefaultOp` was handling this correctly for generic infinite sequences, it was _not_ correctly handling the special case of infinite bit sequences. This led to the issues reported in #1768. This patch fixes #1768 by introducing a `bpBvAtWithDefault` combinator that implements the defaulting behavior above in terms of `bpBvAt`. I've added a test case to demonstrate that the test case from #1768 now works as expected.
SAWCore assumes the invariant that when indexing into an infinite stream using a symbolic index, the mux tree constructed over the index will test each bit in big-endian order. This is the responsibility of the `selectV` function found in `saw-core`, `saw-core-sbv`, and `saw-core-what4`. All of these functions save for `saw-core-what4`'s `selectV` were upholding this invariant, as `saw-core-what4`'s was testing each bit in little-endian order, resulting in the oddities observed in #1703. This corrects the mistake in `saw-core-what4'`s implementation, fixing #1703. It also leaves some more documentation to make the fact that each `selectV` should be proceeding in big-endian order more apparent.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This fixes two bugs that caused infinite SAWCore streams to misbehave:
saw-core: Fix handling ofatWithDefaultfor infinite bit sequencesWhen calling
atWithDefault n d v i,dshould be returned ifiis greater than or equal ton.atWithDefaultis implemented as a primitive, so we must ensure that this is done insaw-core'satWithDefaultOpfunction. WhileatWithDefaultOpwas handling this correctly for generic infinite sequences, it was not correctly handling the special case of infinite bit sequences. This led to the issues reported in #1768.This patch fixes #1768 by introducing a
bpBvAtWithDefaultcombinator that implements the defaulting behavior above in terms ofbpBvAt. I've added a test case to demonstrate that the test case from #1768 now works as expected.saw-core-what4: Build muxes of symbolic indexes in big-endian orderSAWCore assumes the invariant that when indexing into an infinite stream using a symbolic index, the mux tree constructed over the index will test each bit in big-endian order. This is the responsibility of the
selectVfunction found insaw-core,saw-core-sbv, andsaw-core-what4. All of these functions save forsaw-core-what4'sselectVwere upholding this invariant, assaw-core-what4's was testing each bit in little-endian order, resulting in the oddities observed in #1703.This corrects the mistake in
saw-core-what4's implementation, fixing #1703. It also leaves some more documentation to make the fact that eachselectVshould be proceeding in big-endian order more apparent.