Add support for int to float casts

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

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,

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

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

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,

vir/src/data.rs

@@ -64,6 +64,7 @@ pub enum BinOpKind {
     PermSub,
     PermMul,
     PermPermDiv,
+    FractionalPerm,
     Mod,
     // Set ops
     SetUnion,

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",

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(),
         };