[P3-Float-to-Int Conversion] `f32::to_int_unchecked`

Yenyun035 commented 1 month ago

Official Repo Tracking Issue

Tasks :

Write a proof for verifying the absence of arithmetic overflow/underflow and undefined behavior for the function.
Add proofs into a dedicated file, e.g. library/core/src/num/xx.rs
Please make sure not to modify other people's code, since we will be co-working on the same files. Avoid code conflicts as much as possible. Pull code every time a merge is made.

IMP: comment with the branch name you will be working on, with its link.

Ref: https://github.com/rajathkotyal/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md

Yenyun035 commented 2 weeks ago

An error I encountered when running a Kani harness. I both tried to build kani from the updated features/verify-rust-std branch and use the kani script. Both failed.

Reason: float_to_int_unchecked not yet supporting f128 and f16. Remove f128/f16 harnesses temporarily and can run harnesses.

Command: ./scripts/run-kani.sh --kani-args --harness checked_f32_to_int_unchecked_i8

Yenyun035 commented 2 weeks ago

Failed a check: Looking into it

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 commented 2 weeks ago

Guess: The contract is incorrect. Maybe self::MIN and self::MAX refer to the max and min of the float type, not that of the resulting integer type.

Yenyun035 commented 2 weeks ago

Distinct unreachables in f32->i8 result:

Check 1: str::pattern::TwoWaySearcher::byteset_contains.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to shift right with overflow"
         - Location: library/core/src/str/pattern.rs:1454:9 in function str::pattern::TwoWaySearcher::byteset_contains
...
Check 4: ops::range::RangeInclusive::<usize>::into_slice_range.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to add with overflow"
         - Location: library/core/src/ops/range.rs:458:29 in function ops::range::RangeInclusive::<usize>::into_slice_range

Check 5: ptr::const_ptr::<impl *const T>::is_aligned_to::runtime_impl.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: library/core/src/ptr/const_ptr.rs:1645:26 in function ptr::const_ptr::<impl *const T>::is_aligned_to::runtime_impl
...
Check 7: <str::pattern::StrSearcher<'_, '_> as str::pattern::Searcher<'_>>::next.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to add with overflow"
         - Location: library/core/src/str/pattern.rs:1161:29 in function <str::pattern::StrSearcher<'_, '_> as str::pattern::Searcher<'_>>::next
...
Check 54: slice::memchr::memchr.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to multiply with overflow"
         - Location: library/core/src/slice/memchr.rs:29:21 in function slice::memchr::memchr

Check 55: slice::memchr::memchr_aligned.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to multiply with overflow"
         - Location: library/core/src/slice/memchr.rs:82:27 in function slice::memchr::memchr_aligned
...
Check 73: str::pattern::TwoWaySearcher::maximal_suffix.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to add with overflow"
         - Location: library/core/src/str/pattern.rs:1639:38 in function str::pattern::TwoWaySearcher::maximal_suffix
...
Check 89: <&str as str::pattern::Pattern>::is_contained_in.assertion.1
         - Status: UNREACHABLE
         - Description: "index out of bounds: the length is less than or equal to the given index"
         - Location: library/core/src/str/pattern.rs:1001:58 in function <&str as str::pattern::Pattern>::is_contained_in
..
Check 122: str::validations::utf8_acc_cont_byte.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to shift left with overflow"
         - Location: library/core/src/str/validations.rs:20:5 in function str::validations::utf8_acc_cont_byte

Check 123: str::<impl str>::is_char_boundary.assertion.1
         - Status: UNREACHABLE
         - Description: "index out of bounds: the length is less than or equal to the given index"
         - Location: library/core/src/str/mod.rs:211:13 in function str::<impl str>::is_char_boundary

Check 124: num::<impl isize>::overflowing_neg.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to negate with overflow"
         - Location: library/core/src/num/int_macros.rs:2698:18 in function num::<impl isize>::overflowing_neg
...
Check 136: str::pattern::TwoWaySearcher::reverse_maximal_suffix.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to add with overflow"
         - Location: library/core/src/str/pattern.rs:1686:15 in function str::pattern::TwoWaySearcher::reverse_maximal_suffix
...
Check 163: ub_checks::is_valid_allocation_size.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to divide by zero"
         - Location: library/core/src/ub_checks.rs:128:54 in function ub_checks::is_valid_allocation_size
...
Check 173: str::pattern::TwoWaySearcher::byteset_create::{closure#0}.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to shift left with overflow"
         - Location: library/core/src/str/pattern.rs:1449:38 in function str::pattern::TwoWaySearcher::byteset_create::{closure#0}
...
Check 176: str::validations::utf8_first_byte.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to shift right with overflow"
         - Location: library/core/src/str/validations.rs:14:13 in function str::validations::utf8_first_byte
...
Check 180: str::slice_error_fail_rt.assertion.2
         - Status: UNREACHABLE
         - Description: "attempt to add with overflow"
         - Location: library/core/src/str/mod.rs:110:34 in function str::slice_error_fail_rt
...
Check 186: str::pattern::TwoWaySearcher::next::<str::pattern::RejectAndMatch>.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: library/core/src/str/pattern.rs:1469:27 in function str::pattern::TwoWaySearcher::next::<str::pattern::RejectAndMatch>
...
Check 218: slice::memchr::memchr_naive.assertion.1
         - Status: UNREACHABLE
         - Description: "index out of bounds: the length is less than or equal to the given index"
         - Location: library/core/src/slice/memchr.rs:43:12 in function slice::memchr::memchr_naive
...
Check 223: char::convert::char_try_from_u32.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: library/core/src/char/convert.rs:252:44 in function char::convert::char_try_from_u32
...
Check 226: str::pattern::TwoWaySearcher::next::<str::pattern::MatchOnly>.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: library/core/src/str/pattern.rs:1469:27 in function str::pattern::TwoWaySearcher::next::<str::pattern::MatchOnly>
...
Check 252: str::pattern::TwoWaySearcher::new.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to add with overflow"
         - Location: library/core/src/str/pattern.rs:1398:49 in function str::pattern::TwoWaySearcher::new
...
Check 257: ptr::align_offset::mod_inv.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: library/core/src/ptr/mod.rs:1923:49 in function ptr::align_offset::mod_inv
...
Check 266: <slice::iter::Iter<'_, u8> as iter::traits::iterator::Iterator>::rposition::<{closure@/Users/yew005/Docs/Academic/CMU/Fall24/practicum/vrs/library/core/src/str/mod.rs:246:28: 246:31}>.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to subtract with overflow"
         - Location: library/core/src/slice/iter/macros.rs:369:21 in function <slice::iter::Iter<'_, u8> as iter::traits::iterator::Iterator>::rposition::<{closure@<path/to/verify-rust-std/library/core/src/str/mod.rs:246:28: 246:31}>
...
Check 269: str::<impl str>::floor_char_boundary.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to add with overflow"
         - Location: library/core/src/str/mod.rs:249:22 in function str::<impl str>::floor_char_boundary
...
Check 275: str::validations::next_code_point::<'_, slice::iter::Iter<'_, u8>>.assertion.1
         - Status: UNREACHABLE
         - Description: "attempt to shift left with overflow"
         - Location: library/core/src/str/validations.rs:60:14 in function str::validations::next_code_point::<'_, slice::iter::Iter<'_, u8>>

rajathkotyal / verify-rust-std

[P3-Float-to-Int Conversion] `f32::to_int_unchecked` #13