Dominance Analysis - #133
Conversation
|
I am currently working on implementing a dominance tree data structure that closely mirrors with the one defined in LLVM: https://github.com/llvm/llvm-project/blob/main/llvm/include/llvm/Support/GenericDomTree.h |
85e953d to
156344b
Compare
axelcool1234
changed the title
ineol
left a comment
ineol
left a comment
There was a problem hiding this comment.
Thank you!
Maybe we should consider splitting the dominance tree off of the PR to keep it manageable?
I definitely will. I also intend on cleaning up all of these commits because they're a mess. I've been under the weather lately - I was planning on splitting up the PR a couple days ago. I'll get to it soon. Also, thanks for the comments. This'll help me write better Lean code :) |
axelcool1234
changed the title
I just split my work into two PRs. This one now only contains the Dominance Tree. #264 contains the Dataflow Analysis Framework now. |
|
Hi @axelcool1234, can you rebase this PR on main? We'd like to start merging it soon :) |
Ah shoot, sorry about that! I'll get on that |
898562b to
d9ad389
Compare
a4b0a35 to
f77b21c
Compare
ineol
left a comment
ineol
left a comment
There was a problem hiding this comment.
Thank you for rebasing!
I made a superficial review of the style, I haven't looked at the correctness yet.
Could you write a high level explanation of the algorithm/abstract domains etc at the beginning of DominanceAnalysis.lean?
d75db64 to
5d7c15a
Compare
math-fehr
left a comment
math-fehr
left a comment
There was a problem hiding this comment.
Nice! I added some comments, but the design seems good otherwise.
In the tests, can you add one where there is a block that is "disconnected" from any other block. So a block that doesn't have any predecessor. Similarly, a group of blocks that are not dominated by the entry block, because there is no path to them.
Otherwise, I think we should only have the "analysis" part in DominanceAnalysis, and move some of the useful API outside of it in a IR/Dominance.lean file. So you would still need to use the dominance analysis, but the public API functions would be stored there to clearly separate what is useful for computing the analysis, versus what is useful for querying which block dominates which block.
Finally, your notion of dominance does not take into account dominance between regions. Do you know if MLIR uses any other data structure to compute that, and if so, can these be added on top of these ones in the future, or are they incompatible?
| (irCtx : IRContext OpCode) : Option BlockPtr := | ||
| block.getDominatorFact? dfCtx irCtx >>= (·.iDom) | ||
|
|
||
| def getDoms? [FactSpec .dominator] (block : BlockPtr) (dfCtx : DataFlowContext) |
There was a problem hiding this comment.
This function is not used anywhere, can you add a test for it?
There was a problem hiding this comment.
Is it only meant for testing / debugging?
There was a problem hiding this comment.
It'll be used internally by a useful API that Mathieu said should be written in IR/Dominance.lean
There was a problem hiding this comment.
Actually I'll probably move that function to IR/Dominance.lean tonight.
There was a problem hiding this comment.
at present there are some calls to this function from UnitTest/DataFlowFramework/Dominance.lean so I think this is fine?
I don't have an actual use case for this function in mind, but it seems like something that someone might want at some point, and it's less than 15 lines of code, so I'd suggest that we keep it
| let next := dom.getIDom? dfCtx irCtx | ||
| if next = some dom then | ||
| return doms |
There was a problem hiding this comment.
This can be simplified by:
let some next := dom.getIDom? dfCtx irCtx | return doms
There was a problem hiding this comment.
I actually think this would be wrong. I'm checking if the current block, assigned to dom via current.get! is equal to next. I should remove some from if next = some dom though because Lean will coerce, I believe.
There was a problem hiding this comment.
meanwhile claude believes it can be replaced by this
current := (dom.getIDom? dfCtx irCtx).filter (· ≠ dom)
There was a problem hiding this comment.
Sorry, my bad, let's keep it as it is (I find this more readable than the claude version).
There was a problem hiding this comment.
Sorry, my bad, let's keep it as it is (I find this more readable than the claude version).
No worries, the tests didn't use it at first and I changed that. Also I think the claude version is wrong too
5e678a4 to
ca399d0
Compare
ineol
left a comment
ineol
left a comment
There was a problem hiding this comment.
It's starting to look good!
| (irCtx : IRContext OpCode) : Option BlockPtr := | ||
| block.getDominatorFact? dfCtx irCtx >>= (·.iDom) | ||
|
|
||
| def getDoms? [FactSpec .dominator] (block : BlockPtr) (dfCtx : DataFlowContext) |
There was a problem hiding this comment.
Is it only meant for testing / debugging?
|
Thanks @regehr. I'll cover everything else within the next couple hours. |
ba19179 to
4a9b490
Compare
math-fehr
left a comment
math-fehr
left a comment
There was a problem hiding this comment.
Thanks! I think there is just a few functions that need more documentation, but otherwise that's good to me!
Adds FELT_PARITY_ASSESSMENT_2026-05-28.md and demotes plan.md's Felt status row from ✅ to⚠️ so the gap is loudly visible. The assessment answers two scoping questions surfaced this session: 1. **How much more work for "Felt is ported"?** ~12-15 engineer-days, structured as Field registry → verifier checks → modular-reduction in folds → 11 missing folders → NotFieldNative gating → custom assembly format (optional). Soundness is OK today; alignment with LLZK's canonical form is not. 2. **What for replacing the C++ implementation?** Drop-in replacement is 30-60+ engineer-months. Realistic alternative is Strategy A (verified-output oracle, 2-4 mo, we already have 80%) or Strategy E (proof-certificate generator inside llzk-opt, 6-10 mo). Detail in the assessment file covers: the per-feature gap list with file:line anchors, downstream consumer survey of llzk-lib/, the ranked strategy table, recommended next steps for both the port track and the replacement track, highest-risk unknowns, and the "$1000 bet against" scenario list. Driven by two fresh audit agents: - Source-level C++ ↔ Lean gap audit (18 ops, 2 types, 2 attrs, 6 traits, OpInterfaces, folders, verifier, custom asm, tests) - Replacement-feasibility analysis (CLI/CAPI/Python/sibling dialects/passes/analyses/backends) Also flags in plan.md that upstream/main is 37 commits ahead since our last merge — notably Dominance Analysis (opencompl#133), CSE (opencompl#610), WfRewriter.replaceValue API change (opencompl#637), DCE fix (opencompl#649), toolchain bump nightly-2026-05-27 (opencompl#652) that will conflict with our v4.30.0-rc2 Mathlib pin. Not blocking the Felt parity work, but should be absorbed before the next phase boundary. Build/test state unchanged: lake 2563 jobs, lit 356 PASS / 1 UNSUPPORTED / 0 XFAIL / 0 FAIL with LLZK_OPT. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
4 participants
This implements CFG dominance analysis on top of the dataflow framework: #264
This is based off of the Cooper-Harvey-Kennedy algorithm.