Enable sqrt* intrinsics

Requires fixes in CBMC's sqrt* implementations.

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

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

@@ -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/Arith/sqrt.rs

@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn verify_sqrt32() {
+ let positive = 4.0_f32;
+ let negative = -4.0_f32;
+ let negative_zero = -0.0_f32;
+
+ let abs_difference = (positive.sqrt() - 2.0).abs();
+
+ assert!(abs_difference <= f32::EPSILON);
+ assert!(negative.sqrt().is_nan());
+ assert!(negative_zero.sqrt() == negative_zero);
+}
+
+#[kani::proof]
+fn verify_sqrt64() {
+ let positive = 4.0_f64;
+ let negative = -4.0_f64;
+ let negative_zero = -0.0_f64;
+
+ let abs_difference = (positive.sqrt() - 2.0).abs();
+
+ assert!(abs_difference <= 1e-10);
+ assert!(negative.sqrt().is_nan());
+ assert!(negative_zero.sqrt() == negative_zero);
+}