Audit for ceilf* (rust-lang#1262)

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -481,12 +481,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     "https://github.com/model-checking/kani/issues/374"
                 )
             }
-            "ceilf32" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
-            "ceilf64" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
+            "ceilf32" => codegen_simple_intrinsic!(Ceilf),
+            "ceilf64" => codegen_simple_intrinsic!(Ceil),
             "copy" => self.codegen_copy(intrinsic, false, fargs, farg_types, Some(p), loc),
             "copy_nonoverlapping" => unreachable!(
                 "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`"

tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf32.rs

@@ -0,0 +1,65 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `ceilf32` does return:
+//  * The nearest integer above the argument for some concrete cases.
+//  * A value that is closer to infinity in all cases.
+//  * A value such that the difference between it and the argument is between
+//    zero and one.
+#![feature(core_intrinsics)]
+use std::intrinsics::ceilf32;
+
+#[kani::proof]
+fn test_one() {
+    let one = 1.0;
+    let ceil_res = unsafe { ceilf32(one) };
+    assert!(ceil_res == 1.0);
+}
+
+#[kani::proof]
+fn test_one_frac() {
+    let one_frac = 1.2;
+    let ceil_res = unsafe { ceilf32(one_frac) };
+    assert!(ceil_res == 2.0);
+}
+
+#[kani::proof]
+fn test_one_neg() {
+    let one_neg = -1.8;
+    let ceil_res = unsafe { ceilf32(one_neg) };
+    assert!(ceil_res == -1.0);
+}
+
+#[kani::proof]
+fn test_conc() {
+    let conc = -42.6;
+    let ceil_res = unsafe { ceilf32(conc) };
+    assert!(ceil_res == -42.0);
+}
+
+#[kani::proof]
+fn test_conc_sci() {
+    let conc = 5.4e-2;
+    let ceil_res = unsafe { ceilf32(conc) };
+    assert!(ceil_res == 1.0);
+}
+
+#[kani::proof]
+fn test_towards_inf() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    let ceil_res = unsafe { ceilf32(x) };
+    assert!(ceil_res >= x);
+}
+
+#[kani::proof]
+fn test_diff_one() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let ceil_res = unsafe { ceilf32(x) };
+    let diff = (x - ceil_res).abs();
+    // `diff` can be 1.0 if `x` is very small (e.g., 1.840879e-35)
+    assert!(diff <= 1.0);
+    assert!(diff >= 0.0);
+}

tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs

@@ -0,0 +1,65 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `ceilf64` does return:
+//  * The nearest integer above the argument for some concrete cases.
+//  * A value that is closer to infinity in all cases.
+//  * A value such that the difference between it and the argument is between
+//    zero and one.
+#![feature(core_intrinsics)]
+use std::intrinsics::ceilf64;
+
+#[kani::proof]
+fn test_one() {
+    let one = 1.0;
+    let ceil_res = unsafe { ceilf64(one) };
+    assert!(ceil_res == 1.0);
+}
+
+#[kani::proof]
+fn test_one_frac() {
+    let one_frac = 1.2;
+    let ceil_res = unsafe { ceilf64(one_frac) };
+    assert!(ceil_res == 2.0);
+}
+
+#[kani::proof]
+fn test_one_neg() {
+    let one_neg = -1.8;
+    let ceil_res = unsafe { ceilf64(one_neg) };
+    assert!(ceil_res == -1.0);
+}
+
+#[kani::proof]
+fn test_conc() {
+    let conc = -42.6;
+    let ceil_res = unsafe { ceilf64(conc) };
+    assert!(ceil_res == -42.0);
+}
+
+#[kani::proof]
+fn test_conc_sci() {
+    let conc = 5.4e-2;
+    let ceil_res = unsafe { ceilf64(conc) };
+    assert!(ceil_res == 1.0);
+}
+
+#[kani::proof]
+fn test_towards_inf() {
+    let x: f64 = kani::any();
+    kani::assume(!x.is_nan());
+    let ceil_res = unsafe { ceilf64(x) };
+    assert!(ceil_res >= x);
+}
+
+#[kani::proof]
+fn test_diff_one() {
+    let x: f64 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let ceil_res = unsafe { ceilf64(x) };
+    let diff = (x - ceil_res).abs();
+    // `diff` can be 1.0 if `x` is very small (e.g., 5.220244e-54)
+    assert!(diff <= 1.0);
+    assert!(diff >= 0.0);
+}