Update CBMC dependency to 6.5.0

cprover_bindings/src/goto_program/builtin.rs

@@ -59,8 +59,6 @@ pub enum BuiltinFn {
     Rintf,
     Round,
     Roundf,
-    RoundToIntegralF,
-    RoundToIntegral,
     Sin,
     Sinf,
     Sqrt,
@@ -125,9 +123,6 @@ impl Display for BuiltinFn {
             Rintf => "rintf",
             Round => "round",
             Roundf => "roundf",
-            // TODO remove the sort_of prefix once we move up from CBMC 6.4.1
-            RoundToIntegralF => "__sort_of_CPROVER_round_to_integralf",
-            RoundToIntegral => "__sort_of_CPROVER_round_to_integral",
             Sin => "sin",
             Sinf => "sinf",
             Sqrt => "sqrt",
@@ -193,8 +188,6 @@ impl BuiltinFn {
             Rintf => vec![Type::float()],
             Round => vec![Type::double()],
             Roundf => vec![Type::float()],
-            RoundToIntegralF => vec![Type::c_int(), Type::float()],
-            RoundToIntegral => vec![Type::c_int(), Type::double()],
             Sin => vec![Type::double()],
             Sinf => vec![Type::float()],
             Sqrt => vec![Type::double()],
@@ -259,8 +252,6 @@ impl BuiltinFn {
             Rintf => Type::float(),
             Round => Type::double(),
             Roundf => Type::float(),
-            RoundToIntegralF => Type::float(),
-            RoundToIntegral => Type::double(),
             Sin => Type::double(),
             Sinf => Type::float(),
             Sqrt => Type::double(),
@@ -325,8 +316,6 @@ impl BuiltinFn {
             Rintf,
             Round,
             Roundf,
-            RoundToIntegralF,
-            RoundToIntegral,
             Sin,
             Sinf,
             Sqrt,

cprover_bindings/src/goto_program/expr.rs

@@ -190,6 +190,7 @@ pub enum BinaryOperator {
     Bitxor,
     Div,
     Equal,
+    FloatbvRoundToIntegral,
     Ge,
     Gt,
     IeeeFloatEqual,
@@ -1029,6 +1030,7 @@ impl Expr {
                     "vector comparison operators must be typechecked by `typecheck_vector_cmp_expr`"
                 )
             }
+            FloatbvRoundToIntegral => lhs.typ.is_floating_point() && rhs.typ.is_integer(),
         }
     }
 
@@ -1069,6 +1071,11 @@ impl Expr {
                     "return type for vector comparison operators depends on the place type"
                 )
             }
+            FloatbvRoundToIntegral => {
+                unreachable!(
+                    "return type for float-to-integer rounding operator depends on the place type"
+                )
+            }
         }
     }
 
@@ -1311,6 +1318,11 @@ impl Expr {
         let cmp = self.clone().gt(e.clone());
         cmp.ternary(self, e)
     }
+
+    /// floating-point to integer rounding
+    pub fn floatbv_round_to_integral(f: Expr, rm: Expr, ret_typ: Type) -> Expr {
+        expr!(BinOp { op: FloatbvRoundToIntegral, lhs: f, rhs: rm }, ret_typ)
+    }
 }
 
 /// Constructors for self operations

cprover_bindings/src/irep/irep_id.rs

@@ -835,6 +835,7 @@ pub enum IrepId {
     VectorLe,
     VectorGt,
     VectorLt,
+    FloatbvRoundToIntegral,
 }
 
 impl IrepId {
@@ -1717,6 +1718,7 @@ impl Display for IrepId {
             IrepId::VectorLe => "vector-<=",
             IrepId::VectorGt => "vector->",
             IrepId::VectorLt => "vector-<",
+            IrepId::FloatbvRoundToIntegral => "floatbv_round_to_integral",
         };
         write!(f, "{s}")
     }

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::FloatbvRoundToIntegral => IrepId::FloatbvRoundToIntegral,
             BinaryOperator::Ge => IrepId::Ge,
             BinaryOperator::Gt => IrepId::Gt,
             BinaryOperator::IeeeFloatEqual => IrepId::IeeeFloatEqual,

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

@@ -427,20 +427,9 @@ impl GotocCtx<'_> {
             Intrinsic::RotateRight => codegen_intrinsic_binop!(ror),
             Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf),
             Intrinsic::RoundF64 => codegen_simple_intrinsic!(Round),
-            Intrinsic::RoundTiesEvenF32 => self.codegen_round_to_integral(
-                BuiltinFn::RoundToIntegralF,
-                cbmc::RoundingMode::ToNearest,
-                fargs,
-                place,
-                loc,
-            ),
-            Intrinsic::RoundTiesEvenF64 => self.codegen_round_to_integral(
-                BuiltinFn::RoundToIntegral,
-                cbmc::RoundingMode::ToNearest,
-                fargs,
-                place,
-                loc,
-            ),
+            Intrinsic::RoundTiesEvenF32 | Intrinsic::RoundTiesEvenF64 => {
+                self.codegen_round_to_integral(cbmc::RoundingMode::ToNearest, fargs, place, loc)
+            }
             Intrinsic::SaturatingAdd => codegen_intrinsic_binop_with_mm!(saturating_add),
             Intrinsic::SaturatingSub => codegen_intrinsic_binop_with_mm!(saturating_sub),
             Intrinsic::SinF32 => codegen_simple_intrinsic!(Sinf),
@@ -648,24 +637,20 @@ impl GotocCtx<'_> {
         dividend_is_int_min.and(divisor_is_minus_one).not()
     }
 
-    // Builds a call to the round_to_integral CPROVER function with specified cbmc::RoundingMode.
+    // Builds a floatbv_round_to_integral expression with specified cbmc::RoundingMode.
     fn codegen_round_to_integral(
         &mut self,
-        function: BuiltinFn,
         rounding_mode: cbmc::RoundingMode,
         mut fargs: Vec<Expr>,
         place: &Place,
         loc: Location,
     ) -> Stmt {
-        assert!(function == BuiltinFn::RoundToIntegralF || function == BuiltinFn::RoundToIntegral);
-        let mm = self.symbol_table.machine_model();
-        fargs.insert(0, Expr::int_constant(rounding_mode, Type::c_int()));
-        let casted_fargs = Expr::cast_arguments_to_target_equivalent_function_parameter_types(
-            &function.as_expr(),
-            fargs,
-            mm,
-        );
-        let expr = function.call(casted_fargs, loc);
+        let place_ty = self.place_ty_stable(place);
+        let result_type = self.codegen_ty_stable(place_ty);
+        let f = fargs.remove(0);
+        assert!(fargs.is_empty());
+        let rm = Expr::int_constant(rounding_mode, Type::c_int());
+        let expr = Expr::floatbv_round_to_integral(f, rm, result_type);
         self.codegen_expr_to_place_stable(place, expr, loc)
     }
 

kani-dependencies

@@ -1,5 +1,5 @@
 CBMC_MAJOR="6"
-CBMC_MINOR="4"
-CBMC_VERSION="6.4.1"
+CBMC_MINOR="5"
+CBMC_VERSION="6.5.0"
 
 KISSAT_VERSION="4.0.1"

scripts/setup/macos/install_cbmc.sh

@@ -15,4 +15,4 @@ fi
 # Install CBMC for macOS from CBMC tap
 # https://github.com/diffblue/cbmc/blob/develop/doc/ADR/homebrew_tap.md
 brew tap diffblue/cbmc
-brew install diffblue/cbmc/cbmc@${CBMC_VERSION}
+brew install --overwrite diffblue/cbmc/cbmc@${CBMC_VERSION}