From 958cf391cbb11942aa5084eb95b7fa27403bd2fd Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 17 Jul 2026 09:17:44 +0200 Subject: [PATCH] Add support for int to float casts --- prusti-encoder/src/encoders/builtin/cast.rs | 24 +++++++++++++++++++ .../src/encoders/ty/interpretation/float.rs | 14 +++++++++++ .../tests/verify/pass/casts/int_to_float.rs | 19 +++++++++++++++ prusti-viper/src/lib.rs | 1 + viper/src/ast_factory/expression.rs | 11 +++++++++ vir/src/data.rs | 1 + vir/src/debug.rs | 1 + vir/src/gendata.rs | 1 + 8 files changed, 72 insertions(+) create mode 100644 prusti-tests/tests/verify/pass/casts/int_to_float.rs diff --git a/prusti-encoder/src/encoders/builtin/cast.rs b/prusti-encoder/src/encoders/builtin/cast.rs index b3c8f6849b9..a7b056c4058 100644 --- a/prusti-encoder/src/encoders/builtin/cast.rs +++ b/prusti-encoder/src/encoders/builtin/cast.rs @@ -93,6 +93,7 @@ impl TaskEncoder for MirBuiltinCastEnc { let name = match kind { mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize, ..) => "unsize", mir::CastKind::IntToInt => "i2i", + mir::CastKind::IntToFloat => "i2f", other => todo!("cast kind {other:?}"), }; // The unsize cast/methods don't depend on the pointee type (the methods @@ -165,6 +166,29 @@ impl TaskEncoder for MirBuiltinCastEnc { MirBuiltinCastOutput::Simple(fn_idn), ) } + mir::CastKind::IntToFloat => { + let e_op_ty = op_ty.expect_primitive(); + let e_res_ty = res_ty.expect_float(); + + let real_op = vcx.mk_bin_op_expr( + vir::BinOpKind::FractionalPerm, + e_op_ty.snap_to_prim(arg_ex), + vcx.mk_const_expr(vir::ConstData::Int(1)), + ); + let expr = (e_res_ty.from_real)(real_op.downcast_ty()); + + // A value-level (thin) cast: no generic parameters, no precondition. + let fn_idn = FunctionIdn::new(name, op_ty_snap, res_ty_snap); + let function = vcx.mk_function(fn_idn, (arg_decl,), &[], &[], None, Some(expr)); + ( + MirBuiltinCastLocal { + cast: function, + unsize: None, + undo: None, + }, + MirBuiltinCastOutput::Simple(fn_idn), + ) + } mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize, _) => { // Unsizing preserves the (wide) reference snapshot type and only // rewrites the pointer metadata for the new referent. The cast diff --git a/prusti-encoder/src/encoders/ty/interpretation/float.rs b/prusti-encoder/src/encoders/ty/interpretation/float.rs index ba53ecad846..5e624c2a2d0 100644 --- a/prusti-encoder/src/encoders/ty/interpretation/float.rs +++ b/prusti-encoder/src/encoders/ty/interpretation/float.rs @@ -15,6 +15,7 @@ pub struct FloatDomainData<'vir> { pub prim_to_snap: FunctionIdn<'vir, vir::Prim, vir::CSnap>, #[allow(unused)] pub from_bv: FunctionIdn<'vir, vir::CSnap, vir::CSnap>, + pub from_real: FunctionIdn<'vir, vir::Perm, vir::CSnap>, pub fp_eq: FunctionIdn<'vir, (vir::CSnap, vir::CSnap), vir::Bool>, pub fp_add: FunctionIdn<'vir, (vir::CSnap, vir::CSnap), vir::CSnap>, pub fp_sub: FunctionIdn<'vir, (vir::CSnap, vir::CSnap), vir::CSnap>, @@ -191,6 +192,18 @@ pub(crate) fn ty_pure_float<'vir>( ty::FloatTy::F128 => "(_ to_fp 15 113)", }; let from_bv = builder.backend_func("from_bv", (bit_vec.domain)(), builder.self_type(), Some(i)); + let from_real_name: &str = match float { + ty::FloatTy::F16 => "(_ to_fp 5 11) RNE", + ty::FloatTy::F32 => "(_ to_fp 8 24) RNE", + ty::FloatTy::F64 => "(_ to_fp 11 53) RNE", + ty::FloatTy::F128 => "(_ to_fp 15 113) RNE", + }; + let from_real = builder.backend_func( + "from_real", + vir::TYPE_PERM, + builder.self_type(), + Some(from_real_name), + ); let fp_to_real = builder.backend_func( "to_real", @@ -206,6 +219,7 @@ pub(crate) fn ty_pure_float<'vir>( Ok(FloatDomainData { prim_to_snap, from_bv, + from_real, fp_eq, fp_add, fp_sub, diff --git a/prusti-tests/tests/verify/pass/casts/int_to_float.rs b/prusti-tests/tests/verify/pass/casts/int_to_float.rs new file mode 100644 index 00000000000..e1a7ae9b156 --- /dev/null +++ b/prusti-tests/tests/verify/pass/casts/int_to_float.rs @@ -0,0 +1,19 @@ +// This currently works with CVC5 but not with Z3.. + +fn main() { + let x = 100; + let y = x as f32; + assert!(y == 100.0); + + let x = u128::MAX; + let y = x as f32; + assert!(y == f32::INFINITY); + + let x = u8::MAX; + let y = x as f64; + assert!(y == 255.0); + + let x = -5; + let y = x as f32; + assert!(y == -5.0); +} \ No newline at end of file diff --git a/prusti-viper/src/lib.rs b/prusti-viper/src/lib.rs index c89971031c1..20dc03fd8ca 100644 --- a/prusti-viper/src/lib.rs +++ b/prusti-viper/src/lib.rs @@ -230,6 +230,7 @@ impl<'vir, 'v> ToViper<'vir, 'v> for vir::BinOp<'vir> { vir::BinOpKind::PermAdd => ctx.ast.perm_add_with_pos(lhs, rhs, pos), vir::BinOpKind::PermSub => ctx.ast.perm_sub_with_pos(lhs, rhs, pos), vir::BinOpKind::PermMul => ctx.ast.perm_mul_with_pos(lhs, rhs, pos), + vir::BinOpKind::FractionalPerm => ctx.ast.fractional_perm_with_pos(lhs, rhs, pos), vir::BinOpKind::PermPermDiv => ctx.ast.perm_perm_div_with_pos(lhs, rhs, pos), vir::BinOpKind::Mod => ctx.ast.mod_with_pos(lhs, rhs, pos), vir::BinOpKind::Implies => ctx.ast.implies_with_pos(lhs, rhs, pos), diff --git a/viper/src/ast_factory/expression.rs b/viper/src/ast_factory/expression.rs index f3449f38eba..dd0f2bd3832 100644 --- a/viper/src/ast_factory/expression.rs +++ b/viper/src/ast_factory/expression.rs @@ -857,6 +857,17 @@ impl<'a> AstFactory<'a> { ) } + pub fn fractional_perm_with_pos(&self, left: Expr, right: Expr, pos: Position) -> Expr<'a> { + build_ast_node_with_pos!( + self, + Expr, + ast::FractionalPerm, + left.to_jobject(), + right.to_jobject(), + pos.to_jobject() + ) + } + pub fn perm_perm_div_with_pos(&self, left: Expr, right: Expr, pos: Position) -> Expr<'a> { build_ast_node_with_pos!( self, diff --git a/vir/src/data.rs b/vir/src/data.rs index 217cec983a5..7ada402f7ca 100644 --- a/vir/src/data.rs +++ b/vir/src/data.rs @@ -64,6 +64,7 @@ pub enum BinOpKind { PermSub, PermMul, PermPermDiv, + FractionalPerm, Mod, // Set ops SetUnion, diff --git a/vir/src/debug.rs b/vir/src/debug.rs index 527b59421fd..18e1a99fa21 100644 --- a/vir/src/debug.rs +++ b/vir/src/debug.rs @@ -70,6 +70,7 @@ impl<'vir, Curr, Next> Debug for BinOpGenData<'vir, Curr, Next> { BinOpKind::PermSub => "-", BinOpKind::PermMul => "*", BinOpKind::PermPermDiv => "/", + BinOpKind::FractionalPerm => "/", BinOpKind::Mod => "%", BinOpKind::SetUnion => "union", BinOpKind::SetIn => "in", diff --git a/vir/src/gendata.rs b/vir/src/gendata.rs index e4cda651075..2f5f62e5610 100644 --- a/vir/src/gendata.rs +++ b/vir/src/gendata.rs @@ -44,6 +44,7 @@ impl<'vir, Curr, Next> BinOpGenData<'vir, Curr, Next> { | BinOpKind::PermSub | BinOpKind::PermMul | BinOpKind::PermPermDiv => crate::TYPE_PERM.upcast_ty(), + BinOpKind::FractionalPerm => crate::TYPE_PERM.upcast_ty(), BinOpKind::SetUnion => return self.lhs.ty(), };