feat(dataflow): use WfIRContext

UnitTest/DataFlowFramework/DeadCodeAnalysis.lean

@@ -6,8 +6,8 @@ open Veir
 
 -- TODO: Facts not initialized in the Dataflow Analysis Framework are implicitly assumed to be the pessimistic bottom state.
 -- We should not assume this implicitly, but rather encode this in the framework!!!!
-def isBlockLive (dfCtx : DataFlowContext) (block : BlockPtr) (irCtx : IRContext OpCode) : Bool :=
-  match dfCtx.getFact? .liveness (.InsertPoint (InsertPoint.atStart! block irCtx)) with
+def isBlockLive (dfCtx : DataFlowContext) (block : BlockPtr) (irCtx : WfIRContext OpCode) : Bool :=
+  match dfCtx.getFact? .liveness (.InsertPoint (InsertPoint.atStart! block irCtx.raw)) with
   | some fact => fact.live
   | none => false
 
@@ -18,7 +18,7 @@ def isEdgeLive (dfCtx : DataFlowContext) (src dst : BlockPtr) : Bool :=
 
 def checkNamedBlockLiveness
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode)
+    (irCtx : WfIRContext OpCode)
     (blockMap : HashMap String BlockPtr)
     (expected : Array (String × Bool)) : MismatchReport := Id.run do
   let mut report := #[]

UnitTest/DataFlowFramework/Dominance.lean

@@ -31,7 +31,7 @@ private def compareExpectedDominator
     (recovered : RecoveredNames)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let some expectedBlock := recovered.blocks[expectedDom]?
     | return #[s!"dominators {expected.name}: missing block label {expectedDom}"]
   let shouldProperlyDom := expectedDom ≠ expected.name
@@ -55,7 +55,7 @@ private def compareObservedDominator
     (observedBlock : BlockPtr)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let observedByRelation := observedBlock.dominates block dfCtx irCtx
   let observedProperly := observedBlock.properlyDominates block dfCtx irCtx
   let mut report := #[]
@@ -76,7 +76,7 @@ private def compareImmediateDominator
     (recovered : RecoveredNames)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let some block := recovered.blocks[expected.name]?
     | return #[s!"idom {expected.name}: missing block label"]
   let some observedIDom := block.immediateDominator? dfCtx irCtx
@@ -102,7 +102,7 @@ private def compareReachableDominators
     (recovered : RecoveredNames)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let mut report := #[]
   for expectedDom in expected.doms.toArray do
     report := report ++ compareExpectedDominator
@@ -123,7 +123,7 @@ private def compareDominators
     (recovered : RecoveredNames)
     (expected : ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let some block := recovered.blocks[expected.name]?
     | return #[s!"dominators {expected.name}: missing block label"]
   let observedFact? := block.getDominatorFact? dfCtx irCtx
@@ -145,7 +145,7 @@ private def compareNamedDominators
     (recovered : RecoveredNames)
     (expectations : Array ExpectedBlockDominators)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let mut report := #[]
   for expected in expectations do
     report := report ++ compareDominators recovered expected dfCtx irCtx
@@ -156,9 +156,9 @@ private def compareNamedDominators
 private def getNamedOperation?
     (recovered : RecoveredNames)
     (name : String)
-    (irCtx : IRContext OpCode) : Option OperationPtr := do
+    (irCtx : WfIRContext OpCode) : Option OperationPtr := do
   let value ← recovered.values[name]?
-  value.getDefiningOp! irCtx
+  value.getDefiningOp! irCtx.raw
 
 /--
 Compare one expected operation dominance relation.
@@ -167,7 +167,7 @@ private def compareOperationDominance
     (recovered : RecoveredNames)
     (expected : ExpectedOperationDominance)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let some dominator := getNamedOperation? recovered expected.dominator irCtx
     | return #[s!"op dominance {expected.dominator}->{expected.dominated}: missing dominator"]
   let some dominated := getNamedOperation? recovered expected.dominated irCtx
@@ -195,7 +195,7 @@ private def compareNamedOperationDominance
     (recovered : RecoveredNames)
     (expectations : Array ExpectedOperationDominance)
     (dfCtx : DataFlowContext)
-    (irCtx : IRContext OpCode) : MismatchReport := Id.run do
+    (irCtx : WfIRContext OpCode) : MismatchReport := Id.run do
   let mut report := #[]
   for expected in expectations do
     report := report ++ compareOperationDominance recovered expected dfCtx irCtx

UnitTest/DataFlowFramework/Helpers.lean

@@ -77,19 +77,19 @@ Collect all blocks reachable by recursively traversing nested regions in source
 -/
 partial def collectBlocksInSourceOrder
     (op : OperationPtr)
-    (irCtx : IRContext OpCode)
+    (irCtx : WfIRContext OpCode)
     (acc : Array BlockPtr := #[]) : Array BlockPtr := Id.run do
   let mut acc := acc
-  for region in (op.get! irCtx).regions do
-    let region := region.get! irCtx
+  for region in (op.get! irCtx.raw).regions do
+    let region := region.get! irCtx.raw
     let mut currentBlock := region.firstBlock
     while let some block := currentBlock do
       acc := acc.push block
-      let mut currentOp := (block.get! irCtx).firstOp
+      let mut currentOp := (block.get! irCtx.raw).firstOp
       while let some nestedOp := currentOp do
         acc := collectBlocksInSourceOrder nestedOp irCtx acc
-        currentOp := (nestedOp.get! irCtx).next
-      currentBlock := (block.get! irCtx).next
+        currentOp := (nestedOp.get! irCtx.raw).next
+      currentBlock := (block.get! irCtx.raw).next
   acc
 
 /--
@@ -99,22 +99,22 @@ operation results inside each region.
 -/
 partial def collectValuesInSourceOrder
     (top : OperationPtr)
-    (irCtx : IRContext OpCode)
+    (irCtx : WfIRContext OpCode)
     (acc : Array ValuePtr := #[]) : Array ValuePtr := Id.run do
   let mut acc := acc
-  for result in top.getResults! irCtx do
+  for result in top.getResults! irCtx.raw do
     acc := acc.push result
-  for region in (top.get! irCtx).regions do
-    let region := region.get! irCtx
+  for region in (top.get! irCtx.raw).regions do
+    let region := region.get! irCtx.raw
     let mut currentBlock := region.firstBlock
     while let some block := currentBlock do
-      for arg in block.getArguments! irCtx do
+      for arg in block.getArguments! irCtx.raw do
         acc := acc.push arg
-      let mut currentOp := (block.get! irCtx).firstOp
+      let mut currentOp := (block.get! irCtx.raw).firstOp
       while let some nestedOp := currentOp do
         acc := collectValuesInSourceOrder nestedOp irCtx acc
-        currentOp := (nestedOp.get! irCtx).next
-      currentBlock := (block.get! irCtx).next
+        currentOp := (nestedOp.get! irCtx.raw).next
+      currentBlock := (block.get! irCtx.raw).next
   acc
 
 /--
@@ -129,7 +129,7 @@ Recover block and SSA value maps by pairing MLIR source names with IR traversal
 -/
 def recoverNames
     (top : OperationPtr)
-    (irCtx : IRContext OpCode)
+    (irCtx : WfIRContext OpCode)
     (mlir : String) : Except String RecoveredNames := do
   let blockLabels := blockLabelsFromMlir mlir
   let blocks := collectBlocksInSourceOrder top irCtx