[WIP] progress on rewrite lifting#866
Draft
math-fehr wants to merge 31 commits into
Draft
Conversation
![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: f9991b8 | Previous: 0279d19 | Ratio |
|---|---|---|---|
add-fold-worklist/create |
2139000 ns (± 92614) |
1856000 ns (± 92425) |
1.15 |
add-fold-worklist/rewrite |
4068000 ns (± 73918) |
3608000 ns (± 49764) |
1.13 |
add-fold-worklist-local/create |
2246000 ns (± 35654) |
1836000 ns (± 90886) |
1.22 |
add-fold-worklist-local/rewrite |
9471000 ns (± 104880) |
2978000 ns (± 150037) |
3.18 |
add-zero-worklist/create |
2231000 ns (± 92534) |
1840500 ns (± 314471) |
1.21 |
add-zero-worklist/rewrite |
2633000 ns (± 118366) |
2314000 ns (± 294926) |
1.14 |
add-zero-reuse-worklist/create |
1880000 ns (± 126056) |
1536000 ns (± 28249) |
1.22 |
add-zero-reuse-worklist/rewrite |
2183000 ns (± 94152) |
1881000 ns (± 32407) |
1.16 |
mul-two-worklist/create |
2269000 ns (± 88874) |
1848000 ns (± 91490) |
1.23 |
mul-two-worklist/rewrite |
5772000 ns (± 59703) |
5035000 ns (± 89461) |
1.15 |
add-fold-forwards/create |
2253000 ns (± 112506) |
1836000 ns (± 68325) |
1.23 |
add-fold-forwards/rewrite |
3026000 ns (± 74014) |
2759000 ns (± 71360) |
1.10 |
add-zero-forwards/create |
2276000 ns (± 82957) |
1839500 ns (± 93335) |
1.24 |
add-zero-forwards/rewrite |
2044000 ns (± 49176) |
1792500 ns (± 23861) |
1.14 |
add-zero-reuse-forwards/create |
1906000 ns (± 117331) |
1544000 ns (± 19799) |
1.23 |
add-zero-reuse-forwards/rewrite |
1590500 ns (± 41212) |
1403000 ns (± 9633) |
1.13 |
mul-two-forwards/create |
2274000 ns (± 134952) |
1846000 ns (± 77894) |
1.23 |
mul-two-forwards/rewrite |
3796000 ns (± 132053) |
3292000 ns (± 54962) |
1.15 |
add-zero-reuse-first/create |
1948000 ns (± 93709) |
1549500 ns (± 48362) |
1.26 |
add-zero-reuse-first/rewrite |
9000 ns (± 1614) |
10000 ns (± 1776) |
0.90 |
add-zero-lots-of-reuse-first/create |
1943500 ns (± 134602) |
1532000 ns (± 69515) |
1.27 |
add-zero-lots-of-reuse-first/rewrite |
831500 ns (± 72238) |
797000 ns (± 34179) |
1.04 |
This comment was automatically generated by workflow using github-action-benchmark.
math-fehr
force-pushed
the
math-fehr/wip-lifting-list
branch
28 times, most recently
from
cfce77f to
4b27368
Compare
math-fehr
force-pushed
the
math-fehr/wip-lifting-list
branch
from
4b27368 to
3bdb34f
Compare
…ds fields Add WithCreatedOps + eraseOp survival helpers (hSurviveOp/Block/Region) and use them to discharge the bounds-preservation fields of RewrittenAt.of_fromLocalRewrite. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add hOpBnd (bidirectional non-op bounds across the rewrite) to transport ReturnOps freshness; mappingFixesNonResults is the else-branch of rewriteMapping. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add hSurviveVal (value survival across folds + eraseOp when the value's owner is not op) and discharge mapNonResultsInBounds via getResults! membership. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Mark which fields need an extra pattern hypothesis (newValuesInBounds, mapResultsInBounds, newValuesAreResults, newCtxDom, newCtxVerif) vs deep operationList/GetSet plumbing through the foldlM (tgtList, otherBlocks, frame, parentOps, blockArgsPreserved, opRegionsPreserved, regionFirstBlockPreserved). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
math-fehr
force-pushed
the
math-fehr/wip-lifting-list
branch
from
4e366e3 to
d06bc74
Compare
math-fehr
force-pushed
the
math-fehr/wip-lifting-list
branch
from
2497ee7 to
dd42c0b
Compare
math-fehr
force-pushed
the
math-fehr/wip-lifting-list
branch
from
dd42c0b to
e8a1632
Compare
math-fehr
force-pushed
the
math-fehr/wip-lifting-list
branch
from
e8a1632 to
f45dc66
Compare
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
1 participant
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.
This is the current status of proving the lifting between the soundness of local rewrites to module refinements