You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
[pointer] Improve soundness of invariant modeling (#2397)
This commit makes the following improvements:
- Removes the `Inaccessible` aliasing mode. This mode was not unsound,
but it was unnecessary in practice.
- Replaces `Unknown` with `Unaligned` for alignment.
- Replaces `Unknown` with `Uninit` for validity.
Finally, with the exception of `transparent_wrapper_into_inner`, this
commit ensures that all `Ptr` methods which modify the type or validity
of a `Ptr` are sound.
Previously, we modeled validity as "knowledge" about the `Ptr`'s
referent (see #1866 for a more in-depth explanation). In particular, we
assumed that it was always sound to "forget" information about a `Ptr`'s
referent in the same way in which it is sound to "forget" that a `Ptr`
is validly-aligned, converting a `Ptr<T, (_, Aligned, _)>` to a
`Ptr<T, (_, Unaligned, _)>`.
The problem with this approach is that validity doesn't just specify
what bit patterns can be expected to be read from a `Ptr`'s referent, it
also specifies what bit patterns are permitted to be *written* to the
referent. Thus, "forgetting" about validity and expanding the set of
expected bit patterns also expands the set of bit patterns which can be
written.
Consider, for example, "forgetting" that a `Ptr<bool, (_, _, Valid)>` is
bit-valid, and downgrading it to a `Ptr<bool, (_, _, Initialized)>`. If
the aliasing is `Exclusive`, then the resulting `Ptr` would permit
writing arbitrary `u8`s to the referent, violating the bit validity of
the `bool`.
This commit moves us in the direction of a new model, in which changes
to the referent type or the validity of a `Ptr` must abide by the
following rules:
- If the resulting `Ptr` permits mutation of its referent (either via
interior mutation or `Exclusive` aliasing), then the set of allowed
bit patterns in the referent may not expand
- If the original `Ptr` permits mutation of its referent while the
resulting `Ptr` is also live (i.e., via interior mutation on a
`Shared` `Ptr`), then the set of allowed bit patterns in the referent
may not shrink
This commit does not fix `transparent_wrapper_into_inner`, which will
require an overhaul or replacement of the `TransparentWrapper` trait.
Makes progress on #2226, #1866
gherrit-pr-id: I95d6c5cd23eb5ea6629cd6e4b99696913b1ded93
Co-authored-by: Jack Wrenn <jswrenn@amazon.com>
0 commit comments