Use floatbv_mod for floating-point remainder operator

The remainder (%) operator on floating-point types was incorrectly
using CBMC's integer 'mod' operation, which CBMC silently ignores for
floatbv types, producing incorrect verification results.

Use the floatbv_mod binary operator for float/double operands, which
correctly implements IEEE 754 fmod semantics matching Rust's % on
floating-point types.

Resolves #2669

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

cprover_bindings/src/goto_program/expr.rs

@@ -203,6 +203,7 @@ pub enum BinaryOperator {
     Bitxor,
     Div,
     Equal,
+    FloatbvMod,
     FloatbvRoundToIntegral,
     Ge,
     Gt,
@@ -1033,7 +1034,8 @@ impl Expr {
                     || (lhs.typ.is_pointer() && rhs.typ.is_integer())
             }
             // Arithmetic
-            Div | Mod | Mult => lhs.typ == rhs.typ && (lhs.typ.is_numeric() || lhs.typ.is_vector()),
+            Div | Mult => lhs.typ == rhs.typ && (lhs.typ.is_numeric() || lhs.typ.is_vector()),
+            Mod => lhs.typ == rhs.typ && (lhs.typ.is_integer() || lhs.typ.is_vector()),
             // Bitshifts
             Ashr | Lshr | Shl => {
                 lhs.typ.is_integer() && rhs.typ.is_integer()
@@ -1075,6 +1077,7 @@ impl Expr {
                     "vector comparison operators must be typechecked by `typecheck_vector_cmp_expr`"
                 )
             }
+            FloatbvMod => lhs.typ == rhs.typ && lhs.typ.is_floating_point(),
             FloatbvRoundToIntegral => lhs.typ.is_floating_point() && rhs.typ.is_integer(),
         }
     }
@@ -1090,7 +1093,7 @@ impl Expr {
                 }
             }
             // Arithmetic
-            Div | Mod | Mult | Plus => lhs.typ.clone(),
+            Div | FloatbvMod | Mod | Mult | Plus => lhs.typ.clone(),
             // Bitshifts
             Ashr | Lshr | Rol | Ror | Shl => lhs.typ.clone(),
             // Boolean ops
@@ -1186,8 +1189,12 @@ impl Expr {
     }
 
     /// `self % e`
+    /// `self % e`. For floating-point types, emits CBMC's `floatbv_mod` which
+    /// implements C `fmod` semantics (matching Rust's `%` on floats via LLVM `frem`).
+    /// Unlike other `floatbv_*` ops, `floatbv_mod` does not take a rounding mode
+    /// parameter — the result is exact per IEEE 754.
     pub fn rem(self, e: Expr) -> Expr {
-        self.binop(Mod, e)
+        if self.typ().is_floating_point() { self.binop(FloatbvMod, e) } else { self.binop(Mod, e) }
     }
 
     /// `self && e`

cprover_bindings/src/irep/irep_id.rs

@@ -565,6 +565,7 @@ pub enum IrepId {
     FloatbvMinus,
     FloatbvMult,
     FloatbvDiv,
+    FloatbvMod,
     FloatbvRem,
     FloatbvTypecast,
     CompoundLiteral,
@@ -1455,6 +1456,7 @@ impl IrepId {
             IrepId::FloatbvMinus => "floatbv_minus",
             IrepId::FloatbvMult => "floatbv_mult",
             IrepId::FloatbvDiv => "floatbv_div",
+            IrepId::FloatbvMod => "floatbv_mod",
             IrepId::FloatbvRem => "floatbv_rem",
             IrepId::FloatbvTypecast => "floatbv_typecast",
             IrepId::CompoundLiteral => "compound_literal",

cprover_bindings/src/irep/to_irep.rs

@@ -60,6 +60,7 @@ impl ToIrepId for BinaryOperator {
             BinaryOperator::Bitxor => IrepId::Bitxor,
             BinaryOperator::Div => IrepId::Div,
             BinaryOperator::Equal => IrepId::Equal,
+            BinaryOperator::FloatbvMod => IrepId::FloatbvMod,
             BinaryOperator::FloatbvRoundToIntegral => IrepId::FloatbvRoundToIntegral,
             BinaryOperator::Ge => IrepId::Ge,
             BinaryOperator::Gt => IrepId::Gt,

tests/kani/FloatingPoint/float_remainder.rs

@@ -0,0 +1,29 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Regression test for https://github.com/model-checking/kani/issues/2669
+//! Floating-point remainder (%) was producing incorrect results because
+//! CBMC's integer `mod` was used instead of `floatbv_mod`.
+
+/// Symbolic f32 remainder: verify the fmod invariant |result| < |divisor|.
+/// Inputs are i8-to-f32 casts, so both positive and negative values are
+/// exercised without introducing NaN/infinity edge cases.
+#[kani::proof]
+fn check_f32_rem() {
+    let dividend: f32 = kani::any::<i8>().into();
+    let divisor: f32 = kani::any::<i8>().into();
+    kani::assume(divisor != 0.0);
+    let result = dividend % divisor;
+    // fmod invariant: |result| < |divisor|
+    assert!(result.abs() < divisor.abs());
+}
+
+/// Symbolic f64 remainder: same fmod invariant for f64.
+#[kani::proof]
+fn check_f64_rem() {
+    let a: f64 = kani::any::<i8>().into();
+    let b: f64 = kani::any::<i8>().into();
+    kani::assume(b != 0.0);
+    let result = a % b;
+    assert!(result.abs() < b.abs());
+}