[PATCH] D93376: [LangRef] Clarify the semantics of lifetime intrinsics

[Ralf via Phabricator via llvm-commits]

RalfJung added a comment.

> This mixes semantic and implementation of an alloca. Let's not do that.

I'm afraid that happened a long time ago when these intrinsics were added. It is, as far as I can see, not possible to describe the semantic of alloca in a correct way without adding this "magic rule".

You stated what you think the semantics of lifetime.start should be, but what about alloca? Somehow you have to explain the following behavior:

  x = alloca 4
  y = alloca 4
  // assume no lifetime.start in the rest of the function
  // now I can prove that x != y

but

  x = alloca 4
  y = alloca 4
  // Now, x and y may be equal!
  
  lifetime.start x
  ...
  lifetime.end x
  lifetime.start y
  ...
  lifetime.end y

In other words, to describe the *semantics* of alloca (its behavior on the Abstract Machine), we need to "look ahead" and check the lifetime.start of the current function.

Saying "something is dead" on its own doesn't explain the semantics, you have to explain in which way "deadness" is reflected in the Abstract Machine. In particular, one key aspect of the semantics of alloca + lifetime.start is when the allocation (the non-deterministic choice of the address for this local) is made, and how the choice is constrained. Usually for allocation the semantics is that you can pick anything that doesn't overlap with other currently existing allocations, but for alloca in the presence of lifetime.start, this does not work.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D93376