diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index 0ff2296a1024..f925bfcfe58e 100644 --- a/cprover_bindings/src/goto_program/builtin.rs +++ b/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, diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 5805dc4f7280..6f140b67ec84 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/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 diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index 69962edf150e..b3ca7a49ecab 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/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}") } diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 7fd364e5d725..b9cc6978ea85 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/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, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index ac5b44ec4163..88f4763be49e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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, 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) } diff --git a/kani-dependencies b/kani-dependencies index ed8e32faca90..f620835102de 100644 --- a/kani-dependencies +++ b/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" diff --git a/scripts/setup/macos/install_cbmc.sh b/scripts/setup/macos/install_cbmc.sh index dbef341c9e01..6cd65dac1ac9 100755 --- a/scripts/setup/macos/install_cbmc.sh +++ b/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}