From 096f5e12846c6c3cd1fdad7314ca9b78dbcbba24 Mon Sep 17 00:00:00 2001 From: Axel Sorenson Date: Thu, 13 Aug 2026 17:08:23 -0600 Subject: [PATCH 1/5] feat: add control flow branch interface --- Veir.lean | 1 + Veir/Interfaces.lean | 1 + Veir/Interfaces/ControlFlowInterfaces.lean | 110 +++++++++++++++++++++ 3 files changed, 112 insertions(+) create mode 100644 Veir/Interfaces/ControlFlowInterfaces.lean diff --git a/Veir.lean b/Veir.lean index d47277e31..621648c9f 100644 --- a/Veir.lean +++ b/Veir.lean @@ -11,6 +11,7 @@ import Veir.Rewriter.WfRewriter import Veir.Printer import Veir.PatternRewriter.Basic import Veir.Interfaces.FoldInterfaces +import Veir.Interfaces.ControlFlowInterfaces import Veir.Passes.ArithToLLVM.Proofs import Veir.Passes.Canonicalize.Proofs import Veir.Passes.RISCVCombines.Proofs diff --git a/Veir/Interfaces.lean b/Veir/Interfaces.lean index c03a4062f..0946e80cf 100644 --- a/Veir/Interfaces.lean +++ b/Veir/Interfaces.lean @@ -7,3 +7,4 @@ import Veir.Interfaces.RegionKindInterfaces import Veir.Interfaces.SideEffectInterfaces import Veir.Interfaces.DeadCodeInterfaces import Veir.Interfaces.ConstantLikeInterfaces +import Veir.Interfaces.ControlFlowInterfaces diff --git a/Veir/Interfaces/ControlFlowInterfaces.lean b/Veir/Interfaces/ControlFlowInterfaces.lean new file mode 100644 index 000000000..492c9daf9 --- /dev/null +++ b/Veir/Interfaces/ControlFlowInterfaces.lean @@ -0,0 +1,110 @@ +module + +public import Veir.GlobalOpInfo + +/-! +# ControlFlowInterfaces + +This file provides support for querying which operands are forwarded to a successor +and mapping those operands to successor block arguments. +-/ + +namespace Veir + +public section + +/-- The SSA values forwarded from a branch operation to one of its successors. -/ +structure SuccessorOperands where + /-- The SSA values forwarded to the successor. -/ + forwardedOperands : Array ValuePtr +deriving Inhabited, Repr, DecidableEq + +namespace SuccessorOperands + +/-- + Return the SSA value forwarded to a successor block argument. +-/ +def getForwardedOperand? + (operands : SuccessorOperands) (blockArgumentIndex : Nat) : Option ValuePtr := + operands.forwardedOperands[blockArgumentIndex]? + +end SuccessorOperands + +namespace BranchOpInterface + +/-- + Return the operands passed to `successorIndex` of a branch operation. +-/ +def getSuccessorOperands? + (branchOp : OperationPtr) (successorIndex : Nat) (raw : IRContext OpCode) : + Option SuccessorOperands := + let opType := branchOp.getOpType! raw + match opType with + | .cf .br | .llvm .br | .riscv_cf .branch => + -- Unconditional branches have one successor and forward every operation operand. + if branchOp.getNumSuccessors! raw ≠ 1 || successorIndex ≠ 0 then + none + else + some { + forwardedOperands := branchOp.getOperands! raw + } + | _ => do + -- Determine whether this is a supported conditional branch and how many + -- fixed operands appear before its successor operand segments. + let fixedOperandCount ← match opType with + | .cf .cond_br + | .llvm .cond_br + | .riscv_cf .beqz + | .riscv_cf .bnez => some 1 + | .riscv_cf .beq + | .riscv_cf .bne + | .riscv_cf .blt + | .riscv_cf .bge + | .riscv_cf .bltu + | .riscv_cf .bgeu => some 2 + | _ => none + -- Read the operand segment metadata from the operation's typed properties. + let attrs := Properties.toAttrDict opType (branchOp.getProperties! raw opType) + let some (.denseArrayAttr sizes) := attrs["operandSegmentSizes".toUTF8]? | none + let successorCount := branchOp.getNumSuccessors! raw + let segmentSizes := sizes.values + -- Validate the requested successor and the basic shape of the segment metadata. + if successorIndex ≥ successorCount then + none + if segmentSizes.size ≠ fixedOperandCount + successorCount then + none + if segmentSizes.extract 0 fixedOperandCount |>.any (· ≠ 1) then + none + if segmentSizes.any (· < 0) then + none + -- Select the segment corresponding to the requested successor. + let segmentIndex := fixedOperandCount + successorIndex + let forwardedCountRaw ← segmentSizes[segmentIndex]? + let forwardedCount := forwardedCountRaw.toNat + let operandCount := branchOp.getNumOperands! raw + -- Ensure the segment metadata accounts for every operation operand. + let segmentSum := segmentSizes.foldl (init := 0) fun acc value => acc + value.toNat + if segmentSum ≠ operandCount then + none + -- Compute the operation operand index where this successor's forwarded values begin. + let forwardedStart := fixedOperandCount + + (segmentSizes.extract fixedOperandCount segmentIndex).foldl + (init := 0) fun acc value => acc + value.toNat + -- Return only the operands forwarded to the requested successor. + some { + forwardedOperands := (branchOp.getOperands! raw).extract + forwardedStart (forwardedStart + forwardedCount) + } + +/-- Return the SSA value forwarded to a successor block argument. -/ +def getSuccessorOperand? + (branchOp : OperationPtr) (successorIndex blockArgumentIndex : Nat) + (raw : IRContext OpCode) : Option ValuePtr := + getSuccessorOperands? branchOp successorIndex raw >>= fun operands => + operands.getForwardedOperand? blockArgumentIndex + +end BranchOpInterface + +end + +end Veir From ca71ca5bdd4fa9fc09e81d89eb3c4674d905341d Mon Sep 17 00:00:00 2001 From: Axel Sorenson Date: Mon, 17 Aug 2026 14:18:20 -0600 Subject: [PATCH 2/5] Remove checks --- Veir/Interfaces/ControlFlowInterfaces.lean | 25 +++------------------- 1 file changed, 3 insertions(+), 22 deletions(-) diff --git a/Veir/Interfaces/ControlFlowInterfaces.lean b/Veir/Interfaces/ControlFlowInterfaces.lean index 492c9daf9..682a4abb9 100644 --- a/Veir/Interfaces/ControlFlowInterfaces.lean +++ b/Veir/Interfaces/ControlFlowInterfaces.lean @@ -41,13 +41,9 @@ def getSuccessorOperands? let opType := branchOp.getOpType! raw match opType with | .cf .br | .llvm .br | .riscv_cf .branch => - -- Unconditional branches have one successor and forward every operation operand. - if branchOp.getNumSuccessors! raw ≠ 1 || successorIndex ≠ 0 then - none - else - some { - forwardedOperands := branchOp.getOperands! raw - } + some { + forwardedOperands := branchOp.getOperands! raw + } | _ => do -- Determine whether this is a supported conditional branch and how many -- fixed operands appear before its successor operand segments. @@ -66,26 +62,11 @@ def getSuccessorOperands? -- Read the operand segment metadata from the operation's typed properties. let attrs := Properties.toAttrDict opType (branchOp.getProperties! raw opType) let some (.denseArrayAttr sizes) := attrs["operandSegmentSizes".toUTF8]? | none - let successorCount := branchOp.getNumSuccessors! raw let segmentSizes := sizes.values - -- Validate the requested successor and the basic shape of the segment metadata. - if successorIndex ≥ successorCount then - none - if segmentSizes.size ≠ fixedOperandCount + successorCount then - none - if segmentSizes.extract 0 fixedOperandCount |>.any (· ≠ 1) then - none - if segmentSizes.any (· < 0) then - none -- Select the segment corresponding to the requested successor. let segmentIndex := fixedOperandCount + successorIndex let forwardedCountRaw ← segmentSizes[segmentIndex]? let forwardedCount := forwardedCountRaw.toNat - let operandCount := branchOp.getNumOperands! raw - -- Ensure the segment metadata accounts for every operation operand. - let segmentSum := segmentSizes.foldl (init := 0) fun acc value => acc + value.toNat - if segmentSum ≠ operandCount then - none -- Compute the operation operand index where this successor's forwarded values begin. let forwardedStart := fixedOperandCount + (segmentSizes.extract fixedOperandCount segmentIndex).foldl From 598ba9c54f9403834de04b33eb8fe921c2347010 Mon Sep 17 00:00:00 2001 From: Axel Sorenson Date: Mon, 17 Aug 2026 14:20:05 -0600 Subject: [PATCH 3/5] TODO message --- Veir/Interfaces/ControlFlowInterfaces.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Veir/Interfaces/ControlFlowInterfaces.lean b/Veir/Interfaces/ControlFlowInterfaces.lean index 682a4abb9..191c2264d 100644 --- a/Veir/Interfaces/ControlFlowInterfaces.lean +++ b/Veir/Interfaces/ControlFlowInterfaces.lean @@ -59,6 +59,7 @@ def getSuccessorOperands? | .riscv_cf .bltu | .riscv_cf .bgeu => some 2 | _ => none + -- TODO: Move the operandSegmentSizes logic to the respective dialects -- Read the operand segment metadata from the operation's typed properties. let attrs := Properties.toAttrDict opType (branchOp.getProperties! raw opType) let some (.denseArrayAttr sizes) := attrs["operandSegmentSizes".toUTF8]? | none From 65d1e940a5f13ef125a2427fa4b5360bfa44094d Mon Sep 17 00:00:00 2001 From: Axel Sorenson Date: Mon, 17 Aug 2026 14:24:32 -0600 Subject: [PATCH 4/5] GetElem notation --- Veir/Interfaces/ControlFlowInterfaces.lean | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/Veir/Interfaces/ControlFlowInterfaces.lean b/Veir/Interfaces/ControlFlowInterfaces.lean index 191c2264d..8d9340b6b 100644 --- a/Veir/Interfaces/ControlFlowInterfaces.lean +++ b/Veir/Interfaces/ControlFlowInterfaces.lean @@ -19,16 +19,9 @@ structure SuccessorOperands where forwardedOperands : Array ValuePtr deriving Inhabited, Repr, DecidableEq -namespace SuccessorOperands - -/-- - Return the SSA value forwarded to a successor block argument. --/ -def getForwardedOperand? - (operands : SuccessorOperands) (blockArgumentIndex : Nat) : Option ValuePtr := - operands.forwardedOperands[blockArgumentIndex]? - -end SuccessorOperands +instance : GetElem SuccessorOperands Nat ValuePtr + (fun operands blockArgumentIndex => blockArgumentIndex < operands.forwardedOperands.size) where + getElem := fun operands blockArgumentIndex h => operands.forwardedOperands[blockArgumentIndex]'h namespace BranchOpInterface @@ -83,7 +76,7 @@ def getSuccessorOperand? (branchOp : OperationPtr) (successorIndex blockArgumentIndex : Nat) (raw : IRContext OpCode) : Option ValuePtr := getSuccessorOperands? branchOp successorIndex raw >>= fun operands => - operands.getForwardedOperand? blockArgumentIndex + operands[blockArgumentIndex]? end BranchOpInterface From c11cbb56f28bd9ab1eddffa6a187680fa4da6dc9 Mon Sep 17 00:00:00 2001 From: Axel Sorenson Date: Tue, 18 Aug 2026 14:54:30 -0600 Subject: [PATCH 5/5] GetElem? notation --- Veir/Interfaces/ControlFlowInterfaces.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Veir/Interfaces/ControlFlowInterfaces.lean b/Veir/Interfaces/ControlFlowInterfaces.lean index 8d9340b6b..05927d38d 100644 --- a/Veir/Interfaces/ControlFlowInterfaces.lean +++ b/Veir/Interfaces/ControlFlowInterfaces.lean @@ -23,6 +23,10 @@ instance : GetElem SuccessorOperands Nat ValuePtr (fun operands blockArgumentIndex => blockArgumentIndex < operands.forwardedOperands.size) where getElem := fun operands blockArgumentIndex h => operands.forwardedOperands[blockArgumentIndex]'h +instance : GetElem? SuccessorOperands Nat ValuePtr + (fun operands blockArgumentIndex => blockArgumentIndex < operands.forwardedOperands.size) where + getElem? := fun operands blockArgumentIndex => operands.forwardedOperands[blockArgumentIndex]? + namespace BranchOpInterface /--