You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Autoharness aborts the crate on a SIMD comparison instantiated with float lanes (follow-up to #4919) #4950
Follow-up to #4919 / #4927. With #4927, autoharness no longer instantiates generic SIMD helpers with scalars — it picks a real SIMD type instead. But it can pick one whose lanes are floats, and for a SIMD comparison that is still invalid: the mask has to have integer lanes. Kani then raises a hard error that aborts the whole crate:
error: expected return type with integer elements, found `core_arch::x86::__m128` with non-integer `f32`
--> library/stdarch/crates/core_arch/src/simd.rs:8:19
|
8 | let mask: T = crate::intrinsics::simd::simd_gt(a, b);
This is what still blocks the unfiltered autoharness run over the standard library in model-checking/verify-rust-std#687 (core_arch::simd::simd_imax<T: Copy> instantiated with __m128).
Reproducer
#![feature(core_intrinsics, repr_simd)]#![allow(internal_features, non_camel_case_types)]#[repr(simd)]#[derive(Clone,Copy)]pubstructf32x4([f32;4]);#[cfg(kani)]impl kani::Arbitraryforf32x4{fnany() -> Self{f32x4(kani::any())}}// Makes `f32x4` the only candidate, as `__m128` is among `core`'s `Copy` impls.pubtraitLanes:Copy{}implLanesforf32x4{}// Shape of `core_arch::simd::simd_imax`.pubunsafefnimax<T:Lanes>(a:T,b:T) -> T{let mask:T = core::intrinsics::simd::simd_gt(a, b);
core::intrinsics::simd::simd_select(mask, a, b)}
$ kani autoharness -Z autoharness lib.rs --only-codegenerror: expected return type with integer elements, found `f32x4` with non-integer `f32`error: aborting due to 1 previous error
Cause
codegen_comparison_simd (intrinsic.rs:1577 on main) reports the mismatch with span_err and then calls abort_if_errors(), so one bad instantiation stops codegen of the whole crate. invalid_simd_instantiation (#4927) only checks that the operand is SIMD, not the lane-type constraints of the comparison.
In invalid_simd_instantiation, also reject a candidate when a SIMD comparison (simd_eq/ne/lt/le/gt/ge) in the body would get a return type with non-integer lanes.
On nightly-2026-08-21 with #4819, #4869, #4848, #4801 and #4927 applied, I patched the check locally as in (2). Autoharness over the whole of verify-rust-std's library/ with no --include-pattern then completed: exit 0, no panics, harnesses generated for 26,909 functions. So on that library this is the last compile-time blocker.
Activity
Stop a SIMD comparison with float mask lanes from aborting the crate (m…
Report simd_reduce_max/min with a result type other than the lane typ…
Link the generic issue page for an unsupported reduction type
Report simd_reduce_max/min with a result type other than the lane typ…