From 3fa6a18f69cb86c30ec9282a222be163168d5679 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 10:44:51 +0000 Subject: [PATCH 1/2] Enable log2*, log10* intrinsics Requires support in CBMC. --- docs/src/rust-feature-support/intrinsics.md | 8 +++---- .../codegen/intrinsic.rs | 8 +++---- tests/kani/Intrinsics/Math/Arith/log10.rs | 22 +++++++++++++++++++ tests/kani/Intrinsics/Math/Arith/log2.rs | 22 +++++++++++++++++++ 4 files changed, 52 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 0705d3b00f1b..bee64aff32d0 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 | No | | logf64 | No | | 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 3412cba290d2..16f9aa2a1580 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -452,10 +452,10 @@ impl<'tcx> GotocCtx<'tcx> { self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) } "likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0)), - "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" => unstable_codegen!(codegen_simple_intrinsic!(Logf)), "logf64" => unstable_codegen!(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..2d641cde1bcb --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/log10.rs @@ -0,0 +1,22 @@ +// 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(); + + assert!(abs_difference <= f32::EPSILON); +} + +#[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 < 1e-10); +} diff --git a/tests/kani/Intrinsics/Math/Arith/log2.rs b/tests/kani/Intrinsics/Math/Arith/log2.rs new file mode 100644 index 000000000000..be09bb928d23 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/log2.rs @@ -0,0 +1,22 @@ +// 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(); + + assert!(abs_difference <= f32::EPSILON); +} + +#[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 < 1e-10); +} From 9c567a792cac59e142fbe254702d8348c184d8ad Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 12:21:42 +0000 Subject: [PATCH 2/2] Adjust precision --- tests/kani/Intrinsics/Math/Arith/log10.rs | 5 +++-- tests/kani/Intrinsics/Math/Arith/log2.rs | 5 +++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/tests/kani/Intrinsics/Math/Arith/log10.rs b/tests/kani/Intrinsics/Math/Arith/log10.rs index 2d641cde1bcb..4670c72cfeb3 100644 --- a/tests/kani/Intrinsics/Math/Arith/log10.rs +++ b/tests/kani/Intrinsics/Math/Arith/log10.rs @@ -8,7 +8,8 @@ fn verify_log10_32() { // log10(10) - 1 == 0 let abs_difference = (ten.log10() - 1.0).abs(); - assert!(abs_difference <= f32::EPSILON); + // should be <= f32::EPSILON, but CBMC's approximation of log10 makes results less precise + assert!(abs_difference <= 0.03); } #[kani::proof] @@ -18,5 +19,5 @@ fn verify_log10_64() { // log10(100) - 2 == 0 let abs_difference = (hundred.log10() - 2.0).abs(); - assert!(abs_difference < 1e-10); + assert!(abs_difference < 0.03); } diff --git a/tests/kani/Intrinsics/Math/Arith/log2.rs b/tests/kani/Intrinsics/Math/Arith/log2.rs index be09bb928d23..52153f8b368a 100644 --- a/tests/kani/Intrinsics/Math/Arith/log2.rs +++ b/tests/kani/Intrinsics/Math/Arith/log2.rs @@ -8,7 +8,8 @@ fn verify_log2_32() { // log2(2) - 1 == 0 let abs_difference = (two.log2() - 1.0).abs(); - assert!(abs_difference <= f32::EPSILON); + // should be <= f32::EPSILON, but CBMC's approximation of log2 makes results less precise + assert!(abs_difference <= 0.09); } #[kani::proof] @@ -18,5 +19,5 @@ fn verify_log2_64() { // log2(4) - 2 == 0 let abs_difference = (four.log2() - 2.0).abs(); - assert!(abs_difference < 1e-10); + assert!(abs_difference < 0.09); }