Redefine synchronization points to specity the address where control flow re-synchronizes #362
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
asSingleton: check if the given pair is a singleton, returning Nothing otherwise toSingleton: convert the pair to a singleton, if it contains an entry for the given binary
Also add some code for stitching together EquivM and PairGraphM
Previously a sync point was interpreted as the start of a CFAR where control flow would synchronize upon exit. This changes a sync point to be interpreted as exactly the address where control flow re-synchronizes, and instead discovers which CFARs may terminate there. Those CFARs are then converted into merge nodes to continue two-sided analysis.
…ceTree This avoids an issue where the refinement choices would add nodes as siblings to the toplevel node, rather than children. This causes strange output artifacts, where these sibling nodes are always appended to the end of the output, rather than appearing in-order.
…k exit There is a widening step that happens when starting a one-sided analysis, which connects the initial node to its Original variant. This ensures that all of the domain information is carried forward from the two-sided to the one-sided analysis. Previously this widening step happened under the assumption that the current path was the exit from the CFAR where the control flow divergence was discovered. This assumption is too strong in general, since there may be additional block exits in the two-sided analysis.
After some previous optimizations the block exit discovery became reasonably fast, making this cache mostly unnecessary. Currently it clutters the output in cases where the cache contains too many false positives (i.e. after some assertion has made those exits infeasible). With the cache, these false positives are displayed in the "Block Exits" list, with a note saying that they are actually infeasible. With this change, the infeasible branches are dropped early during code discovery/alignment.
Handling a block exit may cause the current node to require re-processing from the beginning (i.e. if an assumption was added or desync/sync points were added). This adds a check between each block exit for cases where the current node is going to require re-analysis, ending the analysis early if it does. This is a small optimization, but also helps clean up the output by reducing the number of redundant entries in the Block Exits list.
danmatichuk
force-pushed
the
dm/desync2
branch
from
f2989a6 to
2d209d8
Compare
Changes the synchronization point to be the address where control flow re-synchronizes (rather than the start of the CFAR)
No need to manually tag the nodes with "Original" and "Patched"; they will already be labelled as such since they are single-sided nodes created from toSingleNode
This is primarily for the benefit of allowing the UI to precisely determine how to hook up the single-sided nodes to their merge point.
The "currentFunc" field of the EquivalenceContext is initially set to an "error" value until a function is under analysis. This field is inspected by validInitState in order to resolve architecture-specific validity constraints that are based on the current function. (Specifically this is needed to resolve the TOC on PPC). This change adds a "withPair" wrapper around "validInitState" to ensure that this field is always set in the EquivalenceContext before it is given to any architecture-specific validity functions.
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.
No description provided.