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

Name	Support	Notes
abort	Yes
add_with_overflow	Yes
arith_offset	Yes
assert_inhabited	Yes
assert_uninit_valid	Yes
assert_zero_valid	Yes
assume	Yes
atomic_and_seqcst	Partial	See Atomics
atomic_and_acquire	Partial	See Atomics
atomic_and_acqrel	Partial	See Atomics
atomic_and_release	Partial	See Atomics
atomic_and_relaxed	Partial	See Atomics
atomic_cxchg_acqrel_acquire	Partial	See Atomics
atomic_cxchg_acqrel_relaxed	Partial	See Atomics
atomic_cxchg_acqrel_seqcst	Partial	See Atomics
atomic_cxchg_acquire_acquire	Partial	See Atomics
atomic_cxchg_acquire_relaxed	Partial	See Atomics
atomic_cxchg_acquire_seqcst	Partial	See Atomics
atomic_cxchg_relaxed_acquire	Partial	See Atomics
atomic_cxchg_relaxed_relaxed	Partial	See Atomics
atomic_cxchg_relaxed_seqcst	Partial	See Atomics
atomic_cxchg_release_acquire	Partial	See Atomics
atomic_cxchg_release_relaxed	Partial	See Atomics
atomic_cxchg_release_seqcst	Partial	See Atomics
atomic_cxchg_seqcst_acquire	Partial	See Atomics
atomic_cxchg_seqcst_relaxed	Partial	See Atomics
atomic_cxchg_seqcst_seqcst	Partial	See Atomics
atomic_cxchgweak_acqrel_acquire	Partial	See Atomics
atomic_cxchgweak_acqrel_relaxed	Partial	See Atomics
atomic_cxchgweak_acqrel_seqcst	Partial	See Atomics
atomic_cxchgweak_acquire_acquire	Partial	See Atomics
atomic_cxchgweak_acquire_relaxed	Partial	See Atomics
atomic_cxchgweak_acquire_seqcst	Partial	See Atomics
atomic_cxchgweak_relaxed_acquire	Partial	See Atomics
atomic_cxchgweak_relaxed_relaxed	Partial	See Atomics
atomic_cxchgweak_relaxed_seqcst	Partial	See Atomics
atomic_cxchgweak_release_acquire	Partial	See Atomics
atomic_cxchgweak_release_relaxed	Partial	See Atomics
atomic_cxchgweak_release_seqcst	Partial	See Atomics
atomic_cxchgweak_seqcst_acquire	Partial	See Atomics
atomic_cxchgweak_seqcst_relaxed	Partial	See Atomics
atomic_cxchgweak_seqcst_seqcst	Partial	See Atomics
atomic_fence_seqcst	Partial	See Atomics
atomic_fence_acquire	Partial	See Atomics
atomic_fence_acqrel	Partial	See Atomics
atomic_fence_release	Partial	See Atomics
atomic_load_seqcst	Partial	See Atomics
atomic_load_acquire	Partial	See Atomics
atomic_load_relaxed	Partial	See Atomics
atomic_load_unordered	Partial	See Atomics
atomic_max_seqcst	Partial	See Atomics
atomic_max_acquire	Partial	See Atomics
atomic_max_acqrel	Partial	See Atomics
atomic_max_release	Partial	See Atomics
atomic_max_relaxed	Partial	See Atomics
atomic_min_seqcst	Partial	See Atomics
atomic_min_acquire	Partial	See Atomics
atomic_min_acqrel	Partial	See Atomics
atomic_min_release	Partial	See Atomics
atomic_min_relaxed	Partial	See Atomics
atomic_nand_seqcst	Partial	See Atomics
atomic_nand_acquire	Partial	See Atomics
atomic_nand_acqrel	Partial	See Atomics
atomic_nand_release	Partial	See Atomics
atomic_nand_relaxed	Partial	See Atomics
atomic_or_seqcst	Partial	See Atomics
atomic_or_acquire	Partial	See Atomics
atomic_or_acqrel	Partial	See Atomics
atomic_or_release	Partial	See Atomics
atomic_or_relaxed	Partial	See Atomics
atomic_singlethreadfence_seqcst	Partial	See Atomics
atomic_singlethreadfence_acquire	Partial	See Atomics
atomic_singlethreadfence_acqrel	Partial	See Atomics
atomic_singlethreadfence_release	Partial	See Atomics
atomic_store_seqcst	Partial	See Atomics
atomic_store_release	Partial	See Atomics
atomic_store_relaxed	Partial	See Atomics
atomic_store_unordered	Partial	See Atomics
atomic_umax_seqcst	Partial	See Atomics
atomic_umax_acquire	Partial	See Atomics
atomic_umax_acqrel	Partial	See Atomics
atomic_umax_release	Partial	See Atomics
atomic_umax_relaxed	Partial	See Atomics
atomic_umin_seqcst	Partial	See Atomics
atomic_umin_acquire	Partial	See Atomics
atomic_umin_acqrel	Partial	See Atomics
atomic_umin_release	Partial	See Atomics
atomic_umin_relaxed	Partial	See Atomics
atomic_xadd_seqcst	Partial	See Atomics
atomic_xadd_acquire	Partial	See Atomics
atomic_xadd_acqrel	Partial	See Atomics
atomic_xadd_release	Partial	See Atomics
atomic_xadd_relaxed	Partial	See Atomics
atomic_xchg_seqcst	Partial	See Atomics
atomic_xchg_acquire	Partial	See Atomics
atomic_xchg_acqrel	Partial	See Atomics
atomic_xchg_release	Partial	See Atomics
atomic_xchg_relaxed	Partial	See Atomics
atomic_xor_seqcst	Partial	See Atomics
atomic_xor_acquire	Partial	See Atomics
atomic_xor_acqrel	Partial	See Atomics
atomic_xor_release	Partial	See Atomics
atomic_xor_relaxed	Partial	See Atomics
atomic_xsub_seqcst	Partial	See Atomics
atomic_xsub_acquire	Partial	See Atomics
atomic_xsub_acqrel	Partial	See Atomics
atomic_xsub_release	Partial	See Atomics
atomic_xsub_relaxed	Partial	See Atomics
blackbox	Yes
bitreverse	Yes
breakpoint	Yes
bswap	Yes
caller_location	No
ceilf32	Yes
ceilf64	Yes
copy	Yes
copy_nonoverlapping	Yes
copysignf32	Yes
copysignf64	Yes
cosf32	Partial	Results are overapproximated; this test explains how
cosf64	Partial	Results are overapproximated; this test explains how
ctlz	Yes
ctlz_nonzero	Yes
ctpop	Yes
cttz	Yes
cttz_nonzero	Yes
discriminant_value	Yes
drop_in_place	No
exact_div	Yes
exp2f32	Partial	Results are overapproximated
exp2f64	Partial	Results are overapproximated
expf32	Partial	Results are overapproximated
expf64	Partial	Results are overapproximated
fabsf32	Yes
fabsf64	Yes
fadd_fast	Yes
fdiv_fast	Partial	#809
float_to_int_unchecked	Partial	#3629
floorf32	Yes
floorf64	Yes
fmaf32	Partial	Results are overapproximated
fmaf64	Partial	Results are overapproximated
fmul_fast	Partial	#809
forget	Yes
frem_fast	No
fsub_fast	Yes
likely	Yes
log10f32	Partial	Results are overapproximated
log10f64	Partial	Results are overapproximated
log2f32	Partial	Results are overapproximated
log2f64	Partial	Results are overapproximated
logf32	Partial	Results are overapproximated
logf64	Partial	Results are overapproximated
maxnumf32	Yes
maxnumf64	Yes
min_align_of	Yes
min_align_of_val	Yes
minnumf32	Yes
minnumf64	Yes
move_val_init	No
mul_with_overflow	Yes
nearbyintf32	Yes
nearbyintf64	Yes
needs_drop	Yes
nontemporal_store	No
offset	Partial	Doesn't check all UB conditions
powf32	Partial	Results are overapproximated
powf64	Partial	Results are overapproximated
powif32	Partial	Results are overapproximated
powif64	Partial	Results are overapproximated
pref_align_of	Yes
prefetch_read_data	No
prefetch_read_instruction	No
prefetch_write_data	No
prefetch_write_instruction	No
ptr_guaranteed_eq	Yes
ptr_guaranteed_ne	Yes
ptr_offset_from	Partial	Doesn't check all UB conditions
raw_eq	Partial	Cannot detect uninitialized memory
rintf32	Yes
rintf64	Yes
rotate_left	Yes
rotate_right	Yes
roundf32	Yes
roundf64	Yes
rustc_peek	No
saturating_add	Yes
saturating_sub	Yes
sinf32	Partial	Results are overapproximated; this test explains how
sinf64	Partial	Results are overapproximated; this test explains how
size_of	Yes
size_of_val	Yes
sqrtf32	Partial	Results are overapproximated
sqrtf64	Partial	Results are overapproximated
sub_with_overflow	Yes
transmute	Partial	Doesn't check all UB conditions
truncf32	Yes
truncf64	Yes
try	No	#267
type_id	Yes
type_name	Yes
typed_swap	Yes
unaligned_volatile_load	No	See Notes - Concurrency
unaligned_volatile_store	No	See Notes - Concurrency
unchecked_add	Yes
unchecked_div	Yes
unchecked_mul	Yes
unchecked_rem	Yes
unchecked_shl	Yes
unchecked_shr	Yes
unchecked_sub	Yes
unlikely	Yes
unreachable	Yes
variant_count	No
volatile_copy_memory	No	See Notes - Concurrency
volatile_copy_nonoverlapping_memory	No	See Notes - Concurrency
volatile_load	Partial	See Notes - Concurrency
volatile_set_memory	No	See Notes - Concurrency
volatile_store	Partial	See Notes - Concurrency
wrapping_add	Yes
wrapping_mul	Yes
wrapping_sub	Yes
write_bytes	Yes

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.

Name	Support	Notes
`simd_add`	Yes
`simd_and`	Yes
`simd_div`	Yes
`simd_eq`	Yes
`simd_extract`	Yes
`simd_ge`	Yes
`simd_gt`	Yes
`simd_insert`	Yes
`simd_le`	Yes
`simd_lt`	Yes
`simd_mul`	Yes
`simd_ne`	Yes
`simd_or`	Yes
`simd_rem`	Yes	Doesn't check for floating point overflow #2669
`simd_shl`	Yes
`simd_shr`	Yes
`simd_shuffle*`	Yes
`simd_sub`	Yes
`simd_xor`	Yes