Conversation
We found this issue while using Isla to prove equivalence between two machine instructions. An unsound simplification caused the check to incorrectly conclude that they were not equivalent. The isla-execute-function -s simplifier pushed extracts through bvadd/bvsub even when lo > 0, losing carries or borrows from lower bits. For 9-bit operands, extracting bit 8 of 0 - 1 yields 1, but extracting bit 8 of each operand before subtracting yields 0. This change restricts arithmetic rewrites to lo == 0 and adds regression tests. Bitwise rewrites remain valid for any slice.
Contributor
|
Thanks. I'm going to commit a slightly different version, including a test that uses the SMT solver for a more thorough check. |
Collaborator
|
I've been experimenting with an E-graph based bitvector simplifier this week, so I might switch to that entirely if it works out. |
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
We found this issue while using Isla to prove equivalence between two machine instructions. With
isla-execute-function -s, an unsound simplification caused the equivalence check to report a false counterexample.For example, consider 8-bit unsigned saturating subtraction implemented using a 9-bit difference:
The simplifier moved the extraction through subtraction, turning d[8] into:
Both extracted bits are zero, so the borrow test always fails. For a = 0, b = 1, the simplified expression returns 255 instead of 0.
Addition has the same issue with carries from discarded lower bits. This patch restricts extract commutation over bvadd and bvsub to slices starting at bit zero, and adds regression tests. Bitwise operations still commute with any slice