Enable powif* intrinsics

docs/src/rust-feature-support/intrinsics.md

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

@@ -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/Intrinsics/Math/Arith/powi.rs

@@ -0,0 +1,18 @@
+// 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());
+    let x2 = x.powi(2);
+    assert!(x2 >= 0.0);
+}
+
+#[kani::proof]
+fn verify_powi64() {
+    let x: f64 = kani::any();
+    kani::assume(x.is_normal());
+    let x2 = x.powi(2);
+    assert!(x2 >= 0.0);
+}