-
Notifications
You must be signed in to change notification settings - Fork 42
document preservation of padding in operations on pointers #695
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
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -111,6 +111,12 @@ The :t:`expression` of a :t:`constant initializer` shall be a | |
| The value of a :t:`constant` is determined by evaluating its | ||
| :t:`constant initializer`. | ||
|
|
||
| :dp:`fls_LmPbrh0Cba8g` | ||
| The :t:`type representation` of the :t:`value` of a :t:`constant initializer` or :t:`static initializer` must only contain bytes with :t:`provenance` where all bytes of some original :t:`pointer` are in the correct order. | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This looks to me to be looser than the wording currently proposed in There's potential philosophical difference here we should discuss of:
Now, the above distinction is not perfect, but I think it gestures to the idea and asks the question of: "should we document compiler behavior, for which there is not yet settled Reference documentation?" Feels like to me the answer is yes. I think that since this PR is intended to land before rust-lang/reference#2138, I think we should either align with that draft's current shape or explicitly decide what FLS wording we want to use for the same merged rustc behavior. I think the cleanest FLS shape is to define the narrow terms that this rule needs in shared const/static-initializer material, then state the rule in those terms. For example: :dp:`...`
:dt:`Provenance-carrying byte` is an initialized byte in the representation of
a :t:`value` that contains a :c:`u8` value and provenance associated with a
:t:`pointer`. General pointer provenance is discussed by :std:`core::ptr`.
:dp:`...`
:dt:`Whole-pointer group` is an adjacent sequence of
:t:`[provenance-carrying byte]s` that consists exactly of all bytes of one
original :t:`pointer` value in their original order.
:dp:`...`
The representation of the final :t:`value` produced by evaluating a
:t:`constant initializer` or :t:`static initializer` shall only contain
:t:`[provenance-carrying byte]s` that are part of a :t:`whole-pointer group`.This helps enable four things:
I'd also suggest we move this out of the
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
You cannot point the reader/programmer/auditor to an unstable external document. After all, it is the job of the FLS to define the stable semantics of provenance. Let's step back a bit. We need to define what "provenance" is. The suggestion below is based on core::ptr provenance. 7.5. Provenance
Legality rules
A :t:`pointer` is a :t:`value` of a :t:`raw pointer type`.
An :t:`indirection value` is either a :t:`pointer` or a :t:`reference`.
An :t:`original indirection value` is an :t:`indirection value` created via allocation.
A :t:`derived indirection value` is an :t:`indirection value` obtained by performing address
or pointer arithmetic on another :t:`indirection value`.
:t:`Provenance` is an optional property of :t:`[indirection value]s which grants the following
permissions:
- :t:`Provenance` restricts the addresses an :t:`indirection value` may point to within a
block of memory.
- :t:`Provenance` restricts the timespan during which an :t:`indirection value` may point to
a block of memory.
- :t:`Provenance` restricts the read/write access an :t:`indirection value` has from/to a
block of memory.
An :t:`original indirection value` always carries :t:`provenance`.
A :t:`derived indirection value` inherits the :t:`provenance` of the :t:`indirection value` it
was created from, if any.
A :t:`well-formed indirection value` is an :t:`indirection value` with :t:`provenance`, where
all bytes that comprise the indirection value are part of the same group.
Undefined Behavior
It is undefined behavior to access memory through an :t:`indirection value` which
does not have :t:`provenance` over that memory.
It is undefined behavior to offset an :t:`indirection value` across the bounds of the
memory block it has :t:`provenance` over.With this in place, we can now tackle the proposed rules: :dp:`...`
If the final :t:`value` produced by evaluating a :t:`constant initializer` or :t:`static
initializer` denotes an :t:`indirection value`, then the final :t:`value` shall be a
:t:`well-formed indirection value`.
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. My suggestions are now available in #707, as requested by Tshepang. |
||
|
|
||
| :dp:`fls_nwgIMLkvD2Ol` | ||
| :dt:`Provenance` is the memory that a :t:`pointer` has permission to access, the timespan during which it can acesss that memory, and if it can access the memory for writes. | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Where did you get this definition from? To me, "provenance" is a property (of something, TBD). According to Merriam-Webster, "provenance" is the origin or source, or the history of ownership.
Member
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. https://doc.rust-lang.org/stable/core/ptr/index.html#provenance maybe I should just call it pointer provenance
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think the bigger risk here is not just where this definition came from, but that it commits FLS to a general provenance model that the upstream Reference text did not define in these PRs. The local wording reads more like a paraphrase of pointer access permissions, while the neighboring rules are about bytes carrying provenance and fragments of an original pointer value. Would it be safer to avoid defining
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I did a quick search across the nightly Reference, and I am not seeing a concrete definition of Orthogonal to this, this rule should have gone into 4.7. Indirection Types 😁 . This comment is still relevant.
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think the concrete fix here is to delete this broad local definition rather than rename it to I see the The Reference handles this by noting the memory model recognizes initialized bytes as carrying optional provenance, and other Reference text points readers to Given that, I still think defining Again, the Reference also says the Rust memory model is incomplete and not fully decided, so I think the FLS should avoid introducing a general provenance definition here. Feels premature. Suggested source-level outcome: If FLS needs terms to make the new rules readable, I would replace uses that depend on this local If definitions are introduced, I agree with @kirtchev-adacore that they should not live under |
||
|
|
||
| .. rubric:: Dynamic Semantics | ||
|
|
||
| :dp:`fls_xezt9hl069h4` | ||
|
|
||
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this sentence captures only one consequence of the upstream rule. In rust-lang/reference#2091, the normative const-eval restriction is broader: integer-like values must not carry provenance, and pointer-like values must either carry no provenance or consist of fragments of the same original pointer value in the correct order. Would it make sense to spec that broader rule, and then treat the ptr-to-non-pointer case here as an implication or example? If the main rule ends up living with shared const/static-initializer material, this sentence could then point back to that broader restriction.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To make this more concrete, I think we should explore porting the broader const-context validity rule from
reference#2091, rather than only the more narrow ptr-to-non-pointer implication currently stated here.One potential shape would be to replace this paragraph with a rule along these lines, preferably in the
Constant Expressionsundefined-behavior material or a shared const-eval subsection rather than as a standalone special case here:This would pair pretty naturally with narrow definitions for
provenance-carrying byteandwhole-pointer groupnear the initializer/provenance rules, rather than a broad definition ofprovenanceitself. Those terms mirror the Reference's byte-level wording without committing FLS to a general provenance model.The important cases from the Reference that need to be represented are:
dyn Traitmetadata is grouped with the pointer-data restriction.Without the broader validity-invariant rule, the PR seems to miss the wrong-order pointer-byte case and recursive/nested validity cases that
reference#2091was specifically written to cover, such as provenance-carrying integer data nested inside a field.