Implement memory initialization state copy functionality #3350
Conversation
There was a problem hiding this comment.
As discussed offline, copying can trigger a delayed UB in the presence of pointer casting from types with different padding bytes location. Can you please mitigate this case here though? We could encode copy operations as unsupported. Or we could also keep a global variable that we set whenever an incompatible cast is performed. Whenever we run copy or copy_nonoverlapping, we can assert that global variable hasn't been set.
|
I am considering waiting until we make some progress with supporting delayed UB triggered by pointer casting with different padding and revisiting this PR then |
This is now properly supported since #3374 has been merged |
kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs
Outdated
Show resolved
Hide resolved
artemagvanian
force-pushed
the
reset-mem-init
branch
from
958354b
to
2eca14d
Compare
That's a good idea. I added a test with a more complex call and control flow structure. I also added a couple of tests checking that this interacts well with delayed UB detection. |
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.
This PR adds support of copying memory initialization state without checks in-between. Every time a copy is performed, the tracked byte is non-deterministically switched.
Resolves #3347
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.