Skip to content

Commit 72323e4

Browse files
Yenyun035rajathkotyalMWDZzhassan-aws
authored
Contracts & Harnesses for f{32,64}::to_int_unchecked (#134)
Towards / Resolves #59 (Resolved) Depends on [this Kani Issue](model-checking/kani#3629) and [this PR](model-checking/kani#3660), as discussed in [this thread](#59 (comment)) in #59 (Resolved) Depends on [this Kani Issue](model-checking/kani#3711) and [this PR](model-checking/kani#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 <rajathkotyal@gmail.com> Co-authored-by: MWDZ <jinjunfeng721@gmail.com> Co-authored-by: Zyad Hassan <zyadh@amazon.com>
1 parent d9780d6 commit 72323e4

File tree

5 files changed

+88
-2
lines changed

5 files changed

+88
-2
lines changed

‎library/core/src/num/f32.rs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,14 @@ use crate::mem;
1818
use crate::num::FpCategory;
1919
use crate::panic::const_assert;
2020

21+
use safety::requires;
22+
23+
#[cfg(kani)]
24+
use crate::kani;
25+
26+
#[allow(unused_imports)]
27+
use crate::ub_checks::float_to_int_in_range;
28+
2129
/// The radix or base of the internal representation of `f32`.
2230
/// Use [`f32::RADIX`] instead.
2331
///
@@ -1054,6 +1062,8 @@ impl f32 {
10541062
without modifying the original"]
10551063
#[stable(feature = "float_approx_unchecked_to", since = "1.44.0")]
10561064
#[inline]
1065+
// is_finite() checks if the given float is neither infinite nor NaN.
1066+
#[requires(self.is_finite() && float_to_int_in_range::<Self, Int>(self))]
10571067
pub unsafe fn to_int_unchecked<Int>(self) -> Int
10581068
where
10591069
Self: FloatToInt<Int>,

‎library/core/src/num/f64.rs‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,13 @@ use crate::intrinsics;
1717
use crate::mem;
1818
use crate::num::FpCategory;
1919
use crate::panic::const_assert;
20+
use safety::requires;
21+
22+
#[cfg(kani)]
23+
use crate::kani;
24+
25+
#[allow(unused_imports)]
26+
use crate::ub_checks::float_to_int_in_range;
2027

2128
/// The radix or base of the internal representation of `f64`.
2229
/// Use [`f64::RADIX`] instead.
@@ -1055,6 +1062,8 @@ impl f64 {
10551062
without modifying the original"]
10561063
#[stable(feature = "float_approx_unchecked_to", since = "1.44.0")]
10571064
#[inline]
1065+
// is_finite() checks if the given float is neither infinite nor NaN.
1066+
#[requires(self.is_finite() && float_to_int_in_range::<Self, Int>(self))]
10581067
pub unsafe fn to_int_unchecked<Int>(self) -> Int
10591068
where
10601069
Self: FloatToInt<Int>,

‎library/core/src/num/mod.rs‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1831,6 +1831,21 @@ mod verify {
18311831
}
18321832
}
18331833

1834+
// Part 3: Float to Integer Conversion function Harness Generation Macro
1835+
macro_rules! generate_to_int_unchecked_harness {
1836+
($floatType:ty, $($intType:ty, $harness_name:ident),+) => {
1837+
$(
1838+
#[kani::proof_for_contract($floatType::to_int_unchecked)]
1839+
pub fn $harness_name() {
1840+
let num1: $floatType = kani::any::<$floatType>();
1841+
let result = unsafe { num1.to_int_unchecked::<$intType>() };
1842+
1843+
assert_eq!(result, num1 as $intType);
1844+
}
1845+
)+
1846+
}
1847+
}
1848+
18341849
// `unchecked_add` proofs
18351850
//
18361851
// Target types:
@@ -2128,4 +2143,46 @@ mod verify {
21282143
generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128);
21292144
generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);
21302145

2146+
// `f{16,32,64,128}::to_int_unchecked` proofs
2147+
//
2148+
// Target integer types:
2149+
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
2150+
//
2151+
// Target contracts:
2152+
// 1. Float is not `NaN` and infinite
2153+
// 2. Float is representable in the return type `Int`, after truncating
2154+
// off its fractional part
2155+
// [requires(self.is_finite() && kani::float::float_to_int_in_range::<Self, Int>(self))]
2156+
//
2157+
// Target function:
2158+
// pub unsafe fn to_int_unchecked<Int>(self) -> Int where Self: FloatToInt<Int>
2159+
generate_to_int_unchecked_harness!(f32,
2160+
i8, checked_f32_to_int_unchecked_i8,
2161+
i16, checked_f32_to_int_unchecked_i16,
2162+
i32, checked_f32_to_int_unchecked_i32,
2163+
i64, checked_f32_to_int_unchecked_i64,
2164+
i128, checked_f32_to_int_unchecked_i128,
2165+
isize, checked_f32_to_int_unchecked_isize,
2166+
u8, checked_f32_to_int_unchecked_u8,
2167+
u16, checked_f32_to_int_unchecked_u16,
2168+
u32, checked_f32_to_int_unchecked_u32,
2169+
u64, checked_f32_to_int_unchecked_u64,
2170+
u128, checked_f32_to_int_unchecked_u128,
2171+
usize, checked_f32_to_int_unchecked_usize
2172+
);
2173+
2174+
generate_to_int_unchecked_harness!(f64,
2175+
i8, checked_f64_to_int_unchecked_i8,
2176+
i16, checked_f64_to_int_unchecked_i16,
2177+
i32, checked_f64_to_int_unchecked_i32,
2178+
i64, checked_f64_to_int_unchecked_i64,
2179+
i128, checked_f64_to_int_unchecked_i128,
2180+
isize, checked_f64_to_int_unchecked_isize,
2181+
u8, checked_f64_to_int_unchecked_u8,
2182+
u16, checked_f64_to_int_unchecked_u16,
2183+
u32, checked_f64_to_int_unchecked_u32,
2184+
u64, checked_f64_to_int_unchecked_u64,
2185+
u128, checked_f64_to_int_unchecked_u128,
2186+
usize, checked_f64_to_int_unchecked_usize
2187+
);
21312188
}

‎library/core/src/ub_checks.rs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -219,12 +219,22 @@ mod predicates {
219219
let _ = (src, dst);
220220
true
221221
}
222+
223+
/// Check if a float is representable in the given integer type
224+
pub fn float_to_int_in_range<Float, Int>(value: Float) -> bool
225+
where
226+
Float: core::convert::FloatToInt<Int>
227+
{
228+
let _ = value;
229+
true
230+
}
222231
}
223232

224233
#[cfg(kani)]
225234
mod predicates {
226235
pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned,
227236
same_allocation};
237+
pub use crate::kani::float::float_to_int_in_range;
228238
}
229239

230240
/// This trait should be used to specify and check type safety invariants for a

‎scripts/run-kani.sh‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -214,15 +214,15 @@ main() {
214214
-Z function-contracts \
215215
-Z mem-predicates \
216216
-Z loop-contracts \
217+
-Z float-lib \
217218
--output-format=terse \
218219
$command_args \
219220
--enable-unstable \
220221
--cbmc-args --object-bits 12
221222
elif [[ "$run_command" == "list" ]]; then
222223
echo "Running Kani list command..."
223-
"$kani_path" list -Z list -Z function-contracts -Z mem-predicates ./library --std > $path/kani_list.txt
224+
"$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std > $path/kani_list.txt
224225
fi
225226
}
226227

227228
main
228-

0 commit comments

Comments
 (0)