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.

Sign up for GitHub

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

Jump to bottom

Add support for in_range #3711

Closed
Yenyun035 opened this issue Nov 12, 2024 · 2 comments · Fixed by #3742
Closed

Add support for in_range #3711

Yenyun035 opened this issue Nov 12, 2024 · 2 comments · Fixed by #3742
Assignees
@zhassan-aws
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests

Comments

@Yenyun035
Copy link

Yenyun035 commented Nov 12, 2024 •
edited
Loading

Requested feature: in_range to check if a float is in the range of the targeting integer type, e.g.

kani::in_range(IntType, floatType, float) or something similar
Example: f32::to_int_unchecked contract
#[requires(self.is_finite() && kani::in_range(Int, Self, self))]
pub unsafe fn to_int_unchecked<Int>(self) -> Int where Self: FloatToInt<Int> {...}

Full Discussion:

Thank you for sharing this. Is it possible to have Kani support this? E.g. expose an in_range(float, floatType, IntType) API that we can directly call. We saw that the Kani internally has codegen_in_range_expr which we think useful.
Thank you! @zhassan-aws

Yes, I think it would be possible. This would likely need to be done through providing a trait and its implementation for different float types so that it can be used with the generic Int. Can you file a feature request in the Kani repo?
@Yenyun035 Yenyun035 added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Nov 12, 2024
@Yenyun035 Yenyun035 mentioned this issue Nov 12, 2024
Merged
@Yenyun035 Yenyun035 mentioned this issue Nov 14, 2024
Merged
@celinval
Copy link
Contributor

We're taking a look at it. Thanks

@celinval celinval added the T-User Tag user issues / requests label Nov 20, 2024
@Yenyun035 Yenyun035 mentioned this issue Nov 22, 2024
Open
@zhassan-aws zhassan-aws mentioned this issue Nov 27, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Nov 28, 2024
@zhassan-aws
Add a Kani function that checks if the range of a float is valid for …
e53511e 
…conversion to int (#3742)

This introduces a new generic Kani function,
`kani::float::float_to_int_in_range`, that can be used for checking if a
floating-point value satisfies the range requirement of the
`to_int_unchecked` methods, e.g
https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked
and
https://doc.rust-lang.org/std/primitive.f64.html#method.to_int_unchecked.

Resolves #3711 

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

Thanks!

@celinval Will the changes be merged into the feature/verify-rust-std branch?

zhassan-aws added a commit to model-checking/verify-rust-std that referenced this issue Dec 4, 2024
@Yenyun035 @rajathkotyal
@MWDZ @zhassan-aws
Contracts & Harnesses for f{32,64}::to_int_unchecked (#134)
72323e4 
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@zhassan-aws zhassan-aws

Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. T-User Tag user issues / requests
Projects
None yet
Milestone
No milestone
3 participants
@celinval @Yenyun035 @zhassan-aws