-
Notifications
You must be signed in to change notification settings - Fork 106
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
Encode the basic refinement of escaped local blocks #753
base: master
Are you sure you want to change the base?
Conversation
I'll look into these issues tomorrow. |
@@ -1890,7 +1891,23 @@ expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local, | |||
return val.refined(val2); | |||
} | |||
|
|||
expr Memory::blockPropertiesRefined(const Pointer &src, const Pointer &tgt) | |||
const { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The code below is moved from Memory::blockRefined
below
@@ -1890,7 +1891,23 @@ expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local, | |||
return val.refined(val2); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If pointer bytes are stored inside an alloca, this will call Pointer::refined.
Pointer::refined is unchanged in this PR, so this is fine.
Ready to be reviewed. |
The updated unit tests succeed, but I'll run LLVM unit tests and see how it goes (not sure I'll be back today). |
…escaped locals to writeonly fns
Four new failures appear, and the reasons are as follows: Transforms/DeadStoreElimination/captures-before-call.ll Transforms/MemCpyOpt/callslot.ll
Transforms/LICM/promote-capture.ll
CEx:
|
For the first two failures, I added tests/alive-tv/calls/writeonly-local.srctgt.ll to this PR that must succeed after the issue is fixed. |
Updated the description to explain from which function reading the diff would start. |
These tests have invalid transformations involving escaped local blocks, but Alive2 doesn't detect the problems even with this PR:
|
This patch checks the bytes of local blocks escaped via fn calls (resolves #435 ).
This check is done when the local block ids are known to be constants (which is common). Otherwise, it fallbacks into the original checking.
The beginning point for reading the diff of this PR would be
Pointer::fninputRefined
.If the pointer bids are constant and local, it now calls
Pointer::encodeLocalPtrRefinement
which is a new member function.Among
Pointer::encodeLocalPtrRefinement
's arguments,readsbytes
is:Memory::blockRefined
)bid_other
optional argument is added. If it issome(bid_other)
, refinement of two local blocksbid
andbid_other
is encoded.Pointer::refined
’s block_refined is still commentized, so recursive pointer refinement call does not happen.Memory::blockPropertiesRefined
).The byval encoding is updated to check the contents as well.
It follows the encoding of the cav paper.