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

[Nikita Popov via Phabricator via llvm-commits]

nikic added a comment.

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).

> 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.


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

https://reviews.llvm.org/D156476