No sqrt just yet

tautschnig · Feb 7, 2024 · fa2ac24 · fa2ac24
1 parent 9fed6e5
commit fa2ac24
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 34 deletions.
diff --git a/docs/src/rust-feature-support/intrinsics.md b/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 | Partial | Results are overapproximated |
-powif64 | Partial | Results are overapproximated |
+powif32 | No | |
+powif64 | No | |
 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 | Partial | Results are overapproximated |
-sqrtf64 | Partial | Results are overapproximated |
+sqrtf32 | No | |
+sqrtf64 | No | |
 sub_with_overflow | Yes | |
 transmute | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/nomicon/transmutes.html) |
 truncf32 | Yes | |

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -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" => codegen_simple_intrinsic!(Sqrtf),
-            "sqrtf64" => codegen_simple_intrinsic!(Sqrt),
+            "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)),
+            "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)),
             "sub_with_overflow" => self.codegen_op_with_overflow(
                 BinaryOperator::OverflowResultMinus,
                 fargs,

diff --git a/tests/kani/Intrinsics/Math/Arith/sqrt.rs b/tests/kani/Intrinsics/Math/Arith/sqrt.rs