From 583f1fcd47cda8bf48cd6528503a6d583fb64a24 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Thu, 21 Apr 2022 16:02:47 -0400 Subject: [PATCH] Disable unaudited intrinsics (#1081) * Disable unaudited intrinsics * Updated intrinsics table * Use `unstable_codegen` macro * Edit link * Disable `copy` tests too --- docs/src/rust-feature-support.md | 63 ++++++++------- .../codegen/intrinsic.rs | 80 +++++++++++-------- tests/expected/copy/expected | 6 -- tests/expected/copy/main.rs | 18 ----- ... cast_abstract_args_to_concrete_fixme2.rs} | 0 .../CopyIntrinsics/{main.rs => main_fixme.rs} | 0 .../{main.rs => main_fixme.rs} | 0 7 files changed, 80 insertions(+), 87 deletions(-) delete mode 100644 tests/expected/copy/expected delete mode 100644 tests/expected/copy/main.rs rename tests/kani/Cast/{cast_abstract_args_to_concrete.rs => cast_abstract_args_to_concrete_fixme2.rs} (100%) rename tests/kani/CopyIntrinsics/{main.rs => main_fixme.rs} (100%) rename tests/kani/VolatileIntrinsics/{main.rs => main_fixme.rs} (100%) diff --git a/docs/src/rust-feature-support.md b/docs/src/rust-feature-support.md index 0780ce958bea..9eaf1afe03ec 100644 --- a/docs/src/rust-feature-support.md +++ b/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,10 @@ bswap | Yes | | caller_location | No | | ceilf32 | No | | ceilf64 | No | | -copy_nonoverlapping | Yes | | -copysignf32 | Yes | | -copysignf64 | Yes | | +copy | No | | +copy_nonoverlapping | No | | +copysignf32 | No | | +copysignf64 | No | | cosf32 | Yes | | cosf64 | Yes | | ctlz | Yes | | @@ -324,10 +325,10 @@ 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 | | @@ -335,25 +336,25 @@ 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 | | @@ -361,10 +362,10 @@ 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,8 +388,8 @@ 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 | | @@ -396,7 +397,7 @@ 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 +409,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 | | diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 04bd220dc13b..5b7f2d553552 100644 --- a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -96,7 +96,7 @@ impl<'tcx> GotocCtx<'tcx> { /// https://doc.rust-lang.org/core/intrinsics/fn.copy.html /// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html /// An intrinsic that translates directly into either memmove (for copy) or memcpy (copy_nonoverlapping) - macro_rules! codegen_intrinsic_copy { + macro_rules! _codegen_intrinsic_copy { ($f:ident) => {{ let src = fargs.remove(0).cast_to(Type::void_pointer()); let dst = fargs.remove(0).cast_to(Type::void_pointer()); @@ -337,6 +337,18 @@ impl<'tcx> GotocCtx<'tcx> { }}; } + macro_rules! unstable_codegen { + ($($tt:tt)*) => {{ + let e = self.codegen_unimplemented( + &format!("'{}' intrinsic", intrinsic), + cbmc_ret_ty, + loc, + "https://github.com/model-checking/kani/issues/new/choose", + ); + self.codegen_expr_to_place(p, e) + }}; + } + if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") { let n: u64 = stripped.parse().unwrap(); return self.codegen_intrinsic_simd_shuffle(fargs, p, cbmc_ret_ty, n); @@ -344,7 +356,7 @@ impl<'tcx> GotocCtx<'tcx> { match intrinsic { "add_with_overflow" => codegen_op_with_overflow!(add_overflow), - "arith_offset" => codegen_wrapping_op!(plus), + "arith_offset" => unstable_codegen!(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), @@ -428,10 +440,10 @@ impl<'tcx> GotocCtx<'tcx> { "ceilf64" => codegen_unimplemented_intrinsic!( "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), + "copy" => unstable_codegen!(_codegen_intrinsic_copy!(Memmove)), + "copy_nonoverlapping" => unstable_codegen!(_codegen_intrinsic_copy!(Memcpy)), + "copysignf32" => unstable_codegen!(codegen_simple_intrinsic!(Copysignf)), + "copysignf64" => unstable_codegen!(codegen_simple_intrinsic!(Copysign)), "cosf32" => codegen_simple_intrinsic!(Cosf), "cosf64" => codegen_simple_intrinsic!(Cos), "ctlz" => codegen_count_intrinsic!(ctlz, true), @@ -445,10 +457,10 @@ 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), + "exp2f32" => unstable_codegen!(codegen_simple_intrinsic!(Exp2f)), + "exp2f64" => unstable_codegen!(codegen_simple_intrinsic!(Exp2)), + "expf32" => unstable_codegen!(codegen_simple_intrinsic!(Expf)), + "expf64" => unstable_codegen!(codegen_simple_intrinsic!(Exp)), "fabsf32" => codegen_simple_intrinsic!(Fabsf), "fabsf64" => codegen_simple_intrinsic!(Fabs), "fadd_fast" => { @@ -467,8 +479,8 @@ 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), + "fmaf32" => unstable_codegen!(codegen_simple_intrinsic!(Fmaf)), + "fmaf64" => unstable_codegen!(codegen_simple_intrinsic!(Fma)), "fmul_fast" => { let fargs_clone = fargs.clone(); let binop_stmt = codegen_intrinsic_binop!(mul); @@ -481,18 +493,18 @@ 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), + "log10f32" => unstable_codegen!(codegen_simple_intrinsic!(Log10f)), + "log10f64" => unstable_codegen!(codegen_simple_intrinsic!(Log10)), + "log2f32" => unstable_codegen!(codegen_simple_intrinsic!(Log2f)), + "log2f64" => unstable_codegen!(codegen_simple_intrinsic!(Log2)), + "logf32" => unstable_codegen!(codegen_simple_intrinsic!(Logf)), + "logf64" => unstable_codegen!(codegen_simple_intrinsic!(Log)), + "maxnumf32" => unstable_codegen!(codegen_simple_intrinsic!(Fmaxf)), + "maxnumf64" => unstable_codegen!(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), + "minnumf32" => unstable_codegen!(codegen_simple_intrinsic!(Fminf)), + "minnumf64" => unstable_codegen!(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 +514,10 @@ 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), + "powf32" => unstable_codegen!(codegen_simple_intrinsic!(Powf)), + "powf64" => unstable_codegen!(codegen_simple_intrinsic!(Pow)), + "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)), + "powif64" => unstable_codegen!(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 +573,8 @@ 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), + "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)), + "sqrtf64" => unstable_codegen!(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!( @@ -579,7 +591,7 @@ 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()) + unstable_codegen!(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), @@ -601,9 +613,13 @@ 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_copy_memory" => unstable_codegen!(codegen_intrinsic_copy!(Memmove)), + "volatile_copy_nonoverlapping_memory" => { + unstable_codegen!(codegen_intrinsic_copy!(Memcpy)) + } + "volatile_load" => { + unstable_codegen!(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) diff --git a/tests/expected/copy/expected b/tests/expected/copy/expected deleted file mode 100644 index 84d6b63763af..000000000000 --- a/tests/expected/copy/expected +++ /dev/null @@ -1,6 +0,0 @@ -SUCCESS\ -memmove source region readable -SUCCESS\ -memmove destination region writeable -SUCCESS\ -assertion failed: *dst == expected_val diff --git a/tests/expected/copy/main.rs b/tests/expected/copy/main.rs deleted file mode 100644 index 890249454867..000000000000 --- a/tests/expected/copy/main.rs +++ /dev/null @@ -1,18 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use std::ptr; - -#[kani::proof] -fn main() { - // TODO: make an overlapping set of locations, and check that it does the right thing for the overlapping region too. - // https://github.com/model-checking/kani/issues/12 - let expected_val = 42; - let src: *const i32 = &expected_val as *const i32; - let mut old_val = 99; - let dst: *mut i32 = &mut old_val; - unsafe { - ptr::copy(src, dst, 1); - assert!(*dst == expected_val); - } -} diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete.rs b/tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs similarity index 100% rename from tests/kani/Cast/cast_abstract_args_to_concrete.rs rename to tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs diff --git a/tests/kani/CopyIntrinsics/main.rs b/tests/kani/CopyIntrinsics/main_fixme.rs similarity index 100% rename from tests/kani/CopyIntrinsics/main.rs rename to tests/kani/CopyIntrinsics/main_fixme.rs diff --git a/tests/kani/VolatileIntrinsics/main.rs b/tests/kani/VolatileIntrinsics/main_fixme.rs similarity index 100% rename from tests/kani/VolatileIntrinsics/main.rs rename to tests/kani/VolatileIntrinsics/main_fixme.rs