Merge branch 'main' into merge-queue

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 | |
@@ -187,8 +187,8 @@ nontemporal_store | No | |
 offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) |
 powf32 | Partial | Results are overapproximated |
 powf64 | Partial | Results are overapproximated |
-powif32 | No | |
-powif64 | No | |
+powif32 | Partial | Results are overapproximated |
+powif64 | Partial | Results are overapproximated |
 pref_align_of | Yes | |
 prefetch_read_data | No | |
 prefetch_read_instruction | No | |

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),
@@ -490,8 +490,8 @@ impl<'tcx> GotocCtx<'tcx> {
             ),
             "powf32" => codegen_simple_intrinsic!(Powf),
             "powf64" => codegen_simple_intrinsic!(Pow),
-            "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
-            "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)),
+            "powif32" => codegen_simple_intrinsic!(Powif),
+            "powif64" => codegen_simple_intrinsic!(Powi),
             "pref_align_of" => codegen_intrinsic_const!(),
             "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
             "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc),

tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs → tests/kani/Cast/cast_abstract_args_to_concrete.rs

@@ -1,9 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// https://github.com/model-checking/kani/issues/555
-// kani-flags: --no-undefined-function-checks
-
 // This regression test is in response to issue #135.
 // The type of the second parameter to powi is a `CInteger`, but
 // the type of `2` here is a `u32`. This test ensures that

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

tests/kani/Intrinsics/Math/Arith/powi.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn verify_powi32() {
+    let x: f32 = kani::any();
+    kani::assume(x.is_normal());
+    kani::assume(x >= 1e-19 || x <= -1e-19);
+    kani::assume(x <= 1.84e19 && x >= -1.84e19);
+    let x2 = x.powi(2);
+    assert!(x2 >= 0.0);
+}
+
+#[kani::proof]
+fn verify_powi64() {
+    let x: f64 = kani::any();
+    kani::assume(x.is_normal());
+    kani::assume(x >= 1e-153 || x <= -1e-153);
+    kani::assume(x <= 1.34e154 && x >= -1.34e154);
+    let x2 = x.powi(2);
+    assert!(x2 >= 0.0);
+}