feat: Add lemmas about setArgumentValues? and the equation lemmas#1076
Open
math-fehr wants to merge 1 commit into
Open
feat: Add lemmas about setArgumentValues? and the equation lemmas#1076math-fehr wants to merge 1 commit into
setArgumentValues? and the equation lemmas#1076math-fehr wants to merge 1 commit into
Conversation
math-fehr
requested review from
ineol,
luisacicolini,
nchappe,
regehr and
tobiasgrosser
math-fehr
force-pushed
the
math-fehr/setarguments-lemmas
branch
from
e672978 to
dd5db4a
Compare
![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: b56e8e2 | Previous: 355e817 | Ratio |
|---|---|---|---|
add-fold-worklist/create |
2270000 ns (± 69697) |
2181000 ns (± 99961) |
1.04 |
add-fold-worklist/rewrite |
3919000 ns (± 53491) |
3981000 ns (± 100718) |
0.98 |
add-fold-worklist-local/create |
2294500 ns (± 134169) |
2210000 ns (± 52837) |
1.04 |
add-fold-worklist-local/rewrite |
3693000 ns (± 49797) |
3801000 ns (± 56650) |
0.97 |
add-zero-worklist/create |
2293000 ns (± 87892) |
2236000 ns (± 93138) |
1.03 |
add-zero-worklist/rewrite |
2519000 ns (± 17254) |
2480000 ns (± 38030) |
1.02 |
add-zero-reuse-worklist/create |
1957500 ns (± 138865) |
1883000 ns (± 77092) |
1.04 |
add-zero-reuse-worklist/rewrite |
2104000 ns (± 44020) |
2118000 ns (± 40784) |
0.99 |
mul-two-worklist/create |
2233000 ns (± 70489) |
2234000 ns (± 81889) |
1.00 |
mul-two-worklist/rewrite |
5547000 ns (± 231310) |
5646000 ns (± 65002) |
0.98 |
add-fold-forwards/create |
2250000 ns (± 111616) |
2275000 ns (± 85850) |
0.99 |
add-fold-forwards/rewrite |
3030000 ns (± 39564) |
3045000 ns (± 29685) |
1.00 |
add-zero-forwards/create |
2381000 ns (± 60326) |
2304500 ns (± 122926) |
1.03 |
add-zero-forwards/rewrite |
1937000 ns (± 20744) |
1969000 ns (± 28336) |
0.98 |
add-zero-reuse-forwards/create |
1922000 ns (± 101541) |
1915000 ns (± 56589) |
1.00 |
add-zero-reuse-forwards/rewrite |
1537500 ns (± 28929) |
1555000 ns (± 16254) |
0.99 |
mul-two-forwards/create |
2271000 ns (± 101205) |
2197000 ns (± 86947) |
1.03 |
mul-two-forwards/rewrite |
3640000 ns (± 71546) |
3766000 ns (± 52462) |
0.97 |
add-zero-reuse-first/create |
1873000 ns (± 70773) |
1889000 ns (± 104414) |
0.99 |
add-zero-reuse-first/rewrite |
8000 ns (± 0) |
9000 ns (± 2164) |
0.89 |
add-zero-lots-of-reuse-first/create |
1916000 ns (± 105386) |
1874000 ns (± 68697) |
1.02 |
add-zero-lots-of-reuse-first/rewrite |
782000 ns (± 20401) |
797000 ns (± 35724) |
0.98 |
This comment was automatically generated by workflow using github-action-benchmark.
| (hMem : value ∈ block.getArguments! ctx.raw) : | ||
| value.dominatesIp (InsertPoint.atStart! block ctx.raw) ctx | ||
|
|
||
| /-- An argument of a block cannot dominate a program point that dominates hde block start. -/ |
Collaborator
There was a problem hiding this comment.
Suggested change
| /-- An argument of a block cannot dominate a program point that dominates hde block start. -/ | |
| /-- An argument of a block cannot dominate a program point that dominates the block start. -/ |
These lemmas are similar to the ones about `setResultValues` in that they show preservation of `EquationLemmaAt` and `DefinesDominating`. These required additional simple lemmas, and additional axioms about dominance.
math-fehr
force-pushed
the
math-fehr/setarguments-lemmas
branch
from
dd5db4a to
b56e8e2
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
2 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.
These lemmas are similar to the ones about
setResultValuesin that they show preservation ofEquationLemmaAtandDefinesDominating.These required additional simple lemmas, and additional axioms about dominance.