feat(dominance): Define operation and block dominance

[math-fehr]

These definitions follow compcertssa definition of dominance (https://compcertssa.gitlabpages.inria.fr/html/compcert.midend.Dom.html) but extended for MLIR's hierarchical dominance.

This PR only contains the definitions, and do not replace yet the axiom in Dominance.lean, nor introduce lemmas about it.

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: a08b254	Previous: db25ec0	Ratio
add-fold-worklist/create	1918000 ns (± 67862)	2260000 ns (± 56688)	0.85
add-fold-worklist/rewrite	3625000 ns (± 50688)	4143000 ns (± 51711)	0.87
add-fold-worklist-local/create	1905000 ns (± 78159)	2293000 ns (± 69305)	0.83
add-fold-worklist-local/rewrite	3481000 ns (± 70361)	3887000 ns (± 121689)	0.90
add-zero-worklist/create	1865000 ns (± 94220)	2313000 ns (± 55361)	0.81
add-zero-worklist/rewrite	2397000 ns (± 39771)	2745000 ns (± 134157)	0.87
add-zero-reuse-worklist/create	1572000 ns (± 23734)	1902000 ns (± 78564)	0.83
add-zero-reuse-worklist/rewrite	1977000 ns (± 13946)	2207000 ns (± 62062)	0.90
mul-two-worklist/create	1911000 ns (± 66125)	2327000 ns (± 52872)	0.82
mul-two-worklist/rewrite	5189000 ns (± 43397)	5844000 ns (± 139184)	0.89
add-fold-forwards/create	1887000 ns (± 15339)	2242000 ns (± 80631)	0.84
add-fold-forwards/rewrite	2674000 ns (± 44136)	3110000 ns (± 46279)	0.86
add-zero-forwards/create	1899000 ns (± 35374)	2231000 ns (± 38676)	0.85
add-zero-forwards/rewrite	1709000 ns (± 32760)	2030000 ns (± 29997)	0.84
add-zero-reuse-forwards/create	1570000 ns (± 77436)	1812000 ns (± 49099)	0.87
add-zero-reuse-forwards/rewrite	1390000 ns (± 22863)	1618000 ns (± 19652)	0.86
mul-two-forwards/create	1911000 ns (± 87701)	2255000 ns (± 75440)	0.85
mul-two-forwards/rewrite	3253000 ns (± 80500)	3800000 ns (± 63816)	0.86
add-zero-reuse-first/create	1567000 ns (± 29273)	1842000 ns (± 61369)	0.85
add-zero-reuse-first/rewrite	10000 ns (± 2047)	8000 ns (± 0)	1.25
add-zero-lots-of-reuse-first/create	1601000 ns (± 57138)	1855000 ns (± 80310)	0.86
add-zero-lots-of-reuse-first/rewrite	752000 ns (± 32538)	825000 ns (± 50738)	0.91

This comment was automatically generated by workflow using github-action-benchmark.

[luisacicolini]

lgtm but I don't have enough context knowledge to have an opinion about the definitions themselves.

[ineol]

Looks like sound defs to me!

[ineol]

is it necessary? I would have thought that since region.hasSSADominance = false implies a single block, dominatorBlock.ProperlyDominates dominatedBlock implies region.hasSSADominance = true

[math-fehr]

So this is the case only if we have ctx.Verified. I felt that it was more precise with this definition, but I'm fine changing it to the definition where we have ctx.Verified.
In all case, I want these definitions to be entirely opaque, so that lemmas would be the one exposing these things.
Let me know if you prefer the ctx.Verified definition.

[regehr]

I'm not sure about proper dominance in graph regions.

MLIR contrains this code in Dominance.cpp:

template <bool IsPostDom>
bool DominanceInfoBase<IsPostDom>::properlyDominatesImpl(
    Block *aBlock, Block::iterator aIt, Block *bBlock, Block::iterator bIt,
    bool enclosingOk) const {
  assert(aBlock && bBlock && "expected non-null blocks");

  // A block iterator (post)dominates, but does not properly (post)dominate,                                  
  // itself unless this is a graph region.                                                                    
  if (aBlock == bBlock && aIt == bIt)
    return !hasSSADominance(aBlock);

doesn't this make it return true for the reflexive, graph region case, whereas your code returns false?

[regehr]

also maybe remove comments about strict dominance since MLIR seems to only talk about proper dominance

[math-fehr]

doesn't this make it return true for the reflexive, graph region case, whereas your code returns false?

Ohhh, I'm going to take a bit trying to understand that, I probably have misunderstood what proper dominance is, and I think I'll go read more info about it, thanks a lot for spotting it!
Probably proper dominance is not just dominance and different for graph regions then, and is something more subtle!

[regehr]

Ohhh, I'm going to take a bit trying to understand that, I probably have misunderstood what proper dominance is, and I think I'll go read more info about it, thanks a lot for spotting it! Probably proper dominance is not just dominance and different for graph regions then, and is something more subtle!

I'm not clear on why MLIR made this choice, though

[regehr]

besides the one thing, LGTM!

[math-fehr]

@ineol, is there a way to have both a name for the argument enclosingOk, while still defining the argument as an index rather than a parameter (meaning the Ancestor case would specify enclosingOk as true, which should simplify casing?)

[ineol]

did you try

inductive BlockPtr.ProperlyDominates ... : (enclosingOk : Bool) → Prop

or did I misunderstand your question?

[regehr]

this LGTM!