From f08a3e99296f669055fa61c640ac916a0033fc31 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 19:56:10 +0100 Subject: [PATCH] Enable powf*, exp*, log* intrinsics (#2996) CBMC provides approximating implementations of these. Resolves: #2966 --- docs/src/rust-feature-support/intrinsics.md | 16 +++++----- .../codegen/intrinsic.rs | 16 +++++----- tests/kani/Intrinsics/Math/Arith/exp.rs | 24 +++++++++++++++ tests/kani/Intrinsics/Math/Arith/exp2.rs | 22 ++++++++++++++ tests/kani/Intrinsics/Math/Arith/log.rs | 22 ++++++++++++++ tests/kani/Intrinsics/Math/Arith/powf32.rs | 15 ++++++++++ tests/kani/Intrinsics/Math/Arith/powf64.rs | 30 +++++++++++++++++++ 7 files changed, 129 insertions(+), 16 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Arith/exp.rs create mode 100644 tests/kani/Intrinsics/Math/Arith/exp2.rs create mode 100644 tests/kani/Intrinsics/Math/Arith/log.rs create mode 100644 tests/kani/Intrinsics/Math/Arith/powf32.rs create mode 100644 tests/kani/Intrinsics/Math/Arith/powf64.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 0705d3b00f1b..7df1a093943f 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -148,10 +148,10 @@ cttz_nonzero | Yes | | discriminant_value | Yes | | drop_in_place | No | | exact_div | Yes | | -exp2f32 | No | | -exp2f64 | No | | -expf32 | No | | -expf64 | No | | +exp2f32 | Partial | Results are overapproximated | +exp2f64 | Partial | Results are overapproximated | +expf32 | Partial | Results are overapproximated | +expf64 | Partial | Results are overapproximated | fabsf32 | Yes | | fabsf64 | Yes | | fadd_fast | Yes | | @@ -170,8 +170,8 @@ log10f32 | No | | log10f64 | No | | log2f32 | No | | log2f64 | No | | -logf32 | No | | -logf64 | No | | +logf32 | Partial | Results are overapproximated | +logf64 | Partial | Results are overapproximated | maxnumf32 | Yes | | maxnumf64 | Yes | | min_align_of | Yes | | @@ -185,8 +185,8 @@ nearbyintf64 | Yes | | needs_drop | Yes | | nontemporal_store | No | | offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) | -powf32 | No | | -powf64 | No | | +powf32 | Partial | Results are overapproximated | +powf64 | Partial | Results are overapproximated | powif32 | No | | powif64 | No | | pref_align_of | 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..0709682afa65 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -420,10 +420,10 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_expr_to_place_stable(place, e) } "exact_div" => self.codegen_exact_div(fargs, place, loc), - "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)), + "exp2f32" => codegen_simple_intrinsic!(Exp2f), + "exp2f64" => codegen_simple_intrinsic!(Exp2), + "expf32" => codegen_simple_intrinsic!(Expf), + "expf64" => codegen_simple_intrinsic!(Exp), "fabsf32" => codegen_simple_intrinsic!(Fabsf), "fabsf64" => codegen_simple_intrinsic!(Fabs), "fadd_fast" => { @@ -456,8 +456,8 @@ impl<'tcx> GotocCtx<'tcx> { "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)), + "logf32" => codegen_simple_intrinsic!(Logf), + "logf64" => codegen_simple_intrinsic!(Log), "maxnumf32" => codegen_simple_intrinsic!(Fmaxf), "maxnumf64" => codegen_simple_intrinsic!(Fmax), "min_align_of" => codegen_intrinsic_const!(), @@ -474,8 +474,8 @@ impl<'tcx> GotocCtx<'tcx> { "offset" => unreachable!( "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`" ), - "powf32" => unstable_codegen!(codegen_simple_intrinsic!(Powf)), - "powf64" => unstable_codegen!(codegen_simple_intrinsic!(Pow)), + "powf32" => codegen_simple_intrinsic!(Powf), + "powf64" => codegen_simple_intrinsic!(Pow), "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)), "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)), "pref_align_of" => codegen_intrinsic_const!(), diff --git a/tests/kani/Intrinsics/Math/Arith/exp.rs b/tests/kani/Intrinsics/Math/Arith/exp.rs new file mode 100644 index 000000000000..4f26fc5b5b96 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/exp.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `expf32` and `expf64` intrinsics, which in turn invoke +// functions modelled in CBMC's math library. These models use approximations as documented in +// CBMC's source code: https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. + +#[kani::proof] +fn verify_exp32() { + let two = 2.0_f32; + let two_sq = std::f32::consts::E * std::f32::consts::E; + let two_exp = two.exp(); + + assert!((two_sq - two_exp).abs() <= 0.192); +} + +#[kani::proof] +fn verify_exp64() { + let two = 2.0_f64; + let two_sq = std::f64::consts::E * std::f64::consts::E; + let two_exp = two.exp(); + + assert!((two_sq - two_exp).abs() <= 0.192); +} diff --git a/tests/kani/Intrinsics/Math/Arith/exp2.rs b/tests/kani/Intrinsics/Math/Arith/exp2.rs new file mode 100644 index 000000000000..91244a383a0a --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/exp2.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `exp2f32` and `exp2f64` intrinsics, which in turn invoke +// functions modelled in CBMC's math library. These models use approximations as documented in +// CBMC's source code: https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. + +#[kani::proof] +fn verify_exp2_32() { + let two = 2.0_f32; + let two_two = two.exp2(); + + assert!((two_two - 4.0).abs() <= 0.345); +} + +#[kani::proof] +fn verify_exp2_64() { + let two = 2.0_f64; + let two_two = two.exp2(); + + assert!((two_two - 4.0).abs() <= 0.345); +} diff --git a/tests/kani/Intrinsics/Math/Arith/log.rs b/tests/kani/Intrinsics/Math/Arith/log.rs new file mode 100644 index 000000000000..1185e8ae4d82 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/log.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `logf32` and `logf64` intrinsics, which in turn invoke +// functions modelled in CBMC's math library. These models use approximations as documented in +// CBMC's source code: https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. + +#[kani::proof] +fn verify_logf32() { + let e = std::f32::consts::E; + let e_log = e.ln(); + + assert!((e_log - 1.0).abs() <= 0.058); +} + +#[kani::proof] +fn verify_logf64() { + let e = std::f64::consts::E; + let e_log = e.ln(); + + assert!((e_log - 1.0).abs() <= 0.058); +} diff --git a/tests/kani/Intrinsics/Math/Arith/powf32.rs b/tests/kani/Intrinsics/Math/Arith/powf32.rs new file mode 100644 index 000000000000..f289171b64b8 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/powf32.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `powf32` intrinsic, which in turn invoke functions modelled in +// CBMC's math library. These models use approximations as documented in CBMC's source code: +// https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. + +#[kani::proof] +fn verify_pow() { + let x: f32 = kani::any(); + kani::assume(x.is_normal()); + kani::assume(x > 1.0 && x < u16::MAX.into()); + let x2 = x.powf(2.0); + assert!(x2 >= 0.0); +} diff --git a/tests/kani/Intrinsics/Math/Arith/powf64.rs b/tests/kani/Intrinsics/Math/Arith/powf64.rs new file mode 100644 index 000000000000..e80ad777c09a --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/powf64.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test will trigger use of the `powf64` intrinsic, which in turn invoke functions modelled in +// CBMC's math library. These models use approximations as documented in CBMC's source code: +// https://github.com/diffblue/cbmc/blob/develop/src/ansi-c/library/math.c. + +pub fn f(a: u64) -> u64 { + const C: f64 = 0.618; + (a as f64).powf(C) as u64 +} + +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::proof] + fn verify_f() { + const LIMIT: u64 = 10; + let x: u64 = kani::any(); + let y: u64 = kani::any(); + // outside these limits our approximation may yield spurious results + kani::assume(x > LIMIT && x < LIMIT * 3); + kani::assume(y > LIMIT && y < LIMIT * 3); + kani::assume(x > y); + let x_ = f(x); + let y_ = f(y); + assert!(x_ >= y_); + } +}