[llvm] [llubi] Experimental support for noalias (PR #195808)

[Zhige Chen via llvm-commits]

nofe1248 wrote:

> I tested this PR, and it does give the noalias semantics that I expect in the examples that I tested, but the protectors and state machines do seem rather complex/inefficient: when there are multiple noalias parameters A, B,... for the same function they will do "symmetrical" transitions and often multiple state machines will reach UB simultaneously. It seems this could be simplified/optimized by tracking (per function activation) whether there was memory access:
> 
> * using noalias parameter A,
> * using noalias parameter B,
> * using noalias parameter ...,
> * not using any noalias parameter (i.e. foreign to all noalias parameters of the function),
> * or using multiple of the above
> 
> Then you have UB iff there was memory access using "multiple of the above" and the memory is written (during the function activation). It seems this would yield UB (or no UB) in exactly the same circumstances as what you have here, but it would track this more directly (less state and transitions). [Note: this optimization is not a new idea, it is essentially the "restricted target set" formulation from Homer and MacDonald in [N3058](https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3058.htm) but from the point-of-view of the memory objects rather than from the restrict pointers.]

I am reworking the implementation along those lines, thanks for the suggestion!

> Another question is about the synthetic actions at the protector end, the part that begins here:
> 
> https://github.com/llvm/llvm-project/blob/834527593b85f7121c6fde57d7d86502335846ae/llvm/tools/llubi/lib/Context.cpp#L1006
> 
> 
> I could never see any effect of these (they always seem to transition to the state they are already in). Do you have an example where these actions make a difference (between UB and no UB)? The blog post that you reference just says they are "necessary for complicated reasons" but we'll need to understand this better than that.

The first version was deliberately a fairly mechanical implementation of the proposed model. I included the protector-end actions because they were part of that model. After investigating this more closely, the motivation in the full Tree Borrows model is clearer. Section 3.2 of the [Tree Borrows paper](https://dl.acm.org/doi/pdf/10.1145/3735592) defines implicit reads or writes when a protector is removed. Section 5 explains that these actions are needed for the relational optimization proof: transformations may insert, delete, or reorder accesses while a protector is active, leaving the source and target permission trees in different states. The end action brings those states back into a sufficiently strong relation when the protector ends. But in llubi's narrower LLVM `noalias` model the end action only repeats an access already processed for the same bytes, and the resulting transition is idempotent.

https://github.com/llvm/llvm-project/pull/195808