feature: PHI Node creation binding

[cpehle]

Still needs test + more bindings.

[tydeu]

Wow! You beat me to the punch! This was the next instruction I was planning on adding (as I will need it for conditional return blocks when emitting LLVM for Lean). Will merge it soon.

[cpehle]

I went through the list of not implemented instructions and considered which might be the most useful :). So this seemed like a good place to contribute.

[tydeu]

Some notes on style:

• I tend to exclude the createAfter and createAtEnd variants of constructors since they can already be done manually by adding the instruction to the end of the block, and the less bindings to maintain, the better. But I am not heavily against them.

• Similarly, for iterators, I would instead use array getters (getIncomingBlocks/getIncomingValues) plus an adder (addIncoming -- which you already have) and deleters (removeIncomingValue). Index-specific getter/setters are not safe, and I would like to keep the code as safe as is feasible.

[cpehle]

• I don't have a strong opinion either way, if it is trivial to implement the equivalent thing in Lean I agree that this would be the way
• I considered whether the Index based setter / getters were desirable, one could follow the Haskell convention of using unsafe as a prefix for such functions, but of course one can entirely omit them
• I will add the array getters

Thanks for your comments, this codebase is teaching me a lot :).

[tydeu]

@cpehle one thing to keep in mind about using Lean's unsafe -- it refers to type safety, not memory safety. While it can be used for the later to alert users that they are doing something questionable, it is still a less than ideal solution.

I also just don't see the use for index-specific getters/setters for something like phi. I don't think one would know which index a value/block is at without first getting the array thus rendering the getter moot. and I would think setIncomingValueForBlock would be the more used setter.

[cpehle]

@cpehle one thing to keep in mind about using Lean's unsafe -- it refers to type safety, not memory safety. While it can be used for the later to alert users that they are doing something questionable, it is still a less than ideal solution.

I just meant the convention in Haskell to prefix functions that are unsafe with that word, like unsafePerformIO or unsafeGetCStr. My thought process was that at least in Haskell one then typically can implement a safe wrapper on top of this. So for example in the case here, if one reserves a sufficient number of slots $n$ in Create, one can prove that setting the $i$-th slot is save if $i < n$.

I also just don't see the use for index-specific getters/setters for something like phi. I don't think one would know which index a value/block is at without first getting the array thus rendering the getter moot. and I would think setIncomingValueForBlock would be the more used setter.

I've added this setter aswell now, when writing FFI I prefer to go for completeness if easily possible, but I will defer to your judgement.

[cpehle]

One other option for the unsafe operations would be to postfix them with an exclamation mark "!", that is what is used in the FloatArray package for unsafe operations.

[tydeu]

@cpehle The ! suffix for functions, according to the Lean standard, is only suppose to be used for functions that may panic (i.e., call panic! or unreachable! on the Lean side. I would highly suggest just removing the index-specific getters/setters. I would also add a getIncoming function that returns an Array (ValueRef x BasicBlockRef) of the pairs.

Also, if any of the cleanup is to tedious for you, don't worry, I will do some cleanup myself after I merge the PR.

[cpehle]

@cpehle The ! suffix for functions, according to the Lean standard, is only suppose to be used for functions that may panic (i.e., call panic! or unreachable! on the Lean side. I would highly suggest just removing the index-specific getters/setters. I would also add a getIncoming function that returns an Array (ValueRef x BasicBlockRef) of the pairs.

Also, if any of the cleanup is to tedious for you, don't worry, I will do some cleanup myself after I merge the PR.

Ok fair enough, as I understand the use case of the Phi Node in the project now, they would not be needed. On the script side I think the way things are currently setup make it hard to use the phi node.

The following does not work

llvm module phiTest do
  define double @baz(i1 %test, double %a, double %b) do
    br1:
      %c1 = fadd double %a %b
      br %ifcont
    br2:
      %c2 = fsub double %a %b
      br %ifcont
    ifcont:
      %iftmp = phi double [ %c1, %br1 ], [ %c2, %br2 ]
      ret double %iftmp

    br %test, %br1, %br2

I think this might be a limitation of the script API at the moment. It should be possible to use the monadic API to first allocate basic blocks manually and then wire things up, but I did not see a way to use (<- read) and still make use of the labels.

[tydeu]

@cpehle see, now this what I was talking about when I said there were still refactors in the works that I still needed to do! 😆

I am planning on supporting an alternate brace-based function body syntax that will wire up the basic blocks first before building them just like you suggested. I also considering having values using the % syntax instead lookup the value with the given name in the function's symbol table and having only the plain ident syntax use the locally defined variable.

In other words, migrating the script implementation from it's current ad-hoc current state to something better designed and written is the core of the refactoring I need to do. Once it's cleaned adding more complete support for LLVM's IR is a much more reasonable proposition.

[cpehle]

😀. I think the solution of SIL (swift intermediate language) and MLIR is quite elegant: Instead of PHI nodes basic blocks take arguments. That doesn't obviate doing something different from what is done now, but might make sense.

[tydeu]

@cpehle That's a wonderful solution! I am still aiming to have the Script DSL be a superset of LLVM IR (hence the need for the brace-based approach), but I think that be a great way to handle phi nodes in the more Lean-style do function syntax.

It would actually resolve the conundrum I was having for implementation a catch-all PHI node return block. Many functions would use such a block, but I didn't want it to be generated in functions that did not. With this solution, it would just be another parameterized basic block.

[cpehle]

@cpehle That's a wonderful solution! I am still aiming to have the Script DSL be a superset of LLVM IR (hence the need for the brace-based approach), but I think that be a great way to handle phi nodes in the more Lean-style do function syntax.

Yes exactly, it also emphasises the fact that basic blocks are secretly let bound local functions (https://www.cs.princeton.edu/~appel/papers/ssafun.pdf). The LLVM dialect in MLIR also supports this style of blocks (https://mlir.llvm.org/docs/Dialects/LLVM/).

[cpehle]

I believe there is still some cleanup to do and some / a lot more tests to write. I might have some time on the weekend, otherwise I'm really occupied the next week, so I can't spend much time on this.

[tydeu]

@cpehle That's fine (I am similarly busy). I'll merge what's here when I have the time and clean it up as necessary.