diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index 819bbb0404..272a461106 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -2264,6 +2264,142 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( expr_vattrs.truncate, ))) } + (TypX::Int(src_range), TypX::Float(dst_bits)) => { + match src_range { + IntRange::Int + | IntRange::Nat + | IntRange::Char + | IntRange::USize + | IntRange::ISize => { + return err_span( + expr.span, + format!( + "Verus does not support `as` cast from `{}` to `f{}`", + vir::ast_util::int_range_to_type_string(src_range), + dst_bits, + ), + ); + } + _ => {} + } + if *dst_bits != 32 && *dst_bits != 64 { + return err_span( + expr.span, + format!("Verus does not support `as` cast to `f{}`", dst_bits), + ); + } + if bctx.ctxt.no_vstd { + return err_span( + expr.span, + "Float `as` cast is not supported with --no-vstd", + ); + } + let fun = vir::fun!("vstd" => "float", "float_cast"); + let from_typ = undecorate_typ(source_vir_ty); + let to_typ = undecorate_typ(&to_vir_ty); + let typ_args = Arc::new(vec![from_typ, to_typ]); + let autospec_usage = + if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final }; + let call_target = CallTarget::Fun( + vir::ast::CallTargetKind::Static, + fun, + typ_args, + Arc::new(vec![]), + autospec_usage, + false, + ); + let args = Arc::new(vec![source_vir_expr.clone()]); + mk_expr(ExprX::Call(call_target, args, None)) + } + (TypX::Float(src_bits), TypX::Int(_dst_range)) => { + let dst_range = match &*undecorate_typ(&to_vir_ty) { + TypX::Int(r) => *r, + _ => unreachable!(), + }; + match dst_range { + IntRange::Int + | IntRange::Nat + | IntRange::Char + | IntRange::USize + | IntRange::ISize => { + return err_span( + expr.span, + format!( + "Verus does not support `as` cast from `f{}` to `{}`", + src_bits, + vir::ast_util::int_range_to_type_string(&dst_range), + ), + ); + } + _ => {} + } + if *src_bits != 32 && *src_bits != 64 { + return err_span( + expr.span, + format!("Verus does not support `as` cast from `f{}`", src_bits), + ); + } + if bctx.ctxt.no_vstd { + return err_span( + expr.span, + "Float `as` cast is not supported with --no-vstd", + ); + } + let fun = vir::fun!("vstd" => "float", "float_cast"); + let from_typ = undecorate_typ(source_vir_ty); + let to_typ = undecorate_typ(&to_vir_ty); + let typ_args = Arc::new(vec![from_typ, to_typ]); + let autospec_usage = + if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final }; + let call_target = CallTarget::Fun( + vir::ast::CallTargetKind::Static, + fun, + typ_args, + Arc::new(vec![]), + autospec_usage, + false, + ); + let args = Arc::new(vec![source_vir_expr.clone()]); + mk_expr(ExprX::Call(call_target, args, None)) + } + (TypX::Float(src_bits), TypX::Float(dst_bits)) if src_bits != dst_bits => { + if (*src_bits != 32 && *src_bits != 64) || (*dst_bits != 32 && *dst_bits != 64) + { + return err_span( + expr.span, + format!( + "Verus does not support `as` cast from `f{}` to `f{}`", + src_bits, dst_bits, + ), + ); + } + if bctx.ctxt.no_vstd { + return err_span( + expr.span, + "Float `as` cast is not supported with --no-vstd", + ); + } + let fun = vir::fun!("vstd" => "float", "float_cast"); + let from_typ = undecorate_typ(source_vir_ty); + let to_typ = undecorate_typ(&to_vir_ty); + let typ_args = Arc::new(vec![from_typ, to_typ]); + let autospec_usage = + if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final }; + let call_target = CallTarget::Fun( + vir::ast::CallTargetKind::Static, + fun, + typ_args, + Arc::new(vec![]), + autospec_usage, + false, + ); + let args = Arc::new(vec![source_vir_expr.clone()]); + mk_expr(ExprX::Call(call_target, args, None)) + } + (TypX::Float(_), TypX::Float(_)) => { + // Same float type, identity cast + Ok(ExprOrPlace::Expr(source_vir_expr)) + } _ => { let to_ty = bctx.types.expr_ty(expr); return err_span( diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs index d83015e474..59ee11b057 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -357,6 +357,7 @@ pub(crate) enum VstdItem { CastSlicePtrToStrPtr, CastStrPtrToSlicePtr, CastPtrToUsize, + FloatCast, RefMutArrayUnsizingCoercion, VecIndex, VecIndexMut, @@ -666,6 +667,7 @@ fn verus_items_map() -> Vec<(&'static str, VerusItem)> { ("verus::vstd::raw_ptr::cast_str_ptr_to_slice_ptr", VerusItem::Vstd(VstdItem::CastStrPtrToSlicePtr, Some(Arc::new("raw_ptr::cast_str_ptr_to_slice_ptr".to_owned())))), ("verus::vstd::raw_ptr::cast_ptr_to_usize", VerusItem::Vstd(VstdItem::CastPtrToUsize, Some(Arc::new("raw_ptr::cast_ptr_to_usize".to_owned())))), ("verus::vstd::raw_ptr::SharedReference", VerusItem::Vstd(VstdItem::SharedReference, Some(Arc::new("raw_ptr::SharedReference".to_owned())))), + ("verus::vstd::float::float_cast", VerusItem::Vstd(VstdItem::FloatCast, Some(Arc::new("float::float_cast".to_owned())))), // SeqFn(vir::interpreter::SeqFn::Last ))), ("verus::verus_builtin::Structural", VerusItem::Marker(MarkerItem::Structural)), diff --git a/source/rust_verify_test/tests/float.rs b/source/rust_verify_test/tests/float.rs index 50485b2c82..5e297efa69 100644 --- a/source/rust_verify_test/tests/float.rs +++ b/source/rust_verify_test/tests/float.rs @@ -50,6 +50,143 @@ test_verify_one_file! { } => Err(err) => assert_one_fails(err) } +test_verify_one_file! { + #[test] int_to_f64_cast verus_code! { + fn test_i32_as_f64(n: i32) { + use vstd::float::float_cast_spec; + let x: f64 = n as f64; + // The ensures predicate should hold for the cast result + assert(float_cast_spec(n, x)); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] int_to_f32_cast verus_code! { + fn test_u32_as_f32(n: u32) { + use vstd::float::float_cast_spec; + let x: f32 = n as f32; + assert(float_cast_spec(n, x)); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] f64_to_int_cast verus_code! { + fn test_f64_as_u32(f: f64) { + use vstd::float::float_cast_spec; + let n: u32 = f as u32; + assert(float_cast_spec(f, n)); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] f32_to_int_cast verus_code! { + fn test_f32_as_i64(f: f32) { + use vstd::float::float_cast_spec; + let n: i64 = f as i64; + assert(float_cast_spec(f, n)); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] float_to_float_cast verus_code! { + fn test_f32_as_f64(f: f32) { + use vstd::float::float_cast_spec; + let d: f64 = f as f64; + assert(float_cast_spec(f, d)); + } + + fn test_f64_as_f32(d: f64) { + use vstd::float::float_cast_spec; + let f: f32 = d as f32; + assert(float_cast_spec(d, f)); + } + } => Ok(()) +} + +test_verify_one_file_with_options! { + #[test] cast_nondeterministic_fail ["vstd"] => verus_code! { + fn test_nondeterministic(n: i32) { + let x: f64 = n as f64; + let y: f64 = n as f64; + assert(x == y); // FAILS: each cast is nondeterministic + } + } => Err(err) => assert_one_fails(err) +} + +test_verify_one_file! { + #[test] cast_same_float_identity verus_code! { + fn test_f64_identity(f: f64) { + let g: f64 = f as f64; + assert(f == g); // Same-type cast is identity + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] cast_usize_to_f64_unsupported verus_code! { + fn test_usize_as_f64(n: usize) { + let x: f64 = n as f64; + } + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `usize` to `f64`") +} + +test_verify_one_file! { + #[test] cast_f64_to_isize_unsupported verus_code! { + fn test_f64_as_isize(f: f64) { + let n: isize = f as isize; + } + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `f64` to `isize`") +} + +test_verify_one_file_with_options! { + #[test] cast_int_to_f16_unsupported ["no-auto-import-verus_builtin"] => code! { + #![cfg_attr(verus_keep_ghost, feature(f16))] + + use verus_builtin::*; + use verus_builtin_macros::*; + + verus! { + fn test_i32_as_f16(n: i32) { + let y: f16 = n as f16; + } + } + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast to `f16`") +} + +test_verify_one_file_with_options! { + #[test] cast_f16_to_int_unsupported ["no-auto-import-verus_builtin"] => code! { + #![cfg_attr(verus_keep_ghost, feature(f16))] + + use verus_builtin::*; + use verus_builtin_macros::*; + + verus! { + fn test_f16_as_i32(f: f16) { + let n: i32 = f as i32; + } + } + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `f16`") +} + +test_verify_one_file_with_options! { + #[test] cast_f16_to_f64_unsupported ["no-auto-import-verus_builtin"] => code! { + #![cfg_attr(verus_keep_ghost, feature(f16))] + + use verus_builtin::*; + use verus_builtin_macros::*; + + verus! { + fn test_f16_as_f64(f: f16) { + let d: f64 = f as f64; + } + } + } => Err(err) => assert_vir_error_msg(err, "Verus does not support `as` cast from `f16` to `f64`") +} + test_verify_one_file! { #[test] f32_ieee verus_code! { // TODO: replace explicit calls to ieee_cast with "as" when support for "as" is added diff --git a/source/vstd/float.rs b/source/vstd/float.rs index 626cac6a94..1e5bb1bf13 100644 --- a/source/vstd/float.rs +++ b/source/vstd/float.rs @@ -102,4 +102,31 @@ pub assume_specification[ ::clone ](f: &f64) -> (res: f64) res == f, ; +#[verifier::external_trait_specification] +pub trait ExIeeeFloatCast { + type ExternalTraitSpecificationFor: IeeeFloatCast; +} + +// TODO: when IEEE float support is merged, this should point to IeeeFloatCast::ieee_cast +pub uninterp spec fn ieee_float_cast, To>(from: From) -> To; + +pub uninterp spec fn float_cast_spec(from: From, to: To) -> bool; + +// Used only for internal Verus translation of "as" operator; +// this is not meant to be called directly by user code, +// and it is not actually compiled to executable code +#[cfg(verus_keep_ghost)] +#[doc(hidden)] +#[verifier::external_body] +#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::float::float_cast")] +#[verifier::when_used_as_spec(ieee_float_cast)] +pub fn float_cast, To>(from: From) -> (to: To) + ensures + float_cast_spec(from, to), + opens_invariants none + no_unwind +{ + unimplemented!{} +} + } // verus!