Audit for maxnumf* and minnumf* intrinsics (rust-lang#1248)

* Enable `maxnumfXX` and `minnumfXX` intrinsics

* Add tests for minnum and maxnum

* Assert against expected result instead of NaN check

* Move expected check to `test_one_nan` in `minnumf64.rs`

Author: adpaco-aws

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

@@ -548,12 +548,12 @@ impl<'tcx> GotocCtx<'tcx> {
             "log2f64" => unstable_codegen!(codegen_simple_intrinsic!(Log2)),
             "logf32" => unstable_codegen!(codegen_simple_intrinsic!(Logf)),
             "logf64" => unstable_codegen!(codegen_simple_intrinsic!(Log)),
-            "maxnumf32" => unstable_codegen!(codegen_simple_intrinsic!(Fmaxf)),
-            "maxnumf64" => unstable_codegen!(codegen_simple_intrinsic!(Fmax)),
+            "maxnumf32" => codegen_simple_intrinsic!(Fmaxf),
+            "maxnumf64" => codegen_simple_intrinsic!(Fmax),
             "min_align_of" => codegen_intrinsic_const!(),
             "min_align_of_val" => codegen_size_align!(align),
-            "minnumf32" => unstable_codegen!(codegen_simple_intrinsic!(Fminf)),
-            "minnumf64" => unstable_codegen!(codegen_simple_intrinsic!(Fmin)),
+            "minnumf32" => codegen_simple_intrinsic!(Fminf),
+            "minnumf64" => codegen_simple_intrinsic!(Fmin),
             "mul_with_overflow" => codegen_op_with_overflow!(mul_overflow),
             "nearbyintf32" => codegen_unimplemented_intrinsic!(
                 "https://github.com/model-checking/kani/issues/1025"

tests/kani/Intrinsics/MaxNum/maxnumf32_fixme.rs

@@ -0,0 +1,55 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `maxnumf32` returns the minimum of two values, except in the
+// following cases:
+//  * If one of the arguments is NaN, the other arguments is returned.
+//  * If both arguments are NaN, NaN is returned.
+#![feature(core_intrinsics)]
+
+// Note: All test cases are failing with the following error:
+// ```
+// Check X: fmaxf.assertion.1
+//          - Status: FAILURE
+//          - Description: "Function with missing definition is unreachable"
+//          - Location: <builtin-library-fmaxf> in function fmaxf
+// ```
+// This is because the `fmaxf` definition is not being found, either because
+// Kani does not produce the right expression (which is strange, because it's
+// doing the same for similar expressions and they work) or CBMC is not picking
+// it for some reason.
+// Tracked in https://github.com/model-checking/kani/issues/1025
+#[kani::proof]
+fn test_general() {
+    let x: f32 = kani::any();
+    let y: f32 = kani::any();
+    kani::assume(!x.is_nan() && !y.is_nan());
+    let res = std::intrinsics::maxnumf32(x, y);
+    if x > y {
+        assert!(res == x);
+    } else {
+        assert!(res == y);
+    }
+}
+
+#[kani::proof]
+fn test_one_nan() {
+    let x: f32 = kani::any();
+    let y: f32 = kani::any();
+    kani::assume((x.is_nan() && !y.is_nan()) || (!x.is_nan() && y.is_nan()));
+    let res = std::intrinsics::maxnumf32(x, y);
+    if x.is_nan() {
+        assert!(res == y);
+    } else {
+        assert!(res == x);
+    }
+}
+
+#[kani::proof]
+fn test_both_nan() {
+    let x: f32 = kani::any();
+    let y: f32 = kani::any();
+    kani::assume(x.is_nan() && y.is_nan());
+    let res = std::intrinsics::maxnumf32(x, y);
+    assert!(res.is_nan());
+}

tests/kani/Intrinsics/MaxNum/maxnumf64.rs

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `maxnumf64` returns the minimum of two values, except in the
+// following cases:
+//  * If one of the arguments is NaN, the other arguments is returned.
+//  * If both arguments are NaN, NaN is returned.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn test_general() {
+    let x: f64 = kani::any();
+    let y: f64 = kani::any();
+    kani::assume(!x.is_nan() && !y.is_nan());
+    let res = std::intrinsics::maxnumf64(x, y);
+    if x > y {
+        assert!(res == x);
+    } else {
+        assert!(res == y);
+    }
+}
+
+#[kani::proof]
+fn test_one_nan() {
+    let x: f64 = kani::any();
+    let y: f64 = kani::any();
+    kani::assume((x.is_nan() && !y.is_nan()) || (!x.is_nan() && y.is_nan()));
+    let res = std::intrinsics::maxnumf64(x, y);
+    if x.is_nan() {
+        assert!(res == y);
+    } else {
+        assert!(res == x);
+    }
+}
+
+#[kani::proof]
+fn test_both_nan() {
+    let x: f64 = kani::any();
+    let y: f64 = kani::any();
+    kani::assume(x.is_nan() && y.is_nan());
+    let res = std::intrinsics::maxnumf64(x, y);
+    assert!(res.is_nan());
+}

tests/kani/Intrinsics/MinNum/minnumf32.rs

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `minnumf32` returns the minimum of two values, except in the
+// following cases:
+//  * If one of the arguments is NaN, the other arguments is returned.
+//  * If both arguments are NaN, NaN is returned.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn test_general() {
+    let x: f32 = kani::any();
+    let y: f32 = kani::any();
+    kani::assume(!x.is_nan() && !y.is_nan());
+    let res = std::intrinsics::minnumf32(x, y);
+    if x < y {
+        assert!(res == x);
+    } else {
+        assert!(res == y);
+    }
+}
+
+#[kani::proof]
+fn test_one_nan() {
+    let x: f32 = kani::any();
+    let y: f32 = kani::any();
+    kani::assume((x.is_nan() && !y.is_nan()) || (!x.is_nan() && y.is_nan()));
+    let res = std::intrinsics::minnumf32(x, y);
+    if x.is_nan() {
+        assert!(res == y);
+    } else {
+        assert!(res == x);
+    }
+}
+
+#[kani::proof]
+fn test_both_nan() {
+    let x: f32 = kani::any();
+    let y: f32 = kani::any();
+    kani::assume(x.is_nan() && y.is_nan());
+    let res = std::intrinsics::minnumf32(x, y);
+    assert!(res.is_nan());
+}

tests/kani/Intrinsics/MinNum/minnumf64.rs

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `minnumf64` returns the minimum of two values, except in the
+// following cases:
+//  * If one of the arguments is NaN, the other arguments is returned.
+//  * If both arguments are NaN, NaN is returned.
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn test_general() {
+    let x: f64 = kani::any();
+    let y: f64 = kani::any();
+    kani::assume(!x.is_nan() && !y.is_nan());
+    let res = std::intrinsics::minnumf64(x, y);
+    if x < y {
+        assert!(res == x);
+    } else {
+        assert!(res == y);
+    }
+}
+
+#[kani::proof]
+fn test_one_nan() {
+    let x: f64 = kani::any();
+    let y: f64 = kani::any();
+    kani::assume((x.is_nan() && !y.is_nan()) || (!x.is_nan() && y.is_nan()));
+    let res = std::intrinsics::minnumf64(x, y);
+    if x.is_nan() {
+        assert!(res == y);
+    } else {
+        assert!(res == x);
+    }
+}
+
+#[kani::proof]
+fn test_both_nan() {
+    let x: f64 = kani::any();
+    let y: f64 = kani::any();
+    kani::assume(x.is_nan() && y.is_nan());
+    let res = std::intrinsics::minnumf64(x, y);
+    assert!(res.is_nan());
+}