Merge remote-tracking branch 'origin/main' into powi-intrinsics

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

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

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

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