Add support for IntToFloat and FloatToInt casts

prusti-encoder/src/encoders/builtin/cast.rs

@@ -3,14 +3,15 @@ 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,
     builtin::{MetadataCastEnc, ValueCastEnc},
     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::<IntRealCastEnc>(())?;
+                    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::<IntRealCastEnc>(())?;
+                    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));
                     (

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<FloatDomainData<'vir>, 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,

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);
+        }
+    }
+}

prusti-encoder/src/encoders/ty/interpretation/mod.rs

@@ -1,2 +1,3 @@
 pub mod bitvec;
 pub mod float;
+pub mod int_real_cast;

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);

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);

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
+}

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);
+}

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;
+}