feature: PHI Instruction creation

Papyrus/IR/InstructionRefs.lean

@@ -403,3 +403,74 @@ def createCall
   CallInstRef.create (← self.getFunctionType) self args name
 
 end FunctionRef
+
+--------------------------------------------------------------------------------
+-- # PHI
+--------------------------------------------------------------------------------
+
+/--
+  A reference to an external LLVM
+  [PHINode](https://llvm.org/doxygen/classllvm_1_1PHINode.html).
+-/
+structure PHINodeRef extends InstructionRef, ValueRef
+instance : Coe PHINodeRef InstructionRef := ⟨(·.toInstructionRef)⟩
+instance : Coe PHINodeRef ValueRef := ⟨(·.toValueRef)⟩
+
+namespace PHINodeRef
+/-- Create a new phi node instruction. -/
+@[extern "papyrus_phi_node_create"]
+constant create (type : @& TypeRef) (numReservedValues : UInt32 := 0) (name : @& String := "") : IO PHINodeRef
+
+/-- Create a new phi node instruction at the end of a given basic block.  -/
+@[extern "papyrus_phi_node_create_at_end"]
+constant createAtEnd (type : @& TypeRef) (numReservedValues : UInt32 := 0) (name : @& String := "") (bb : @& BasicBlockRef) : IO PHINodeRef
+
+/-- Create a new phi node instruction after the given instruction.  -/
+@[extern "papyrus_phi_node_create_after"]
+constant createAfter (type : @& TypeRef) (numReservedValues : UInt32 := 0) (name : @& String := "") (inst : @& InstructionRef) : IO PHINodeRef
+
+/-- get incoming value number i  -/
+@[extern "papyrus_phi_node_get_incoming_value"]
+constant getIncomingValue (node : @& PHINodeRef) (i : UInt32) : IO ValueRef
+
+/-- set incoming value number i -/
+@[extern "papyrus_phi_node_set_incoming_value"]
+constant setIncomingValue (node : @& PHINodeRef) (i : UInt32) (value : @& ValueRef) : IO PUnit
+
+/-- get incoming block number i  -/
+@[extern "papyrus_phi_node_get_incoming_block"]
+constant getIncomingBlock (node : @& PHINodeRef) (i : UInt32) : IO BasicBlockRef
+
+/-- set incoming block number i -/
+@[extern "papyrus_phi_node_set_incoming_block"]
+constant setIncomingBlock (node : @& PHINodeRef) (i : UInt32) (value : @& BasicBlockRef) : IO PUnit
+
+/-- add an incoming value to the phi node list -/
+@[extern "papyrus_phi_node_add_incoming"]
+constant addIncoming (node : @& PHINodeRef) (value : @& ValueRef) (bb : @& BasicBlockRef) : IO PUnit
+
+/-- get blocks branching to this phi node -/
+@[extern "papyrus_phi_node_get_blocks"]
+constant getBlocks (node : @& PHINodeRef) : IO (Array BasicBlockRef)
+
+/-- get incoming values to this phi node -/
+@[extern "papyrus_phi_node_incoming_values"]
+constant getValues (node : @& PHINodeRef) : IO (Array ValueRef)
+
+/-- set incoming value for block -/
+@[extern "papyrus_phi_node_set_incoming_value"]
+constant setIncomingValueForBlock (node : @& PHINodeRef) (bb : @& BasicBlockRef) (value : @& ValueRef) : IO PUnit
+
+/-- get incoming value for block -/
+@[extern "papyrus_phi_node_set_incoming_value"]
+constant getIncomingValueForBlock (node : @& PHINodeRef) (bb : @& BasicBlockRef) : IO ValueRef
+
+/-- whether all blocks have an incoming value -/
+@[extern "papyrus_phi_node_is_complete"]
+constant isComplete (node : @& PHINodeRef) : IO Bool
+
+/-- whether the phi node merges together the same value -/
+@[extern "papyrus_phi_node_has_constant_or_undef_value"]
+constant hasConstantOrUndefValue (node : @& PHINodeRef) : IO Bool
+
+end PHINodeRef

c/src/instruction.cpp

@@ -433,4 +433,131 @@ extern "C" lean_obj_res papyrus_call_inst_create
 	return lean_io_result_mk_ok(mkValueRef(copyLink(typeRef), i));
 }
 
+//------------------------------------------------------------------------------
+// PHI
+//------------------------------------------------------------------------------
+
+// Get the LLVM StoreInst pointer wrapped in an object.
+PHINode* toPHINode(lean_object* instRef) {
+	return llvm::cast<PHINode>(toValue(instRef));
+}
+
+// Get a reference to a newly created phi instruction.
+extern "C" lean_obj_res papyrus_phi_node_create
+	(b_lean_obj_res typeRef, unsigned numReservedValues, b_lean_obj_res nameObj, lean_obj_arg /* w */)
+{
+	auto i = PHINode::Create(toType(typeRef), numReservedValues, refOfString(nameObj));
+	return lean_io_result_mk_ok(mkValueRef(copyLink(typeRef), i));
+}
+
+// Get a reference to a newly created phi instruction inserted at the end of the given basic block
+extern "C" lean_obj_res papyrus_phi_node_create_at_end
+	(b_lean_obj_res typeRef, unsigned numReservedValues, b_lean_obj_res nameObj, b_lean_obj_res bb, lean_obj_arg /* w */)
+{
+	auto i = PHINode::Create(toType(typeRef), numReservedValues, refOfString(nameObj), toBasicBlock(bb));
+	return lean_io_result_mk_ok(mkValueRef(copyLink(typeRef), i));
+}
+
+// Get a reference to a newly created phi instruction inserted after the given instruction
+extern "C" lean_obj_res papyrus_phi_node_create_after
+	(b_lean_obj_res typeRef, unsigned numReservedValues, b_lean_obj_res nameObj, b_lean_obj_res inst, lean_obj_arg /* w */)
+{
+	auto i = PHINode::Create(toType(typeRef), numReservedValues, refOfString(nameObj), toInstruction(inst));
+	return lean_io_result_mk_ok(mkValueRef(copyLink(typeRef), i));
+}
+
+// return incoming value number i
+extern "C" lean_obj_res papyrus_phi_node_get_incoming_value
+	(b_lean_obj_res instRef, unsigned i, lean_obj_arg /* w */)
+{
+	auto val = toPHINode(instRef)->getIncomingValue(i);
+	return lean_io_result_mk_ok(mkValueRef(copyLink(instRef), val));
+}
+
+// set incoming value number i
+extern "C" lean_obj_res papyrus_phi_node_set_incoming_value
+	(b_lean_obj_res instRef, unsigned i, b_lean_obj_res val, lean_obj_arg /* w */) {
+	toPHINode(instRef)->setIncomingValue(i, toValue(val));
+	return lean_io_result_mk_ok(lean_box(0));
+}
+
+// return incoming block number i
+extern "C" lean_obj_res papyrus_phi_node_get_incoming_block
+	(b_lean_obj_res instRef, unsigned i, lean_obj_arg /* w */)
+{
+	auto bb = toPHINode(instRef)->getIncomingBlock(i);
+	return lean_io_result_mk_ok(mkValueRef(copyLink(instRef), bb));
+}
+
+// set incoming block number i
+extern "C" lean_obj_res papyrus_phi_node_set_incoming_block
+	(b_lean_obj_res instRef, unsigned i, b_lean_obj_res val, lean_obj_arg /* w */) {
+	toPHINode(instRef)->setIncomingBlock(i, toBasicBlock(val));
+	return lean_io_result_mk_ok(lean_box(0));
+}
+
+// add an incoming value to the end of the PHI list
+extern "C" lean_obj_res papyrus_phi_node_add_incoming
+	(b_lean_obj_res instRef, b_lean_obj_res val, b_lean_obj_res bb, lean_obj_arg /* w */) {
+	toPHINode(instRef)->addIncoming(toValue(val), toBasicBlock(bb));
+	return lean_io_result_mk_ok(lean_box(0));
+} 
+
+// get the array of blocks of this phi node
+extern "C" lean_obj_res papyrus_phi_node_blocks
+	(b_lean_obj_res instRef, lean_obj_arg /* w */) {
+	auto link = borrowLink(instRef);
+	auto blocks = toPHINode(instRef)->blocks();
+	lean_object* arr = lean_alloc_array(0, PAPYRUS_DEFAULT_ARRAY_CAPCITY);
+	for (auto& block : blocks) {
+		lean_inc_ref(link);
+		arr = lean_array_push(arr, mkValueRef(link, block.get()));
+	}
+	return lean_io_result_mk_ok(arr);
+}
+
+// get array of incoming values for phi node
+extern "C" lean_obj_res papyrus_phi_node_incoming_values
+	(b_lean_obj_res instRef, lean_obj_arg /* w */) {
+
+	auto link = borrowLink(instRef);
+	auto values = toPHINode(instRef)->incoming_values();
+	lean_object* arr = lean_alloc_array(0, PAPYRUS_DEFAULT_ARRAY_CAPCITY);
+	for (auto& value : values) {
+		lean_inc_ref(link);
+		arr = lean_array_push(arr, mkValueRef(value, block.get()));
+	}
+	return lean_io_result_mk_ok(arr);
+}
+
+// set incoming value of block
+extern "C" lean_obj_res papyrus_phi_node_set_incoming_value_for_block
+	(b_lean_obj_res instRef, b_lean_obj_res bb, b_lean_obj_res val, lean_obj_arg /* w */) {
+	toPHINode(instRef)->setIncomingValueForBlock(toBasicBlock(bb), toValue(val));
+	return lean_io_result_mk_ok(lean_box(0));
+}
+
+// return incoming value for given block
+extern "C" lean_obj_res papyrus_phi_node_get_incoming_value
+	(b_lean_obj_res instRef, b_lean_obj_res bb, lean_obj_arg /* w */)
+{
+	auto val = toPHINode(instRef)->getIncomingValueForBlock(bb);
+	return lean_io_result_mk_ok(mkValueRef(copyLink(instRef), val));
+}
+
+// whether the phi node has incoming values for all predecessors 
+extern "C" uint8_t papyrus_phi_node_is_complete
+	(b_lean_obj_res instRef, lean_obj_arg /* w */)
+{
+	return toPHINode(instRef)->isComplete();
+}
+
+extern "C" uint8_t papyrus_phi_node_has_constant_or_undef_value
+	(b_lean_obj_res instRef, lean_obj_arg /* w */)
+{
+	return toPHINode(instRef)->hasConstantOrUndefValue();
+}
+
+
+
 } // end namespace papyrus

test/run/ir/instructionRefs.lean

@@ -129,3 +129,19 @@ def assertBEq [Repr α] [BEq α] (expected actual : α) : IO PUnit := do
   let inst ← CallInstRef.create fnTy fn #[]
   assertBEq ValueKind.instruction inst.valueKind
   assertBEq InstructionKind.call inst.instructionKind
+
+-- `PHI Node`
+#eval LlvmM.run do
+  let i8Ty ← int8Type.getRef -- type of the PHI Node
+  let then_ ← BasicBlockRef.create "then"
+  let else_ ← BasicBlockRef.create "else"
+  let merge_ ← BasicBlockRef.create "ifcont"
+  let inst ← CondBrInstRef.create then_ else_ (← ConstantIntRef.ofBool true)
+  let thenValue ← ConstantIntRef.ofUInt8 0
+  let elseValue ← ConstantIntRef.ofUInt8 2
+  let phi ← PHINodeRef.createAtEnd i8Ty (numReservedValues := 2) (name := "iftmp") (bb := merge_)
+  phi.addIncoming thenValue then_
+  phi.addIncoming elseValue else_
+
+  assertBEq (← phi.isComplete) true
+  let values ← phi.getValues