Towards / Resolves rust-lang#59 (Resolved) Depends on [this Kani Issue](model-checking/kani#3629) and [this PR](model-checking/kani#3660), as discussed in [this thread](model-checking#59 (comment)) in rust-lang#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 rust-lang#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>

State effect calculation too aggressive. #134

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions