Audit for truncf* (rust-lang#1250)

Author: adpaco-aws

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

@@ -631,12 +631,8 @@ impl<'tcx> GotocCtx<'tcx> {
             "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)),
             "sub_with_overflow" => codegen_op_with_overflow!(sub_overflow),
             "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, p),
-            "truncf32" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
-            "truncf64" => codegen_unimplemented_intrinsic!(
-                "https://github.com/model-checking/kani/issues/1025"
-            ),
+            "truncf32" => codegen_simple_intrinsic!(Truncf),
+            "truncf64" => codegen_simple_intrinsic!(Trunc),
             "try" => {
                 codegen_unimplemented_intrinsic!(
                     "https://github.com/model-checking/kani/issues/267"

tests/kani/Intrinsics/Math/Rounding/Trunc/truncf32.rs

@@ -0,0 +1,61 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `truncf32` does return:
+//  * The integral part of the argument for some concrete cases.
+//  * A value that is closer to zero 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::truncf32;
+
+#[kani::proof]
+fn test_one() {
+    let one = 1.0;
+    let trunc_res = unsafe { truncf32(one) };
+    assert!(trunc_res == 1.0);
+}
+
+#[kani::proof]
+fn test_one_frac() {
+    let one_frac = 1.9;
+    let trunc_res = unsafe { truncf32(one_frac) };
+    assert!(trunc_res == 1.0);
+}
+
+#[kani::proof]
+fn test_conc() {
+    let conc = -42.6;
+    let trunc_res = unsafe { truncf32(conc) };
+    assert!(trunc_res == -42.0);
+}
+
+#[kani::proof]
+fn test_conc_sci() {
+    let conc = 5.4e-2;
+    let trunc_res = unsafe { truncf32(conc) };
+    assert!(trunc_res == 0.0);
+}
+
+#[kani::proof]
+fn test_towards_zero() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    let trunc_res = unsafe { truncf32(x) };
+    if x.is_sign_positive() {
+        assert!(trunc_res <= x);
+    } else {
+        assert!(trunc_res >= x);
+    }
+}
+
+#[kani::proof]
+fn test_diff_one() {
+    let x: f32 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let trunc_res = unsafe { truncf32(x) };
+    let diff = (x - trunc_res).abs();
+    assert!(diff < 1.0);
+    assert!(diff >= 0.0);
+}

tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs

@@ -0,0 +1,61 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `truncf64` does return:
+//  * The integral part of the argument for some concrete cases.
+//  * A value that is closer to zero 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::truncf64;
+
+#[kani::proof]
+fn test_one() {
+    let one = 1.0;
+    let trunc_res = unsafe { truncf64(one) };
+    assert!(trunc_res == 1.0);
+}
+
+#[kani::proof]
+fn test_one_frac() {
+    let one_frac = 1.9;
+    let trunc_res = unsafe { truncf64(one_frac) };
+    assert!(trunc_res == 1.0);
+}
+
+#[kani::proof]
+fn test_conc() {
+    let conc = -42.6;
+    let trunc_res = unsafe { truncf64(conc) };
+    assert!(trunc_res == -42.0);
+}
+
+#[kani::proof]
+fn test_conc_sci() {
+    let conc = 5.4e-2;
+    let trunc_res = unsafe { truncf64(conc) };
+    assert!(trunc_res == 0.0);
+}
+
+#[kani::proof]
+fn test_towards_zero() {
+    let x: f64 = kani::any();
+    kani::assume(!x.is_nan());
+    let trunc_res = unsafe { truncf64(x) };
+    if x.is_sign_positive() {
+        assert!(trunc_res <= x);
+    } else {
+        assert!(trunc_res >= x);
+    }
+}
+
+#[kani::proof]
+fn test_diff_one() {
+    let x: f64 = kani::any();
+    kani::assume(!x.is_nan());
+    kani::assume(!x.is_infinite());
+    let trunc_res = unsafe { truncf64(x) };
+    let diff = (x - trunc_res).abs();
+    assert!(diff < 1.0);
+    assert!(diff >= 0.0);
+}