feat(Rewriter): introduce eraseOp!/replaceValue! and clear remaining pass sorries#968
Open
tobiasgrosser wants to merge 6 commits into
Open
feat(Rewriter): introduce eraseOp!/replaceValue! and clear remaining pass sorries#968tobiasgrosser wants to merge 6 commits into
tobiasgrosser wants to merge 6 commits into
Conversation
Converts the directly-convertible createOp/replaceOp call sites in Common.lean, RISCV64Sdag.lean, InstCombine.lean, Canonicalize.lean, ModArithToArith.lean, and MIRCombinesVeir.lean to the panicking `!` variants, dropping their sorry-filled proof obligations. Common.lean, RISCV64Sdag.lean, and Canonicalize.lean are now fully sorry-free; the other three still carry sorries from replaceValue/eraseOp, which don't have `!` variants yet.
…pass sorries Adds PatternRewriter.eraseOp! and .replaceValue!, mechanical panicking wrappers over the existing WfRewriter.eraseOp!/replaceValue!. Uses them (plus the earlier createOp!/replaceOp!) to clear the remaining sorries in InstCombine, ModArithToArith, MIRCombinesVeir, CastsReconciliation, DCE, RISCVCombines/Combine, and CSE (which calls WfRewriter directly). RISCV64Branches.lean is intentionally left untouched: its let-else fallbacks around these calls are a genuine graceful-skip path rather than an always-true proof obligation, so converting to `!` would silently turn skips into panics.
Rename unused opInBounds/cast/lhs bindings to _ across the passes touched by the createOp!/replaceOp!/eraseOp!/replaceValue! conversion. The whole project now builds with zero warnings.
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
VeIR Benchmarks
Details
| Benchmark suite | Current: 1c5ca1e | Previous: b8265aa | Ratio |
|---|---|---|---|
add-fold-worklist/create |
2138000 ns (± 28190) |
2434000 ns (± 160814) |
0.88 |
add-fold-worklist/rewrite |
3358000 ns (± 22165) |
3947500 ns (± 56105) |
0.85 |
add-fold-worklist-local/create |
2146000 ns (± 106347) |
2386000 ns (± 117421) |
0.90 |
add-fold-worklist-local/rewrite |
2901000 ns (± 146305) |
3322500 ns (± 19159) |
0.87 |
add-zero-worklist/create |
2129000 ns (± 16799) |
2406000 ns (± 109136) |
0.88 |
add-zero-worklist/rewrite |
2242000 ns (± 13145) |
2501000 ns (± 29385) |
0.90 |
add-zero-reuse-worklist/create |
1754000 ns (± 46382) |
2069000 ns (± 69158) |
0.85 |
add-zero-reuse-worklist/rewrite |
1888000 ns (± 55911) |
2093000 ns (± 17355) |
0.90 |
mul-two-worklist/create |
2134000 ns (± 18055) |
2233000 ns (± 45758) |
0.96 |
mul-two-worklist/rewrite |
4879000 ns (± 25401) |
5578000 ns (± 83143) |
0.87 |
add-fold-forwards/create |
2143000 ns (± 37785) |
2254000 ns (± 34802) |
0.95 |
add-fold-forwards/rewrite |
2649000 ns (± 31124) |
2977000 ns (± 15110) |
0.89 |
add-zero-forwards/create |
2121500 ns (± 119864) |
2289000 ns (± 70319) |
0.93 |
add-zero-forwards/rewrite |
1771000 ns (± 112162) |
1951000 ns (± 10968) |
0.91 |
add-zero-reuse-forwards/create |
1764000 ns (± 31228) |
1916000 ns (± 120621) |
0.92 |
add-zero-reuse-forwards/rewrite |
1431000 ns (± 15540) |
1551000 ns (± 35552) |
0.92 |
mul-two-forwards/create |
2151500 ns (± 108004) |
2356000 ns (± 73814) |
0.91 |
mul-two-forwards/rewrite |
3193500 ns (± 144348) |
3575000 ns (± 63979) |
0.89 |
add-zero-reuse-first/create |
1728000 ns (± 23884) |
1906500 ns (± 78414) |
0.91 |
add-zero-reuse-first/rewrite |
10000 ns (± 1832) |
8000 ns (± 2040) |
1.25 |
add-zero-lots-of-reuse-first/create |
1740000 ns (± 44831) |
1819000 ns (± 82223) |
0.96 |
add-zero-lots-of-reuse-first/rewrite |
768000 ns (± 14188) |
783000 ns (± 27096) |
0.98 |
This comment was automatically generated by workflow using github-action-benchmark.
Collaborator
I disagree with this, we should also convert the ones in |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
PatternRewriter.eraseOp!and.replaceValue!, mechanical panicking wrappers over the existingWfRewriter.eraseOp!/replaceValue!.createOp!/replaceOp!) to clear the remaining sorries inInstCombine,ModArithToArith,MIRCombinesVeir,CastsReconciliation,DCE,RISCVCombines/Combine, andCSE(which callsWfRewriterdirectly).RISCV64Branches.leanis intentionally left untouched: itslet some x := ... | return cfallbacks around these calls are a genuine graceful-skip path rather than an always-true proof obligation, so converting to!would silently turn skips into panics.