Skip to content

feat(veir): make eraseOp keep going, if it makes more things dead#1082

Draft
regehr wants to merge 8 commits into
mainfrom
regehr/eraseOp-recursive
Draft

feat(veir): make eraseOp keep going, if it makes more things dead#1082
regehr wants to merge 8 commits into
mainfrom
regehr/eraseOp-recursive

Conversation

@regehr

@regehr regehr commented Jul 15, 2026

Copy link
Copy Markdown
Collaborator

the annoying thing here is how many tests it affects, but I think this is a good change. what we want is to not need to constantly run DCE, but rather only after we unavoidably create dead code.

@regehr regehr self-assigned this Jul 15, 2026

@github-actions github-actions Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

VeIR Benchmarks

Details
Benchmark suite Current: 3923bc1 Previous: f70c398 Ratio
add-fold-worklist/create 1876000 ns (± 48716) 1698500 ns (± 144734) 1.10
add-fold-worklist/rewrite 3656000 ns (± 36383) 2807500 ns (± 36099) 1.30
add-fold-worklist-local/create 1930000 ns (± 94840) 1708000 ns (± 122459) 1.13
add-fold-worklist-local/rewrite 4581000 ns (± 61638) 2676500 ns (± 103155) 1.71
add-zero-worklist/create 1943000 ns (± 62500) 1600000 ns (± 51203) 1.21
add-zero-worklist/rewrite 2743000 ns (± 25636) 1771000 ns (± 42318) 1.55
add-zero-reuse-worklist/create 1612000 ns (± 35394) 1367000 ns (± 106897) 1.18
add-zero-reuse-worklist/rewrite 2383000 ns (± 28752) 1473500 ns (± 32862) 1.62
mul-two-worklist/create 1912000 ns (± 88330) 1626000 ns (± 145372) 1.18
mul-two-worklist/rewrite 5412000 ns (± 116478) 3942000 ns (± 52162) 1.37
add-fold-forwards/create 1970000 ns (± 84509) 1717000 ns (± 94946) 1.15
add-fold-forwards/rewrite 2650000 ns (± 9602) 2065000 ns (± 32473) 1.28
add-zero-forwards/create 1917000 ns (± 94318) 1693000 ns (± 150829) 1.13
add-zero-forwards/rewrite 1727000 ns (± 17478) 1358500 ns (± 23875) 1.27
add-zero-reuse-forwards/create 1580000 ns (± 74742) 1362000 ns (± 124332) 1.16
add-zero-reuse-forwards/rewrite 1370000 ns (± 15434) 1090000 ns (± 34043) 1.26
mul-two-forwards/create 1883000 ns (± 35422) 1670500 ns (± 118430) 1.13
mul-two-forwards/rewrite 3203000 ns (± 41476) 2493000 ns (± 69745) 1.28
add-zero-reuse-first/create 1577000 ns (± 65793) 1448000 ns (± 110815) 1.09
add-zero-reuse-first/rewrite 9000 ns (± 2501) 8000 ns (± 1840) 1.13
add-zero-lots-of-reuse-first/create 1589000 ns (± 51892) 1412000 ns (± 113104) 1.13
add-zero-lots-of-reuse-first/rewrite 761000 ns (± 33650) 589500 ns (± 15398) 1.29

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

@math-fehr math-fehr left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! I added a few style/organization comments, but otherwise all good!

Comment thread Veir/IR/Basic.lean Outdated
Comment thread Veir/IR/OpInfo.lean Outdated
Comment on lines +240 to +252
let ctx := rewriter.ctx.raw
-- Ops defining this op's operands may become dead or newly canonicalizable
-- once the uses from `op` disappear; re-enqueue those with at most one
-- remaining user, mirroring MLIR's `addOperandsToWorklist`.
let mut worklist := rewriter.worklist.remove op
for operand in op.getOperands ctx hOp do
let some defOp := operand.getDefiningOp! ctx | continue
if useChainHasAtMostOneUserBesides ctx (operand.getFirstUse! ctx) op none 1_000_000_000 then
worklist := worklist.push defOp
return { rewriter with
ctx := WfRewriter.eraseOp rewriter.ctx op opRegions opUses hOp,
hasDoneAction := true,
worklist := rewriter.worklist.remove op,
worklist

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you know the reason why we first walk the op operands, then we erase the operation?
Compared to first erasing the operation, then checking if some of the values are unused at that point?
That would make this code simpler

Comment on lines +260 to +269
if hOp : op.InBounds rewriter.ctx.raw then
if opRegions : op.getNumRegions! rewriter.ctx.raw = 0 then
if opUses : !op.hasUses! rewriter.ctx.raw then
rewriter.eraseOp op opRegions opUses hOp
else
panic! "PatternRewriter.eraseOp! failed: operation has uses"
else
panic! "PatternRewriter.eraseOp! failed: operation has regions"
else
panic! "PatternRewriter.eraseOp! failed: operation is out of bounds"

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the reason of changing this?
I would agree that I prefer this version (and same for all the other ops here), but I don't understand why you need this change

Comment on lines +416 to +418
if hdead : op.getNumRegions! rewriter.ctx.raw = 0
∧ !op.hasUses! rewriter.ctx.raw
∧ !op.hasSideEffects rewriter.ctx.raw then

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should you add a isTriviallyDead function (that you could put in Interface/ as well) for this?
This would also help me a lot since proving deletion of a isTriviallyDead operation would be a helper function.

@regehr
regehr marked this pull request as draft July 15, 2026 19:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants