feat(riscv): zext/sext/trunc proofs for legal types#898
Conversation
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
VeIR Benchmarks
Details
| Benchmark suite | Current: d7f9fec | Previous: f3e725d | Ratio |
|---|---|---|---|
add-fold-worklist/create |
2366000 ns (± 96707) |
2223500 ns (± 122225) |
1.06 |
add-fold-worklist/rewrite |
3887000 ns (± 176170) |
3965500 ns (± 89540) |
0.98 |
add-fold-worklist-local/create |
2225000 ns (± 110648) |
2288000 ns (± 111516) |
0.97 |
add-fold-worklist-local/rewrite |
3337500 ns (± 81933) |
3292000 ns (± 25338) |
1.01 |
add-zero-worklist/create |
2328500 ns (± 638934) |
2255000 ns (± 66342) |
1.03 |
add-zero-worklist/rewrite |
2517500 ns (± 614424) |
2519000 ns (± 63834) |
1.00 |
add-zero-reuse-worklist/create |
1921000 ns (± 36780) |
1863500 ns (± 92562) |
1.03 |
add-zero-reuse-worklist/rewrite |
2122000 ns (± 56325) |
2113500 ns (± 72069) |
1.00 |
mul-two-worklist/create |
2309500 ns (± 148167) |
2206000 ns (± 51266) |
1.05 |
mul-two-worklist/rewrite |
5567000 ns (± 76174) |
5691000 ns (± 99052) |
0.98 |
add-fold-forwards/create |
2378000 ns (± 44145) |
2280000 ns (± 105405) |
1.04 |
add-fold-forwards/rewrite |
2990000 ns (± 39896) |
2994000 ns (± 28711) |
1.00 |
add-zero-forwards/create |
2276000 ns (± 104856) |
2200000 ns (± 54875) |
1.03 |
add-zero-forwards/rewrite |
1920000 ns (± 50362) |
1941000 ns (± 29150) |
0.99 |
add-zero-reuse-forwards/create |
1888500 ns (± 106703) |
1867000 ns (± 91207) |
1.01 |
add-zero-reuse-forwards/rewrite |
1553000 ns (± 107512) |
1545000 ns (± 36923) |
1.01 |
mul-two-forwards/create |
2282500 ns (± 132689) |
2182000 ns (± 33679) |
1.05 |
mul-two-forwards/rewrite |
3673000 ns (± 98764) |
3606000 ns (± 35316) |
1.02 |
add-zero-reuse-first/create |
1876000 ns (± 91912) |
1868500 ns (± 106690) |
1.00 |
add-zero-reuse-first/rewrite |
8000 ns (± 1640) |
8000 ns (± 1470) |
1 |
add-zero-lots-of-reuse-first/create |
1904000 ns (± 123065) |
1895500 ns (± 88481) |
1.00 |
add-zero-lots-of-reuse-first/rewrite |
782500 ns (± 27980) |
788500 ns (± 19819) |
0.99 |
This comment was automatically generated by workflow using github-action-benchmark.
|
Very cool. I am curious, where did you derive these pattern from? Are these from LLVM? I would appreciate on paragraph in the PR message how |
|
thank you for the review @tobiasgrosser, addressed |
| See: https://github.com/llvm/llvm-project/blob/16a0a1042f7e4e5a0c667096fcdeb5803e06d120/llvm/lib/Target/RISCV/GISel/RISCVLegalizerInfo.cpp#L171-L179 | ||
| -/ | ||
| def isLegalExtOpWidth (w : Nat) : Bool := | ||
| w = 16 ∨ w = 32 |
There was a problem hiding this comment.
I don't understand the rationale for not supporting sext/zext from 8 bits -- there are RISC-V instructions for these operations, I think?
There was a problem hiding this comment.
afaiu from the legalizer they are not legal (?), am I misunderstanding?
| veir_bv_decide | ||
|
|
||
| /-- | ||
| Prove the correctness of the `zext` lowering pattern `i8` -> `i16` |
There was a problem hiding this comment.
totally up to you if you want to do it, but this code might be shorter if you define a generic [sz]ext_x_y theorem and then instantiate it many times
|
Let's merge this for now. :-) |
3 participants
We add the remaining correctness proofs for the isel patterns of sext/zext/trunc types for legal types within RV64
and update the tests accordingly. We also check the condition on the relation between the width of the input and output types (e.g., for sext, the return type's width must be greater than the operand's).
Legal extensions are: i16 -> i64, i16 -> i32, i32 -> i64, while truncation is always legal (as described in the legalizer).
The patterns are based on the inspection of llc's behaviour.