Skip to content

Remove PtrWrite hook#1176

Merged
danielsn merged 4 commits intomodel-checking:mainfrom
danielsn:pointer-hook
Jul 13, 2022
Merged

Remove PtrWrite hook#1176
danielsn merged 4 commits intomodel-checking:mainfrom
danielsn:pointer-hook

Conversation

@danielsn
Copy link
Contributor

@danielsn danielsn commented May 6, 2022

Description of changes:

The PtrWrite hook is no longer necessary given that we support the underlying intrinsics.

Resolved issues:

Resolves #1173

Call-outs:

Removing the PtrRead hook makes the regression timeout. Only removing PtrWrite for now. #1175

Testing:

  • How is this change tested? Existing tests

  • Is this a refactor change? No

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@danielsn danielsn requested a review from a team as a code owner May 6, 2022 17:10
Copy link
Contributor

@tedinski tedinski left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Was this just legacy from before we had intrinsic handling code?

Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought that removing this hook would still require you to add implementations for write and write_unaligned as intrinsics, but this does not seem to be the case. So the code for handling these "writes" must be somewhere else.

Can you please find out where the code handling these "writes" is? The regular version should have an alignment check as in codegen_volatile_store.

@adpaco-aws adpaco-aws mentioned this pull request May 13, 2022
4 tasks
@danielsn danielsn self-assigned this May 25, 2022
@danielsn
Copy link
Contributor Author

Blocked on diffblue/cbmc#6856

@danielsn danielsn dismissed adpaco-aws’s stale review July 13, 2022 14:35

#1201 Fixed Adrian's issue

@danielsn danielsn merged commit e6142a4 into model-checking:main Jul 13, 2022
@danielsn danielsn deleted the pointer-hook branch July 13, 2022 16:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

No open projects
Status: Done

Development

Successfully merging this pull request may close these issues.

Remove PtrWrite hook

3 participants