SAFETY documentation may be inconsistent with soundness verification specifications

language design Unsafe Code Guidelines
21

I don't know what you mean. Types have a single invariant, that is the implicit precondition of all safe functions that receive a value of the type.

22

As far as I understand, there are indeed some cases where we cannot find a way for easier to verify, as stated in the part 8.4 of my note. The entangled unsafe fields make it always have a library-level invariants breaking window.

23

I agree that this is theoretically possible. However, the example you linked to is contrived, and I think it's likely to be very rare that doing so is actually useful in practical code. Even if it is useful sometimes, it would still be an improvement to avoid it in the cases where it's easily (and performantly) avoidable.

2 Likes
24

Sorry for being ambiguous. Let's say std::string::String. The invariant of String has two parts (which I was calling it two invariants): The UTF-8 part, and the initialized memory part. An unsafe function that affects the UTF-8 part without initialization one allows the modified String being observed by those safe functions that only need the initialization part, and vice versa. The question is that, although the SAFETY documentation only serves in those unsafe functions, this complicated scenario also makes those safe functions' pre-conditions special.

25

Maybe that's complicated, but that's an accurate description of the truth. I think that's how it should be done. Note though that the standard library never documents robustness, because it's conservative for stability reasons. So here's an example with MyString instead:

/// UTF-8 encoded string with 3 type states:
/// - Safe (the default): the string is initialized and UTF-8
/// - Bytes: the string is initialized but not necessarily UTF-8
/// - Garbage: the string is not necessarily initialized
pub struct MyString(MyVec<u8>);
impl MyString {
    /// Robustness (requires): self must be Garbage
    // (This requirement is weaker than the default, making the function robust.)
    pub fn len(&self) -> usize { self.0.len() }

    /// Robustness (requires): self must be Bytes
    pub fn as_bytes(&self) -> &[u8] { &self.0[..] }

    /// Safety (requires): bytes between self.len() and new_len must be
    /// initialized and UTF-8
    pub unsafe fn set_len_v1(&mut self, new_len: usize) { self.0.set_len(new_len) }

    /// Robustness (requires): self must be Bytes
    /// Safety:
    /// - (requires) bytes between self.len() and new_len must be initialized
    /// - (ensures) the result is Bytes
    // (This guarantee is weaker than the default, making the function unsafe.)
    pub unsafe fn set_len_v2(&mut self, new_len: usize) { self.0.set_len(new_len) }

    /// Robustness (requires): self must be Garbage
    /// Safety (ensures): the result is Garbage
    pub unsafe fn set_len_v3(&mut self, new_len: usize) { self.0.set_len(new_len) }
}
26

There is no function in String that breaks its UTF-8 encoding. If there was one, it would be a bug. This is unrelated to whether the function is unsafe or not.

27

I believe they were referring to something like String::as_mut_vec(). The safety documentation doesn't require the caller to only write UTF-8 to the returned reference (contrary to what I would have expected), so you could call that function to break UTF-8.

1 Like
28

I see. That seems inconsistent to me because String's documentation also says:

Strings are always valid UTF-8.

Is dropping such a non-UTF-8 String allowed?

29

This assumes that new_len > self.len(). I don't think there should be a safety requirement on the now-out-of-length bytes.

Also, are there no constraints with capacity?

30

"Strings are always valid UTF-8" is a library-level invariant, which allows temporarily broken, as long as that breaking state is not observed by language-level unsafe usage. And the dropping is typically an observation, so I guess that is not allowed.

31

Me too. My experience is that the standard library usually tries to be conservative regarding unsafe functions. In particular, it tries to make sure the safety invariant of non-generic types always hold (you can't temporarily break them). For generic types it's different (for some reason). For example transmute only talks about the validity invariant which is what it needs to avoid UB during the call (not to avoid UB after the call).

Given that <String as Drop>::drop() is part of the standard library, it assumes its input to be UTF-8. So no, dropping such an unsafe value is not allowed. (But anyway, probably the current safety documentation is poorly worded and didn't mean to allow unsafe values to be built.)

That was just an example, not an attempt at describing precisely what a hypothetical non-conservative String API could be. That's orthogonal to the discussion.

32

My read of the safety documentation there is that it allows temporally writing non-UTF-8 into the Vec, but that it must contain valid UTF-8 upon the &mut Vec being dropped. Perhaps this could be worded more clearly in the documentation.

33

That reading would make sense yes. If that's the intent, then the wording is not clear in my opinion. I would expect something like:

This function is unsafe because the returned &mut Vec allows writing bytes which are not valid UTF-8 and the rest of the standard library assumes that Strings are valid UTF-8. The caller must guarantee that the &mut Vec contains valid UTF-8 when dropped.

34

allowing safe functions to have pre-conditions

I should note that we have language for this in common usage — the safety preconditions of safe functions are by definition the types' safety requirements. These are only rarely publicly documented directly on the type, though; instead the usual style is to describe the safety requirements of each unsafe function to not break the type's safety requirements.

It is, however, still sound to rely on a weaker set of preconditions, often called the validity or language requirements. If you have a separately communicated guarantee, such as by being the author of the code in question, it's considered sound to suspend safety so long as you do not break validity (language invariants).

Safe functions with weaker preconditions than the implied ones have been proposed to call "robust" or "super-safe." But it's important to note that unsafe functions also have the implied safety conditions, and are also allowed to relax them by communicating guarantees.

The best name I've come up with for this interaction is "permitted unsafety" (see the end of this post).

[Vec::set_len as an example]

Personally, now that we have Vec::spare_capacity_mut, I much prefer the style of filling before set_len. Before that method, you'd need to use Vec::as_mut_ptr and a pointer offset to access the spare slots, which is much less convenient and more error prone than the set first approach. Before 1.37,

The danger in the set-first approach is unwind safety. If you do anything much more than a ptr::copy, you risk an unwind that leaves the Vec in an unsafe state. Avoiding this, where possible, is strongly preferable, because proving unwind freedom is a much more difficult proof than most other unsafe conditions we tend to work with.

Most of the time, a cleverer API can allow avoiding temporarily suspending type safety requirements. But in some cases, doing so doesn't make the code any better, or maybe can't even be written. Consider RawVec::grow, roughly (simplified to only relevant parts):

struct RawVec {
    // SAFETY: is allocated with `self.cap`
    ptr: NonNull<u8>,
    cap: usize,
}

fn RawVec::grow(&mut self, new_cap: usize) -> Result<()> {
    let new_ptr = unsafe { realloc(self.ptr, self.cap, new_cap)? };
    // type safety requirement broken here
    self.ptr = new_ptr;
    self.cap = new_cap;
    // type safety requirement restored here
    Ok(())
}

fn <RawVec as Drop>::drop(&mut self) {
    if self.cap != 0 {
        unsafe { dealloc(self.ptr, self.cap) };
    }
}

To write this without breaking the type invariant would require something like:

fn RawVec::into_raw_parts(self) -> (NonNull<u8>, usize) {
    let this = ManuallyDrop::new(self);
    (this.ptr, this.cap)
}

fn RawVec::grow(&mut self, new_cap: usize) -> Result<()> {
    let this = mem::take(self);
    // note: places a default value in `*self`
    let (old_ptr, old_cap) = Self::into_raw_parts(this);
    let try_new_ptr = unsafe { realloc(old_ptr, old_cap, new_cap) };
    match try_new_ptr {
        Ok(new_ptr) => {
            *self = RawVec { ptr: new_ptr, cap: new_cap };
            // note: drops the default value from `*self`
            Ok(())
        }
        Err(e) => {
            *self = RawVec { ptr: old_ptr, cap: old_cap };
            // note: drops the default value from `*self`
            Err(e.into())
        }
    }
}

This requires more safety-critical code with more places to get it wrong even though it makes the same number of unsafe calls[1]. Furthermore, this only works because RawVec has a reasonable empty default value to stick in *self temporarily. In C++ that's called an "arbitrary but valid [to delete] state" like you get left over after moving out of an object. Part of the elegance of Rust's destructive move semantics is that types don't need to have a default "null" value.

Obviously it's a good idea that if people are using the weaker preconditions that don't include all of the type safety requirement, that should be documented somehow. Unfortunately I don't have any insights on how to do so, especially without cluttering the docs for the 99% use case that doesn't need to do so.

The best idea I've had is to have a “permitted unsafety” section on unsafe functions like Vec::set_len that lay out the weaker preconditions as well as the postcondotions that you need to fulfill in order to return to safety. Putting the list of safe functions of the type you're allowed to call with a partially-uninit Vec in the Vec::set_len documentation puts that information where it matters (users of set_len) without cluttering the other functionality to discuss this niche case.

As an example draft wording:

Safety

  • new_len must be less than or equal to capacity().
  • The elements at old_len..new_len must be initialized.

Permitted Unsafety

It is unsafe but permitted for elements at old_len..new_len to be uninitialized. To restore safety, you must ensure all of these elements have been initialized.

Until safety has been restored, you must not drop this value. The only safe functions to call with this unsafe value are:

  • Vec::allocator
  • Vec::as_ptr and Vec::as_mut_ptr
  • Vec::capacity
  • Vec::len and Vec::set_len
  • Vec::into_parts[_with_alloc] and Vec::into_raw_parts[_with_alloc]

  1. If we're being strict, the fields should be unsafe to write. This would add one unsafe block to the in-place version around the critical section which breaks the type safety requirement, and would add two to the re-place version for each of the struct constructors. But the safety-critical into_raw_parts still remains unmarked; it's unsafe to trust but not to write, by design. ↩︎

3 Likes
35

This is a symptom of String::as_mut_vec having a safety requirement which is not a precondition, but a "postconstraint." What the docs try to say is that you are allowed to write non-UTF-8 to the vector (which is temporarily necessary to edit non-ASCII contents), but you MUST (in order to satisfy the requirements for safety) ensure that the bytes are valid UTF-8 before releasing the borrow and allowing code to access the String value.

Accurate and accessible language around this kind of "postconstraint" is hard, and we don't have consistent documentation patterns for them yet. They're bad API design, generally speaking (preconditions and type level invariants are much easier to reason about and prove), only to be reached for when necessary and to implement safer subsets of the functionality. IIRC, the only two cases of "postconstraints" in the stdlib are String::as_mut_vec, str::as_bytes_mut, and the big one: unchecked Pin access (get_unchecked_mut, map_unchecked_mut, and into_inner_unchecked).

transmute is a bit of a special case and exception that proves the rule, due to its status as an intrinsic. It also doesn't have a documented # Safety section! I would argue that if it did, that section should mention that the produced value must be a safe Dst as well as a valid one.

Unfortunately, the stdlib docs don't really expose the explicit idea of type-level safety invariants; the std's conservative style is to document every unsafe fn's safety preconditions such that std's safety invariants are publicly just "the value was produced by a series of safe operations."

That there is a split between public safety/library requirements and private validity/language ones is a decided deal, but the exact language for discussing such isn't fully agreed upon yet. Thus transmute's docs describe the behavior and validity requirements and leave the safety requirements up to the developer to derive.

2 Likes
36

I forgot about that, so there's actually 2 levels of conservatism in the standard library:

  • Strong requirements on unsafe functions such that safety invariants are not violated. In other words, values should be well-typed (which is not always convenient).
  • Not committing on a definition of the safety invariant, but instead use a flexible definition based on the current set of operations. Such strategy is why we have soundness conflicts (doing better is hard).
37

I did see many occurrences of "robust", but I didn't know its concrete definition in Rust. I wonder if there is a pre-RFC or something that introduces this concept for further discussion.

38

The robust terminology comes from the unsafe mental model, but that document does more than just introduce this concept. Also the definition is more general than just "safe functions with weaker preconditions".

The shortest definition is: robust is the dual of unsafe in APIs.

A longer definition is: where unsafe means "safety requirements on the user of the API", robust means "safety guarantees for the user of the API" or equivalently "safety requirements on the author of the API".

An important note and source of confusion, is that "requirements and guarantees" are orthogonal to "preconditions and postconditions". You can have guarantees in preconditions and requirements in postconditions. This is a consequence of the fact that values don't need to be well-typed in Rust, leading to the existence of unsafe values. Accepting unsafe values makes a function robust. Returning unsafe values makes a function unsafe.

39

So this is even not in a pre-RFC state. I really think there should be a comprehensive summary around the tightly-coupled concepts: unsafe -- SAFETY documentation -- two kinds of invariants -- soundness verification -- safety contract. That summary may not bring new ideas, but just summarize all proposed solutions, and most importantly, the extent of people's consensus.

The first reason is that those concepts have been too messy and non-official. For instance, about the two kinds of invariants (which I believe almost everyone agree it is true), there are only three articles in the Internet to talk about it (afaik), and none is in the official documentation, while the std doc suddenly mentions it here. Another example is the robust. Although it is vital to a proper model of library unsafety, and has been mentioned by many people, it is still not broadly discussed and I guess not broadly accepted.

The second reason is that those concepts are important both for library developers and soundness verifiers. Although some of those concepts haven't had all-agreed solutions, at least people should be aware of it, and may further discuss about it when writing safety critical applications. For instance, when browsing issues of verify-rust-std, I found that that community may be thinking that set_len must have all new slots initialized before call (in my understanding) here (See the third bullet in "Required direction to reach APPROVE"). I don't know if that community has been aware of those concepts, and if not, I'm afraid that lots of works may not work as we expect. And just clarify myself, I do not mean that we should immediately come up with an all-agreed solution or model for those concepts, since the explorations of practical works can further enhance the solutions. However, I do think a comprehensive summary could help people be aware of those things.

1 Like
40

I don't think anything from the unsafe mental model should make it to Rust. If safety contracts are properly done (which I'm pretty sure they will in 5 to 10 years), they should be able to cover everything in the unsafe mental model (which is just a type system approach to the program logic approach of safety contracts).

I agree and we're not alone to believe so. I know other people and organizations who are also pondering writing learning materials around unsafe. That takes time: unsafe is a difficult and vast landscape. One of my hope is that some Unsafe Rust Working Group would come to life and host such information. (Note that this is different from the UCG, which goal is to figure out the Rust operational semantics. The Unsafe Rust WG would depend on the UCG.) I've been made aware of safer-rust · GitHub but they're too focused on their projects and tools to be useful to the whole Rust community.

There's a good reason for that. In Rust, all functions are robust, because unsafe code may rely on their correctness. This means that safe code can cause UB outside its dependencies, but that's by language design. Robust becomes useful only if you care about safety, and want to prevent safe code to cause UB. This means you work in a sub-ecosystem with different policies and must review third-party crates against your policies.

We came to the same conclusion in this thread right? That's the standard library being conservative.

I would be surprised if they're not. Those concepts usually become visible after some amount of exposure to unsafe, which they should have had.

I totally agree, but what do you suggest?

1 Like