Deduplicate stack ARG InlineReturn edges based on InlineEntry lval and args
#1828
Conversation
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
4 tasks
sim642
added
debugging
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.
PR #1827 caused some ARG tests to fail unexpectedly.
Actually, on the surface it seems to have fixed something: there were TODOs about duplicate
InlineReturn-s in the tests. However, this is very strange because that PR shouldn't change anything about ARGs.#1128 causes some unnecessary additional contexts and paths and these end up reflected in the ARG if not deduplicated correctly. It doesn't matter if you call
__VERIFIER_assert(x == 0)or__VERIFIER_assert(x == 2)if both arguments are definitely true at the call site. And that's what this PR fixes.#1128 still exists and should be fixed for general performance, even if this PR deduplicates its inefficiency.
PR #1827 increases precision of
branchwhich makes the ARG itself more precise and unintentionally fixes the two ARG tests for the wrong reasons.TODO