Enable powf*, exp*, log* intrinsics

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,10 +185,10 @@ 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 | |
-powif32 | No | |
-powif64 | No | |
+powf32 | Partial | Results are overapproximated |
+powf64 | Partial | Results are overapproximated |
+powif32 | Partial | Results are overapproximated |
+powif64 | Partial | Results are overapproximated |
 pref_align_of | Yes | |
 prefetch_read_data | No | |
 prefetch_read_instruction | No | |
@@ -211,8 +211,8 @@ sinf32 | Partial | Results are overapproximated; [this test](https://github.com/
 sinf64 | Partial | Results are overapproximated; [this test](https://github.com/model-checking/kani/blob/main/tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs) explains how |
 size_of | Yes | |
 size_of_val | Yes | |
-sqrtf32 | No | |
-sqrtf64 | No | |
+sqrtf32 | Partial | Results are overapproximated |
+sqrtf64 | Partial | Results are overapproximated |
 sub_with_overflow | Yes | |
 transmute | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/nomicon/transmutes.html) |
 truncf32 | 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,10 +474,10 @@ 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)),
-            "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
-            "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)),
+            "powf32" => codegen_simple_intrinsic!(Powf),
+            "powf64" => codegen_simple_intrinsic!(Pow),
+            "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),
             "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc),
@@ -555,8 +555,8 @@ impl<'tcx> GotocCtx<'tcx> {
             "simd_xor" => codegen_intrinsic_binop!(bitxor),
             "size_of" => unreachable!(),
             "size_of_val" => codegen_size_align!(size),
-            "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)),
-            "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)),
+            "sqrtf32" => codegen_simple_intrinsic!(Sqrtf),
+            "sqrtf64" => codegen_simple_intrinsic!(Sqrt),
             "sub_with_overflow" => self.codegen_op_with_overflow(
                 BinaryOperator::OverflowResultMinus,
                 fargs,

tests/kani/Intrinsics/Math/powf64.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+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_);
+    }
+}