Skip to content

Commit

Permalink
Disable unaudited intrinsics (model-checking#1081)
Browse files Browse the repository at this point in the history 
* Disable unaudited intrinsics

* Updated intrinsics table

* Use `unstable_codegen` macro

* Edit link

* Disable `copy` tests too
  • Loading branch information
@adpaco-aws @tedinski
adpaco-aws authored and tedinski committed Apr 21, 2022
1 parent b1c9744 commit 61e163b
Show file tree
Hide file tree
Showing 7 changed files with 80 additions and 87 deletions.
63 changes: 32 additions & 31 deletions docs/src/rust-feature-support.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 | |
Expand Down Expand Up @@ -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 | |
Expand All @@ -324,47 +325,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 | |
Expand All @@ -387,16 +388,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 | |
Expand All @@ -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 | |
Expand Down
80 changes: 48 additions & 32 deletions src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down Expand Up @@ -337,14 +337,26 @@ 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);
}

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),
Expand Down Expand Up @@ -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),
Expand All @@ -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" => {
Expand All @@ -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);
Expand All @@ -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"
Expand All @@ -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),
Expand Down Expand Up @@ -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!(
Expand All @@ -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),
Expand All @@ -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)
Expand Down
6 changes: 0 additions & 6 deletions tests/expected/copy/expected
View file

This file was deleted.

18 changes: 0 additions & 18 deletions tests/expected/copy/main.rs
View file

This file was deleted.

0 ...ni/Cast/cast_abstract_args_to_concrete.rs → .../cast_abstract_args_to_concrete_fixme2.rs
View file
File renamed without changes.
0 tests/kani/CopyIntrinsics/main.rs → tests/kani/CopyIntrinsics/main_fixme.rs
View file
File renamed without changes.
0 tests/kani/VolatileIntrinsics/main.rs → tests/kani/VolatileIntrinsics/main_fixme.rs
View file
File renamed without changes.

0 comments on commit 61e163b

Please sign in to comment.