Skip to content

Autoharness aborts the crate on a SIMD comparison instantiated with float lanes (follow-up to #4919) #4950

Closed

Description

@feliperodri

Summary

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)]
pub struct f32x4([f32; 4]);

#[cfg(kani)]
impl kani::Arbitrary for f32x4 {
    fn any() -> Self { f32x4(kani::any()) }
}

// Makes `f32x4` the only candidate, as `__m128` is among `core`'s `Copy` impls.
pub trait Lanes: Copy {}
impl Lanes for f32x4 {}

// Shape of `core_arch::simd::simd_imax`.
pub unsafe fn imax<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-codegen
error: 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.

Suggested fix

Either or both, in the same shape as #4927:

  1. 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.
  2. Replace the span_err + abort_if_errors() in the comparison codegen with codegen_unimplemented_stmt, as Report a SIMD intrinsic monomorphized with a scalar instead of crashing #4927 does for its own guard, so it fails the harness that reaches it instead of the crate.

Verified

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.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

Projects

No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions