[PATCH] D156476: [IR] Mark `llvm.trap` as `memory(inaccessiblemem: write)`

[Nuno Lopes via Phabricator via llvm-commits]

nlopes accepted this revision.
nlopes added a comment.
This revision is now accepted and ready to land.

In D156476#4541682 <https://reviews.llvm.org/D156476#4541682>, @nikic wrote:

> In D156476#4541615 <https://reviews.llvm.org/D156476#4541615>, @nlopes wrote:
>
>> In D156476#4540161 <https://reviews.llvm.org/D156476#4540161>, @nikic wrote:
>>
>>> Yeah, good point. mustprogress + readonly = willreturn, so we need to force a write memory effect to avoid that. In that case `memory(inaccessiblemem: write)` does seem like the best we can do.
>>
>> I don't know why that equality must hold.
>
> Here is what LangRef says about mustprogress:
>
>> This attribute indicates that the function is required to return, unwind, or interact with the environment in an observable way e.g. via a volatile memory access, I/O, or other synchronization.
>
> We assume that the "interact with the environment" part of this requires at least (something modeled as) a memory write. This means that for a readonly function, the only way to satisfy mustprogress is to return (where return can also be an unwind).
>
> Edit: To clarify, this is supposed to be an implication, not an equality. We certainly can't deduce mustprogress and readonly from willreturn.
>
>> A function that doesn't return doesn't have to write to memory. We can think of the state has having a `halt` bit, to where trap, exit(), etc, write to.  (exit() reads memory because it executes global destructors though, while trap doesn't).
>
> That `halt` bit is effectively what `inaccessiblemem: write` models.

I was thinking that this bit is part of the state machine, not of the memory. But it's fair enough to exclude bits that are observable by the program. We have to be careful with functions with float operations and so on, since those can't be nowrite with this definition (as they may read/write rounding mode, etc).

But fair enough, I'm good with that definition. Thanks!


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D156476/new/

https://reviews.llvm.org/D156476