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

Basic support for memory initialization checks for unions #3444

Merged
merged 22 commits into from
Aug 27, 2024
Merged

Basic support for memory initialization checks for unions #3444

merged 22 commits into from
Aug 27, 2024

Conversation

artemagvanian
Copy link
Contributor

This PR introduces very basic support for memory initialization checks for unions.

As of now, the following is supported:

  • Unions can be created
  • Union fields can be assigned to
  • Union fields can be read from
  • Unions can be assigned directly to another union

For more information about planned functionality, see #3300

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

@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Aug 16, 2024
celinval
celinval reviewed Aug 19, 2024
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just reviewed the tests and the library changes for now since the rest will likely be simpler after your other PR is merged. Thanks!

tests/expected/uninit/unions.rs Outdated Show resolved Hide resolved
tests/expected/uninit/fixme_unions.rs Outdated Show resolved Hide resolved
@artemagvanian artemagvanian marked this pull request as ready for review August 22, 2024 19:58
@artemagvanian artemagvanian requested a review from a team as a code owner August 22, 2024 19:58
zhassan-aws
zhassan-aws reviewed Aug 23, 2024
View reviewed changes
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice!

library/kani/src/mem_init.rs Outdated Show resolved Hide resolved
library/kani/src/mem_init.rs Outdated Show resolved Hide resolved
library/kani/src/mem_init.rs Show resolved Hide resolved
tests/expected/uninit/fixme_unions.rs Outdated Show resolved Hide resolved
tests/expected/uninit/fixme_unions.rs Outdated Show resolved Hide resolved
tests/expected/uninit/fixme_unions.rs Outdated Show resolved Hide resolved
tests/expected/uninit/unions.rs Show resolved Hide resolved
tests/expected/uninit/unions.rs Outdated Show resolved Hide resolved
tests/expected/uninit/unions.rs Show resolved Hide resolved
tests/expected/uninit/fixme_unions.rs Show resolved Hide resolved
zhassan-aws
zhassan-aws approved these changes Aug 26, 2024
View reviewed changes
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Only a few nits.

kani-compiler/src/kani_middle/transform/check_uninit/mod.rs Outdated Show resolved Hide resolved
tests/expected/uninit/fixme_unions.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/transform/check_uninit/mod.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/transform/check_uninit/mod.rs Outdated Show resolved Hide resolved
@artemagvanian artemagvanian added this pull request to the merge queue Aug 27, 2024
Merged via the queue into model-checking:main with commit db9c45c Aug 27, 2024
27 checks passed
@artemagvanian artemagvanian deleted the uninit-unions branch August 27, 2024 02:41
@artemagvanian artemagvanian mentioned this pull request Aug 27, 2024
Open
14 tasks
@zhassan-aws zhassan-aws mentioned this pull request Sep 3, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request Sep 4, 2024
@zhassan-aws
Bump Kani version to 0.55.0 (#3486)
603f9bf 
These are the auto-generated release notes:

## What's Changed
* Update CBMC build instructions for Amazon Linux 2 by @tautschnig in
#3431
* Handle intrinsics systematically by @artemagvanian in
#3422
* Bump tests/perf/s2n-quic from `445f73b` to `ab9723a` by @dependabot in
#3434
* Automatic cargo update to 2024-08-12 by @github-actions in
#3433
* Actually apply CBMC patch by @tautschnig in
#3436
* Update features/verify-rust-std branch by @feliperodri in
#3435
* Add test related to issue 3432 by @celinval in
#3439
* Implement memory initialization state copy functionality by
@artemagvanian in #3350
* Bump tests/perf/s2n-quic from `ab9723a` to `80b93a7` by @dependabot in
#3453
* Make points-to analysis handle all intrinsics explicitly by
@artemagvanian in #3452
* Automatic cargo update to 2024-08-19 by @github-actions in
#3450
* Add loop scanner to tool-scanner by @qinheping in
#3443
* Avoid corner-cases by grouping instrumentation into basic blocks and
using backward iteration by @artemagvanian in
#3438
* Re-enabled hierarchical logs in the compiler by @celinval in
#3449
* Fix ICE due to mishandling of Aggregate rvalue for raw pointers to
`str` by @celinval in #3448
* Automatic cargo update to 2024-08-26 by @github-actions in
#3459
* Bump tests/perf/s2n-quic from `80b93a7` to `8f7c04b` by @dependabot in
#3460
* Update deny action by @zhassan-aws in
#3461
* Basic support for memory initialization checks for unions by
@artemagvanian in #3444
* Adjust test patterns so as not to check for trivial properties by
@tautschnig in #3464
* Clarify comment in RFC Template by @carolynzech in
#3462
* RFC: Source-based code coverage by @adpaco-aws in
#3143
* Adopt Rust's source-based code coverage instrumentation by @adpaco-aws
in #3119
* Upgrade toolchain to 08/28 by @jaisnan in
#3454
* Extra tests and bug fixes to the delayed UB instrumentation by
@artemagvanian in #3419
* Upgrade Toolchain to 8/29 by @carolynzech in
#3468
* Automatic toolchain upgrade to nightly-2024-08-30 by @github-actions
in #3469
* Extend name resolution to support qualified paths (Partial Fix) by
@celinval in #3457
* Partially integrate uninit memory checks into `verify_std` by
@artemagvanian in #3470
* Update Toolchain to 9/1 by @carolynzech in
#3478
* Automatic cargo update to 2024-09-02 by @github-actions in
#3480
* Bump tests/perf/s2n-quic from `8f7c04b` to `1ff3a9c` by @dependabot in
#3481
* Automatic toolchain upgrade to nightly-2024-09-02 by @github-actions
in #3479
* Automatic toolchain upgrade to nightly-2024-09-03 by @github-actions
in #3482
* RFC for List Subcommand by @carolynzech in
#3463
* Add tests for fixed issues. by @carolynzech in
#3484


**Full Changelog**:
kani-0.54.0...kani-0.55.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@celinval celinval celinval left review comments

@zhassan-aws zhassan-aws zhassan-aws approved these changes

Assignees
No one assigned
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@artemagvanian @celinval @zhassan-aws