Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove redundant "valid pointer" checks from memory loads and stores. #310

Merged
merged 2 commits into from
Aug 8, 2022

Conversation

robdockins
Copy link
Contributor

The internal memory model operations already assert the same checks.

CF #300

The internal memory model operations already assert the same checks.
@robdockins
Copy link
Contributor Author

SAW CI is passing with this change, so I think we are probably good on that front.

GaloisInc/saw-script#1722

@robdockins
Copy link
Contributor Author

Should I be concerned about the GHC 9.2.2 build fail? I don't see how it could be related to this.

@travitch
Copy link
Contributor

travitch commented Aug 8, 2022

No, it is fine. Looks like the runner crashed again. Feel free to merge when you feel like it

@robdockins robdockins merged commit d952555 into master Aug 8, 2022
@travitch travitch deleted the rwd/redundant-checks branch August 8, 2022 21:27
RyanGlScott added a commit to GaloisInc/ambient-verifier that referenced this pull request Mar 1, 2023
This bumps the `macaw` submodule to bring in the changes from
GaloisInc/macaw#310, which removes some redundant
pointer validity checks from `macaw-symbolic`'s load- and store-related
operations. Because the verifier's test suite counts the number of goals
generated, this has the effect of reducing the overall number of goals in some
test cases. I have confirmed (by manual inspection) that the goals that were
removed with this patch all come from the redundant checks removed in the
`macaw` patch.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants