Fix issues with how we compute DST size #3687

celinval · 2024-11-06T00:29:06Z

This change fixes how we compute size of the object in our mem predicates, and provide user visible methods to try to retrieve the size of the object if known and valid (checked_size_of_raw and checked_align_of_raw.

Fixes #3612
Fixes #3627

Call-outs

To simplify this PR, I moved the following changes to their own PRs:

I also removed the fix for the intrinsics size_of_val and align_of_val from this PR, and I will create a follow up PR once this one is merged.

1. Add proper bounds check for `size_of_val` intrinsics. 2. Refactor how we compute size of the object in our mem predicates. 3. Provide user visible methods to try to retrieve the size of the object if known and valid.

kani-compiler/src/kani_middle/abi.rs

- Assume for now that we cannot compute foreign object size.

kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs

celinval · 2024-11-14T04:27:31Z

FYI, I'm going to create a fix for the std in a separate PR. Also I think I could break down this PR into two if needed.

celinval · 2024-11-14T20:16:00Z

After a second thought, I'm going to try to break this change into the following PRs:

Aggregate fix + Abi module: Fix codegen for rvalue aggregate raw pointer to an adt with slice tail #3644
Refactoring of of kani_functions: Improve Kani handling of function markers #3718
Adding the checked APIs and fix of mem predicates: Fix issues with how we compute DST size #3687 (this PR)
Fix intrinsics implementation

Note that 1 and 2 are fairly independent, but 3 will depend on 1 and 2, while 4 will depend on them all.

Change our library to use `kanitool::fn_marker` instead of rustc's internal `rustc_diagnostic_item` to mark functions in the Kani library that are required for Kani compiler. Also, validate and cache Kani's functions upfront to detect any incoherence between our libraries and our compiler. Note that I am moving the code from #3687 that started this migration to this new PR, and I decided to move almost our entire code base out of the diagnostic item with the exception of our SIMD bitmask model and the shadow memory for uninit checks. Finally, I changed our standard library codegen to be a regular test in our script based suite. I also changed it to inject `kani_core` so we can remove hacks in our goto-c codegen. 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: Carolyn Zech <cmzech@amazon.com>

Conflicts: - kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs - kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs - kani-compiler/src/kani_middle/abi.rs - kani-compiler/src/kani_middle/attributes.rs - kani-compiler/src/kani_middle/kani_functions.rs - kani-compiler/src/kani_middle/transform/check_uninit/mod.rs - kani-compiler/src/kani_middle/transform/kani_intrinsics.rs - kani-compiler/src/kani_middle/transform/mod.rs - kani-compiler/src/kani_queries/mod.rs - library/kani_core/src/mem.rs - library/kani_core/src/mem_init.rs

Revert changes to intrinsics and remove tests for now

carolynzech

I don't understand what the safety check hook is for--as far as I can tell, we never invoke it. How does it fit into the size and alignment fixes you're doing? Did you forget to invoke it somewhere, or am I missing something?
Otherwise, all of these comments are just nits. Beautiful tests!
(Edit: per offline discussion, safety check will be used for Rust intrinsics in a subsequent PR).

library/kani_core/src/models.rs

kani-compiler/src/kani_middle/transform/kani_intrinsics.rs

tests/kani/MemPredicates/foreign_type.rs

Co-authored-by: Carolyn Zech <cmzech@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

Fix issues with how we compute DST size

283a7f1

1. Add proper bounds check for `size_of_val` intrinsics. 2. Refactor how we compute size of the object in our mem predicates. 3. Provide user visible methods to try to retrieve the size of the object if known and valid.

github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Nov 6, 2024

celinval marked this pull request as ready for review November 12, 2024 21:03

celinval requested a review from a team as a code owner November 12, 2024 21:03

Merge branch 'main' into issue-3612-can-deref-2

f805e34

celinval force-pushed the issue-3612-can-deref-2 branch from b47ae6d to f805e34 Compare November 12, 2024 21:13

celinval commented Nov 12, 2024

View reviewed changes

kani-compiler/src/kani_middle/abi.rs Outdated Show resolved Hide resolved

Fix aggregate, place handle and implement safety_check

24992d3

celinval marked this pull request as draft November 13, 2024 01:28

celinval added 2 commits November 13, 2024 12:50

Cleanup code and add more tests

e06eef5

- Assume for now that we cannot compute foreign object size.

Better handling of foreign types

0128e68

celinval commented Nov 13, 2024

View reviewed changes

kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs Outdated Show resolved Hide resolved

celinval marked this pull request as ready for review November 13, 2024 21:48

Fix regression failures

61ea50b

celinval marked this pull request as draft November 14, 2024 20:16

This was referenced Nov 14, 2024

Fix codegen for rvalue aggregate raw pointer to an adt with slice tail #3644

Merged

Improve Kani handling of function markers #3718

Merged

celinval added 2 commits November 18, 2024 13:02

Move fixes to <size|align>_of_val to a new PR

a10a746

Revert changes to intrinsics and remove tests for now

celinval force-pushed the issue-3612-can-deref-2 branch from fe47946 to a10a746 Compare November 18, 2024 21:29

celinval marked this pull request as ready for review November 18, 2024 21:29

carolynzech self-assigned this Nov 19, 2024

carolynzech reviewed Nov 22, 2024

View reviewed changes

carolynzech approved these changes Nov 22, 2024

View reviewed changes

celinval and others added 3 commits November 21, 2024 17:04

Apply suggestions from code review

5c4d5b7

Co-authored-by: Carolyn Zech <cmzech@amazon.com>

Update library/kani_core/src/models.rs

97e9048

Add more comments and split test

f3736cc

celinval enabled auto-merge November 22, 2024 19:42

celinval added this pull request to the merge queue Nov 22, 2024

Merged via the queue into model-checking:main with commit 19adf79 Nov 22, 2024
26 checks passed

tautschnig mentioned this pull request Dec 13, 2024

Bump Kani version to 0.57.0 #3777

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix issues with how we compute DST size #3687

Fix issues with how we compute DST size #3687

celinval commented Nov 6, 2024 •

edited

Loading

celinval commented Nov 14, 2024

celinval commented Nov 14, 2024 •

edited

Loading

carolynzech left a comment •

edited

Loading

Fix issues with how we compute DST size #3687

Fix issues with how we compute DST size #3687

Conversation

celinval commented Nov 6, 2024 • edited Loading

Call-outs

celinval commented Nov 14, 2024

celinval commented Nov 14, 2024 • edited Loading

carolynzech left a comment • edited Loading

Choose a reason for hiding this comment

celinval commented Nov 6, 2024 •

edited

Loading

celinval commented Nov 14, 2024 •

edited

Loading

carolynzech left a comment •

edited

Loading