Contracts & Harnesses for `f{32,64}::to_int_unchecked` by Yenyun035 · Pull Request #134 · model-checking/verify-rust-std

Yenyun035 · 2024-10-24T04:07:34Z

Towards #59

(Resolved) Depends on this Kani Issue and this PR, as discussed in this thread in #59

(Resolved) Depends on this Kani Issue and this PR

(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.

…to-int-unchecked

…-0011-core-nums-yenyunw-f32-to-int-unchecked

…to-int-unchecked

…-0011-core-nums-yenyunw-f32-to-int-unchecked

Yenyun035 · 2024-11-08T21:11:17Z

@celinval @carolynzech @zhassan-aws @feliperodri I was able to run f32->i8 harness. One of the checks failed, and I guess it is because the contract is incorrect. Specifically, I think the Self::MAX and Self::MIN in the contract is referring to the max and min of the float type instead of the resulting integer type. Therefore, I tried to change the contract to use <Int>::MIN/MAX (because the doc mentioned "Be representable in the return type Int"), and it gave me "associated item not found in Int" error. I only found FloatToInt and did not find any docs related to Int.

My confusion is, how can I refer to the max/min of the resulting integer type given that the type parameters accessible from the context of the contract are Self and Int?

Check 14: <f32 as convert::num::FloatToInt>::to_int_unchecked.arithmetic_overflow.2
- Status: FAILURE
- Description: "float_to_int_unchecked: attempt to convert a value out of range of the target integer"
- Location: library/core/src/convert/num.rs:30:30 in function <f32 as convert::num::FloatToInt>::to_int_unchecked

Yenyun035 · 2024-11-09T07:51:56Z

My confusion is, how can I refer to the max/min of the resulting integer type given that the type parameters accessible from the context of the contract are Self and Int?

I found this workaround, inspired by this TypeChecker, and was able to run the f32->i8 harness (see here for unreachables). It took a while (~1.5 minutes) after compilation (Finished dev profile...) to start running the harness (Checking harness num::verify::checked_f32_to_int_unchecked_i8...), which is generally slower than previous harnesses.

// Tested for f32->i8
#[requires(self.is_finite() && ((type_name::<Int>().contains("i8") && self >= i8::MIN as Self) && (self <= i8::MAX as Self)))]
SUMMARY:
** 0 of 1283 failed (95 unreachable)
VERIFICATION:- SUCCESSFUL
Verification Time: 10.796687s
Complete - 1 successfully verified harnesses, 0 failures, 1 total.

While this workaround might work, I think it would be too messy in the end. I'm wondering if it's possible to have a macro generating functions that check if the float value is in the bound of an integer type, as shown in the example below. However, I think it might cause circular dependency. If there is no better way to make the contract cleaner, maybe we could still proceed with the aforementioned approach.

use core::any::type_name;// Not sure where to place; Not sure if this works.macro_rules! generate_is_in_range_check {($floatType:ty, $($intType:ty, $intStr:expr),+) => {
$(pubfn is_in_range<Int>(num: $floatType) -> bool{
type_name::<$intType>().contains($intStr) && num >= <$intType>::MINas $floatType && num <= <$intType>::MAXas $floatType
})+
}}generate_is_in_range_check!(f32,i8,"i8");Then the contract becomes:#[requires(self.is_finite() && is_in_range::<Int>(self))]

By the way, I also tried the TypeId::of comparison but got this error:

Contract:
#[requires(self.is_finite() && ((TypeId::of::<Int>() == TypeId::of::<i8> && self >= i8::MIN as Self) && (self <= i8::MAX as Self)))]
Result:
error[E0310]: the parameter type `Int` may not live long enough
--> /Users/yew005/Docs/Academic/CMU/Fall24/practicum/vrs/library/core/src/num/f32.rs:1078:38
|
1078 | #[requires(self.is_finite() && ((TypeId::of::<Int>() == TypeId::of::<i8>() && self >= i8::MIN as Self) && (self <= i8::MA...
| ^^^^^^^^^^^^^^^^^^^
| |
| the parameter type `Int` must be valid for the static lifetime...
| ...so that the type `Int` will meet its required lifetime bounds
|
help: consider adding an explicit lifetime bound
|
1079 | pub unsafe fn to_int_unchecked<Int: 'static>(self) -> Int
| +++++++++

@celinval @carolynzech @zhassan-aws @feliperodri I would appreciate any ideas and advice!

zhassan-aws · 2024-11-10T19:23:21Z

I think you should be able to define a macro that matches on the Int type, e.g.

macro_rules! foo {(u8, ...) => { ... }(u16, ...) => { ... }
....}

and use it in the contract.

Yenyun035 · 2024-11-11T23:12:08Z

I think you should be able to define a macro that matches on the Int type, ... and use it in the contract.

@feliperodri Thank you for your response! I tried this approach by adding the macro in mod verify in mod.rs and calling it in the function contract. However, as shown below, it gave me the error "no rules expected Int." I expected that if Int is type i8, it should match the first, i.e., (i8, ...) case. From the output, it looks like the Int and i8 etc primitive types are different. I'm. wondering why it happened. Appreciate any insights!

// mod.rspubmod verify {macro_rules! is_in_range {(i8, $floatType:ty, $num:ident) => { $num >= i8::MINas $floatType && $num <= i8::MAXas $floatType };(i16, $floatType:ty, $num:ident) => { $num >= i16::MINas $floatType && $num <= i16::MAXas $floatType };(i32, $floatType:ty, $num:ident) => { $num >= i32::MINas $floatType && $num <= i32::MAXas $floatType };(i64, $floatType:ty, $num:ident) => { $num >= i64::MINas $floatType && $num <= i64::MAXas $floatType };(i128, $floatType:ty, $num:ident) => { $num >= i128::MINas $floatType && $num <= i128::MAXas $floatType };(isize, $floatType:ty, $num:ident) => { $num >= isize::MINas $floatType && $num <= isize::MAXas $floatType };(u8, $floatType:ty, $num:ident) => { $num >= u8::MINas $floatType && $num <= u8::MAXas $floatType };(u16, $floatType:ty, $num:ident) => { $num >= u16::MINas $floatType && $num <= u16::MAXas $floatType };(u32, $floatType:ty, $num:ident) => { $num >= u32::MINas $floatType && $num <= u32::MAXas $floatType };(u64, $floatType:ty, $num:ident) => { $num >= u64::MINas $floatType && $num <= u64::MAXas $floatType };(u128, $floatType:ty, $num:ident) => { $num >= u128::MINas $floatType && $num <= u128::MAXas $floatType };(usize, $floatType:ty, $num:ident) => { $num >= usize::MINas $floatType && $num <= usize_isize_to_xe_bytes_doc::MAXas $floatType };}pub(crate)use is_in_range;}// Call in to_int_unchecked contract (f32.rs)usesuper::num::verify::is_in_range;#[requires(self.is_finite() && is_in_range!(Int,Self,self))]// Result
error: no rules expected `Int`
--> /path/to/repo/vrs/library/core/src/num/f32.rs:1076:49
|
1076 | #[requires(self.is_finite() && is_in_range!(Int,Self,self))]
| ^^^ no rules expected this token in macro call
|
::: /path/to/repo/vrs/library/core/src/num/mod.rs:1693:5
|
1693 | macro_rules! is_in_range {
| ------------------------ when calling this macro
|
note:while trying to match `i8`
--> /path/to/repo/vrs/library/core/src/num/mod.rs:1694:10
|
1694 | (i8, $floatType:ty, $num:ident) => { $num >= i8::MINas $floatType && $num <= i8::MAXas $floatType };
|

zhassan-aws · 2024-11-12T00:38:34Z

I see. The other alternative I could think of is to define a trait that provides min and max methods and implement it for each of the Int types. I'm not sure if there's a clean way to require Int to implement this trait though without affecting the non-Kani build.

zhassan-aws · 2024-11-12T01:03:34Z

There's also the issue of imprecision when casting an int value to a float. For instance, i32::MAX as f32 is 2147483647 as f32 which is 2147483648.0 (see #134). This means that the contract pre-condition is valid for the f32 value 2147483648.0 even though it's out of the range of an i32.

Not sure what the best approach here is. Both MIRI and (now) Kani have their own internal methods to check if the values are in range (e.g. see rust-lang/miri#1325). I wonder whether those can be somehow exposed in the library. Ideally, there should be a float_to_int_checked method, in which case we can just check if it returns Some.

Yenyun035 · 2024-11-12T04:30:54Z

There's also the issue of imprecision when casting an int value to a float. ...

Thank you for pointing this out! We will pay attention to it.

The other alternative I could think of is to define a trait ...
Both MIRI and (now) Kani have their own internal methods.... I wonder whether those can be somehow exposed in the library...

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

zhassan-aws · 2024-11-12T19:20:44Z

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 · 2024-11-12T20:26:42Z

@zhassan-aws I just filed this Feature Request. Thank you!

celinval · 2024-11-30T01:19:44Z

Hi @Yenyun035, we have updated the Kani version in this repo. You should be able to use the new API

Yenyun035 · 2024-11-30T05:27:35Z

@celinval Thank you! I have run Kani on all harnesses and updated the results in the above. It's ready for review now 👍

To compile, we need to add the -Z float-lib flag.

celinval · 2024-12-02T18:06:42Z

@celinval Thank you! I have run Kani on all harnesses and updated the results in the above. It's ready for review now 👍
To compile, we need to add the -Z float-lib flag.

Can you please add that to run-kani.sh around here:

verify-rust-std/scripts/run-kani.sh

Lines 214 to 216 in 7e8a03d

 -Z function-contracts \ 
 -Z mem-predicates \ 
 -Z loop-contracts \ 

Yenyun035 · 2024-12-03T07:49:02Z

@celinval @tautschnig @carolynzech @feliperodri Could you please review this PR and #163 as well? Thank you!

Yenyun035 · 2024-12-03T19:33:18Z

@zhassan-aws Thank you. Fixed.

Yenyun035 · 2024-12-03T23:10:35Z

unused import: use crate::ub_checks::float_to_int_in_range;

I found one of the checks failed due to the above error, but the function is indeed used in the contract:

#[requires(self.is_finite() && float_to_int_in_range::<Self,Int>(self))]

zhassan-aws · 2024-12-03T23:16:01Z

Try putting the import under #[cfg(kani)]

celinval

Thanks!!

Yenyun035 · 2024-12-04T07:23:04Z

@celinval Thank you. I fixed the import for this and #163.

Yenyun035and others added 9 commits October 22, 2024 09:46

f32 test harness & contracts
95d11f3

Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-f32-…
88f7363
…to-int-unchecked

Fix contracts && Initial draft of macro and harnesses
227d9ac

Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-f32-…
b875696
…to-int-unchecked

Merge main
70fe5d9

Merge branch 'main' of github.com:rajathkotyal/verify-rust-std into c…
5742a89
…-0011-core-nums-yenyunw-f32-to-int-unchecked

f128_float_to_int proofs
082ea5a

Fix comment
bb00a72

Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-f32-…
88c3411
…to-int-unchecked

Yenyun035 changed the title ~~Contracts & Harnesses for f32::to_int_unchecked~~Contracts & Harnesses for to_int_uncheckedOct 30, 2024

Yenyun035and others added 5 commits October 30, 2024 12:44

Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked
a661c16

Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-f32-…
c85ce2a
…to-int-unchecked

f64_float_to_int proofs
573e0a8

Merge branch 'main' of github.com:rajathkotyal/verify-rust-std into c…
39c6d63
…-0011-core-nums-yenyunw-f32-to-int-unchecked

Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked
1171a9c

Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked
869fe66

Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked
47b31f4

Yenyun035 mentioned this pull request Nov 12, 2024
Add support for in_range model-checking/kani#3711
Closed

Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked
13b1c22

carolynzech assigned zhassan-aws and carolynzech Nov 13, 2024

Yenyun035 marked this pull request as ready for review November 30, 2024 05:26

Yenyun035 requested a review from a team as a code owner November 30, 2024 05:26

tautschnig assigned celinval Dec 1, 2024

Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked
6898b71

celinval reviewed Dec 2, 2024
View reviewed changes

Comment threadlibrary/core/src/num/f32.rs Outdated

Yenyun035 added 3 commits December 2, 2024 13:39

Enable float-lib in kani script
1b08327

Add float_to_int_in_range to ub_checks && Fix contracts
895f055

Fix dummy float_to_int_in_range
8aefc7c

Yenyun035 requested a review from celinval December 3, 2024 00:29

Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked
e9200b2

zhassan-aws approved these changes Dec 3, 2024
View reviewed changes

Comment threadlibrary/core/src/ub_checks.rs Outdated
Comment threadlibrary/core/src/ub_checks.rs Outdated

Yenyun035and others added 2 commits December 3, 2024 11:31

Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked
0fec08b

Fix import and format
e4d69a7

Fix import
3afbb9d

zhassan-aws removed their assignment Dec 4, 2024

Add -Z float-lib to list command
7b978eb

celinval approved these changes Dec 4, 2024
View reviewed changes

Comment threadlibrary/core/src/num/f32.rs Outdated
Comment threadlibrary/core/src/num/f64.rs Outdated

Fix import
5efede8

zhassan-aws enabled auto-merge (squash) December 4, 2024 15:37

Merge branch 'main' into c-0011-core-nums-yenyunw-f32-to-int-unchecked
6e7838f

zhassan-aws approved these changes Dec 4, 2024
View reviewed changes

zhassan-aws merged commit 72323e4 into model-checking:mainDec 4, 2024

Uh oh!

Conversation

Yenyun035 commented Oct 24, 2024• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Changes

Verification Results

Uh oh!

Yenyun035 commented Nov 8, 2024• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Yenyun035 commented Nov 9, 2024

Uh oh!

zhassan-aws commented Nov 10, 2024

Uh oh!

Yenyun035 commented Nov 11, 2024• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

zhassan-aws commented Nov 12, 2024

Uh oh!

zhassan-aws commented Nov 12, 2024

Uh oh!

Yenyun035 commented Nov 12, 2024

Uh oh!

zhassan-aws commented Nov 12, 2024

Uh oh!

Yenyun035 commented Nov 12, 2024

Uh oh!

celinval commented Nov 30, 2024

Uh oh!

Yenyun035 commented Nov 30, 2024• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

celinval commented Dec 2, 2024

Uh oh!

Uh oh!

Yenyun035 commented Dec 3, 2024• edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Yenyun035 commented Dec 3, 2024

Uh oh!

Yenyun035 commented Dec 3, 2024

Uh oh!

zhassan-aws commented Dec 3, 2024

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Yenyun035 commented Dec 4, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Yenyun035 commented Oct 24, 2024•
edited
Loading

Yenyun035 commented Nov 8, 2024•
edited
Loading

Yenyun035 commented Nov 11, 2024•
edited
Loading

Yenyun035 commented Nov 30, 2024•
edited
Loading

Yenyun035 commented Dec 3, 2024•
edited
Loading