From c7b315f22fa225132c87ab4051a1159b0b8ca08b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 15:18:34 +0200 Subject: [PATCH] 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); +}