[srivatsansamraj]

Follow-up to #4934, from @feliperodri's review there.

rustc rejects simd_reduce_max and simd_reduce_min when 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 a u8x4 reduced into a u32 was 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 a u8x4 into a u32 and an i8 and 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.

[srivatsansamraj]

@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 u8 lanes into a u32), rustc refuses it, but Kani used to accept it and verify the harness. Now Kani reports it as unsupported, the same way it handles bad mask types in SIMD comparisons. One check in codegen_simd_reduce_max_min and one test.

[Copilot]

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

• The diagnostic links to issue #4950, but this unsupported case is about simd_reduce_{max,min}… · New
• The Description: lines appear to start with a double-quote but never close it, which is likely to… · New

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/min when the return type differs from the SIMD lane type.
• Introduce a new expected test that exercises the unsupported behavior for u8x4 -> u32 and u8x4 -> 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}

[feliperodri]

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:

1. The link points to #4950, which covers SIMD comparisons. This case is about reduction return types, so link to #4934 or a new issue.
2. The Description: lines in expected open a quote and never close it. Close it, to match the other expected files.
3. Six jobs are cancelled. Please re-run them.

[feliperodri]

Thanks. The link now points to the generic issue page. I withdraw my point on the unclosed quote: expected files match by substring, and the ubuntu and macos-15-intel regression jobs pass with this test.

compile-timer-long fails in the analyzer step after normal timings, and the macos-14 jobs are cancelled by the runner. Neither comes from this change. Approving.