Pre-RFC: Safety Property System

libs
21

The definition of ValidCStr is mem(p+len, p+len+1) = '\0' according to the primitive-sp of tag-std.

I think a better name for it would just be CStr?

And we could just define a SP to include them all, and name it ValidCStr, since SP are composable and custom. The grain of a SP depends on the crate author.

I think the reason to see five properties like that on an API is what we see from the safety doc comments: CStr in std::ffi - Rust

Yes, we can support that like this:

#[safety::discharges {
  ValidCStr(ptr, _), ValidPtr(ptr, i8, _), NonNull(ptr), ValidNum(compute_nul_pos(ptr), 0..=isize::MAX), Alias(ptr, ret)
}]

as long as macro syntax is supported by the compiler: Rust Playground

And in principle, we can make SP arguments a bit smarter if the tool queries more info from rustc. We can know the type of ptr, and there's single argument, so why not elide it to be:

#[discharges {  ValidCStr, ValidPtr, NonNull, ValidNum, Alias(*name, &STRUCTS) }]

The less we write, the more info from rustc. See Future possibilities Interaction with Rust type system in our proposal.

Also note that we can use safety::discharge; to import the proc-macro for shorter code.

If there's a need to elaborate a SP in discharge macro, here's how to do

#[discharges {
   ValidPtr("Detailed reasons to help readers understand why ptr is valid"),
   ValidCStr, NonNull, ValidNum, Alias(*name, &STRUCTS)
 }]
1 Like
22

On reddit, Matthieum left some great comments, so we can still simplify #[discharges] for a shorter syntax and grouped SPs:

#[safety {
  ValidPtr, Align, Init: "`self.head_tail()` returns two slices to live elements";
  NotOwned: "because we incremented...";
  Alias(elem, head.iter());
}]
unsafe { ptr::read(elem) }

Very close to structured safety comments:

//  SAFETY
//  - ValidPtr, Aligned: by invariant.
//  - Init: `head` is a slice of initialized elements.
//  - NotOwned: because we incremented...
//  - Alias: ...
2 Likes
23

Quote my comments from #all-hands-2025 > Naming safety requirements & invariants @ :speech_balloon::

Goal for Safety Standard: Always use the same wording for the same situation.

In our proposal, each unsafe requirement is represented as a tag to clarify a safety property (SP). The definition of an SP is stored in a project configuration JSON file. The format for an SP spec includes:

  • Tag name: Must be an identifier.
  • Tag arguments: Parameters associated with the tag.
  • Tag type: One of precond, hazard, or option. Precond as default.
  • Tag description: A static string or a dynamic string interpolation related to the arguments.

This ensures that everyone understands the semantics of each SP, eliminating any potential misinterpretation of direct and indirect safety requirements for unsafe functions or calls. Tags are rendered through rustdoc from their descriptions, ensuring that safety documentation is as accurate as the spec.

Before submitting a PR or patch, our tool automatically checks that these tags are correctly defined and discharged. This strongly ensures the rigid consistency of safety properties, requirements, and documentation.

Our tool provides detailed reports on any changes to SP specifications, SP usage, or referenced entities. These reports help reviewers assess the nature of the changes and their potential impacts.

An example of the snippet from Banno's slides

/// # Safety
///
/// The provided pointer must point at a valid struct of type `Self`.
#[inline]
unsafe fn raw_get_work(ptr: *mut Self) -> *mut Work<T, ID> {
    let ptr = ptr as *mut u8;
    // SAFETY: The caller promises that the pointer is valid.
    unsafe { ptr.add(Self::OFFSET).cast() }
}

our syntax of SP usage is:

#[safety { ValidPtr(ptr) }]
unsafe fn raw_get_work(ptr: *mut Self) -> *mut Work<T, ID> {
    let ptr = ptr as *mut u8;

    #[safety { InBound, ValidNum }]
    unsafe { ptr.add(Self::OFFSET).cast() }
}

InBound and ValidNum are SPs from the safety doc of ptr.add(count), so they are just discharged on the unsafe call. These SPs can be found in primitive-sp and json data.

If entity reference is supported and preferred, we can write this:

#[safety { ValidPtr(ptr): ref(HasWorkInvariant) }]
unsafe fn raw_get_work(ptr: *mut Self) -> *mut Work<T, ID> { ... }

#[ref(HasWorkInvariant)]
pub unsafe trait HasWork<T, const ID: u64 = 0> {...}
24

I wonder if, then, for something integrated with the language you'd rather have these be proper items in a crate somewhere. Could then use "real" name resolution to mention them, with core::ptr defining the bunch it has in its docs today, for example.

If that let rustdoc copy the summary line over and cross-link to the full definition of the predicate too, which seems like it'd be really nice when reading the docs for unsafe fn/trait, as well as for avoiding manual copy-pasting of those details all over the place.

(That necessarily avoids any "two people used the same ident" problems too.)

5 Likes
25

From what I can tell, you're suggesting the following practice right?

// in core::ptr module or my local module:

pub mod invariants {
    /// Invariants for a Rust pointer.
    pub struct Invariants {
        /// Here's what <https://doc.rust-lang.org/std/ptr/index.html#safety> shows today.
        pub valid_ptr: (),
        /// Here's what <https://doc.rust-lang.org/std/ptr/index.html#alignment> shows today.
        pub alignment: (),
        /// <https://doc.rust-lang.org/std/ptr/index.html#allocated-object>
        pub allocated: (),
        /// <https://doc.rust-lang.org/std/ptr/index.html#provenance>
        pub provenance: (),
    }
}

#[cfg(doc)]
use invariants::Invariants;

/// Ref full [`Invariants`] for a pointer.
///
/// Ref [valid_ptr](Invariants::valid_ptr)
pub struct MyProperty {}

Then by the power of intra rustdoc linking, it's easy to link a primitive [1] SP or invariant in rendered webpages:

safety-tag-item

We can have reverse links as well:

impl Invariants {
    /// # Reverse Linkage
    ///
    /// - [MyProperty](crate::MyProperty)
    pub fn valid_ptr(self) {}
}

1112×833 72 KB

  1. or any :face_with_monocle: ↩︎

26

I don't know how lang-integrated you're thinking of this being, and TBH didn't have any particularly specific thoughts about how to spell it.

Assuming going whole-hog on integration, you could make a new kind of item, like

/// A pointer is aligned when its address is a multiple of its `align_of_val`.
///
/// Valid raw pointers as defined above are not necessarily properly aligned (where
/// "proper" alignment is defined by the pointee type, i.e., `*const T` must be
/// aligned to `align_of::<T>()`). However, most functions require their
/// arguments to be properly aligned, and will explicitly state
/// this requirement in their documentation by including this . Notable exceptions to this are
/// [`read_unaligned`] and [`write_unaligned`].
///
/// When a function requires proper alignment, it does so even if the access
/// has size 0, i.e., even if memory is not actually touched. Consider using
/// [`NonNull::dangling`] in such cases.
pub k@bikeshed_safety_predicate AlignedFor<T>(ptr: impl PointerLike);

And rustdoc could make it a safety.AlignedFor.html file, and you can use it to bring it in-scope for shorter requires and discharges list.

Like it could be

unsafe(AlignedFor<T>(p)) fn foo<T>(p: *const T) { ... }

and

hold_my_beer(AlignedFor<u32>(q)) {
    foo(q);
}

But if the goal is to keep it as just macros, rather than any special syntax, then obviously something very different from that :stuck_out_tongue:

1 Like
27

Thank you for inspiring lovely interactions with rustdoc.

If SP rustdoc pages are required someday, we could generate each SP through function item: e.g.

871×683 36.8 KB

28

That is not how I would format those docs. Put the human readable description front and center. The formal stuff should be at the bottom for the experts. Maybe even in a "show details" that has to be expanded.

Remember, most users are not experts or even knowledge in formal verification.

1 Like
29

It's just an example to show SPs in separate rustdoc webpages.

Don't worry. Formal stuff are mainly used in analysis, not in normal docs.

It's worth noting that once project JSON config and structured SPs are available, more structured contents are possible.

Say we can generate these phony SP function items: unsafe function docs can link to them, detailed description is in single page instead of a part of long page, and more info such as stats or reverse links to unsafe functions etc.

30

I don't think it should be based on a config, but as @scottmcm suggested, be defined in the source. And it should definitely not use json: toml is the de-facto standard in the rust community for tooling configs.

Toml is much nicer for a human to write than json, and supports comments (which vanilla json does not).

31

It's definitely possible to have SPs in source code.

I haven't started on writing configuration-based code yet. So here's my scheme to support it without config

  1. define an SP item in proper module: maybe a function, struct, enum or const
  2. run build.rs in project crate to extract all SPs into an output file
  3. #[safety] proc-macro reads the file to determine what tokens should be generated
  4. the output file will also be used in linter to analyze property discharging

Does it sound good?

32

Why is this needed, if this has proper compiler integration (which I assume is the end goal)? Build.rs has to run before the rest of the compile process can start, and this slows down the overall build as a result.

I think we should aim to avoid slowing down the build whenever possible.

33

I don't think there will be compiler integration for this RFC, because the linter and proc-macro are enough today to implement this safety property sytem AFAICT.

The goal we hope on Rust project side is to put fundamental safety properties in libcore/libstd/alloc/... crates, which will probably be achieved by verify-rust-std instead of by libs team. I'm not sure yet, as we're only starting experimenting this system on our own.

Our linter is indeed intergrated into the compiler as rustc driver, so we can see HIRs and MIRs for source code.

If we only have tool attribute to work, the output file is needless.

But we want to generate standard safety docs, and possibly external verification attributes, so a #[safety] macro may expand to three kinds of macro:

#[doc = "`src` must be [valid] for reads.\n\n[valid]: https://doc.rust-lang.org/std/ptr/index.html#safety"]
#[safety_tool::...] // our tool attribute
#[kani::requires(kani::mem::can_dereference(src))] // external verification attribute

This modifies AST, so #[safety] must know exact info from given SP idents to generate tokens. While proc-macro can't see through SP items, info must be pre-computed before proc-macro is working.

Edit: the main reason to have a config file is to less depend on source code. Consider versions: different projects may require different versions of rust toolchain. None of libstd versions has SPs. So a shared config file for libcore can be used in Rust for Linux and Asterinas. You may argue that this conflicts with the precision of the system, but in reality we have to take action step by step towards the goal.

34

The problem I see if this is pervasive in the ecosystem, what is the effects on compile times? Proc macros and build scripts both result in increased build times.

If this could be done as a tool attribute instead, would that be better? Custom tool attributes are unstable as far as I know, but maybe that is a way forward. Could we not add support for these tool attributes to rustdoc too?

If a toml config would result in faster build times than having things defined in the code, that is the lesser of two evils in my opinion.

1 Like
35

Maybe slightly longer, but tolerable. IDK

I'm unsure if it's a good idea to let #[doc] recognize tool attr. Tool attrs are only verbatim forwarded through rustc to linters.

The reasons to have proc-macros are

  • to emit more tokens as exhibited above: #[doc], #[safety_tool], and possible external verification attrs such as #[kani]
  • to workaround tool attr's namespace limit: #[safety] fails to compile, while at least one extra path followed safety compiles. Rust Playground
    • So we may need a proc-macro wrapper for now: #[safety] wraps #[safety_tool::inner] :smiley:
  • If we have declarative macro_rules! attribute macros, compilation times will be reduced.
  • It's awesome if we have reflection and comptime to let macros access type information.
36

I‘ve opened a thread on zulipchat channel to discuss there for people using zulipchat often.

37

Opened a real RFC PR, more on clippy:

#![feature(custom_inner_attributes)]
#![clippy::safety(invariant::ValidPtr)] // 💡

pub mod invariant {
    #[clippy::safety::tag]
    pub fn ValidPtr() {}
}

#[clippy::safety { ValidPtr }] // 💡
pub unsafe fn read<T>(ptr: *const T) {}

fn main() {
    #[clippy::safety { ValidPtr }] // 💡
    unsafe { read(&()) };
}
4 Likes