Repository navigation
Report simd_reduce_max/min with a result type other than the lane type as unsupported - #5044
srivatsansamraj wants to merge 2 commits into
Conversation
|
@CYJ904 @Tianshu-Huang @wodex1nhaoIeng @acearyanarun for review. Felipe's follow-up from #4934: if a harness reduces a SIMD vector into a type that isn't its lane type (say |
github-actions
Bot
added
Z-EndToEndBenchCI
feliperodri
added
[C] Bug
There was a problem hiding this comment.
Warning
Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.
Copilot review overview
2 open issues
What changed in this PR
Adds a guard to treat simd_reduce_max/min calls with a non-lane return type as unsupported in Kani, matching rustc’s restriction and preventing autoharness-generated cases from being (incorrectly) verified.
Changes:
- Add a codegen check rejecting
simd_reduce_max/minwhen the return type differs from the SIMD lane type. - Introduce a new expected test that exercises the unsupported behavior for
u8x4 -> u32andu8x4 -> i8. - Add expected output capturing the two harness failures.
| File | Description |
|---|---|
| tests/expected/intrinsics/simd-reduce-result-type/main.rs | New regression test invoking reductions with mismatched return types. |
| tests/expected/intrinsics/simd-reduce-result-type/expected | Expected failure output for the new regression test. |
| kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | Adds the unsupported-construct check and reuses computed return type for casting. |
Review effort: Lite
| "`{intrinsic_str}` with the result type `{ret_ty}` (lane type `{lane_ty}`)" | ||
| ), | ||
| loc, | ||
| "https://github.com/model-checking/kani/issues/4950", |
There was a problem hiding this comment.
Done in 658abbc43: it links the generic issue page now.
| Status: FAILURE\ | ||
| Description: "`simd_reduce_max` with the result type `u32` (lane type `u8`) is not currently supported by Kani | ||
| Status: FAILURE\ | ||
| Description: "`simd_reduce_min` with the result type `i8` (lane type `u8`) is not currently supported by Kani |
There was a problem hiding this comment.
This is the multi-line format of expected files, and the test passes with it.
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
The fix is small and correct: a reduction into a type other than the lane type becomes an unsupported construct, and both cases fail in the test.
Before merge:
…e as unsupported rustc rejects these with E0511 in its codegen backend, which Kani replaces, so Kani accepted them and cast the result: a u8x4 reduced into a u32 was verified. Report them as an unsupported construct, as the SIMD comparisons do for an invalid mask (model-checking#4950).
model-checking#4950 is about SIMD comparisons, not reductions.
da2bcc0 to
658abbc
Compare
Follow-up to #4934, from @feliperodri's review there.
rustc rejects
simd_reduce_maxandsimd_reduce_minwhen the result type is not the lane type (E0511: expected return type 'u8' (element of input 'u8x16')), but that check lives in rustc's codegen backend, which Kani replaces. Kani accepted such a call and cast the result, so au8x4reduced into au32was verified. No crate that compiles with rustc reaches this, but autoharness can, through a generic helper.This reports those calls as an unsupported construct, the way the SIMD comparisons handle an invalid mask type since #4950. Reductions with the lane type are unchanged.
Testing: a new expected test,
simd-reduce-result-type, reduces au8x4into au32and ani8and expects both harnesses to fail as unsupported. With the check removed, both harnesses verify and the test fails. The existing reduction tests (simd-reduce-float,Intrinsics/SIMD/Reduction) still pass.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.