diff --git a/prusti-encoder/src/encoders/builtin/cast.rs b/prusti-encoder/src/encoders/builtin/cast.rs index b3c8f6849b9..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, @@ -11,6 +11,7 @@ use crate::encoders::{ ty::{ LazyRustTy, RustTy, RustTyDecomposition, TySpecifics, generics::{GParams, GenericParamsEnc}, + interpretation::int_real_cast::IntRealCastEnc, use_pure::TyUsePureEnc, }, }; @@ -93,6 +94,8 @@ impl TaskEncoder for MirBuiltinCastEnc { let name = match kind { 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 @@ -153,7 +156,83 @@ 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)); + ( + MirBuiltinCastLocal { + cast: function, + unsize: None, + undo: None, + }, + MirBuiltinCastOutput::Simple(fn_idn), + ) + } + mir::CastKind::IntToFloat => { + let e_op_ty = op_ty.expect_primitive(); + let e_res_ty = res_ty.expect_float(); + + 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); + + 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::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 int_real_cast_domain = deps.require_dep::(())?; + let expr = (int_real_cast_domain.to_int)(real_op); + + // 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( + (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); + 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 ba53ecad846..dde17a27d93 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}, @@ -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>, @@ -23,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>, @@ -39,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", @@ -81,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", @@ -139,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()), @@ -184,13 +193,25 @@ 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_bv = builder.backend_func( + "from_bv", + (bit_vec.domain)(), + builder.self_type(), + Some(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, + builder.self_type(), + Some(from_real_name), + ); let fp_to_real = builder.backend_func( "to_real", @@ -206,6 +227,7 @@ pub(crate) fn ty_pure_float<'vir>( Ok(FloatDomainData { prim_to_snap, from_bv, + from_real, fp_eq, fp_add, fp_sub, @@ -214,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/int_real_cast.rs b/prusti-encoder/src/encoders/ty/interpretation/int_real_cast.rs new file mode 100644 index 00000000000..acbf2ecf988 --- /dev/null +++ b/prusti-encoder/src/encoders/ty/interpretation/int_real_cast.rs @@ -0,0 +1,72 @@ +use task_encoder::TaskEncoder; +use vir::{DomainGenData, FunctionIdn, ViperIdent}; + +#[derive(Debug, Clone, Copy)] +pub struct IntRealCastDomain<'vir> { + pub from_int: FunctionIdn<'vir, vir::Int, vir::Perm>, + pub to_int: FunctionIdn<'vir, vir::Perm, vir::Int>, +} + +pub struct IntRealCastEnc; + +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> = IntRealCastDomain<'vir>; + + type EncodingError = (); + + fn task_to_key<'vir>(task: &Self::TaskDescription<'vir>) -> Self::TaskKey<'vir> { + *task + } + + 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| { + deps.emit_output_ref(*task_key, ())?; + + let domain_name = "s_IntRealCast"; + + 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, + 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, 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, + &[], + &[], + vcx.alloc_slice(&[from_int_data, to_int_data]), + None, + ); + + 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 2191de28d60..0cbd30c61fc 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 int_real_cast; 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); diff --git a/prusti-encoder/src/lib.rs b/prusti-encoder/src/lib.rs index e12c49b1a54..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, + interpretation::{bitvec::BitVecEnc, int_real_cast::IntRealCastEnc}, 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); + IntRealCastEnc::emit_outputs(&mut program); program.header("predicates"); crate::encoders::TyUseImpureEnc::emit_outputs(&mut program); 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..0ec70d8a360 --- /dev/null +++ b/prusti-tests/tests/verify/fail/casts/int_to_float.rs @@ -0,0 +1,23 @@ +// 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); //~ERROR: the asserted expression might not hold + + let x = u128::MAX; + let y = x as f32; + assert!(y == f32::INFINITY); //~ERROR: the asserted expression might not hold + + let x = u8::MAX; + let y = x as f64; + assert!(y == 255.0); //~ERROR: the asserted expression might not hold + + let x = -5; + let y = x as f32; + assert!(y == -5.0); //~ERROR: the asserted expression might not hold + + let x = 9007199254740993i64; + assert!(x as f32 == 9007199254740992.0); //~ERROR: the asserted expression might not hold +} \ No newline at end of file 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 new file mode 100644 index 00000000000..b141089db1f --- /dev/null +++ b/prusti-tests/tests/verify/pass/casts/int_to_float.rs @@ -0,0 +1,15 @@ +fn main() { + let x = 100; + let y = x as f32; + + let x = u128::MAX; + let y = x as f32; + + let x = u8::MAX; + let y = x as f64; + + let x = -5; + let y = x as f32; + + let x = 9007199254740993i64 as f32; +} \ No newline at end of file