[feliperodri]

-Z autoharness crashed the compiler on a generic helper whose body calls a SIMD intrinsic but whose type parameter carries no SIMD bound. Autoharness picked T = i32, and the SIMD comparison codegen unwrapped the vector length of a scalar. core_arch::simd::simd_imin<T: Copy> has exactly this shape, so core failed codegen, which is what blocks the unfiltered autoharness path in model-checking/verify-rust-std#687.

Update after merging main: #4922 has since added the codegen guard (the crash no longer happens on main; the call is reported as an unsupported construct), so this PR is now the autoharness side of that fix: it stops autoharness from choosing such instantiations in the first place.

rustc's codegen backends reject these monomorphizations (E0511: invalid monomorphization of simd_ltintrinsic: expected SIMD input type, found non-SIMDi32``), but Kani replaces the backend, so such calls reach Kani's codegen: from a harness that calls imin::<i32> directly, and from instantiations that autoharness synthesizes.

Codegen. #4922's guard is kept as is (behaviour, message and issue link); its inline list of the 21 SIMD intrinsics is replaced by Intrinsic::simd_vector_operand, which names the operand that must be a vector and lives next to try_match_simd, so a new SIMD intrinsic is added in one place and the autoharness filter below uses the same list. simd_splat is the only one whose vector is the return type rather than the first argument.

Autoharness stops choosing those instantiations. A candidate type is rejected when it would make a SIMD intrinsic call in the function's own body invalid. On the reproducer this is better than skipping: autoharness moves on and picks the #[repr(simd)] type, so imin is verified rather than reported. Where no candidate is SIMD, the function is skipped with a reason that names the intrinsic instead of blaming trait bounds the candidate does satisfy.

What it deliberately leaves. A generic function that reaches the invalid instantiation one level down, through a call, is still only caught in codegen, so its harness fails rather than being skipped. Detecting that needs a transitive walk with composed substitutions, like has_const_generic_precondition does for const blocks; filed as #4926, and the new test pins the current behaviour so that fix has to update it.

Testing. tests/script-based-pre/autoharness_simd_non_simd_instantiation covers the reproducer, the one-level-down case, and a function whose SIMD operand types are fixed (unaffected). I confirmed it fails without the fix, and that a deliberately wrong expectation fails the test. After merging main: the test, all 39 script-based-pre autoharness tests, the expected SIMD tests (including #4922's simd-scalar-operand) and the kani SIMD tests pass, as do fmt and both clippy invocations. The kani, expected, ui, cargo-kani and script-based-pre suites pass, as do fmt and clippy.

One thing worth a reviewer's eye: the candidate check calls instance.body(), which skip_reason then calls again for the chosen instance, so a generic function now costs one extra stable-MIR conversion. It happens only for candidates that already satisfy the predicates, which is normally one per function, and rustc caches the underlying monomorphization — but say if you would rather it were hoisted or pre-filtered.

I could not confirm the core case end to end locally: simd_imin is present in the pinned toolchain's stdarch, but kani autoharness --std failed while building compiler_builtins, before reaching any Kani code. The evidence here is that the test reproduces the same shape.

Follow-up to #4922, which resolved #4919.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Copilot review overview

🟢 Approval recommended

The shared guard, candidate filtering, diagnostics, and regression coverage consistently implement the stated behavior.

Review effort: Balanced
Findings: None

What changed in this PR

Prevents autoharness from selecting scalar monomorphizations for directly called SIMD intrinsics, complementing #4922’s codegen guard.

Changes:

• Centralizes SIMD vector-operand identification.
• Filters invalid autoharness candidates while preserving the documented transitive limitation.
• Adds regression coverage for direct, transitive, and fixed-type SIMD calls.

File	Description
kani-compiler/​src/​intrinsics.rs	Centralizes SIMD vector-operand selection.
kani-compiler/​src/​kani_middle/​codegen_units.rs	Rejects invalid scalar SIMD candidates.
kani-compiler/​src/​codegen_cprover_gotoc/​codegen/​intrinsic.rs	Reuses the shared SIMD operand helper.
tests/​script-based-pre/​autoharness_simd_non_simd_instantiation/​simd_generic.rs	Defines regression scenarios.
tests/​script-based-pre/​autoharness_simd_non_simd_instantiation/​check.sh	Validates harness selection and completion.
tests/​script-based-pre/​autoharness_simd_non_simd_instantiation/​config.yml	Registers the script-based test.
tests/​script-based-pre/​autoharness_simd_non_simd_instantiation/​expected	Records expected test output.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.