From c7b315f22fa225132c87ab4051a1159b0b8ca08b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 15:18:34 +0200 Subject: [PATCH 1/2] Enable log2*, log10* intrinsics (#3001) Implemented in CBMC in https://github.com/diffblue/cbmc/pull/8195. --- docs/src/rust-feature-support/intrinsics.md | 8 +++---- .../codegen/intrinsic.rs | 8 +++---- tests/kani/Intrinsics/Math/Arith/log10.rs | 23 +++++++++++++++++++ tests/kani/Intrinsics/Math/Arith/log2.rs | 23 +++++++++++++++++++ 4 files changed, 54 insertions(+), 8 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Arith/log10.rs create mode 100644 tests/kani/Intrinsics/Math/Arith/log2.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 49a1f0845ecc..501a9952f05e 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -166,10 +166,10 @@ forget | Yes | | frem_fast | No | | fsub_fast | Yes | | likely | Yes | | -log10f32 | No | | -log10f64 | No | | -log2f32 | No | | -log2f64 | No | | +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 | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 29ea69eeb39b..12352190e6e2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -466,10 +466,10 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_expr_to_place_stable(place, Expr::c_false(), loc) } "likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc), - "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)), + "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), diff --git a/tests/kani/Intrinsics/Math/Arith/log10.rs b/tests/kani/Intrinsics/Math/Arith/log10.rs new file mode 100644 index 000000000000..4670c72cfeb3 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/log10.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_log10_32() { + let ten = 10.0f32; + + // log10(10) - 1 == 0 + let abs_difference = (ten.log10() - 1.0).abs(); + + // should be <= f32::EPSILON, but CBMC's approximation of log10 makes results less precise + assert!(abs_difference <= 0.03); +} + +#[kani::proof] +fn verify_log10_64() { + let hundred = 100.0_f64; + + // log10(100) - 2 == 0 + let abs_difference = (hundred.log10() - 2.0).abs(); + + assert!(abs_difference < 0.03); +} diff --git a/tests/kani/Intrinsics/Math/Arith/log2.rs b/tests/kani/Intrinsics/Math/Arith/log2.rs new file mode 100644 index 000000000000..52153f8b368a --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/log2.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_log2_32() { + let two = 2.0f32; + + // log2(2) - 1 == 0 + let abs_difference = (two.log2() - 1.0).abs(); + + // should be <= f32::EPSILON, but CBMC's approximation of log2 makes results less precise + assert!(abs_difference <= 0.09); +} + +#[kani::proof] +fn verify_log2_64() { + let four = 4.0_f64; + + // log2(4) - 2 == 0 + let abs_difference = (four.log2() - 2.0).abs(); + + assert!(abs_difference < 0.09); +} From 6ae3f00c88a458abc381057456780af9e7d7e451 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 16:54:19 +0200 Subject: [PATCH 2/2] Enable powif* intrinsics (#2999) These are supported by CBMC with https://github.com/diffblue/cbmc/pull/8192 merged. Resolves: #2763 --- docs/src/rust-feature-support/intrinsics.md | 4 ++-- .../codegen/intrinsic.rs | 4 ++-- ...2.rs => cast_abstract_args_to_concrete.rs} | 3 --- .../cast_abstract_args_to_concrete_fixme.rs | 24 ------------------- tests/kani/Intrinsics/Math/Arith/powi.rs | 22 +++++++++++++++++ 5 files changed, 26 insertions(+), 31 deletions(-) rename tests/kani/Cast/{cast_abstract_args_to_concrete_fixme2.rs => cast_abstract_args_to_concrete.rs} (92%) delete mode 100644 tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs create mode 100644 tests/kani/Intrinsics/Math/Arith/powi.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 501a9952f05e..f97db5d8ab6c 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -187,8 +187,8 @@ nontemporal_store | No | | offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) | powf32 | Partial | Results are overapproximated | powf64 | Partial | Results are overapproximated | -powif32 | No | | -powif64 | No | | +powif32 | Partial | Results are overapproximated | +powif64 | Partial | Results are overapproximated | pref_align_of | Yes | | prefetch_read_data | No | | prefetch_read_instruction | No | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 12352190e6e2..91f7ea20c9b1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -490,8 +490,8 @@ impl<'tcx> GotocCtx<'tcx> { ), "powf32" => codegen_simple_intrinsic!(Powf), "powf64" => codegen_simple_intrinsic!(Pow), - "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)), - "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)), + "powif32" => codegen_simple_intrinsic!(Powif), + "powif64" => codegen_simple_intrinsic!(Powi), "pref_align_of" => codegen_intrinsic_const!(), "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc), diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs b/tests/kani/Cast/cast_abstract_args_to_concrete.rs similarity index 92% rename from tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs rename to tests/kani/Cast/cast_abstract_args_to_concrete.rs index 51067e0e0a73..6694f799493a 100644 --- a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs +++ b/tests/kani/Cast/cast_abstract_args_to_concrete.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// https://github.com/model-checking/kani/issues/555 -// kani-flags: --no-undefined-function-checks - // This regression test is in response to issue #135. // The type of the second parameter to powi is a `CInteger`, but // the type of `2` here is a `u32`. This test ensures that diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs b/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs deleted file mode 100644 index faeb74c5d66a..000000000000 --- a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs +++ /dev/null @@ -1,24 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test is a modified version of cast_abstract_args_to_concrete_fixme.rs. -//! The original test requires --no-undefined-function-checks to pass. This is an issue that -//! require investigation. See https://github.com/model-checking/kani/issues/555. -//! -//! Once this issue is fixed. Please remove this test and remove the kani flag from the original -//! test: --no-undefined-function-check - -fn main() { - let _x32 = 1.0f32.powi(2); - let _x64 = 1.0f64.powi(2); - - unsafe { - let size: libc::size_t = mem::size_of::(); - let my_num: *mut libc::c_void = libc::malloc(size); - if my_num.is_null() { - panic!("failed to allocate memory"); - } - let my_num2 = libc::memset(my_num, 1, size); - libc::free(my_num); - } -} diff --git a/tests/kani/Intrinsics/Math/Arith/powi.rs b/tests/kani/Intrinsics/Math/Arith/powi.rs new file mode 100644 index 000000000000..c7986d18a9ef --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/powi.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_powi32() { + let x: f32 = kani::any(); + kani::assume(x.is_normal()); + kani::assume(x >= 1e-19 || x <= -1e-19); + kani::assume(x <= 1.84e19 && x >= -1.84e19); + let x2 = x.powi(2); + assert!(x2 >= 0.0); +} + +#[kani::proof] +fn verify_powi64() { + let x: f64 = kani::any(); + kani::assume(x.is_normal()); + kani::assume(x >= 1e-153 || x <= -1e-153); + kani::assume(x <= 1.34e154 && x >= -1.34e154); + let x2 = x.powi(2); + assert!(x2 >= 0.0); +}