Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration #3438
Conversation
|
Can you please describe what the corner-cases are? |
I expanded a little bit on that in the PR description. I encountered this corner case when testing enabling instrumentation with standard library. I am not sure of the exact configuration that triggered it, but the general issue was that skipping only the first statement in the new basic block when splitting was not enough and instrumentation was caught in the infinite loop. |
There was a problem hiding this comment.
I think this logic to track which instructions we still need to visit is adding unnecessary complexity to this code. You mentioned that @jsalzbergedu suggested visiting the basic blocks in reverse order. I think that would make this code much cleaner, don't you think?
Also, since this is meant to fix an issue, I expect at least one test that ensures this issue doesn't regress later. Thanks
That's a good idea! I implemented a version of it, and it seemed to make the code significantly cleaner. The only issue, which has nothing to do with the approach itself, is that I can't call |
artemagvanian
changed the title
kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
Outdated
Show resolved
Hide resolved
kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
Outdated
Show resolved
Hide resolved
kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
Outdated
Show resolved
Hide resolved
kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
Outdated
Show resolved
Hide resolved
I'm wondering if you missed this comment. Can you please add a test? |
|
I wonder if there was a bug in the experiment itself, not in the instrumentation. It is a bit unsettling that this potential bug is not clearly understood, but the new approach seems safe. Can you still please ensure we have tests that add multiple instrumentation for a single MIR instruction? Thanks |
I added tests where an instruction gets instrumented more than once. Regarding the experiment, I ran a naive version of delayed UB checks, where instead of filtering places to instrument by aliasing, all of the places get instrumented. I ran it under the assumption that places added by instrumentation will be correctly skipped, which was not the case. |
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 is a follow-up to #3374.
Its main purpose is to properly handle a corner-case when multiple instrumentation instructions are added to the same instruction and not all of them are skipped during subsequent instrumentation.
For example, if instrumentation is added after a terminator, a new basic block will be created, containing the added instrumentation. However, we currently only mark the first statement (or the terminator, if there are none) of the new basic block as skipped for subsequent instrumentation. That means that if instrumentation in this case contains some instrumentation targets itself, it will never terminate.
Coincidentally, this is not currently the case, but could lead to subtle bugs if we decide to change instrumentation. In fact, this bug was only surfaced when I experimented with checking all memory accesses, which introduced significantly more checks. Ultimately, this shows that the current way to avoiding instrumentation is limited and needs to be changed.
The PR introduces the following changes:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.