Enable log2*, log10* intrinsics (model-checking#3001)

Implemented in CBMC in diffblue/cbmc#8195.

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