Unsupported: calls to LLVM intrinsics (InstanceKind::LlvmIntrinsic)

Description

As of nightly-2026-08-21 (rustc 1.100), calls to LLVM intrinsics resolve to their own InstanceKind::LlvmIntrinsic. rustc creates this instance kind for any DefKind::Fn whose symbol name starts with llvm. — in practice the extern "unadjusted" declarations in stdarch/core_arch (SSE, AVX, NEON, and friends):

// rustc_ty_utils/src/instance.rs
} else if tcx.def_kind(def_id) == DefKind::Fn
    && let Some(name) = tcx.codegen_fn_attrs(def_id).symbol_name
    && name.as_str().starts_with("llvm.")
{
    ty::InstanceKind::LlvmIntrinsic(def_id)
}

Like InstanceKind::Intrinsic and InstanceKind::Virtual, these have no callable MIR — codegen is expected to handle them in the caller. rustc additionally refuses to compute a FnAbi for them; fn_abi_adjust_for_abi asserts:

assertion `left != right` failed: fn_abi_of_instance should not be called on LLVM intrinsics

Kani has no model for LLVM intrinsics, and since it cannot obtain a FnAbi it cannot even codegen the call's arguments. So codegen_funcall reports such a call as an unsupported construct:

call to LLVM intrinsic `llvm.…` is not currently supported by Kani

This is an UnsupportedConstruct check at the call site, so it only fails verification if the call is actually reachable.

Prior behaviour

Before 1.100 these were foreign items (InstanceKind::Item with is_foreign_item()), so they went through Kani's FFI shim path and produced an equivalent call to foreign "Unadjusted" function … unsupported-construct check. The behaviour is therefore unchanged in substance — only the message and the code path differ.

What full support would require

Modelling the individual LLVM intrinsics that matter, most likely the SIMD ones, similar to how Kani already models #[rustc_intrinsic] intrinsics in codegen/intrinsic.rs. Verifying code that reaches a platform intrinsic is unsupported until then.

Reproducer

Any harness that reaches an extern "unadjusted" llvm.* declaration, e.g. via core::arch SIMD.

Upgrade Rust toolchain to nightly-2026-08-21

Upgrade Rust toolchain to nightly-2026-08-21 (model-checking#4768)

More evidence for this issue. Kani hit it while verifying these 3 crate(s):

Minimal reproducer (Kani 0.68.0):

use core::arch::x86_64::*;
#[cfg(kani)]
#[kani::proof]
fn spin() { core::hint::spin_loop(); }

#[cfg(kani)]
#[kani::proof]
fn pshufb() {
    let a = unsafe { _mm_set1_epi8(1) };
    let b = unsafe { _mm_set1_epi8(0) };
    let _c = unsafe { _mm_shuffle_epi8(a, b) };
}

#[cfg(kani)]
#[kani::proof]
fn packuswb() {
    let a = unsafe { _mm_set1_epi16(300) };
    let _c = unsafe { _mm_packus_epi16(a, a) };
}

#[cfg(kani)]
#[kani::proof]
fn pause() {
    unsafe { _mm_pause() };
}

#[cfg(kani)]
#[kani::proof]
fn xgetbv() {
    let _v = unsafe { _xgetbv(0) };
}

$ cargo kani -Z unstable-options --harness xgetbv --harness-timeout 5m
- Description: "call to LLVM intrinsic `llvm.x86.xgetbv` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/4770"
Failed Checks: call to LLVM intrinsic `llvm.x86.xgetbv` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/4770
** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details.
 - Description: "call to LLVM intrinsic `llvm.x86.ssse3.pshuf.b.128` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/4
Failed Checks: call to LLVM intrinsic `llvm.x86.ssse3.pshuf.b.128` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/477
 - Description: "call to LLVM intrinsic `llvm.x86.sse2.packuswb.128` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/4

Context: we ran AI agents that use the Kani agent plugin (#5059) to verify 101 of the most downloaded crates on crates.io with Kani 0.68.0, CBMC 6.11.0 and nightly-2026-10-22. The minimal reproducer above was re-run by hand with the same versions. This text was written with AI assistance.

Navigation Menu

Repository navigation

Unsupported: calls to LLVM intrinsics (InstanceKind::LlvmIntrinsic) #4770

Description

Prior behaviour

What full support would require

Reproducer

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Unsupported: calls to LLVM intrinsics (InstanceKind::LlvmIntrinsic) #4770

Description

Description

Prior behaviour

What full support would require

Reproducer

Activity

feliperodri commented on Nov 6, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions