Check that fast math intrinsic results are finite

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

@@ -365,12 +365,24 @@ impl GotocCtx<'_, '_> {
             Intrinsic::FaddFast => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(plus);
-                self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
+                self.add_fast_math_finiteness_checks(
+                    intrinsic_str,
+                    fargs_clone,
+                    place,
+                    binop_stmt,
+                    span,
+                )
             }
             Intrinsic::FdivFast => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(div);
-                self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
+                self.add_fast_math_finiteness_checks(
+                    intrinsic_str,
+                    fargs_clone,
+                    place,
+                    binop_stmt,
+                    span,
+                )
             }
             Intrinsic::FloatToIntUnchecked => self.codegen_float_to_int_unchecked(
                 intrinsic_str,
@@ -387,13 +399,25 @@ impl GotocCtx<'_, '_> {
             Intrinsic::FmulFast => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(mul);
-                self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
+                self.add_fast_math_finiteness_checks(
+                    intrinsic_str,
+                    fargs_clone,
+                    place,
+                    binop_stmt,
+                    span,
+                )
             }
             Intrinsic::Forget => Stmt::skip(loc),
             Intrinsic::FsubFast => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(sub);
-                self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
+                self.add_fast_math_finiteness_checks(
+                    intrinsic_str,
+                    fargs_clone,
+                    place,
+                    binop_stmt,
+                    span,
+                )
             }
             Intrinsic::IsValStaticallyKnown => {
                 // Returning false is sound according do this intrinsic's documentation:
@@ -692,21 +716,24 @@ impl GotocCtx<'_, '_> {
     }
 
     // Fast math intrinsics for floating point operations like `fadd_fast`
-    // assume that their inputs are finite:
+    // require that both their inputs AND their result are finite:
     // https://doc.rust-lang.org/std/intrinsics/fn.fadd_fast.html
-    // This function adds assertions to the statement which performs the
-    // operation and checks for overflow failures.
-    fn add_finite_args_checks(
+    // This function adds assertions to check that the arguments are finite
+    // (precondition) and that the result is also finite (postcondition).
+    // Producing a non-finite result (e.g., overflow to infinity) is UB.
+    fn add_fast_math_finiteness_checks(
         &mut self,
         intrinsic: &str,
         mut fargs: Vec<Expr>,
+        place: &Place,
         stmt: Stmt,
         span: Span,
     ) -> Stmt {
         let arg1 = fargs.remove(0);
         let arg2 = fargs.remove(0);
         let msg1 = format!("first argument for {intrinsic} is finite");
         let msg2 = format!("second argument for {intrinsic} is finite");
+        let msg_result = format!("result of {intrinsic} is finite");
         let loc = self.codegen_span_stable(span);
         let finite_check1 = self.codegen_assert_assume(
             arg1.is_finite(),
@@ -720,7 +747,20 @@ impl GotocCtx<'_, '_> {
             msg2.as_str(),
             loc,
         );
-        Stmt::block(vec![finite_check1, finite_check2, stmt], loc)
+        // Check that the result is also finite (it's UB if the result overflows
+        // to infinity or produces NaN).
+        let result_expr = unwrap_or_return_codegen_unimplemented_stmt!(
+            self,
+            self.codegen_place_stable(place, loc)
+        )
+        .goto_expr;
+        let finite_check_result = self.codegen_assert_assume(
+            result_expr.is_finite(),
+            PropertyClass::FiniteCheck,
+            msg_result.as_str(),
+            loc,
+        );
+        Stmt::block(vec![finite_check1, finite_check2, stmt, finite_check_result], loc)
     }
 
     fn div_does_not_overflow(&self, a: Expr, b: Expr) -> Expr {

tests/kani/Intrinsics/FastMath/add_result_overflow_f32.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Regression test for: fadd_fast with finite inputs producing an infinite result.
+// The Rust documentation states that fast math intrinsics have UB if the result
+// is not finite (infinite or NaN), not just if the inputs are non-finite.
+// Previously, Kani only checked that inputs were finite, missing cases where
+// finite inputs produce an infinite result (e.g., f32::MAX + f32::MAX).
+
+// kani-verify-fail
+
+#![feature(core_intrinsics)]
+
+/// Check that fadd_fast detects overflow to infinity as UB.
+/// f32::MAX + f32::MAX overflows to infinity, which is UB for fadd_fast.
+#[kani::proof]
+fn fadd_fast_result_overflow_f32() {
+    let a = f32::MAX;
+    let _r = unsafe { core::intrinsics::fadd_fast(a, a) };
+}

tests/kani/Intrinsics/FastMath/div_result_overflow_f32.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Regression test for: fdiv_fast with finite inputs producing an infinite result.
+// The Rust documentation states that fast math intrinsics have UB if the result
+// is not finite (infinite or NaN), not just if the inputs are non-finite.
+// Previously, Kani only checked that inputs were finite, missing cases where
+// finite inputs produce an infinite result (e.g., f32::MAX / f32::MIN_POSITIVE).
+
+// kani-verify-fail
+
+#![feature(core_intrinsics)]
+
+/// Check that fdiv_fast detects overflow to infinity as UB.
+/// f32::MAX / f32::MIN_POSITIVE overflows to infinity, which is UB for fdiv_fast.
+#[kani::proof]
+fn fdiv_fast_result_overflow_f32() {
+    let a = f32::MAX;
+    let b = f32::MIN_POSITIVE;
+    let _r = unsafe { core::intrinsics::fdiv_fast(a, b) };
+}

tests/kani/Intrinsics/FastMath/mul_result_overflow_f32.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Regression test for: fmul_fast with finite inputs producing an infinite result.
+// The Rust documentation states that fast math intrinsics have UB if the result
+// is not finite (infinite or NaN), not just if the inputs are non-finite.
+// Previously, Kani only checked that inputs were finite, missing cases where
+// finite inputs produce an infinite result (e.g., f32::MAX * 2.0).
+
+// kani-verify-fail
+
+#![feature(core_intrinsics)]
+
+/// Check that fmul_fast detects overflow to infinity as UB.
+/// f32::MAX * 2.0 overflows to infinity, which is UB for fmul_fast.
+#[kani::proof]
+fn fmul_fast_result_overflow_f32() {
+    let a = f32::MAX;
+    let b = 2.0f32;
+    let _r = unsafe { core::intrinsics::fmul_fast(a, b) };
+}

tests/kani/Intrinsics/FastMath/sub_result_overflow_f32.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Regression test for: fsub_fast with finite inputs producing an infinite result.
+// The Rust documentation states that fast math intrinsics have UB if the result
+// is not finite (infinite or NaN), not just if the inputs are non-finite.
+// Previously, Kani only checked that inputs were finite, missing cases where
+// finite inputs produce an infinite result (e.g., (-f32::MAX) - f32::MAX).
+
+// kani-verify-fail
+
+#![feature(core_intrinsics)]
+
+/// Check that fsub_fast detects overflow to negative infinity as UB.
+/// (-f32::MAX) - f32::MAX overflows to negative infinity, which is UB for fsub_fast.
+#[kani::proof]
+fn fsub_fast_result_overflow_f32() {
+    let a = -f32::MAX;
+    let b = f32::MAX;
+    let _r = unsafe { core::intrinsics::fsub_fast(a, b) };
+}

tests/kani/Pointers/wrapping_add_not_ub.rs

@@ -0,0 +1,42 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Regression test: ptr.wrapping_add(usize::MAX) should not be flagged as UB
+// under default settings. wrapping_add is explicitly defined in Rust as
+// performing wrapping pointer arithmetic, which is always safe (though the
+// resulting pointer may not be dereferenceable).
+//
+// Note: With --extra-pointer-checks (unstable), CBMC's --pointer-overflow-check
+// may produce a false positive for this case. This is a known limitation of
+// the unstable feature.
+
+/// Verify that wrapping_add with extreme offsets is not UB.
+#[kani::proof]
+fn pointer_wrapping_add_max() {
+    let data = [0u8; 1];
+    let ptr = data.as_ptr();
+    // wrapping_add is always safe, even with extreme values
+    let wrapped = ptr.wrapping_add(usize::MAX);
+    // The wrapped pointer should differ from the original
+    // (unless the address space wraps perfectly, which is platform-dependent)
+    let _ = wrapped;
+}
+
+/// Verify that wrapping_sub with extreme offsets is not UB.
+#[kani::proof]
+fn pointer_wrapping_sub_max() {
+    let data = [0u8; 1];
+    let ptr = data.as_ptr();
+    let wrapped = ptr.wrapping_sub(usize::MAX);
+    let _ = wrapped;
+}
+
+/// Verify wrapping_add with a moderate offset beyond allocation bounds.
+#[kani::proof]
+fn pointer_wrapping_add_beyond_alloc() {
+    let data = [0u8; 4];
+    let ptr = data.as_ptr();
+    // Offset beyond allocation but within address space — still not UB for wrapping_add
+    let wrapped = ptr.wrapping_add(1000);
+    let _ = wrapped;
+}