Deduplicate instruction prefixes when disassembling #43
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
|
Still to come is a comparison of profiling reports for large SAW proofs before and after this patch to compare the memory usage. In the meantime, this patch is in a suitable state for review. |
travitch
reviewed
Jun 30, 2022
travitch
reviewed
Jun 30, 2022
travitch
approved these changes
Jun 30, 2022
Previously, the opcode lookup table would encode every possible permutation of allowable prefixes for each instruction as a separate path. This is expensive in both space and time, as observed in #40. The new approach taken in this patch, as described in `Note [x86_64 disassembly]` in `Flexdis86.Disassembler`, is to only encode the VEX prefixe and opcode bytes in the lookup table, leaving out all other forms of prefix bytes entirely. Instead, disassembly will start by eagerly parsing as many prefix bytes as possible, proceeding to parse opcode bytes after the first non-prefix byte is encountered. After identifying the possible instructions from the opcode, we will then narrow down exactly which instruction it is by validating them against the set of parsed prefixes. As noted in `Note [x86_64 disassembly]`, we had to add some special cases for `nop`-like instructions—namely, `endbr32`, endbr64`, `pause`, and `xchg`—to avoid some prefix byte–related ambiguity. The new handling for `xchg` is more accurate than it was before, so this patch fixes #42 as a side effect. This patch also addresses part (1) of #40 in that it should reduce the amount of memory usage that the lookup table takes, although there is potentially more work to be done (see part (2) of #40).
RyanGlScott
force-pushed
the
T40-part-one
branch
from
2466b43 to
9ec23fa
Compare
|
Here is a heap profiling report for the same SAW proof as in #40 (comment), but with the patch in #43 applied:
|
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this pull request
Jul 1, 2022
This patch brings in the changes from GaloisInc/flexdis86#43, which redesigns the x86_64 disassembler in `flexdis86` to use a substantially smaller lookup table, thereby saving a fair bit of resident memory when doing x86-related proofs.
robdockins
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Jul 1, 2022
This patch brings in the changes from GaloisInc/flexdis86#43, which redesigns the x86_64 disassembler in `flexdis86` to use a substantially smaller lookup table, thereby saving a fair bit of resident memory when doing x86-related proofs.
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.
Previously, the opcode lookup table would encode every possible permutation of allowable prefixes for each instruction as a separate path. This is expensive in both space and time, as observed in #40. The new approach taken in this patch, as described in
Note [x86_64 disassembly]inFlexdis86.Disassembler, is to only encode the VEX prefixe and opcode bytes in the lookup table, leaving out all other forms of prefix bytes entirely. Instead, disassembly will start by eagerly parsing as many prefix bytes as possible, proceeding to parse opcode bytes after the first non-prefix byte is encountered. After identifying the possible instructions from the opcode, we will then narrow down exactly which instruction it is by validating them against the set of parsed prefixes.As noted in
Note [x86_64 disassembly], we had to add some special cases fornop-like instructions—namely,endbr32,endbr64,pause, andxchg—to avoid some prefix byte–related ambiguity. The new handling forxchgis more accurate than it was before, so this patch fixes #42 as a side effect. This patch also addresses part (1) of #40 in that it should reduce the amount of memory that the lookup table uses, although there is potentially more work to be done (see part (2) of #40).