Contracts & Harnesses for [f16, f128] to_int_unchecked #163

MWDZ · 2024-11-14T01:12:59Z

Towards #59

Changes

Added contracts for f{16,128}::to_int_unchecked (located in library/core/src/num/f[16, 32].rs)
Added a macro for generating to_int_unchecked harnesses
Added harnesses for to_int_unchecked of each integer type i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize --- 12 harnesses in total.

Revalidation

Per the discussion in Challenge 11: Safety of Methods for Numeric Primitive Types #59, we have to build and run Kani from feature/verify-rust-std branch.
To revalidate the verification results, run the following command. <harness_to_run> can be either num::verify to run all harnesses or num::verify::<harness_name> (e.g. checked_f32_to_int_unchecked_i8) to run a specific harness.

kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Yenyun035 · 2024-11-14T01:17:00Z

Note: This PR is similar to PR #134 -- it depends on Kani Issue #3711. In addition, as far as I know, float_to_int_unchecked has not supported f16 and f128 (please correct me if this is resolved @celinval).

…hecked

Yenyun035 · 2024-11-30T05:42:17Z

Note: This PR is similar to PR #134 -- it depends on Kani Issue #3711.

Resolved. Once tested, it's ready for review.

…hecked

Yenyun035 · 2024-12-02T06:42:39Z

@celinval @zhassan-aws Why could f16 and f128 harnesses pass all Kani verification checks given that float_to_int_unchecked is not currently supported for f16 and f128?

zhassan-aws · 2024-12-02T19:39:22Z

@Yenyun035 Support for f16 and f128 was added in model-checking/kani#3701.

Yenyun035 · 2024-12-02T21:46:28Z

Support for f16 and f128 was added in model-checking/kani#3701.

Got it. Thanks! That makes sense.

Yenyun035 · 2024-12-02T22:13:24Z

Depends on #134, as discussed here (updated ub_checks and kani script).

…hecked

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>

tautschnig · 2024-12-04T17:32:24Z

@MWDZ Now that #134 has been merged, could you please resolve conflicts?

celinval

Thanks!

library/core/src/num/mod.rs

…hecked

Yenyun035 · 2024-12-04T18:46:58Z

@tautschnig @celinval Thank you. Conflicts resolved. Harnesses un-commented. 👍

…hecked

feat: add f16, f128 to_int harness

055d138

Yenyun035 and others added 3 commits November 13, 2024 17:17

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

060ca3d

…hecked

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

9cba6ed

…hecked

fix: add placeholder to to_int_uncheck

1293c9c

tautschnig assigned MWDZ Nov 27, 2024

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

ab44dd1

…hecked

Yenyun035 mentioned this pull request Nov 29, 2024

Contracts & Harnesses for f{32,64}::to_int_unchecked #134

Merged

Yenyun035 and others added 3 commits November 29, 2024 21:19

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

459b5b2

…hecked

Fix contracts, import, comments

a9276e6

Fix harness names

63ae66b

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

68e809d

…hecked

MWDZ marked this pull request as ready for review December 2, 2024 22:07

MWDZ requested a review from a team as a code owner December 2, 2024 22:07

Fix contracts

2727ced

Yenyun035 and others added 4 commits December 2, 2024 17:49

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

91415ad

…hecked

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

b9c194a

…hecked

Fix import

5cae656

Fix import

2d3c57f

celinval reviewed Dec 4, 2024

View reviewed changes

library/core/src/num/mod.rs Outdated Show resolved Hide resolved

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

3466c30

…hecked

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

663e070

…hecked

zhassan-aws approved these changes Dec 4, 2024

View reviewed changes

Merge branch 'main' into c-0011-core-nums-junfeng-f16-f128-to-int-unc…

c22c6c3

…hecked

feliperodri approved these changes Dec 5, 2024

View reviewed changes

feliperodri enabled auto-merge (squash) December 5, 2024 05:29

feliperodri merged commit 30c756d into model-checking:main Dec 5, 2024
9 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Contracts & Harnesses for [f16, f128] to_int_unchecked #163

Contracts & Harnesses for [f16, f128] to_int_unchecked #163

MWDZ commented Nov 14, 2024

Yenyun035 commented Nov 14, 2024 •

edited

Loading

Yenyun035 commented Nov 30, 2024

Yenyun035 commented Dec 2, 2024 •

edited

Loading

zhassan-aws commented Dec 2, 2024

Yenyun035 commented Dec 2, 2024 •

edited

Loading

Yenyun035 commented Dec 2, 2024 •

edited

Loading

tautschnig commented Dec 4, 2024

celinval left a comment •

edited

Loading

Yenyun035 commented Dec 4, 2024

Contracts & Harnesses for [f16, f128] to_int_unchecked #163

Contracts & Harnesses for [f16, f128] to_int_unchecked #163

Conversation

MWDZ commented Nov 14, 2024

Changes

Revalidation

Yenyun035 commented Nov 14, 2024 • edited Loading

Yenyun035 commented Nov 30, 2024

Yenyun035 commented Dec 2, 2024 • edited Loading

zhassan-aws commented Dec 2, 2024

Yenyun035 commented Dec 2, 2024 • edited Loading

Yenyun035 commented Dec 2, 2024 • edited Loading

tautschnig commented Dec 4, 2024

celinval left a comment • edited Loading

Choose a reason for hiding this comment

Yenyun035 commented Dec 4, 2024

Yenyun035 commented Nov 14, 2024 •

edited

Loading

Yenyun035 commented Dec 2, 2024 •

edited

Loading

Yenyun035 commented Dec 2, 2024 •

edited

Loading

Yenyun035 commented Dec 2, 2024 •

edited

Loading

celinval left a comment •

edited

Loading