From 958cf391cbb11942aa5084eb95b7fa27403bd2fd Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 17 Jul 2026 09:17:44 +0200 Subject: [PATCH 1/7] 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(), }; From 5f9b68c0c5c5561d088f340aff45e7cfca02044b Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 17 Jul 2026 14:53:17 +0200 Subject: [PATCH 2/7] add suport for float to int casts --- prusti-encoder/src/encoders/builtin/cast.rs | 53 +++++++++++-- .../src/encoders/ty/interpretation/float.rs | 13 +++- .../src/encoders/ty/interpretation/mod.rs | 1 + .../src/encoders/ty/interpretation/real.rs | 76 +++++++++++++++++++ prusti-encoder/src/lib.rs | 3 +- .../tests/verify/pass/casts/float_to_int.rs | 41 ++++++++++ .../tests/verify/pass/casts/int_to_float.rs | 4 + 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 | 2 - vir/src/make.rs | 22 ++++++ 13 files changed, 205 insertions(+), 24 deletions(-) create mode 100644 prusti-encoder/src/encoders/ty/interpretation/real.rs create mode 100644 prusti-tests/tests/verify/pass/casts/float_to_int.rs diff --git a/prusti-encoder/src/encoders/builtin/cast.rs b/prusti-encoder/src/encoders/builtin/cast.rs index a7b056c4058..9a6665c3678 100644 --- a/prusti-encoder/src/encoders/builtin/cast.rs +++ b/prusti-encoder/src/encoders/builtin/cast.rs @@ -11,6 +11,7 @@ use crate::encoders::{ ty::{ LazyRustTy, RustTy, RustTyDecomposition, TySpecifics, generics::{GParams, GenericParamsEnc}, + interpretation::real::RealEnc, use_pure::TyUsePureEnc, }, }; @@ -94,6 +95,7 @@ impl TaskEncoder for MirBuiltinCastEnc { mir::CastKind::PointerCoercion(ty::adjustment::PointerCoercion::Unsize, ..) => "unsize", mir::CastKind::IntToInt => "i2i", mir::CastKind::IntToFloat => "i2f", + mir::CastKind::FloatToInt => "f2i", other => todo!("cast kind {other:?}"), }; // The unsize cast/methods don't depend on the pointee type (the methods @@ -170,11 +172,9 @@ impl TaskEncoder for MirBuiltinCastEnc { 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 real_domain = deps.require_dep::(())?; + let real_op = (real_domain.from_int)(e_op_ty.snap_to_prim(arg_ex)); + let expr = (e_res_ty.from_real)(real_op.downcast_ty()); // A value-level (thin) cast: no generic parameters, no precondition. @@ -189,6 +189,49 @@ impl TaskEncoder for MirBuiltinCastEnc { MirBuiltinCastOutput::Simple(fn_idn), ) } + mir::CastKind::FloatToInt => { + let e_op_ty = op_ty.expect_float(); + let e_res_ty = res_ty.expect_primitive(); + let result_kind = result_ty.expect_primitive().kind(); + + // real to int will always round down (also for negative numbers) - truncate first + let arg_ex_trunc = (e_op_ty.fp_trunc)(arg_ex); + + let real_op = (e_op_ty.fp_to_real)(arg_ex_trunc); + let real_domain = deps.require_dep::(())?; + let expr = (real_domain.to_int)(real_op.upcast_ty()); + + let expr = vcx.get_val_or_ty_bound(expr.downcast_ty(), result_kind); + + // Handle infinity and NaN cases + let expr = vcx.mk_ternary_expr( + (e_op_ty.fp_is_infinite)(arg_ex), + vcx.mk_ternary_expr( + (e_op_ty.fp_is_positive)(arg_ex), + vcx.get_max_int(result_kind).upcast_ty(), + vcx.get_min_int(result_kind).upcast_ty(), + ), + vcx.mk_ternary_expr( + (e_op_ty.fp_is_nan)(arg_ex), + vcx.mk_const_expr(vir::ConstData::Int(0)), + expr.upcast_ty(), + ), + ); + + let expr = e_res_ty.prim_to_snap(expr); + + // 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 5e624c2a2d0..d11755aafdc 100644 --- a/prusti-encoder/src/encoders/ty/interpretation/float.rs +++ b/prusti-encoder/src/encoders/ty/interpretation/float.rs @@ -24,6 +24,7 @@ pub struct FloatDomainData<'vir> { pub fp_trunc: FunctionIdn<'vir, vir::CSnap, vir::CSnap>, pub fp_is_nan: FunctionIdn<'vir, vir::CSnap, vir::Bool>, pub fp_is_infinite: FunctionIdn<'vir, vir::CSnap, vir::Bool>, + pub fp_is_positive: FunctionIdn<'vir, vir::CSnap, vir::Bool>, pub fp_lt: FunctionIdn<'vir, (vir::CSnap, vir::CSnap), vir::Bool>, pub fp_leq: FunctionIdn<'vir, (vir::CSnap, vir::CSnap), vir::Bool>, pub fp_gt: FunctionIdn<'vir, (vir::CSnap, vir::CSnap), vir::Bool>, @@ -40,7 +41,7 @@ pub(crate) fn ty_pure_float<'vir>( float: ty::FloatTy, prim_to_snap: FunctionIdn<'vir, vir::Prim, vir::CSnap>, ) -> Result, EncodeFullError<'vir, TyPureEnc>> { - let i = match float { + let backend_type = match float { ty::FloatTy::F16 => vcx.alloc_slice(&[ vcx.alloc(BackendInterpretationPair { key: "SMTLIB", @@ -82,7 +83,7 @@ pub(crate) fn ty_pure_float<'vir>( }), ]), }; - builder.set_interpretation(i); + builder.set_interpretation(backend_type); let fp_eq = builder.backend_func( "eq", @@ -140,6 +141,13 @@ pub(crate) fn ty_pure_float<'vir>( Some("fp.isInfinite"), ); + let fp_is_positive = builder.backend_func( + "is_positive", + builder.self_type(), + vir::TYPE_BOOL, + Some("fp.isPositive"), + ); + let fp_lt = builder.backend_func( "lt", (builder.self_type(), builder.self_type()), @@ -228,6 +236,7 @@ pub(crate) fn ty_pure_float<'vir>( fp_trunc, fp_is_nan, fp_is_infinite, + fp_is_positive, fp_lt, fp_leq, fp_gt, diff --git a/prusti-encoder/src/encoders/ty/interpretation/mod.rs b/prusti-encoder/src/encoders/ty/interpretation/mod.rs index 2191de28d60..3ae6a9720fb 100644 --- a/prusti-encoder/src/encoders/ty/interpretation/mod.rs +++ b/prusti-encoder/src/encoders/ty/interpretation/mod.rs @@ -1,2 +1,3 @@ pub mod bitvec; pub mod float; +pub mod real; diff --git a/prusti-encoder/src/encoders/ty/interpretation/real.rs b/prusti-encoder/src/encoders/ty/interpretation/real.rs new file mode 100644 index 00000000000..8692bbab916 --- /dev/null +++ b/prusti-encoder/src/encoders/ty/interpretation/real.rs @@ -0,0 +1,76 @@ +use task_encoder::TaskEncoder; +use vir::{CastType, DomainGenData, DomainIdnCSnap, FunctionIdn, ViperIdent}; + +#[derive(Debug, Clone, Copy)] +pub struct RealDomain<'vir> { + pub from_int: FunctionIdn<'vir, vir::Prim, vir::Prim>, + pub to_int: FunctionIdn<'vir, vir::Prim, vir::Prim>, +} + +pub struct RealEnc; + +impl TaskEncoder for RealEnc { + task_encoder::encoder_cache!(RealEnc); + const ENCODER_NAME: &'static str = "real encoder"; + + type TaskDescription<'vir> = (); + + type OutputFullLocal<'vir> = &'vir DomainGenData<'vir, (), !>; + + type OutputFullDependency<'vir> = RealDomain<'vir>; + + type EncodingError = (); + + fn task_to_key<'vir>(task: &Self::TaskDescription<'vir>) -> Self::TaskKey<'vir> { + *task + } + + fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { + for output in Self::all_outputs_local_no_errors(program) { + program.add_domain(output); + } + } + + fn do_encode_full<'vir>( + task_key: &Self::TaskKey<'vir>, + deps: &mut task_encoder::TaskEncoderDependencies<'vir, Self>, + ) -> task_encoder::EncodeFullResult<'vir, Self> { + vir::with_vcx(|vcx| { + let domain_name = "s_Real"; + + let domain_ident = DomainIdnCSnap::new(vir::ViperIdent::new(domain_name), 0); + let from_int_name = vir::vir_format!(vcx, "{}_from_int", domain_name); + + let from_int = FunctionIdn::new( + ViperIdent::new(from_int_name), + vir::TYPE_INT.upcast_ty(), + vir::TYPE_PERM.upcast_ty(), + ); + + let from_int_data = vcx.mk_domain_function(from_int, false, Some("to_real")); + + let to_int_name = vir::vir_format!(vcx, "{}_to_int", domain_name); + + let to_int = FunctionIdn::new( + ViperIdent::new(to_int_name), + vir::TYPE_PERM.upcast_ty(), + vir::TYPE_INT.upcast_ty(), + ); + + let to_int_data = vcx.mk_domain_function(to_int, false, Some("to_int")); + + let functions = &[from_int_data, to_int_data]; + + let domain_data = vcx.mk_domain::<(), !>( + domain_ident.name(), + &[], + &[], + vcx.alloc_slice(functions), + None, + ); + + deps.emit_output_ref(*task_key, ())?; + Ok((domain_data, RealDomain { from_int, to_int })) + }) + } +} diff --git a/prusti-encoder/src/lib.rs b/prusti-encoder/src/lib.rs index e12c49b1a54..ef742656cf2 100644 --- a/prusti-encoder/src/lib.rs +++ b/prusti-encoder/src/lib.rs @@ -26,7 +26,7 @@ use crate::encoders::{ generics::{ GArgsCastEnc, r#trait::TraitEnc, trait_fn::TraitFnEnc, trait_impls::TraitImplEnc, }, - interpretation::bitvec::BitVecEnc, + interpretation::{bitvec::BitVecEnc, real::RealEnc}, lifted::{TyConstructorEnc, TypeOfEnc}, }, }; @@ -105,6 +105,7 @@ pub fn test_entrypoint<'tcx>( program.header("snapshots"); crate::encoders::TyUsePureEnc::emit_outputs(&mut program); BitVecEnc::emit_outputs(&mut program); + RealEnc::emit_outputs(&mut program); program.header("predicates"); crate::encoders::TyUseImpureEnc::emit_outputs(&mut program); diff --git a/prusti-tests/tests/verify/pass/casts/float_to_int.rs b/prusti-tests/tests/verify/pass/casts/float_to_int.rs new file mode 100644 index 00000000000..b6faf49a181 --- /dev/null +++ b/prusti-tests/tests/verify/pass/casts/float_to_int.rs @@ -0,0 +1,41 @@ +fn main() { + let x = 100.0; + let y = x as i32; + assert!(y == 100); + + let x2 = 36.9; + let y2 = x2 as u32; + assert!(y2 == 36); + + let x3 = -36.9; + let y3 = x3 as u32; + assert!(y3 == 0); + + let x4 = -36.9; + let y4 = x4 as i32; + assert!(y4 == -36); + + let x5 = 1000.5; + let y5 = x5 as u8; + assert!(y5 == 255); + + let x6 = -1000.5; + let y6 = x6 as i8; + assert!(y6 == -128); + + let x7 = -36.3; + let y7 = x7 as i32; + assert!(y7 == -36); + + let x8 = f64::INFINITY; + let y8 = x8 as i32; + assert!(y8 == i32::MAX); + + let x9 = f64::NEG_INFINITY; + let y9 = x9 as i32; + assert!(y9 == i32::MIN); + + let x10 = f64::NAN; + let y10 = x10 as i32; + assert!(y10 == 0); +} \ No newline at end of file diff --git a/prusti-tests/tests/verify/pass/casts/int_to_float.rs b/prusti-tests/tests/verify/pass/casts/int_to_float.rs index e1a7ae9b156..b5c8596b7a6 100644 --- a/prusti-tests/tests/verify/pass/casts/int_to_float.rs +++ b/prusti-tests/tests/verify/pass/casts/int_to_float.rs @@ -16,4 +16,8 @@ fn main() { let x = -5; let y = x as f32; assert!(y == -5.0); + + let x = 9007199254740993i64; + assert!(x == 9007199254740993); + assert!(x as f32 == 9007199254740992.0); } \ No newline at end of file diff --git a/prusti-viper/src/lib.rs b/prusti-viper/src/lib.rs index 20dc03fd8ca..c89971031c1 100644 --- a/prusti-viper/src/lib.rs +++ b/prusti-viper/src/lib.rs @@ -230,7 +230,6 @@ 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 dd0f2bd3832..f3449f38eba 100644 --- a/viper/src/ast_factory/expression.rs +++ b/viper/src/ast_factory/expression.rs @@ -857,17 +857,6 @@ 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 7ada402f7ca..217cec983a5 100644 --- a/vir/src/data.rs +++ b/vir/src/data.rs @@ -64,7 +64,6 @@ pub enum BinOpKind { PermSub, PermMul, PermPermDiv, - FractionalPerm, Mod, // Set ops SetUnion, diff --git a/vir/src/debug.rs b/vir/src/debug.rs index 18e1a99fa21..527b59421fd 100644 --- a/vir/src/debug.rs +++ b/vir/src/debug.rs @@ -70,7 +70,6 @@ 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 2f5f62e5610..05dde6228e6 100644 --- a/vir/src/gendata.rs +++ b/vir/src/gendata.rs @@ -44,8 +44,6 @@ 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(), }; ty.as_dyn() diff --git a/vir/src/make.rs b/vir/src/make.rs index 0b4f733bece..1a78e034669 100644 --- a/vir/src/make.rs +++ b/vir/src/make.rs @@ -1210,4 +1210,26 @@ impl<'tcx> VirCtxt<'tcx> { } exp } + + pub fn get_val_or_ty_bound<'vir>( + &'vir self, + mut exp: ExprInt<'vir>, + rust_ty: &ty::TyKind, + ) -> ExprInt<'vir> { + let min = self.get_min_int(rust_ty); + let max = self.get_max_int(rust_ty); + exp = self.mk_ternary_expr( + self.mk_bin_op_expr(BinOpKind::CmpLt, exp, min) + .downcast_ty(), + min, + exp, + ); + exp = self.mk_ternary_expr( + self.mk_bin_op_expr(BinOpKind::CmpGt, exp, max) + .downcast_ty(), + max, + exp, + ); + exp + } } From 601f1c49828ee0819965e6ef17c8be2bf62a29f4 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Fri, 17 Jul 2026 16:58:09 +0200 Subject: [PATCH 3/7] implement PR feedback --- .../src/encoders/ty/interpretation/float.rs | 18 +++++++++--------- prusti-encoder/src/encoders/ty/pure.rs | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/prusti-encoder/src/encoders/ty/interpretation/float.rs b/prusti-encoder/src/encoders/ty/interpretation/float.rs index d11755aafdc..821bf0b8012 100644 --- a/prusti-encoder/src/encoders/ty/interpretation/float.rs +++ b/prusti-encoder/src/encoders/ty/interpretation/float.rs @@ -1,6 +1,6 @@ use prusti_rustc_interface::middle::ty; use task_encoder::{EncodeFullError, TaskEncoderDependencies}; -use vir::{BackendInterpretationPair, CallableIdn, FunctionIdn, VirCtxt}; +use vir::{BackendInterpretationPair, CallableIdn, FunctionIdn, VirCtxt, vir_format}; use crate::encoders::ty::{ interpretation::bitvec::{BitVecEnc, BitVecSize}, @@ -193,19 +193,19 @@ pub(crate) fn ty_pure_float<'vir>( ty::FloatTy::F128 => BitVecSize::BitVec128, })?; - let i = match float { + let from_bv_name = match float { ty::FloatTy::F16 => "(_ to_fp 5 11)", ty::FloatTy::F32 => "(_ to_fp 8 24)", ty::FloatTy::F64 => "(_ to_fp 11 53)", 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_bv = builder.backend_func( + "from_bv", + (bit_vec.domain)(), + builder.self_type(), + Some(from_bv_name), + ); + let from_real_name = vir_format!(vcx, "{} RNE", from_bv_name); let from_real = builder.backend_func( "from_real", vir::TYPE_PERM, diff --git a/prusti-encoder/src/encoders/ty/pure.rs b/prusti-encoder/src/encoders/ty/pure.rs index a8228b81c6f..7c6b64b8f4b 100644 --- a/prusti-encoder/src/encoders/ty/pure.rs +++ b/prusti-encoder/src/encoders/ty/pure.rs @@ -693,7 +693,7 @@ impl<'vir> DomainBuilder<'vir> { name: &str, args: A::Tys<'vir>, ret: Type<'vir, T>, - interpretation: Option<&'static str>, + interpretation: Option<&'vir str>, ) -> FunctionIdn<'vir, A, T> { let name = vir::vir_format!(self.vcx, "{}_{name}", self.name); let ident = FunctionIdn::new(vir::ViperIdent::new(name), args, ret); From 393cc6403bb59f837f0ec36962d60945c7117d2d Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Mon, 20 Jul 2026 12:15:39 +0200 Subject: [PATCH 4/7] implement PR feedback --- prusti-encoder/src/encoders/builtin/cast.rs | 5 +---- prusti-encoder/src/encoders/ty/interpretation/float.rs | 2 +- prusti-encoder/src/encoders/ty/interpretation/real.rs | 8 +++----- vir/src/make.rs | 2 +- 4 files changed, 6 insertions(+), 11 deletions(-) diff --git a/prusti-encoder/src/encoders/builtin/cast.rs b/prusti-encoder/src/encoders/builtin/cast.rs index 9a6665c3678..2fda8e1aeec 100644 --- a/prusti-encoder/src/encoders/builtin/cast.rs +++ b/prusti-encoder/src/encoders/builtin/cast.rs @@ -156,7 +156,6 @@ impl TaskEncoder for MirBuiltinCastEnc { }; let expr = e_res_ty.prim_to_snap(wrapped); - // 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)); ( @@ -177,7 +176,6 @@ impl TaskEncoder for MirBuiltinCastEnc { 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)); ( @@ -201,7 +199,7 @@ impl TaskEncoder for MirBuiltinCastEnc { let real_domain = deps.require_dep::(())?; let expr = (real_domain.to_int)(real_op.upcast_ty()); - let expr = vcx.get_val_or_ty_bound(expr.downcast_ty(), result_kind); + let expr = vcx.get_clamped_val(expr.downcast_ty(), result_kind); // Handle infinity and NaN cases let expr = vcx.mk_ternary_expr( @@ -220,7 +218,6 @@ impl TaskEncoder for MirBuiltinCastEnc { let expr = e_res_ty.prim_to_snap(expr); - // 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)); ( diff --git a/prusti-encoder/src/encoders/ty/interpretation/float.rs b/prusti-encoder/src/encoders/ty/interpretation/float.rs index 821bf0b8012..dde17a27d93 100644 --- a/prusti-encoder/src/encoders/ty/interpretation/float.rs +++ b/prusti-encoder/src/encoders/ty/interpretation/float.rs @@ -205,7 +205,7 @@ pub(crate) fn ty_pure_float<'vir>( builder.self_type(), Some(from_bv_name), ); - let from_real_name = vir_format!(vcx, "{} RNE", from_bv_name); + let from_real_name = vir_format!(vcx, "{from_bv_name} RNE"); let from_real = builder.backend_func( "from_real", vir::TYPE_PERM, diff --git a/prusti-encoder/src/encoders/ty/interpretation/real.rs b/prusti-encoder/src/encoders/ty/interpretation/real.rs index 8692bbab916..a01726c2bf9 100644 --- a/prusti-encoder/src/encoders/ty/interpretation/real.rs +++ b/prusti-encoder/src/encoders/ty/interpretation/real.rs @@ -39,7 +39,7 @@ impl TaskEncoder for RealEnc { let domain_name = "s_Real"; let domain_ident = DomainIdnCSnap::new(vir::ViperIdent::new(domain_name), 0); - let from_int_name = vir::vir_format!(vcx, "{}_from_int", domain_name); + let from_int_name = vir::vir_format!(vcx, "{domain_name}_from_int"); let from_int = FunctionIdn::new( ViperIdent::new(from_int_name), @@ -49,7 +49,7 @@ impl TaskEncoder for RealEnc { let from_int_data = vcx.mk_domain_function(from_int, false, Some("to_real")); - let to_int_name = vir::vir_format!(vcx, "{}_to_int", domain_name); + let to_int_name = vir::vir_format!(vcx, "{domain_name}_to_int"); let to_int = FunctionIdn::new( ViperIdent::new(to_int_name), @@ -59,13 +59,11 @@ impl TaskEncoder for RealEnc { let to_int_data = vcx.mk_domain_function(to_int, false, Some("to_int")); - let functions = &[from_int_data, to_int_data]; - let domain_data = vcx.mk_domain::<(), !>( domain_ident.name(), &[], &[], - vcx.alloc_slice(functions), + vcx.alloc_slice(&[from_int_data, to_int_data]), None, ); diff --git a/vir/src/make.rs b/vir/src/make.rs index 1a78e034669..727e6e22dac 100644 --- a/vir/src/make.rs +++ b/vir/src/make.rs @@ -1211,7 +1211,7 @@ impl<'tcx> VirCtxt<'tcx> { exp } - pub fn get_val_or_ty_bound<'vir>( + pub fn get_clamped_val<'vir>( &'vir self, mut exp: ExprInt<'vir>, rust_ty: &ty::TyKind, From a4de0ea374889fb29a64aebe202177bed622b74b Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Mon, 20 Jul 2026 15:11:03 +0200 Subject: [PATCH 5/7] implement PR feedback --- prusti-encoder/src/encoders/builtin/cast.rs | 15 +++--- .../{real.rs => int_real_cast.rs} | 52 +++++++++---------- .../src/encoders/ty/interpretation/mod.rs | 2 +- prusti-encoder/src/lib.rs | 4 +- vir/src/gendata.rs | 1 + 5 files changed, 37 insertions(+), 37 deletions(-) rename prusti-encoder/src/encoders/ty/interpretation/{real.rs => int_real_cast.rs} (60%) diff --git a/prusti-encoder/src/encoders/builtin/cast.rs b/prusti-encoder/src/encoders/builtin/cast.rs index 2fda8e1aeec..d3b404fc46a 100644 --- a/prusti-encoder/src/encoders/builtin/cast.rs +++ b/prusti-encoder/src/encoders/builtin/cast.rs @@ -11,7 +11,7 @@ use crate::encoders::{ ty::{ LazyRustTy, RustTy, RustTyDecomposition, TySpecifics, generics::{GParams, GenericParamsEnc}, - interpretation::real::RealEnc, + interpretation::int_real_cast::IntRealCastEnc, use_pure::TyUsePureEnc, }, }; @@ -171,10 +171,11 @@ impl TaskEncoder for MirBuiltinCastEnc { let e_op_ty = op_ty.expect_primitive(); let e_res_ty = res_ty.expect_float(); - let real_domain = deps.require_dep::(())?; - let real_op = (real_domain.from_int)(e_op_ty.snap_to_prim(arg_ex)); + let int_real_cast_domain = deps.require_dep::(())?; + let real_op = + (int_real_cast_domain.from_int)(e_op_ty.snap_to_prim(arg_ex).downcast_ty()); - let expr = (e_res_ty.from_real)(real_op.downcast_ty()); + let expr = (e_res_ty.from_real)(real_op); let fn_idn = FunctionIdn::new(name, op_ty_snap, res_ty_snap); let function = vcx.mk_function(fn_idn, (arg_decl,), &[], &[], None, Some(expr)); @@ -196,10 +197,10 @@ impl TaskEncoder for MirBuiltinCastEnc { let arg_ex_trunc = (e_op_ty.fp_trunc)(arg_ex); let real_op = (e_op_ty.fp_to_real)(arg_ex_trunc); - let real_domain = deps.require_dep::(())?; - let expr = (real_domain.to_int)(real_op.upcast_ty()); + let int_real_cast_domain = deps.require_dep::(())?; + let expr = (int_real_cast_domain.to_int)(real_op); - let expr = vcx.get_clamped_val(expr.downcast_ty(), result_kind); + let expr = vcx.get_clamped_val(expr, result_kind); // Handle infinity and NaN cases let expr = vcx.mk_ternary_expr( diff --git a/prusti-encoder/src/encoders/ty/interpretation/real.rs b/prusti-encoder/src/encoders/ty/interpretation/int_real_cast.rs similarity index 60% rename from prusti-encoder/src/encoders/ty/interpretation/real.rs rename to prusti-encoder/src/encoders/ty/interpretation/int_real_cast.rs index a01726c2bf9..acbf2ecf988 100644 --- a/prusti-encoder/src/encoders/ty/interpretation/real.rs +++ b/prusti-encoder/src/encoders/ty/interpretation/int_real_cast.rs @@ -1,23 +1,23 @@ use task_encoder::TaskEncoder; -use vir::{CastType, DomainGenData, DomainIdnCSnap, FunctionIdn, ViperIdent}; +use vir::{DomainGenData, FunctionIdn, ViperIdent}; #[derive(Debug, Clone, Copy)] -pub struct RealDomain<'vir> { - pub from_int: FunctionIdn<'vir, vir::Prim, vir::Prim>, - pub to_int: FunctionIdn<'vir, vir::Prim, vir::Prim>, +pub struct IntRealCastDomain<'vir> { + pub from_int: FunctionIdn<'vir, vir::Int, vir::Perm>, + pub to_int: FunctionIdn<'vir, vir::Perm, vir::Int>, } -pub struct RealEnc; +pub struct IntRealCastEnc; -impl TaskEncoder for RealEnc { - task_encoder::encoder_cache!(RealEnc); - const ENCODER_NAME: &'static str = "real encoder"; +impl TaskEncoder for IntRealCastEnc { + task_encoder::encoder_cache!(IntRealCastEnc); + const ENCODER_NAME: &'static str = "int_real_cast encoder"; type TaskDescription<'vir> = (); type OutputFullLocal<'vir> = &'vir DomainGenData<'vir, (), !>; - type OutputFullDependency<'vir> = RealDomain<'vir>; + type OutputFullDependency<'vir> = IntRealCastDomain<'vir>; type EncodingError = (); @@ -25,50 +25,48 @@ impl TaskEncoder for RealEnc { *task } - fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { - for output in Self::all_outputs_local_no_errors(program) { - program.add_domain(output); - } - } - fn do_encode_full<'vir>( task_key: &Self::TaskKey<'vir>, deps: &mut task_encoder::TaskEncoderDependencies<'vir, Self>, ) -> task_encoder::EncodeFullResult<'vir, Self> { vir::with_vcx(|vcx| { - let domain_name = "s_Real"; + deps.emit_output_ref(*task_key, ())?; + + let domain_name = "s_IntRealCast"; - let domain_ident = DomainIdnCSnap::new(vir::ViperIdent::new(domain_name), 0); + let domain_ident = vir::ViperIdent::new(domain_name); let from_int_name = vir::vir_format!(vcx, "{domain_name}_from_int"); let from_int = FunctionIdn::new( ViperIdent::new(from_int_name), - vir::TYPE_INT.upcast_ty(), - vir::TYPE_PERM.upcast_ty(), + vir::TYPE_INT, + vir::TYPE_PERM, ); let from_int_data = vcx.mk_domain_function(from_int, false, Some("to_real")); let to_int_name = vir::vir_format!(vcx, "{domain_name}_to_int"); - let to_int = FunctionIdn::new( - ViperIdent::new(to_int_name), - vir::TYPE_PERM.upcast_ty(), - vir::TYPE_INT.upcast_ty(), - ); + let to_int = + FunctionIdn::new(ViperIdent::new(to_int_name), vir::TYPE_PERM, vir::TYPE_INT); let to_int_data = vcx.mk_domain_function(to_int, false, Some("to_int")); let domain_data = vcx.mk_domain::<(), !>( - domain_ident.name(), + domain_ident, &[], &[], vcx.alloc_slice(&[from_int_data, to_int_data]), None, ); - deps.emit_output_ref(*task_key, ())?; - Ok((domain_data, RealDomain { from_int, to_int })) + Ok((domain_data, IntRealCastDomain { from_int, to_int })) }) } + + fn emit_outputs<'vir>(program: &mut task_encoder::Program<'vir>) { + for output in Self::all_outputs_local_no_errors(program) { + program.add_domain(output); + } + } } diff --git a/prusti-encoder/src/encoders/ty/interpretation/mod.rs b/prusti-encoder/src/encoders/ty/interpretation/mod.rs index 3ae6a9720fb..0cbd30c61fc 100644 --- a/prusti-encoder/src/encoders/ty/interpretation/mod.rs +++ b/prusti-encoder/src/encoders/ty/interpretation/mod.rs @@ -1,3 +1,3 @@ pub mod bitvec; pub mod float; -pub mod real; +pub mod int_real_cast; diff --git a/prusti-encoder/src/lib.rs b/prusti-encoder/src/lib.rs index ef742656cf2..9de6be038f5 100644 --- a/prusti-encoder/src/lib.rs +++ b/prusti-encoder/src/lib.rs @@ -26,7 +26,7 @@ use crate::encoders::{ generics::{ GArgsCastEnc, r#trait::TraitEnc, trait_fn::TraitFnEnc, trait_impls::TraitImplEnc, }, - interpretation::{bitvec::BitVecEnc, real::RealEnc}, + interpretation::{bitvec::BitVecEnc, int_real_cast::IntRealCastEnc}, lifted::{TyConstructorEnc, TypeOfEnc}, }, }; @@ -105,7 +105,7 @@ pub fn test_entrypoint<'tcx>( program.header("snapshots"); crate::encoders::TyUsePureEnc::emit_outputs(&mut program); BitVecEnc::emit_outputs(&mut program); - RealEnc::emit_outputs(&mut program); + IntRealCastEnc::emit_outputs(&mut program); program.header("predicates"); crate::encoders::TyUseImpureEnc::emit_outputs(&mut program); diff --git a/vir/src/gendata.rs b/vir/src/gendata.rs index 05dde6228e6..e4cda651075 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::SetUnion => return self.lhs.ty(), }; ty.as_dyn() From e16f4fb779d0a828177920afa1a1f7f83cc57018 Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Tue, 21 Jul 2026 11:53:18 +0200 Subject: [PATCH 6/7] move tests to fail --- .../tests/verify/fail/casts/int_to_float.rs | 24 +++++++++++++++++++ .../tests/verify/pass/casts/int_to_float.rs | 12 ++-------- 2 files changed, 26 insertions(+), 10 deletions(-) create mode 100644 prusti-tests/tests/verify/fail/casts/int_to_float.rs diff --git a/prusti-tests/tests/verify/fail/casts/int_to_float.rs b/prusti-tests/tests/verify/fail/casts/int_to_float.rs new file mode 100644 index 00000000000..ebc69204ca4 --- /dev/null +++ b/prusti-tests/tests/verify/fail/casts/int_to_float.rs @@ -0,0 +1,24 @@ +// The result of these casts can currently not be verified using Z3. +// Once Z3 supports these cases, replace pass/casts/int_to_float.rs with this file. + +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); + + let x = 9007199254740993i64; + assert!(x == 9007199254740993); + assert!(x as f32 == 9007199254740992.0); +} \ No newline at end of file diff --git a/prusti-tests/tests/verify/pass/casts/int_to_float.rs b/prusti-tests/tests/verify/pass/casts/int_to_float.rs index b5c8596b7a6..b141089db1f 100644 --- a/prusti-tests/tests/verify/pass/casts/int_to_float.rs +++ b/prusti-tests/tests/verify/pass/casts/int_to_float.rs @@ -1,23 +1,15 @@ -// 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); - - let x = 9007199254740993i64; - assert!(x == 9007199254740993); - assert!(x as f32 == 9007199254740992.0); + + let x = 9007199254740993i64 as f32; } \ No newline at end of file From ab33848ad0b562ade48210912e21fdc072dc3bec Mon Sep 17 00:00:00 2001 From: Thomas Mayerl Date: Tue, 21 Jul 2026 17:32:31 +0200 Subject: [PATCH 7/7] implement PR feedback --- prusti-encoder/src/encoders/builtin/cast.rs | 18 +++++++++++++-- .../tests/verify/fail/casts/int_to_float.rs | 11 +++++----- vir/src/make.rs | 22 ------------------- 3 files changed, 21 insertions(+), 30 deletions(-) diff --git a/prusti-encoder/src/encoders/builtin/cast.rs b/prusti-encoder/src/encoders/builtin/cast.rs index d3b404fc46a..69ce33c642d 100644 --- a/prusti-encoder/src/encoders/builtin/cast.rs +++ b/prusti-encoder/src/encoders/builtin/cast.rs @@ -3,7 +3,7 @@ use prusti_rustc_interface::{ span::symbol, }; use task_encoder::{EncodeFullResult, TaskEncoder, TaskEncoderDependencies}; -use vir::{CastType, FunctionIdn, MethodIdn}; +use vir::{BinOpKind, CastType, FunctionIdn, MethodIdn}; use crate::encoders::{ TyUseImpureEnc, @@ -200,7 +200,21 @@ impl TaskEncoder for MirBuiltinCastEnc { let int_real_cast_domain = deps.require_dep::(())?; let expr = (int_real_cast_domain.to_int)(real_op); - let expr = vcx.get_clamped_val(expr, result_kind); + // clamp result + let min = vcx.get_min_int(result_kind); + let max = vcx.get_max_int(result_kind); + let expr = vcx.mk_ternary_expr( + vcx.mk_bin_op_expr(BinOpKind::CmpLt, expr, min) + .downcast_ty(), + min, + expr, + ); + let expr = vcx.mk_ternary_expr( + vcx.mk_bin_op_expr(BinOpKind::CmpGt, expr, max) + .downcast_ty(), + max, + expr, + ); // Handle infinity and NaN cases let expr = vcx.mk_ternary_expr( diff --git a/prusti-tests/tests/verify/fail/casts/int_to_float.rs b/prusti-tests/tests/verify/fail/casts/int_to_float.rs index ebc69204ca4..0ec70d8a360 100644 --- a/prusti-tests/tests/verify/fail/casts/int_to_float.rs +++ b/prusti-tests/tests/verify/fail/casts/int_to_float.rs @@ -4,21 +4,20 @@ fn main() { let x = 100; let y = x as f32; - assert!(y == 100.0); + assert!(y == 100.0); //~ERROR: the asserted expression might not hold let x = u128::MAX; let y = x as f32; - assert!(y == f32::INFINITY); + assert!(y == f32::INFINITY); //~ERROR: the asserted expression might not hold let x = u8::MAX; let y = x as f64; - assert!(y == 255.0); + assert!(y == 255.0); //~ERROR: the asserted expression might not hold let x = -5; let y = x as f32; - assert!(y == -5.0); + assert!(y == -5.0); //~ERROR: the asserted expression might not hold let x = 9007199254740993i64; - assert!(x == 9007199254740993); - assert!(x as f32 == 9007199254740992.0); + assert!(x as f32 == 9007199254740992.0); //~ERROR: the asserted expression might not hold } \ No newline at end of file diff --git a/vir/src/make.rs b/vir/src/make.rs index 727e6e22dac..0b4f733bece 100644 --- a/vir/src/make.rs +++ b/vir/src/make.rs @@ -1210,26 +1210,4 @@ impl<'tcx> VirCtxt<'tcx> { } exp } - - pub fn get_clamped_val<'vir>( - &'vir self, - mut exp: ExprInt<'vir>, - rust_ty: &ty::TyKind, - ) -> ExprInt<'vir> { - let min = self.get_min_int(rust_ty); - let max = self.get_max_int(rust_ty); - exp = self.mk_ternary_expr( - self.mk_bin_op_expr(BinOpKind::CmpLt, exp, min) - .downcast_ty(), - min, - exp, - ); - exp = self.mk_ternary_expr( - self.mk_bin_op_expr(BinOpKind::CmpGt, exp, max) - .downcast_ty(), - max, - exp, - ); - exp - } }