Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for float_to_int_unchecked #3629

Open
celinval opened this issue Oct 22, 2024 · 3 comments · May be fixed by #3660
Open

Add support for float_to_int_unchecked #3629

celinval opened this issue Oct 22, 2024 · 3 comments · May be fixed by #3660
Assignees

Comments

@celinval
Copy link
Contributor

          Hi @carolynzech @celinval @feliperodri @zhassan-aws 

When I was testing my harness for f32::to_int_unchecked, I encountered the error indicating that float_to_int_unchecked is not currently supported by Kani, as shown below. Is it possible to support it?

SUMMARY:
 ** 1 of 1277 failed (1276 undetermined)
Failed Checks: float_to_int_unchecked is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose
 File: "/Users/yew005/Docs/Academic/CMU/Fall24/practicum/verify-rust-std/library/core/src/convert/num.rs", line 30, in <f32 as convert::num::FloatToInt<i32>>::to_int_unchecked

VERIFICATION:- FAILED
** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details.
Verification Time: 5.8839436s

Summary:
Verification failed for - num::verify::checked_to_int_unchecked_f32
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

library/core/src/convert/num.rs Line 20 to 35:

20 macro_rules! impl_float_to_int {
21     ($Float:ty => $($Int:ty),+) => {
22         #[unstable(feature = "convert_float_to_int", issue = "67057")]
23         impl private::Sealed for $Float {}
24         $(
25             #[unstable(feature = "convert_float_to_int", issue = "67057")]
26             impl FloatToInt<$Int> for $Float {
27                 #[inline]
28                 unsafe fn to_int_unchecked(self) -> $Int {
29                     // SAFETY: the safety contract must be upheld by the caller.
30                     unsafe { crate::intrinsics::float_to_int_unchecked(self) }
31                 }
32            }
33         )+
34     }
35 }

Test harness:

#[kani::proof_for_contract(f32::to_int_unchecked)]
pub fn checked_to_int_unchecked_f32() {
    let num1: f32 = kani::any::<f32>();

    let result = unsafe { num1.to_int_unchecked::<i32>() };

    assert_eq!(result, num1 as i32);
}

Contracts added to f32::to_int_unchecked (in library/core/src/num/f32.rs):

/// # Safety
///
/// The value must:
///
/// * Not be `NaN`
/// * Not be infinite
/// * Be representable in the return type `Int`, after truncating off its fractional part
/// ...
#[requires(!self.is_nan() && !self.is_infinite())]
#[requires(self >= Self::MIN && self <= Self::MAX)]
pub unsafe fn to_int_unchecked<Int>(self) -> Int
where
    Self: FloatToInt<Int>,
{ ... }

Thank you very much!

Originally posted by @Yenyun035 in model-checking/verify-rust-std#59 (comment)

@Yenyun035
Copy link

Yenyun035 commented Oct 29, 2024

@zhassan-aws @celinval Hello! May I know if there are any updates to share for this issue? Thank you very much!

@zhassan-aws
Copy link
Contributor

@Yenyun035 I'm currently working on it. The PR should be out by tomorrow.

@zhassan-aws zhassan-aws linked a pull request Oct 30, 2024 that will close this issue
@zhassan-aws
Copy link
Contributor

#3660 adds support for f32 and f64.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants