Fix calling convention preconditions #9
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
Before this fix, the preconditions were too weak. In particular, in the case of a function which returns a large value on the stack, they allowed for a return value region in high memory that wraps around 0, potentially clobbering a stack in low memory. This fix strengthens the preconditions to forbid this. Signed-off-by: Nick Spinale <[email protected]>
|
I know that this branch isn't under development, I just wanted to document this bug with a concrete fix. As far as I can tell, this bug is also present in the |
|
I'd suggest a first-line of "disallow stack value return wrap-around" or something, but other than that thumbs up. Sad to hear that it sounds like there are many other confounding bugs, but nice to see improvement! |
Xaphiosis
approved these changes
Dec 13, 2024
lsf37
approved these changes
Dec 13, 2024
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.
Before this fix, the preconditions for function calls at the assembly level were too weak. In particular, in the case of a function which returns a large value on the stack, they allowed for a return value region in high memory that wraps around 0, potentially clobbering a stack in low memory. This prevented the tool from being able to verify refinement in a few specific cases, as the SMT solver was able to find counterexamples where this clobbering happens.
This fix strengthens the preconditions to forbid such clobbering, aligning with the calling convention we are modeling.
This fix effectively changes part of the precondition from
sp <= r0 && sp <= r0 + len(var_c_rets)tosp <= r0 <= r0 + len(var_c_rets). The former permits the problematic case wherer0 + len(var_c_rets) < r0, whereas the latter does not.