Add support for int to float casts#189
Conversation
| ty::FloatTy::F128 => BitVecSize::BitVec128, | ||
| })?; | ||
|
|
||
| let i = match float { |
There was a problem hiding this comment.
Give this as proper name. backend_type, maybe?
| 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 { |
| | BinOpKind::PermPermDiv => crate::TYPE_PERM.upcast_ty(), | ||
| BinOpKind::FractionalPerm => crate::TYPE_PERM.upcast_ty(), |
There was a problem hiding this comment.
| | BinOpKind::PermPermDiv => crate::TYPE_PERM.upcast_ty(), | |
| BinOpKind::FractionalPerm => crate::TYPE_PERM.upcast_ty(), | |
| | BinOpKind::PermPermDiv | |
| | BinOpKind::FractionalPerm => crate::TYPE_PERM.upcast_ty(), |
| 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)), | ||
| ); |
There was a problem hiding this comment.
On Zulip you said:
Surely, this is not the best way [...]
What would the alternatives be? What happens if we cast integers that can't be represented exactly by a float, and is the behaviour consistent with Rust? For example:
fn main() {
let x = 9007199254740993i64;
println!("{}", x);
println!("{}", x as f64);
}Since x is beyond the maximum safe integer for f64, this prints:
9007199254740993
9007199254740992
There was a problem hiding this comment.
What would the alternatives be?
I just realized during adding support for float->int that it makes more sense to use the SMT function to convert from int to real instead of doing the division. I'll probably close this PR and open a new PR for float->int and int->float
There was a problem hiding this comment.
And yes the case you mentioned works
| @@ -0,0 +1,19 @@ | |||
| // This currently works with CVC5 but not with Z3.. | |||
There was a problem hiding this comment.
This is not a terribly useful comment (nor the right style). Why does it not work with Z3? Do any of the assertions here work? Can we add assertions to make it work?
Either way maybe this should not be in the testsuite. (Yet? Ever?) We could have some tests which are CVC5-specific, in which case we should configure them as such using comments that provide the requisite flags to Prusti (and indirectly Silicon) to make it use CVC5.
There was a problem hiding this comment.
Z3 just somehow fails to reason about it. Even cases like 1 -> 1.0 fail. This seems to be more like a Z3 issue. Therefore, I added the test case since we can now create a proper encoding for this cast without crashing. Even if the resulting Viper file doesn't verify with Z3
There was a problem hiding this comment.
Interestingly, Z3 only struggles with int -> float. float -> int (which is more complicated because of the bounds checking) is not a problem
2 participants
This PR adds support for IntToFloat casts by converting the Viper Int to a Viper Perm (Real) and using this to create an SMT float. This does currently not seem to work with z3 (Verification fails) but it works without issues with cvc5 (see test file).