Unsafe fields cannot define a correct moment to check conditions

For unsafe methods, the safety requirements can be divided into exact two categories: requirements before invoking (Vec::set_len requires new elements are initialized before this function), and requirements after invoking (Pin::new_unchecked requires no move after, ManuallyDrop::drop requires no use after). Violating the requirement is immediate UB, even if the requirement is repaired in a short time. The std documentation has a great example for this.

However, for unsafe fields, things become complex. Let's take the example in the lang meeting of unsafe fields:

struct CacheArcCount<T> {
    // SAFETY: This `Arc`'s `ref_count` must equal the
    // value of the `ref_count` field.
    unsafe arc: Arc<T>,
    // SAFETY: See [`CacheArcCount::arc`].
    unsafe ref_count: usize,
}

Then how can we write a correct ref_increment?

fn ref_increment(&mut self) -> Arc<T> {
    let new_value = unsafe { Arc::clone(&self.arc) };
    unsafe { self.ref_count += 1; }
    new_value
}

(Let's assume that there is some drop guard to make sure self.ref_count is decremented if the new value is dropped. That is off topic)

This code is obviously correct in current Rust without unsafe fields. And considering unsafe fields, the safety requirement of self.arc and self.ref_count is always held before and after self.ref_increment, but not inside it.

After the new_value is created, and before incrementing self.ref_count, the contract that "This Arc's ref_count must equal the value of the ref_count field" is not held. Is this code unsound in terms of unsafe fields?

This can actually lead to safety problem if:

fn ref_increment2(&mut self) -> Arc<T> {
    let new_value = unsafe { Arc::clone(&self.arc) };
    some_func_may_panic();
    unsafe { self.ref_count += 1; }
    new_value
}

Then, here we go, an exception safety violation!

As a result, the core problem of this post is that:

How to define the moment that unsafe fields' contracts need to be held?

For an intuitive point of view, where the answer is "anytime", then there could be no sound version of ref_increment.

2 Likes

The safety invariant of an unsafe field is a library invariant, not a compiler invariant. As such violating it doesn't cause immediate UB. Instead you are required to ensure the invariant gets upheld before you pass it to any code that doesn't explicitly document that it doesn't depend on the library invariant holding for avoiding UB. ref_increment correctly ensures this and is thus not UB.

4 Likes

This code is wrong in a way which might possibly undermine your example: if you do cac.ref_increment().clone(), this increases the refcount of arc (due to cloning an Arc that's a clone of it) but not the ref_count field (which Arc doesn't know about), so the two are out of sync now.

This is of course true, but if we try to make unsafe validation strictly formal I find the question interesting. And given that unsafe fields' almost sole purpose is to tighten the formality of validating unsafe, this is probably a fair question.

2 Likes

Both Vec::set_len and Pin::new_unchecked have "library" safety requirements, so violating them is not immediate UB, it's just "library UB". You can Vec::set_len before actually initializing those additional elements. That's fine as long as safe code outside your unit of implementation always sees a Vec value that satisfies its safety invariant.

As @bjorn3 said above, unsafe fields just have library invariant, not language invariant. So you can break them freely within your unit of implementation. You just need to restore/uphold them at your public boundary (your public API and the public API of your dependencies). The whole question being what's your unit of implementation: a function, a module, a crate? You get to choose, but must be consistent in that choice throughout that unit of implementation.

1 Like

That is not true. A future implementation of Vec::set_len() would be within its rights to assert, or even assert_unchecked(), that the elements which set_len()’s safety conditions say must be initialized are in fact initialized when set_len() is called.

The entire definition of “library UB”, as I understand it, is that it is a circumstance that may or may not be “language UB”, but which the library is always allowed to upgrade into immediate “language UB” in a future compatible release.

3 Likes

The std documentation that I linked in my post states different (as far as I understood)

use std::mem;

let mut v = vec![65, 122];
// Build a `String` using the contents of `v`
let s = unsafe { String::from_raw_parts(v.as_mut_ptr(), v.len(), v.capacity()) };
// leak `v` because its memory is now managed by `s`
mem::forget(v);  // ERROR - v is invalid and must not be passed to a function
assert_eq!(s, "Az");
// `s` is implicitly dropped and its memory deallocated.

There are two issues with the above example:

  • If more code were added between the construction of String and the invocation of mem::forget(), a panic within it would cause a double free because the same memory is handled by both v and s.
  • After calling v.as_mut_ptr() and transmitting the ownership of the data to s, the v value is invalid. Even when a value is just moved to mem::forget (which won’t inspect it), some types have strict requirements on their values that make them invalid when dangling or no longer owned. Using invalid values in any way, including passing them to or returning them from functions, constitutes undefined behavior and may break the assumptions made by the compiler.

Anyway, I do wonder if there any "official" formal definition of "library invariant" and "language invariant". I only found it in several blogs or issues, like Ralf's blog, Rust magazine blog, this GitHub issue. Are there any verification engines, like kani or verus, that aware this thing?

My bad, I was working under the context of the same unit of implementation (either a custom Vec or within std), because the unsafe fields were private, which would be like having Vec::set_len be private, which means being in the same unit of implementation.

For public unsafe fields it's indeed more interesting, and I believe the answer is similar to public unsafe functions. It is immediate UB (not sure when it could actually be language UB though, but it should be assumed that it could).

I would expect any tool that deals with unsafe code to be able to say whether the safety invariant holds or not (within the same unit of implementation, which is where it makes sense to violate the safety invariant).

In RefinedRust there's the #raw notation to talk about the representation of a type, without its safety invariant.

In VeriFast my understanding is that you always have to state whether the safety invariant holds, so by default it doesn't hold.

A future implementation may do that. But the current one doesn't. Therefore, if you consider UB as defined by the Abstract Machine / Miri ("language UB"), then calling set_len incorrectly is currently not immediate UB.

The entire thread seems predicated on not teasing apart these subtleties properly. I don't think unsafe code causes any new issues / questions here: writing to an unsafe field is fully equivalent to writing to a normal field in terms of the Abstract Machine / Miri ("language UB"). So if you are analyzing for "language UB", you can just ignore it. And when analyzing for library UB, you already have to have something in your tool that represents the safety invariant of each type; unsafe fields are merely a marker that such an invariant is present on certain fields. So IOW if you are using such a tool then unsafe fields don't really change anything for you. It is only if you are not using such tools that unsafe fields come into play: they enable the compiler to remind you that there is a proof obligation to re-establish the custom safety invariant.

1 Like

Yes, I didn't know library UB vs language UB at the time I posted. I think I understood these a little bit more, especially by reading your excellent blog.

Yes, the concept of library-UB does solve the problem, if I understood it right: library invariants allows to be broken temporarily as long as it is not exposed.

Another question arises is that, do current std doc's SAFETY requirements follow this model? Is it only when "become immediate UB" appears in the doc that the doc represents a language invariants? I find myself quite confused which safety invariant allows temporarily broken (like Vec::set_len), while which does not (like ptr::offset).

Isn't that analogous to saying: "the current version of rustc compiles the unchecked_add in my function into add in assembly and that works fine for overflow and thus it's not currently UB"? UB is supposed to be about what is allowed to happen by the specs rather than what currently happens in today's version of the library. Library UB is still UB even if the current version of the library doesn't use its full freedom to cause mayhem today, just like language UB is still UB even if the current version of rustc doesn't use its full freedom to cause mayhem or Miri doesn't detect it.

It is analogous, if you want to introduce a distinction between "language UB" and "de-facto UB". But you have to introduce that distinction to make the analogy. And we don't really find it helpful to track "de-facto UB" as a separate thing, whereas "language UB" is very useful as a separate concept -- it is specified very differently from library UB (operational semantics in an Abstract Machine, vs a more axiomatic style that is also much harder to formalize).