Fix store borrow verification #59360
Conversation
eeckstein
commented
Jun 10, 2022
eeckstein
commented
- fix verification of store_borrow locations in the MemoryLifetimeVerifier
- document that a store_borrow location must not be modified by other instructions in SIL.rst
In case of a single-block location, the verification of store_borrow locations didn't work in all cases.
…ther instructions.
|
@swift-ci test |
|
LGTM |
1 similar comment
|
LGTM |
| @@ -3745,6 +3745,8 @@ store_borrow | |||
|
|
|||
| Stores the value ``%0`` to a stack location ``%1``, which must be an | |||
| ``alloc_stack $T``. | |||
| The stack location must not be modified by other instructions than | |||
| ``store_borrow``. | |||
There was a problem hiding this comment.
The stack location must not be modified by other instructions than
store_borrow.
This is a type-level semantic restriction. So you're saying that we infer type information from the existence of a store_borrow somewhere on the same address (obvious IR design fail). Where do we check that a store_borrow's address is always derived from an alloc_stack, and that for the same alloc_stack all uses end in a known read-only operation?
There was a problem hiding this comment.
It's even stricter: the destination address of a store_borrow must be an alloc_stack (not just derived from). That's verified in the SILVerifier. I was considering added a flag to alloc_stack to indicate a store-borrow location, but given that it's really easy to derive and verify, I think a flag is not really needed.
Alternatively we could also combine store_borrow and alloc_stack into a single instruction.
, and that for the same alloc_stack all uses end in a known read-only operation?
That's verified in the MemoryLifetimeVerifier
There was a problem hiding this comment.
I don't think an alloc_stack flag helps. It's just that the entire concept of a "borrow-only location" was buried in the memory verifier, so it just seemed like a shortcut to avoid doing stronger verification. I didn't see any separate logic that does: check all uses of a borrow-only location to prove they are read-only. I bet ownership verification would be simpler if we could assume that invariant.
