-
Notifications
You must be signed in to change notification settings - Fork 13
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.
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
Revise Safety Analysis #15
Comments
jswrenn
added a commit
to jswrenn/rust
that referenced
this issue
Feb 27, 2024
Migrate to a simplified safety analysis that does not use visibility. Closes rust-lang/project-safe-transmute#15
matthiaskrgr
added a commit
to matthiaskrgr/rust
that referenced
this issue
Feb 29, 2024
…=compiler-errors Safe Transmute: Revise safety analysis This PR migrates `BikeshedIntrinsicFrom` to a simplified safety analysis (described [here](rust-lang/project-safe-transmute#15)) that does not rely on analyzing the visibility of types and fields. The revised analysis treats primitive types as safe, and user-defined types as potentially carrying safety invariants. If Rust gains explicit (un)safe fields, this PR is structured so that it will be fairly easy to thread support for those annotations into the analysis. Notably, this PR removes the `Context` type parameter from `BikeshedIntrinsicFrom`. Most of the files changed by this PR are just UI tests tweaked to accommodate the removed parameter. r? `@compiler-errors`
rust-timer
added a commit
to rust-lang-ci/rust
that referenced
this issue
Mar 1, 2024
Rollup merge of rust-lang#121681 - jswrenn:nix-visibility-analysis, r=compiler-errors Safe Transmute: Revise safety analysis This PR migrates `BikeshedIntrinsicFrom` to a simplified safety analysis (described [here](rust-lang/project-safe-transmute#15)) that does not rely on analyzing the visibility of types and fields. The revised analysis treats primitive types as safe, and user-defined types as potentially carrying safety invariants. If Rust gains explicit (un)safe fields, this PR is structured so that it will be fairly easy to thread support for those annotations into the analysis. Notably, this PR removes the `Context` type parameter from `BikeshedIntrinsicFrom`. Most of the files changed by this PR are just UI tests tweaked to accommodate the removed parameter. r? `@compiler-errors`
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This issue tracks the design work to revise and simplify
BikeshedIntrinsicFrom
's safety analysis.Background
Safe transmutation requires reasoning about whether transmuted fields carry safety invariants. A safe transmutation between two value types is only safe if the destination type does not maintain safety invariants on its fields. A safe transmutation between two mutable reference types requires that both that the source and destination are free of invariants.
Status Quo
At present,
BikeshedIntrinsicFrom
uses a visibility-based analysis to determine safety: the trait takes aContext
type parameter which represents the location at which the transmutation is occurring. This design is described in-depth by MCP411 and summarized below.When analyzing the safety of a transmutation, the compiler pretends it is sitting at the definition location of the type provided for
Context
, and checks that theDst
(and, if necessary,Src
) type is fully implicitly constructible (i.e., you can recursively call the implicit constructors of its fields and those field's fields, and so on, to construct theDst
). If this check passes, then the transmute isn't constructingDst
in a way that couldn't be achieved without safe code.Motivation
The visibility-based analyses has several drawbacks.
Drawback 1: Limited Utility
In general, it is not true that the ability to safely modify or construct a field means that it is free of safety invariants. Since Rust does not presently have a notion of
unsafe
fields, all fields are safely constructible and mutable in their defining context. See The Scope of Unsafe for additional information about this problem.Drawback 2: Difficulty of Sound Implementation
A visibility-based analysis is difficult to implement completely. The implicit constructibility of a field does not depend only on its type's visibility and implicit constructibility of its fields, but also the visibility of the modules that the type is defined in. The "pub-in-priv trick" complicates this analysis from "inspecting type definitions" to "thoroughly exploring the reachability of fields in the module graph".
Proposal
We will remove the visibility based analysis. The
Context
parameter will be removed fromBikeshedIntrinsicFrom
, simplifying its definition to:Implementations of$T$ that are free of safety invariants shall be defined as:
BikeshedIntriniscFrom
without the assumption of safety will only be emitted if fields constructed or rendered mutable by the transmutation are free from safety invariants. The set of such typesPractically speaking, this means that
Src: BikeshedIntriniscFrom<Dst, Assume::NOTHING>
for all primitiveSrc
andDst
(provided that validity requirements are fulfilled); e.g.,u8: BikeshedIntriniscFrom<i8, Assume::NOTHING>
.Since Rust does not currently have any way for users to denote that their fields carry safety invariants,
Assume::SAFETY
will be required for most analyses of user-defined types. If Rust gains (un)safe fields in the future, our safety analysis can be updated to incorporate that information.This design has several advantages:
Implementation
This section is a note to myself. Feel free to stop reading here!
Status Quo
The transmutability analysis represents types, first, as a
Tree
of definition elements:The visibility analysis centers on
Def
nodes, which represent the definitions of types and fields. The accessibility of these definitions from theScope
parameter type can be queried from theQueryContext
:The visibility analysis over these
Tree
s is the first stage of analyzing transmutability:In the above routine, inaccessible branches of the layout tree are pruned from the destination type. If the remaining tree is uninhabited (either because it started as uninhabited or because it has no visible branches), we reject the transmutation.
Revised Implementation
Roughly speaking, the revised implementation is almost entirely the same, but with a few tweaks:
Scope
/Context
parameter is eliminated from the public API and the analysisDef
nodes are only emitted for fieldsDef
is modified to carry ahas_safety_invariants
flagtrue
false
The text was updated successfully, but these errors were encountered: