Enable powf*, exp*, log* intrinsics (#2996)

CBMC provides approximating implementations of these.

Resolves: #2966

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 | |

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!(),

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);
+}

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);
+}

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);
+}

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);
+}

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_);
+ }
+}