# 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 | No | |

exp2f64 | No | |

expf32 | No | |

expf64 | No | |

fabsf32 | Yes | |

fabsf64 | Yes | |

fadd_fast | Yes | |

fdiv_fast | Partial | #809 |

float_to_int_unchecked | No | |

floorf32 | Yes | |

floorf64 | Yes | |

fmaf32 | No | |

fmaf64 | No | |

fmul_fast | Partial | #809 |

forget | Yes | |

frem_fast | No | |

fsub_fast | Yes | |

likely | Yes | |

log10f32 | No | |

log10f64 | No | |

log2f32 | No | |

log2f64 | No | |

logf32 | No | |

logf64 | No | |

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 | No | |

powf64 | No | |

powif32 | No | |

powif64 | No | |

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 | No | |

sqrtf64 | No | |

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 | |

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 |