Disable unaudited intrinsics

docs/src/rust-feature-support.md

@@ -210,7 +210,7 @@ Name | Support | Notes |
 --- | --- | --- |
 abort | Yes | |
 add_with_overflow | Yes | |
-arith_offset | Yes | |
+arith_offset | No | |
 assert_inhabited | Partial | [#751](https://github.com/model-checking/kani/issues/751) |
 assert_uninit_valid | Yes | |
 assert_zero_valid | Yes | |
@@ -311,9 +311,9 @@ bswap | Yes | |
 caller_location | No | |
 ceilf32 | No | |
 ceilf64 | No | |
-copy_nonoverlapping | Yes | |
-copysignf32 | Yes | |
-copysignf64 | Yes | |
+copy_nonoverlapping | No | |
+copysignf32 | No | |
+copysignf64 | No | |
 cosf32 | Yes | |
 cosf64 | Yes | |
 ctlz | Yes | |
@@ -324,47 +324,47 @@ cttz_nonzero | Yes | |
 discriminant_value | Yes | |
 drop_in_place | No | |
 exact_div | Yes | |
-exp2f32 | Yes | |
-exp2f64 | Yes | |
-expf32 | Yes | |
-expf64 | Yes | |
+exp2f32 | No | |
+exp2f64 | No | |
+expf32 | No | |
+expf64 | No | |
 fabsf32 | Yes | |
 fabsf64 | Yes | |
 fadd_fast | Yes | |
 fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
 float_to_int_unchecked | No | |
 floorf32 | No | |
 floorf64 | No | |
-fmaf32 | Yes | |
-fmaf64 | Yes | |
+fmaf32 | No | |
+fmaf64 | No | |
 fmul_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
 forget | Yes | |
 frem_fast | No | |
 fsub_fast | Yes | |
 likely | Yes | |
-log2f32 | Yes | |
-log2f64 | Yes | |
-log10f32 | Yes | |
-log10f64 | Yes | |
-logf32 | Yes | |
-logf64 | Yes | |
-maxnumf32 | Yes | |
-maxnumf64 | Yes | |
+log10f32 | No | |
+log10f64 | No | |
+log2f32 | No | |
+log2f64 | No | |
+logf32 | No | |
+logf64 | No | |
+maxnumf32 | No | |
+maxnumf64 | No | |
 min_align_of | Yes | |
 min_align_of_val | Yes | |
-minnumf32 | Yes | |
-minnumf64 | Yes | |
+minnumf32 | No | |
+minnumf64 | No | |
 move_val_init | No | |
 mul_with_overflow | Yes | |
 nearbyintf32 | No | |
 nearbyintf64 | No | |
 needs_drop | Yes | |
 nontemporal_store | No | |
 offset | Partial | Missing undefined behavior checks |
-powf32 | Yes | |
-powf64 | Yes | |
-powif32 | Yes | |
-powif64 | Yes | |
+powf32 | No | |
+powf64 | No | |
+powif32 | No | |
+powif64 | No | |
 pref_align_of | Yes | |
 prefetch_read_data | No | |
 prefetch_read_instruction | No | |
@@ -387,16 +387,16 @@ sinf32 | Yes | |
 sinf64 | Yes | |
 size_of | Yes | |
 size_of_val | Yes | |
-sqrtf32 | Yes | |
-sqrtf64 | Yes | |
+sqrtf32 | No | |
+sqrtf64 | No | |
 sub_with_overflow | Yes | |
 transmute | Yes | |
 truncf32 | No | |
 truncf64 | No | |
 try | No | [#267](https://github.com/model-checking/kani/issues/267) |
 type_id | Yes | |
 type_name | Yes | |
-unaligned_volatile_load | Partial | See [Notes - Concurrency](#concurrency) |
+unaligned_volatile_load | No | See [Notes - Concurrency](#concurrency) |
 unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) |
 unchecked_add | Yes | |
 unchecked_div | Yes | |
@@ -408,11 +408,11 @@ unchecked_sub | Yes | |
 unlikely | Yes | |
 unreachable | Yes | |
 variant_count | No | |
-volatile_copy_memory | Partial | See [Notes - Concurrency](#concurrency) |
-volatile_copy_nonoverlapping_memory | Partial | See [Notes - Concurrency](#concurrency) |
-volatile_load | Partial | See [Notes - Concurrency](#concurrency) |
+volatile_copy_memory | No | See [Notes - Concurrency](#concurrency) |
+volatile_copy_nonoverlapping_memory | No | See [Notes - Concurrency](#concurrency) |
+volatile_load | No | See [Notes - Concurrency](#concurrency) |
 volatile_set_memory | No | See [Notes - Concurrency](#concurrency) |
-volatile_store | No | See [Notes - Concurrency](#concurrency) |
+volatile_store | Partial | See [Notes - Concurrency](#concurrency) |
 wrapping_add | Yes | |
 wrapping_mul | Yes | |
 wrapping_sub | Yes | |

src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -344,7 +344,6 @@ impl<'tcx> GotocCtx<'tcx> {
 
         match intrinsic {
             "add_with_overflow" => codegen_op_with_overflow!(add_overflow),
-            "arith_offset" => codegen_wrapping_op!(plus),
             "assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span),
             "assert_uninit_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
             "assert_zero_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
@@ -429,9 +428,6 @@ impl<'tcx> GotocCtx<'tcx> {
                 "https://github.com/model-checking/kani/issues/1025"
             ),
             "copy" => codegen_intrinsic_copy!(Memmove),
-            "copy_nonoverlapping" => codegen_intrinsic_copy!(Memcpy),
-            "copysignf32" => codegen_simple_intrinsic!(Copysignf),
-            "copysignf64" => codegen_simple_intrinsic!(Copysign),
             "cosf32" => codegen_simple_intrinsic!(Cosf),
             "cosf64" => codegen_simple_intrinsic!(Cos),
             "ctlz" => codegen_count_intrinsic!(ctlz, true),
@@ -445,10 +441,6 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_expr_to_place(p, e)
             }
             "exact_div" => self.codegen_exact_div(fargs, p, loc),
-            "exp2f32" => codegen_simple_intrinsic!(Exp2f),
-            "exp2f64" => codegen_simple_intrinsic!(Exp2),
-            "expf32" => codegen_simple_intrinsic!(Expf),
-            "expf64" => codegen_simple_intrinsic!(Exp),
             "fabsf32" => codegen_simple_intrinsic!(Fabsf),
             "fabsf64" => codegen_simple_intrinsic!(Fabs),
             "fadd_fast" => {
@@ -467,8 +459,6 @@ impl<'tcx> GotocCtx<'tcx> {
             "floorf64" => codegen_unimplemented_intrinsic!(
                 "https://github.com/model-checking/kani/issues/1025"
             ),
-            "fmaf32" => codegen_simple_intrinsic!(Fmaf),
-            "fmaf64" => codegen_simple_intrinsic!(Fma),
             "fmul_fast" => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(mul);
@@ -481,18 +471,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
             }
             "likely" => self.codegen_expr_to_place(p, fargs.remove(0)),
-            "log10f32" => codegen_simple_intrinsic!(Log10f),
-            "log10f64" => codegen_simple_intrinsic!(Log10),
-            "log2f32" => codegen_simple_intrinsic!(Log2f),
-            "log2f64" => codegen_simple_intrinsic!(Log2),
-            "logf32" => codegen_simple_intrinsic!(Logf),
-            "logf64" => codegen_simple_intrinsic!(Log),
-            "maxnumf32" => codegen_simple_intrinsic!(Fmaxf),
-            "maxnumf64" => codegen_simple_intrinsic!(Fmax),
             "min_align_of" => codegen_intrinsic_const!(),
             "min_align_of_val" => codegen_size_align!(align),
-            "minnumf32" => codegen_simple_intrinsic!(Fminf),
-            "minnumf64" => codegen_simple_intrinsic!(Fmin),
             "mul_with_overflow" => codegen_op_with_overflow!(mul_overflow),
             "nearbyintf32" => codegen_unimplemented_intrinsic!(
                 "https://github.com/model-checking/kani/issues/1025"
@@ -502,10 +482,6 @@ impl<'tcx> GotocCtx<'tcx> {
             ),
             "needs_drop" => codegen_intrinsic_const!(),
             "offset" => codegen_op_with_overflow_check!(add_overflow),
-            "powf32" => codegen_simple_intrinsic!(Powf),
-            "powf64" => codegen_simple_intrinsic!(Pow),
-            "powif32" => codegen_simple_intrinsic!(Powif),
-            "powif64" => codegen_simple_intrinsic!(Powi),
             "pref_align_of" => codegen_intrinsic_const!(),
             "ptr_guaranteed_eq" => codegen_intrinsic_boolean_binop!(eq),
             "ptr_guaranteed_ne" => codegen_intrinsic_boolean_binop!(neq),
@@ -561,8 +537,6 @@ impl<'tcx> GotocCtx<'tcx> {
             "simd_xor" => codegen_intrinsic_binop!(bitxor),
             "size_of" => codegen_intrinsic_const!(),
             "size_of_val" => codegen_size_align!(size),
-            "sqrtf32" => codegen_simple_intrinsic!(Sqrtf),
-            "sqrtf64" => codegen_simple_intrinsic!(Sqrt),
             "sub_with_overflow" => codegen_op_with_overflow!(sub_overflow),
             "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, p),
             "truncf32" => codegen_unimplemented_intrinsic!(
@@ -578,9 +552,6 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             "type_id" => codegen_intrinsic_const!(),
             "type_name" => codegen_intrinsic_const!(),
-            "unaligned_volatile_load" => {
-                self.codegen_expr_to_place(p, fargs.remove(0).dereference())
-            }
             "unchecked_add" => codegen_op_with_overflow_check!(add_overflow),
             "unchecked_div" => codegen_op_with_div_overflow_check!(div),
             "unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow),
@@ -601,9 +572,6 @@ impl<'tcx> GotocCtx<'tcx> {
                 "unreachable",
                 loc,
             ),
-            "volatile_copy_memory" => codegen_intrinsic_copy!(Memmove),
-            "volatile_copy_nonoverlapping_memory" => codegen_intrinsic_copy!(Memcpy),
-            "volatile_load" => self.codegen_expr_to_place(p, fargs.remove(0).dereference()),
             "volatile_store" => {
                 assert!(self.place_ty(p).is_unit());
                 self.codegen_volatile_store(instance, intrinsic, fargs, loc)