Add support for float_to_int_unchecked #3660

zhassan-aws · 2024-10-30T06:23:00Z

This PR adds support for the float_to_int_unchecked intrinsic for f32 and f64.

Towards #3629

Keeping it as draft till I add more tests.

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

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

tautschnig · 2024-10-30T10:19:48Z

Please don't forget to update docs/src/rust-feature-support/intrinsics.md.

zhassan-aws · 2024-10-31T00:46:24Z

Please don't forget to update docs/src/rust-feature-support/intrinsics.md.

Thanks for the reminder. Added.

zhassan-aws · 2024-10-31T02:05:16Z

This PR could use quite a bit of cleanup, especially around hard-coded values and unit tests. In particular, it's probably better to store the hard-coded values using their byte representation as opposed to their decimal one.

celinval

Should we be worried about the cast using as logic?

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

zhassan-aws · 2024-10-31T06:45:25Z

I did a fairly big overhaul of the PR in 08531f6:

I've added all the constants using their byte representation. This is to avoid any questionable casts using as. These constants are now the single source of truth.
I added unit tests that verify that all the values are indeed lower and upper bounds of the corresponding int/uint types. The tests use BigInt to guarantee they work for all int types.
I removed the unit tests that were checking that the decimal value can be represented as f32/f64 because we're no longer using decimal values anywhere.

@celinval This should address some of your comments.

celinval · 2024-11-01T04:25:04Z

I'm really sorry, I think you might've misunderstood my comment about the as. I think we should be using as in the kani-compiler code since this is getting rustc's values as the source of truth.

My comment about the as is about Kani's implementation of casting float to integer using as. I would expect the same bounds to be used for both, but it sounds like we don't.

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

zhassan-aws · 2024-11-01T06:31:24Z

I'm really sorry, I think you might've misunderstood my comment about the as. I think we should be using as in the kani-compiler code since this is getting rustc's values as the source of truth.

Not at all. I was planning to make this change before your comment. The reason is that casting a decimal value into a floating-point value can have surprising behavior. For example, this program:

    println!("{}", u32::MAX);
    let f1: f32 = u32::MAX as f32;
    let f2: f32 = u32::MAX as f32 + 1.0;
    let f3: f32 = (u32::MAX as u128 + 1) as f32;
    
    println!("{:.32}", f1);
    println!("{:.32}", f2);
    println!("{:.32}", f3);

prints:

4294967295
4294967296.00000000000000000000000000000000
4294967296.00000000000000000000000000000000
4294967296.00000000000000000000000000000000

So casting the decimal value u32::MAX (4294967295) to a float results in a different number. This is because the cast operation rounds to the nearest number that can be represented as an f32. In other words, when assigning an f32 a decimal value, the actual value it stores may end up being different (could be smaller or larger). This calculator, which @tautschnig pointed out to me helped me determine the correct bounds:

https://www.h-schmidt.net/FloatConverter/IEEE754.html

One way to specify a floating-point value unambiguously is to use the byte representation. This is the reason I switched to it.

zhassan-aws · 2024-11-06T02:53:36Z

I made a few final touches:

Moved most of the code to a new float_utils module to avoid polluting intrinsics.rs (Thanks @celinval for the suggestion)
I added the code I used to determine the bounds as a unit test. If run with --nocapture, it'll print the constants.
I added a small optimization that skips the comparison if the bound is +/- infinity.

@tautschnig @celinval Let me know if you want to take another look. Otherwise, I'll go ahead and merge.

celinval

It's fine by me. Thanks!

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>

@zhassan-aws

Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.56.0"/version = "0.57.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Remove the overflow checks for wrapping_offset by @zhassan-aws in model-checking#3589 * `kani-cov`: A coverage tool for Kani by @adpaco-aws in model-checking#3121 * Automatic toolchain upgrade to nightly-2024-10-04 by @github-actions in model-checking#3570 * Automatic toolchain upgrade to nightly-2024-10-05 by @github-actions in model-checking#3591 * Automatic toolchain upgrade to nightly-2024-10-06 by @github-actions in model-checking#3592 * Exclude Charon from workspace by @zhassan-aws in model-checking#3580 * Support fully-qualified --package arguments by @celinval in model-checking#3593 * Automatic toolchain upgrade to nightly-2024-10-07 by @github-actions in model-checking#3595 * Automatic toolchain upgrade to nightly-2024-10-08 by @github-actions in model-checking#3597 * Automatic cargo update to 2024-10-14 by @github-actions in model-checking#3598 * Bump tests/perf/s2n-quic from `17171ec` to `7752afb` by @dependabot in model-checking#3601 * Automatic toolchain upgrade to nightly-2024-10-09 by @github-actions in model-checking#3600 * Automatic toolchain upgrade to nightly-2024-10-10 by @github-actions in model-checking#3602 * Automatic toolchain upgrade to nightly-2024-10-11 by @github-actions in model-checking#3603 * Loop Contracts Annotation for While-Loop by @qinheping in model-checking#3151 * Automatic toolchain upgrade to nightly-2024-10-12 by @github-actions in model-checking#3604 * Update toolchain to 2024-10-15 by @zhassan-aws in model-checking#3605 * Automatic toolchain upgrade to nightly-2024-10-16 by @github-actions in model-checking#3607 * Implement proper function pointer handling for validity checks by @celinval in model-checking#3606 * Update toolchain to 2024-10-17 by @zhassan-aws in model-checking#3610 * Add fn that checks pointers point to same allocation by @celinval in model-checking#3583 * Automatic toolchain upgrade to nightly-2024-10-18 by @github-actions in model-checking#3613 * [aeneas] Preserve variable names by @zhassan-aws in model-checking#3560 * [Breaking change] Make `kani::check` private by @celinval in model-checking#3614 * Emit an error when proof_for_contract function is not found by @zhassan-aws in model-checking#3609 * Automatic toolchain upgrade to nightly-2024-10-19 by @github-actions in model-checking#3617 * Automatic toolchain upgrade to nightly-2024-10-20 by @github-actions in model-checking#3619 * Update test small_slice_eq by @qinheping in model-checking#3618 * Automatic toolchain upgrade to nightly-2024-10-21 by @github-actions in model-checking#3621 * Automatic cargo update to 2024-10-21 by @github-actions in model-checking#3622 * Bump tests/perf/s2n-quic from `7752afb` to `cd0314b` by @dependabot in model-checking#3625 * Update coverage flag in docs by @zhassan-aws in model-checking#3626 * Automatic toolchain upgrade to nightly-2024-10-22 by @github-actions in model-checking#3628 * Automatic toolchain upgrade to nightly-2024-10-23 by @github-actions in model-checking#3635 * Remove dead Option layer from run_piped by @zhassan-aws in model-checking#3634 * Add `free(0)` to codegen of loop contracts by @qinheping in model-checking#3637 * [Lean] Rename user-facing options from Aeneas to Lean by @zhassan-aws in model-checking#3630 * Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in model-checking#3636 * Automatic toolchain upgrade to nightly-2024-10-24 by @github-actions in model-checking#3639 * Add regular & fixme tests for function contracts by @celinval in model-checking#3371 * Call `goto-instrument` with `DFCC` only once by @qinheping in model-checking#3642 * Build and include `kani-cov` in the bundle by @adpaco-aws in model-checking#3641 * Fix loop contracts transformation when loops in branching by @qinheping in model-checking#3640 * Update toolchain to 10/25 by @carolynzech in model-checking#3648 * Automatic toolchain upgrade to nightly-2024-10-26 by @github-actions in model-checking#3651 * Automatic toolchain upgrade to nightly-2024-10-27 by @github-actions in model-checking#3652 * Bump tests/perf/s2n-quic from `cd0314b` to `ed9db08` by @dependabot in model-checking#3655 * Automatic cargo update to 2024-10-28 by @github-actions in model-checking#3654 * Automatic toolchain upgrade to nightly-2024-10-28 by @github-actions in model-checking#3653 * Reduce the number of object bits for refcell test by @zhassan-aws in model-checking#3656 * Move any_slice_from_array to kani_core by @qinheping in model-checking#3646 * Upgrade toolchain to 2024-10-29 by @zhassan-aws in model-checking#3658 * Add a timeout option by @zhassan-aws in model-checking#3649 * Upgrade toolchain to 2024-10-30 by @tautschnig in model-checking#3661 * Upgrade Rust toolchain to 2024-10-31 by @zhassan-aws in model-checking#3668 * Upgrade toolchain to 2024-11-01 by @tautschnig in model-checking#3671 * Automatic toolchain upgrade to nightly-2024-11-02 by @github-actions in model-checking#3673 * Implement `Arbitrary` for `Range*` by @c410-f3r in model-checking#3666 * Automatic toolchain upgrade to nightly-2024-11-03 by @github-actions in model-checking#3674 * codegen: Ask the layout if it is uninhabited, not its impl detail by @workingjubilee in model-checking#3675 * Automatic cargo update to 2024-11-04 by @github-actions in model-checking#3677 * Bump tests/perf/s2n-quic from `192de7d` to `65d55a4` by @dependabot in model-checking#3678 * Update dependencies following Audit workflow failure. by @remi-delmas-3000 in model-checking#3680 * Harness output individual files by @Alexander-Aghili in model-checking#3360 * Update Charon submodule to 2024-11-04 by @zhassan-aws in model-checking#3686 * Add support for float_to_int_unchecked by @zhassan-aws in model-checking#3660 * Change `same_allocation` to accept wide pointers by @celinval in model-checking#3684 * Automatic upgrade of CBMC from 6.3.1 to 6.4.0 by @github-actions in model-checking#3689 * Derive `Arbitrary` for enums with a single variant by @AlgebraicWolf in model-checking#3692 * Update cbmc-viewer to 3.10 by @remi-delmas-3000 in model-checking#3683 * Apply loop contracts only if there exists some usage by @qinheping in model-checking#3694 * Remove symtab json support by @celinval in model-checking#3695 * Remove CBMC viewer and visualize option by @zhassan-aws in model-checking#3699 * Ignore derivative in Cargo deny by @qinheping in model-checking#3708 * Upgrade Rust toolchain to 2024-11-08 by @zhassan-aws in model-checking#3703 * Automatic cargo update to 2024-11-11 by @github-actions in model-checking#3704 * Update verify-std-check workflow to enable loop contracts by @qinheping in model-checking#3705 * Automatic toolchain upgrade to nightly-2024-11-09 by @github-actions in model-checking#3709 * Bump tests/perf/s2n-quic from `65d55a4` to `cb41b35` by @dependabot in model-checking#3706 * Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in model-checking#3701 * Upgrade toolchain to nightly-2024-11-11 by @qinheping in model-checking#3710 * Automatic toolchain upgrade to nightly-2024-11-12 by @github-actions in model-checking#3713 * Update charon submodule by @zhassan-aws in model-checking#3716 * Revert "Ignore derivative in Cargo deny" by @qinheping in model-checking#3712 * Upgrade toolchain to nightly-2024-11-13 by @qinheping in model-checking#3715 * Automatic toolchain upgrade to nightly-2024-11-14 by @github-actions in model-checking#3719 * Automatic toolchain upgrade to nightly-2024-11-15 by @github-actions in model-checking#3720 * Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in model-checking#3644 * Improve Kani handling of function markers by @celinval in model-checking#3718 * Automatic toolchain upgrade to nightly-2024-11-16 by @github-actions in model-checking#3722 * Automatic toolchain upgrade to nightly-2024-11-17 by @github-actions in model-checking#3724 * Automatic cargo update to 2024-11-18 by @github-actions in model-checking#3723 * Bump tests/perf/s2n-quic from `cb41b35` to `4c3ba69` by @dependabot in model-checking#3725 * Automatic toolchain upgrade to nightly-2024-11-18 by @github-actions in model-checking#3727 * Enable contracts for const generic functions by @qinheping in model-checking#3726 * List Subcommand Improvements by @carolynzech in model-checking#3729 * Automatic toolchain upgrade to nightly-2024-11-19 by @github-actions in model-checking#3730 * add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in model-checking#3721 * Fix issues with how we compute DST size by @celinval in model-checking#3687 * Bump tests/perf/s2n-quic from `4c3ba69` to `c84ba19` by @dependabot in model-checking#3736 * Fix size and alignment computation for intrinsics by @celinval in model-checking#3734 * Automatic cargo update to 2024-11-25 by @github-actions in model-checking#3735 * Cleanup a few internal compiler deps by @celinval in model-checking#3739 * Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in model-checking#3742 * Dropping support for Ubuntu 18.04 / AL2. by @thanhnguyen-aws in model-checking#3744 * Update toolchain to nightly-2024-11-26 by @celinval in model-checking#3740 * Automatic upgrade of CBMC from 6.4.0 to 6.4.1 by @github-actions in model-checking#3748 * Automatic cargo update to 2024-12-02 by @github-actions in model-checking#3749 * Update download-artifact, upload-artifact and checkout to v4 by @thanhnguyen-aws in model-checking#3745 * Bump tests/perf/s2n-quic from `c84ba19` to `96d2e22` by @dependabot in model-checking#3750 * Upgrade toolchain to 2024-11-27 by @tautschnig in model-checking#3751 * Upgrade toolchain to 2024-11-28 by @tautschnig in model-checking#3753 * Setup/CI: cleanup Ubuntu 18.04 and cbmc-viewer left-overs and enable 24.04 by @tautschnig in model-checking#3758 * Automatic cargo update to 2024-12-09 by @github-actions in model-checking#3766 * Bump tests/perf/s2n-quic from `96d2e22` to `e4a2365` by @dependabot in model-checking#3767 * Upgrade toolchain to 2024-12-09 by @carolynzech in model-checking#3768 * Add out of bounds check for `offset` intrinsics by @celinval in model-checking#3755 * Upgrade toolchain to 2024-12-12 by @carolynzech in model-checking#3774 * Automatic toolchain upgrade to nightly-2024-12-13 by @github-actions in model-checking#3775 ## New Contributors * @c410-f3r made their first contribution in model-checking#3666 * @workingjubilee made their first contribution in model-checking#3675 * @Alexander-Aghili made their first contribution in model-checking#3360 * @AlgebraicWolf made their first contribution in model-checking#3692 * @thanhnguyen-aws made their first contribution in model-checking#3721 **Full Changelog**: model-checking/kani@kani-0.56.0...kani-0.57.0

@zhassan-aws

Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.56.0"/version = "0.57.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Remove the overflow checks for wrapping_offset by @zhassan-aws in #3589 * `kani-cov`: A coverage tool for Kani by @adpaco-aws in #3121 * Automatic toolchain upgrade to nightly-2024-10-04 by @github-actions in #3570 * Automatic toolchain upgrade to nightly-2024-10-05 by @github-actions in #3591 * Automatic toolchain upgrade to nightly-2024-10-06 by @github-actions in #3592 * Exclude Charon from workspace by @zhassan-aws in #3580 * Support fully-qualified --package arguments by @celinval in #3593 * Automatic toolchain upgrade to nightly-2024-10-07 by @github-actions in #3595 * Automatic toolchain upgrade to nightly-2024-10-08 by @github-actions in #3597 * Automatic cargo update to 2024-10-14 by @github-actions in #3598 * Bump tests/perf/s2n-quic from `17171ec` to `7752afb` by @dependabot in #3601 * Automatic toolchain upgrade to nightly-2024-10-09 by @github-actions in #3600 * Automatic toolchain upgrade to nightly-2024-10-10 by @github-actions in #3602 * Automatic toolchain upgrade to nightly-2024-10-11 by @github-actions in #3603 * Loop Contracts Annotation for While-Loop by @qinheping in #3151 * Automatic toolchain upgrade to nightly-2024-10-12 by @github-actions in #3604 * Update toolchain to 2024-10-15 by @zhassan-aws in #3605 * Automatic toolchain upgrade to nightly-2024-10-16 by @github-actions in #3607 * Implement proper function pointer handling for validity checks by @celinval in #3606 * Update toolchain to 2024-10-17 by @zhassan-aws in #3610 * Add fn that checks pointers point to same allocation by @celinval in #3583 * Automatic toolchain upgrade to nightly-2024-10-18 by @github-actions in #3613 * [aeneas] Preserve variable names by @zhassan-aws in #3560 * [Breaking change] Make `kani::check` private by @celinval in #3614 * Emit an error when proof_for_contract function is not found by @zhassan-aws in #3609 * Automatic toolchain upgrade to nightly-2024-10-19 by @github-actions in #3617 * Automatic toolchain upgrade to nightly-2024-10-20 by @github-actions in #3619 * Update test small_slice_eq by @qinheping in #3618 * Automatic toolchain upgrade to nightly-2024-10-21 by @github-actions in #3621 * Automatic cargo update to 2024-10-21 by @github-actions in #3622 * Bump tests/perf/s2n-quic from `7752afb` to `cd0314b` by @dependabot in #3625 * Update coverage flag in docs by @zhassan-aws in #3626 * Automatic toolchain upgrade to nightly-2024-10-22 by @github-actions in #3628 * Automatic toolchain upgrade to nightly-2024-10-23 by @github-actions in #3635 * Remove dead Option layer from run_piped by @zhassan-aws in #3634 * Add `free(0)` to codegen of loop contracts by @qinheping in #3637 * [Lean] Rename user-facing options from Aeneas to Lean by @zhassan-aws in #3630 * Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in #3636 * Automatic toolchain upgrade to nightly-2024-10-24 by @github-actions in #3639 * Add regular & fixme tests for function contracts by @celinval in #3371 * Call `goto-instrument` with `DFCC` only once by @qinheping in #3642 * Build and include `kani-cov` in the bundle by @adpaco-aws in #3641 * Fix loop contracts transformation when loops in branching by @qinheping in #3640 * Update toolchain to 10/25 by @carolynzech in #3648 * Automatic toolchain upgrade to nightly-2024-10-26 by @github-actions in #3651 * Automatic toolchain upgrade to nightly-2024-10-27 by @github-actions in #3652 * Bump tests/perf/s2n-quic from `cd0314b` to `ed9db08` by @dependabot in #3655 * Automatic cargo update to 2024-10-28 by @github-actions in #3654 * Automatic toolchain upgrade to nightly-2024-10-28 by @github-actions in #3653 * Reduce the number of object bits for refcell test by @zhassan-aws in #3656 * Move any_slice_from_array to kani_core by @qinheping in #3646 * Upgrade toolchain to 2024-10-29 by @zhassan-aws in #3658 * Add a timeout option by @zhassan-aws in #3649 * Upgrade toolchain to 2024-10-30 by @tautschnig in #3661 * Upgrade Rust toolchain to 2024-10-31 by @zhassan-aws in #3668 * Upgrade toolchain to 2024-11-01 by @tautschnig in #3671 * Automatic toolchain upgrade to nightly-2024-11-02 by @github-actions in #3673 * Implement `Arbitrary` for `Range*` by @c410-f3r in #3666 * Automatic toolchain upgrade to nightly-2024-11-03 by @github-actions in #3674 * codegen: Ask the layout if it is uninhabited, not its impl detail by @workingjubilee in #3675 * Automatic cargo update to 2024-11-04 by @github-actions in #3677 * Bump tests/perf/s2n-quic from `192de7d` to `65d55a4` by @dependabot in #3678 * Update dependencies following Audit workflow failure. by @remi-delmas-3000 in #3680 * Harness output individual files by @Alexander-Aghili in #3360 * Update Charon submodule to 2024-11-04 by @zhassan-aws in #3686 * Add support for float_to_int_unchecked by @zhassan-aws in #3660 * Change `same_allocation` to accept wide pointers by @celinval in #3684 * Automatic upgrade of CBMC from 6.3.1 to 6.4.0 by @github-actions in #3689 * Derive `Arbitrary` for enums with a single variant by @AlgebraicWolf in #3692 * Update cbmc-viewer to 3.10 by @remi-delmas-3000 in #3683 * Apply loop contracts only if there exists some usage by @qinheping in #3694 * Remove symtab json support by @celinval in #3695 * Remove CBMC viewer and visualize option by @zhassan-aws in #3699 * Ignore derivative in Cargo deny by @qinheping in #3708 * Upgrade Rust toolchain to 2024-11-08 by @zhassan-aws in #3703 * Automatic cargo update to 2024-11-11 by @github-actions in #3704 * Update verify-std-check workflow to enable loop contracts by @qinheping in #3705 * Automatic toolchain upgrade to nightly-2024-11-09 by @github-actions in #3709 * Bump tests/perf/s2n-quic from `65d55a4` to `cb41b35` by @dependabot in #3706 * Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in #3701 * Upgrade toolchain to nightly-2024-11-11 by @qinheping in #3710 * Automatic toolchain upgrade to nightly-2024-11-12 by @github-actions in #3713 * Update charon submodule by @zhassan-aws in #3716 * Revert "Ignore derivative in Cargo deny" by @qinheping in #3712 * Upgrade toolchain to nightly-2024-11-13 by @qinheping in #3715 * Automatic toolchain upgrade to nightly-2024-11-14 by @github-actions in #3719 * Automatic toolchain upgrade to nightly-2024-11-15 by @github-actions in #3720 * Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in #3644 * Improve Kani handling of function markers by @celinval in #3718 * Automatic toolchain upgrade to nightly-2024-11-16 by @github-actions in #3722 * Automatic toolchain upgrade to nightly-2024-11-17 by @github-actions in #3724 * Automatic cargo update to 2024-11-18 by @github-actions in #3723 * Bump tests/perf/s2n-quic from `cb41b35` to `4c3ba69` by @dependabot in #3725 * Automatic toolchain upgrade to nightly-2024-11-18 by @github-actions in #3727 * Enable contracts for const generic functions by @qinheping in #3726 * List Subcommand Improvements by @carolynzech in #3729 * Automatic toolchain upgrade to nightly-2024-11-19 by @github-actions in #3730 * add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in #3721 * Fix issues with how we compute DST size by @celinval in #3687 * Bump tests/perf/s2n-quic from `4c3ba69` to `c84ba19` by @dependabot in #3736 * Fix size and alignment computation for intrinsics by @celinval in #3734 * Automatic cargo update to 2024-11-25 by @github-actions in #3735 * Cleanup a few internal compiler deps by @celinval in #3739 * Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in #3742 * Dropping support for Ubuntu 18.04 / AL2. by @thanhnguyen-aws in #3744 * Update toolchain to nightly-2024-11-26 by @celinval in #3740 * Automatic upgrade of CBMC from 6.4.0 to 6.4.1 by @github-actions in #3748 * Automatic cargo update to 2024-12-02 by @github-actions in #3749 * Update download-artifact, upload-artifact and checkout to v4 by @thanhnguyen-aws in #3745 * Bump tests/perf/s2n-quic from `c84ba19` to `96d2e22` by @dependabot in #3750 * Upgrade toolchain to 2024-11-27 by @tautschnig in #3751 * Upgrade toolchain to 2024-11-28 by @tautschnig in #3753 * Setup/CI: cleanup Ubuntu 18.04 and cbmc-viewer left-overs and enable 24.04 by @tautschnig in #3758 * Automatic cargo update to 2024-12-09 by @github-actions in #3766 * Bump tests/perf/s2n-quic from `96d2e22` to `e4a2365` by @dependabot in #3767 * Upgrade toolchain to 2024-12-09 by @carolynzech in #3768 * Add out of bounds check for `offset` intrinsics by @celinval in #3755 * Upgrade toolchain to 2024-12-12 by @carolynzech in #3774 * Automatic toolchain upgrade to nightly-2024-12-13 by @github-actions in #3775 ## New Contributors * @c410-f3r made their first contribution in #3666 * @workingjubilee made their first contribution in #3675 * @Alexander-Aghili made their first contribution in #3360 * @AlgebraicWolf made their first contribution in #3692 * @thanhnguyen-aws made their first contribution in #3721 **Full Changelog**: kani-0.56.0...kani-0.57.0 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: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Carolyn Zech <cmzech@amazon.com>

zhassan-aws added 2 commits October 29, 2024 23:20

Add support for float_to_int_unchecked

88a0af4

Add one more test

293b748

github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Oct 30, 2024

tautschnig approved these changes Oct 30, 2024

View reviewed changes

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs Outdated Show resolved Hide resolved

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs Outdated Show resolved Hide resolved

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs Outdated Show resolved Hide resolved

Add more tests

56ea3f3

zhassan-aws marked this pull request as ready for review October 31, 2024 00:39

zhassan-aws requested a review from a team as a code owner October 31, 2024 00:39

zhassan-aws mentioned this pull request Oct 31, 2024

Add support for float_to_int_unchecked #3629

Closed

zhassan-aws added 2 commits October 30, 2024 17:45

Update documentation

d49291c

Merge branch 'main' into float-to-int-intrinsic

3aa243e

celinval reviewed Oct 31, 2024

View reviewed changes

Clean-up

08531f6

zhassan-aws added 2 commits October 30, 2024 23:57

Clarify comment

f6a4d28

Include a check that u128::MAX does not need a bound

5dbd3bc

Yenyun035 mentioned this pull request Nov 1, 2024

Contracts & Harnesses for f{32,64}::to_int_unchecked model-checking/verify-rust-std#134

Merged

celinval reviewed Nov 1, 2024

View reviewed changes

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs Outdated Show resolved Hide resolved

zhassan-aws added 3 commits November 5, 2024 14:20

Merge branch 'main' into float-to-int-intrinsic

df44869

Move code that computes in-range expression to a new module

9a32883

Merge branch 'main' into float-to-int-intrinsic

9dbeb98

celinval approved these changes Nov 6, 2024

View reviewed changes

Clippy fix

7cce2a3

zhassan-aws enabled auto-merge November 6, 2024 05:49

zhassan-aws added this pull request to the merge queue Nov 6, 2024

Merged via the queue into model-checking:main with commit 0dc09a7 Nov 6, 2024
27 checks passed

zhassan-aws deleted the float-to-int-intrinsic branch November 6, 2024 06:44

tautschnig mentioned this pull request Dec 13, 2024

Bump Kani version to 0.57.0 #3777

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add support for float_to_int_unchecked #3660

Add support for float_to_int_unchecked #3660

Uh oh!

zhassan-aws commented Oct 30, 2024 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig commented Oct 30, 2024

Uh oh!

zhassan-aws commented Oct 31, 2024

Uh oh!

zhassan-aws commented Oct 31, 2024

Uh oh!

celinval left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zhassan-aws commented Oct 31, 2024 •

edited

Loading

Uh oh!

celinval commented Nov 1, 2024

Uh oh!

Uh oh!

zhassan-aws commented Nov 1, 2024 •

edited

Loading

Uh oh!

zhassan-aws commented Nov 6, 2024

Uh oh!

celinval left a comment

Uh oh!

Uh oh!

Uh oh!

Add support for float_to_int_unchecked #3660

Add support for float_to_int_unchecked #3660

Uh oh!

Conversation

zhassan-aws commented Oct 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig commented Oct 30, 2024

Uh oh!

zhassan-aws commented Oct 31, 2024

Uh oh!

zhassan-aws commented Oct 31, 2024

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zhassan-aws commented Oct 31, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

celinval commented Nov 1, 2024

Uh oh!

Uh oh!

zhassan-aws commented Nov 1, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

zhassan-aws commented Nov 6, 2024

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

zhassan-aws commented Oct 30, 2024 •

edited

Loading

zhassan-aws commented Oct 31, 2024 •

edited

Loading

zhassan-aws commented Nov 1, 2024 •

edited

Loading