Instrumentation for delayed UB stemming from uninitialized memory #3374
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
14 tasks
zhassan-aws
reviewed
Jul 27, 2024
kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
Outdated
Show resolved
Hide resolved
zhassan-aws
approved these changes
Jul 29, 2024
Co-authored-by: Celina G. Val <celinval@amazon.com>
Merged
via the queue into
model-checking:main
with commit Aug 5, 2024
f2831f4
26 of 27 checks passed
This was referenced Aug 5, 2024
github-merge-queue bot
pushed a commit
that referenced
this pull request
Aug 9, 2024
## 0.54.0 ### Major Changes * We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts. * We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros. * We enabled support for concrete playback for harness that contains stubs or function contracts. * We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs. ### Breaking Changes * The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default. ## What's Changed * Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in #3332 * Fix visibility of some Kani intrinsics by @artemagvanian in #3323 * Function Contracts: Modify Slices by @pi314mm in #3295 * Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in #3344 * Add support for global transformations by @artemagvanian in #3348 * Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in #3283 * Fix contract handling of promoted constants and constant static by @celinval in #3305 * Bump CBMC Viewer to 3.9 by @tautschnig in #3373 * Update to CBMC version 6.1.1 by @tautschnig in #2995 * Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in #3270 * Enable concrete playback for contract and stubs by @celinval in #3389 * Add code scanner tool by @celinval in #3120 * Enable contracts in associated functions by @celinval in #3363 * Enable log2*, log10* intrinsics by @tautschnig in #3001 * Enable powif* intrinsics by @tautschnig in #2999 * Enable fma* intrinsics by @tautschnig in #3002 * Enable sqrt* intrinsics by @tautschnig in #3000 * Remove assigns clause for ZST pointers by @carolynzech in #3417 * Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in #3374 * Unify kani library and kani core logic by @jaisnan in #3333 * Stabilize pointer-to-reference cast validity checks by @artemagvanian in #3426 * Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri ## New Contributors * @carolynzech made their first contribution in #3387 **Full Changelog**: kani-0.53.0...kani-0.54.0 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
github-merge-queue bot
pushed a commit
that referenced
this pull request
Aug 22, 2024
…using backward iteration (#3438) 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: - Group instrumentation into separate basic blocks instead of adding instructions one-by-one. - Use backward iteration to avoid having to reason about which instructions need to be skipped. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
github-merge-queue bot
pushed a commit
that referenced
this pull request
Aug 28, 2024
This PR is a follow-up to #3374. It introduces the following changes: - Instrument more writes to avoid the case when points-to analysis overapproximates too much. - Add extra tests featuring safe abstractions from standard library. 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
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
As #3324 mentioned, delayed UB triggered by accessing uninitialized memory was previously mitigated by injecting
assert!(false)for every possible source of it; this PR adds all the necessary infrastructure and minimal support for detecting it properly.The process of detecting and instrumenting places is as follows:
Not all language constructs are currently supported -- see the tracking issue (#3300) for the full list of limitations.
Resolves #3324
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.