Intrinsics

The tables below try to summarize the current support in Kani for Rust intrinsics. We define the level of support similar to how we indicate Rust feature support:

  • Yes: The intrinsic is fully supported. We are not aware of any issue with it.
  • Partial: The intrinsic is at least partially supported. We are aware of some issue with with it.
  • No: The intrinsic is not supported.

In general, code generation for unsupported intrinsics follows the rule described in Rust feature support - Code generation for unsupported features.

Any intrinsic not appearing in the tables below is considered not supported. Please open a feature request if your code depends on an unsupported intrinsic.

Compiler intrinsics

NameSupportNotes
abortYes
add_with_overflowYes
arith_offsetYes
assert_inhabitedYes
assert_uninit_validYes
assert_zero_validYes
assumeYes
atomic_and_seqcstPartialSee Atomics
atomic_and_acquirePartialSee Atomics
atomic_and_acqrelPartialSee Atomics
atomic_and_releasePartialSee Atomics
atomic_and_relaxedPartialSee Atomics
atomic_cxchg_acqrel_acquirePartialSee Atomics
atomic_cxchg_acqrel_relaxedPartialSee Atomics
atomic_cxchg_acqrel_seqcstPartialSee Atomics
atomic_cxchg_acquire_acquirePartialSee Atomics
atomic_cxchg_acquire_relaxedPartialSee Atomics
atomic_cxchg_acquire_seqcstPartialSee Atomics
atomic_cxchg_relaxed_acquirePartialSee Atomics
atomic_cxchg_relaxed_relaxedPartialSee Atomics
atomic_cxchg_relaxed_seqcstPartialSee Atomics
atomic_cxchg_release_acquirePartialSee Atomics
atomic_cxchg_release_relaxedPartialSee Atomics
atomic_cxchg_release_seqcstPartialSee Atomics
atomic_cxchg_seqcst_acquirePartialSee Atomics
atomic_cxchg_seqcst_relaxedPartialSee Atomics
atomic_cxchg_seqcst_seqcstPartialSee Atomics
atomic_cxchgweak_acqrel_acquirePartialSee Atomics
atomic_cxchgweak_acqrel_relaxedPartialSee Atomics
atomic_cxchgweak_acqrel_seqcstPartialSee Atomics
atomic_cxchgweak_acquire_acquirePartialSee Atomics
atomic_cxchgweak_acquire_relaxedPartialSee Atomics
atomic_cxchgweak_acquire_seqcstPartialSee Atomics
atomic_cxchgweak_relaxed_acquirePartialSee Atomics
atomic_cxchgweak_relaxed_relaxedPartialSee Atomics
atomic_cxchgweak_relaxed_seqcstPartialSee Atomics
atomic_cxchgweak_release_acquirePartialSee Atomics
atomic_cxchgweak_release_relaxedPartialSee Atomics
atomic_cxchgweak_release_seqcstPartialSee Atomics
atomic_cxchgweak_seqcst_acquirePartialSee Atomics
atomic_cxchgweak_seqcst_relaxedPartialSee Atomics
atomic_cxchgweak_seqcst_seqcstPartialSee Atomics
atomic_fence_seqcstPartialSee Atomics
atomic_fence_acquirePartialSee Atomics
atomic_fence_acqrelPartialSee Atomics
atomic_fence_releasePartialSee Atomics
atomic_load_seqcstPartialSee Atomics
atomic_load_acquirePartialSee Atomics
atomic_load_relaxedPartialSee Atomics
atomic_load_unorderedPartialSee Atomics
atomic_max_seqcstPartialSee Atomics
atomic_max_acquirePartialSee Atomics
atomic_max_acqrelPartialSee Atomics
atomic_max_releasePartialSee Atomics
atomic_max_relaxedPartialSee Atomics
atomic_min_seqcstPartialSee Atomics
atomic_min_acquirePartialSee Atomics
atomic_min_acqrelPartialSee Atomics
atomic_min_releasePartialSee Atomics
atomic_min_relaxedPartialSee Atomics
atomic_nand_seqcstPartialSee Atomics
atomic_nand_acquirePartialSee Atomics
atomic_nand_acqrelPartialSee Atomics
atomic_nand_releasePartialSee Atomics
atomic_nand_relaxedPartialSee Atomics
atomic_or_seqcstPartialSee Atomics
atomic_or_acquirePartialSee Atomics
atomic_or_acqrelPartialSee Atomics
atomic_or_releasePartialSee Atomics
atomic_or_relaxedPartialSee Atomics
atomic_singlethreadfence_seqcstPartialSee Atomics
atomic_singlethreadfence_acquirePartialSee Atomics
atomic_singlethreadfence_acqrelPartialSee Atomics
atomic_singlethreadfence_releasePartialSee Atomics
atomic_store_seqcstPartialSee Atomics
atomic_store_releasePartialSee Atomics
atomic_store_relaxedPartialSee Atomics
atomic_store_unorderedPartialSee Atomics
atomic_umax_seqcstPartialSee Atomics
atomic_umax_acquirePartialSee Atomics
atomic_umax_acqrelPartialSee Atomics
atomic_umax_releasePartialSee Atomics
atomic_umax_relaxedPartialSee Atomics
atomic_umin_seqcstPartialSee Atomics
atomic_umin_acquirePartialSee Atomics
atomic_umin_acqrelPartialSee Atomics
atomic_umin_releasePartialSee Atomics
atomic_umin_relaxedPartialSee Atomics
atomic_xadd_seqcstPartialSee Atomics
atomic_xadd_acquirePartialSee Atomics
atomic_xadd_acqrelPartialSee Atomics
atomic_xadd_releasePartialSee Atomics
atomic_xadd_relaxedPartialSee Atomics
atomic_xchg_seqcstPartialSee Atomics
atomic_xchg_acquirePartialSee Atomics
atomic_xchg_acqrelPartialSee Atomics
atomic_xchg_releasePartialSee Atomics
atomic_xchg_relaxedPartialSee Atomics
atomic_xor_seqcstPartialSee Atomics
atomic_xor_acquirePartialSee Atomics
atomic_xor_acqrelPartialSee Atomics
atomic_xor_releasePartialSee Atomics
atomic_xor_relaxedPartialSee Atomics
atomic_xsub_seqcstPartialSee Atomics
atomic_xsub_acquirePartialSee Atomics
atomic_xsub_acqrelPartialSee Atomics
atomic_xsub_releasePartialSee Atomics
atomic_xsub_relaxedPartialSee Atomics
blackboxYes
bitreverseYes
breakpointYes
bswapYes
caller_locationNo
ceilf32Yes
ceilf64Yes
copyYes
copy_nonoverlappingYes
copysignf32Yes
copysignf64Yes
cosf32PartialResults are overapproximated; this test explains how
cosf64PartialResults are overapproximated; this test explains how
ctlzYes
ctlz_nonzeroYes
ctpopYes
cttzYes
cttz_nonzeroYes
discriminant_valueYes
drop_in_placeNo
exact_divYes
exp2f32No
exp2f64No
expf32No
expf64No
fabsf32Yes
fabsf64Yes
fadd_fastYes
fdiv_fastPartial#809
float_to_int_uncheckedNo
floorf32Yes
floorf64Yes
fmaf32No
fmaf64No
fmul_fastPartial#809
forgetYes
frem_fastNo
fsub_fastYes
likelyYes
log10f32No
log10f64No
log2f32No
log2f64No
logf32No
logf64No
maxnumf32Yes
maxnumf64Yes
min_align_ofYes
min_align_of_valYes
minnumf32Yes
minnumf64Yes
move_val_initNo
mul_with_overflowYes
nearbyintf32Yes
nearbyintf64Yes
needs_dropYes
nontemporal_storeNo
offsetPartialDoesn't check all UB conditions
powf32No
powf64No
powif32No
powif64No
pref_align_ofYes
prefetch_read_dataNo
prefetch_read_instructionNo
prefetch_write_dataNo
prefetch_write_instructionNo
ptr_guaranteed_eqYes
ptr_guaranteed_neYes
ptr_offset_fromPartialDoesn't check all UB conditions
raw_eqPartialCannot detect uninitialized memory
rintf32Yes
rintf64Yes
rotate_leftYes
rotate_rightYes
roundf32Yes
roundf64Yes
rustc_peekNo
saturating_addYes
saturating_subYes
sinf32PartialResults are overapproximated; this test explains how
sinf64PartialResults are overapproximated; this test explains how
size_ofYes
size_of_valYes
sqrtf32No
sqrtf64No
sub_with_overflowYes
transmutePartialDoesn't check all UB conditions
truncf32Yes
truncf64Yes
tryNo#267
type_idYes
type_nameYes
unaligned_volatile_loadNoSee Notes - Concurrency
unaligned_volatile_storeNoSee Notes - Concurrency
unchecked_addYes
unchecked_divYes
unchecked_mulYes
unchecked_remYes
unchecked_shlYes
unchecked_shrYes
unchecked_subYes
unlikelyYes
unreachableYes
variant_countNo
volatile_copy_memoryNoSee Notes - Concurrency
volatile_copy_nonoverlapping_memoryNoSee Notes - Concurrency
volatile_loadPartialSee Notes - Concurrency
volatile_set_memoryNoSee Notes - Concurrency
volatile_storePartialSee Notes - Concurrency
wrapping_addYes
wrapping_mulYes
wrapping_subYes
write_bytesYes

Atomics

All atomic intrinsics are compiled as an atomic block where the operation is performed. But as noted in Notes - Concurrency, Kani support for concurrent verification is limited and not used by default. Verification on code containing atomic intrinsics should not be trusted given that Kani assumes the code to be sequential.

Platform intrinsics

Intrinsics from the platform_intrinsics feature.

NameSupportNotes
simd_addYes
simd_andYes
simd_divYesDoesn't check for overflow cases #1970
simd_eqYes
simd_extractYes
simd_geYes
simd_gtYes
simd_insertYes
simd_leYes
simd_ltYes
simd_mulYes
simd_neYes
simd_orYes
simd_remYesDoesn't check for overflow cases #1970
simd_shlYesDoesn't check for overflow cases #1963
simd_shrYesDoesn't check for overflow cases #1963
simd_shuffle*Yes
simd_subYes
simd_xorYes