From 72323e497d4b4cd9e64f6d5cf204b4345eca5835 Mon Sep 17 00:00:00 2001 From: Yenyun035 <57857379+Yenyun035@users.noreply.github.com> Date: Wed, 4 Dec 2024 09:21:17 -0800 Subject: [PATCH] Contracts & Harnesses for `f{32,64}::to_int_unchecked` (#134) Towards / Resolves #59 (Resolved) Depends on [this Kani Issue](https://github.com/model-checking/kani/issues/3629) and [this PR](https://github.com/model-checking/kani/pull/3660), as discussed in [this thread](https://github.com/model-checking/verify-rust-std/issues/59#issuecomment-2428184293) in #59 (Resolved) Depends on [this Kani Issue](https://github.com/model-checking/kani/issues/3711) and [this PR](https://github.com/model-checking/kani/pull/3742) (Resolved) Waiting for Kani PR#3742 merged into `feature/verify-rust-std` f16 and f128 are in #163 ### Changes * Added contracts for `f{32,64}::to_int_unchecked` (located in `library/core/src/num/f{32,64}.rs`) * Added a macro for generating `to_int_unchecked` harnesses * Added harnesses for `f{32,64}to_int_unchecked` of each integer type * `i8`, `i16`, `i32`, `i64`, `i128`, `isize`, `u8`, `u16`, `u32`, `u64`, `u128`, `usize` --- 12 harnesses in total. ### Verification Results To compile, we need to add the `-Z float-lib` flag. ``` Checking harness num::verify::checked_f32_to_int_unchecked_usize... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.424911s Checking harness num::verify::checked_f64_to_int_unchecked_u128... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.8557353s Checking harness num::verify::checked_f32_to_int_unchecked_u16... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.195041s Checking harness num::verify::checked_f32_to_int_unchecked_i8... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.2361426s Checking harness num::verify::checked_f64_to_int_unchecked_i32... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.3952055s Checking harness num::verify::checked_f64_to_int_unchecked_i128... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 7.5295496s Checking harness num::verify::checked_f64_to_int_unchecked_u16... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.2897367s Checking harness num::verify::checked_f32_to_int_unchecked_i64... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.58576s Checking harness num::verify::checked_f64_to_int_unchecked_i16... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.2046432s Checking harness num::verify::checked_f32_to_int_unchecked_i128... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.8473463s Checking harness num::verify::checked_f32_to_int_unchecked_u8... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.131122s Checking harness num::verify::checked_f32_to_int_unchecked_i16... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.436728s Checking harness num::verify::checked_f32_to_int_unchecked_u128... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.666422s Checking harness num::verify::checked_f64_to_int_unchecked_u8... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.17829s Checking harness num::verify::checked_f32_to_int_unchecked_i32... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.6507607s Checking harness num::verify::checked_f64_to_int_unchecked_i64... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 7.3081775s Checking harness num::verify::checked_f64_to_int_unchecked_u64... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 7.0912967s Checking harness num::verify::checked_f64_to_int_unchecked_i8... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.4602604s Checking harness num::verify::checked_f64_to_int_unchecked_usize... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.9098988s Checking harness num::verify::checked_f64_to_int_unchecked_u32... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.557031s Checking harness num::verify::checked_f64_to_int_unchecked_isize... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 7.1193557s Checking harness num::verify::checked_f32_to_int_unchecked_u64... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.7919626s Checking harness num::verify::checked_f32_to_int_unchecked_u32... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.557074s Checking harness num::verify::checked_f32_to_int_unchecked_isize... VERIFICATION RESULT: ** 0 of 136 failed VERIFICATION:- SUCCESSFUL Verification Time: 6.710118s Complete - 24 successfully verified harnesses, 0 failures, 24 total. ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: rajathmCMU Co-authored-by: MWDZ Co-authored-by: Zyad Hassan --- library/core/src/num/f32.rs | 10 ++++++ library/core/src/num/f64.rs | 9 ++++++ library/core/src/num/mod.rs | 57 +++++++++++++++++++++++++++++++++++ library/core/src/ub_checks.rs | 10 ++++++ scripts/run-kani.sh | 4 +-- 5 files changed, 88 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index 47dfce7530fb7..fffc403470508 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -18,6 +18,14 @@ use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; +use safety::requires; + +#[cfg(kani)] +use crate::kani; + +#[allow(unused_imports)] +use crate::ub_checks::float_to_int_in_range; + /// The radix or base of the internal representation of `f32`. /// Use [`f32::RADIX`] instead. /// @@ -1054,6 +1062,8 @@ impl f32 { without modifying the original"] #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] + // is_finite() checks if the given float is neither infinite nor NaN. + #[requires(self.is_finite() && float_to_int_in_range::(self))] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, diff --git a/library/core/src/num/f64.rs b/library/core/src/num/f64.rs index c89023c1ae490..166fb2d329a5a 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.rs @@ -17,6 +17,13 @@ use crate::intrinsics; use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; +use safety::requires; + +#[cfg(kani)] +use crate::kani; + +#[allow(unused_imports)] +use crate::ub_checks::float_to_int_in_range; /// The radix or base of the internal representation of `f64`. /// Use [`f64::RADIX`] instead. @@ -1055,6 +1062,8 @@ impl f64 { without modifying the original"] #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] + // is_finite() checks if the given float is neither infinite nor NaN. + #[requires(self.is_finite() && float_to_int_in_range::(self))] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 761ae7ab06ff0..15452a7a508fc 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1831,6 +1831,21 @@ mod verify { } } + // Part 3: Float to Integer Conversion function Harness Generation Macro + macro_rules! generate_to_int_unchecked_harness { + ($floatType:ty, $($intType:ty, $harness_name:ident),+) => { + $( + #[kani::proof_for_contract($floatType::to_int_unchecked)] + pub fn $harness_name() { + let num1: $floatType = kani::any::<$floatType>(); + let result = unsafe { num1.to_int_unchecked::<$intType>() }; + + assert_eq!(result, num1 as $intType); + } + )+ + } + } + // `unchecked_add` proofs // // Target types: @@ -2128,4 +2143,46 @@ mod verify { generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128); generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize); + // `f{16,32,64,128}::to_int_unchecked` proofs + // + // Target integer types: + // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total + // + // Target contracts: + // 1. Float is not `NaN` and infinite + // 2. Float is representable in the return type `Int`, after truncating + // off its fractional part + // [requires(self.is_finite() && kani::float::float_to_int_in_range::(self))] + // + // Target function: + // pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt + generate_to_int_unchecked_harness!(f32, + i8, checked_f32_to_int_unchecked_i8, + i16, checked_f32_to_int_unchecked_i16, + i32, checked_f32_to_int_unchecked_i32, + i64, checked_f32_to_int_unchecked_i64, + i128, checked_f32_to_int_unchecked_i128, + isize, checked_f32_to_int_unchecked_isize, + u8, checked_f32_to_int_unchecked_u8, + u16, checked_f32_to_int_unchecked_u16, + u32, checked_f32_to_int_unchecked_u32, + u64, checked_f32_to_int_unchecked_u64, + u128, checked_f32_to_int_unchecked_u128, + usize, checked_f32_to_int_unchecked_usize + ); + + generate_to_int_unchecked_harness!(f64, + i8, checked_f64_to_int_unchecked_i8, + i16, checked_f64_to_int_unchecked_i16, + i32, checked_f64_to_int_unchecked_i32, + i64, checked_f64_to_int_unchecked_i64, + i128, checked_f64_to_int_unchecked_i128, + isize, checked_f64_to_int_unchecked_isize, + u8, checked_f64_to_int_unchecked_u8, + u16, checked_f64_to_int_unchecked_u16, + u32, checked_f64_to_int_unchecked_u32, + u64, checked_f64_to_int_unchecked_u64, + u128, checked_f64_to_int_unchecked_u128, + usize, checked_f64_to_int_unchecked_usize + ); } diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs index 5598c7bb41d38..9b7a64a43000e 100644 --- a/library/core/src/ub_checks.rs +++ b/library/core/src/ub_checks.rs @@ -219,12 +219,22 @@ mod predicates { let _ = (src, dst); true } + + /// Check if a float is representable in the given integer type + pub fn float_to_int_in_range(value: Float) -> bool + where + Float: core::convert::FloatToInt + { + let _ = value; + true + } } #[cfg(kani)] mod predicates { pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned, same_allocation}; + pub use crate::kani::float::float_to_int_in_range; } /// This trait should be used to specify and check type safety invariants for a diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index e32bb22c23f56..a576717849aca 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -214,15 +214,15 @@ main() { -Z function-contracts \ -Z mem-predicates \ -Z loop-contracts \ + -Z float-lib \ --output-format=terse \ $command_args \ --enable-unstable \ --cbmc-args --object-bits 12 elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." - "$kani_path" list -Z list -Z function-contracts -Z mem-predicates ./library --std > $path/kani_list.txt + "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std > $path/kani_list.txt fi } main -