Two Kinds of Invariants: Safety and Validity

Unsafe code (in the sense of "code that must be specially audited to ensure UB-freedom") extends beyond unsafe {} blocks. For example, taking a reference to a partially initialized value and passing it to a safe function can and should be OK if the safe function is in the same module (or even crate, though stylistically I'd prefer to avoid that) and is deliberately written to be able to handle this. And that's for functions -- for unsafe {} blocks, I see no reason at all to ascribe much meaning to the syntactic extent of the block (as long as the code compiles). In particular, this distinction:

just seems adversarial to programmers for no reason. Both should be OK. What matters is that the value with broken safety-invariant doesn't escape to code that assumes the safety-invariant – which is all unknown code, but not necessarily safe code in the same library.

@RalfJung

I am glad to see that some of my previous ideas in comments on @nikomatsakis 's last blog post was presented in this blog. Specifically, the difference between ! and &!. I highlight the following:

while &! does not have a safe inhabitant, it is possible to have data that is valid for &! . After all, it does not have to point to a valid ! (which would be impossible).

For the same logic,

so validity for (T, U) requires that the first field is valid at T , and the second field is valid at U .

means (u32,!) is like !, it can never be valid.

Now the problem becomes: should we allow partial initialization on an invalid place?

I guess this also implies that partial initialization on invalid place should never be allowed, even in unsafe code.

I fully admit that I may be going a bit aggressive here, and may be over-applying a stretched conclusion. But I hope with the other notes here I can argue why this wouldn't be a horrible place to end up.


The intent of the direction I pulled this in, being the end of unsafe {} blocks, is one that I've seen in a few places: no one seems to be exactly certain where an unsafe block should end. The nomicon discusses this: changing safe code can break unsafe variants because safety is a global concern.

I don't see any reasons where this would require unsafe blocks around safe code. Safe code, by definition, cannot put values into an unsafe state. I guess, in the overly-aggressive-sanitizer specification, inbetween every line of code is an assertion that every place is valid, and inbetween every safe line of code is an assertion that every place is safe. (In my example I'm using field assignment as a proxy for writing out unsafe setters.)

This means that it's still fine for safe code to block calls to unsafe temporary violations of safety, just that the unsafe {} block delimits the scope in which values may be not in a safe state.

I don't think it's an unreasonable goal to say that structs should minimize the amount of time they're in a not-safe state; after all that means that you have to be really picky about panic points while a type is in an inconsistent state. It seems useful to say "this isn't in an unsafe block, thus the types are in a safe state", which also implies panic safety.

My interpretation boils down to whether this is the desired state of affairs. If we say that a reference is only safe if it points to a safe T, then it falls out of that definition that where safety holds, dereferencable-n-times and thus the de-ref optimization is valid.

I don't think it's much of a burden to require arguments to a safe function to be in a safe state. And the de-ref optimization shows that it's useful in at least one case. I don't disagree that a singular model covering safe and unsafe isn't simpler, though.

I know at least for my code, however, I have a strong preference for the former blocking of the two, as the unsafe {} block should be the unit of unsafety where possible.


I realize that safe code putting a same-module type into an unsafe state complicates things a lot, and the musing I'm outputting is likely more restrictive than the eventual model wants to be. But I think it's an interesting way of considering it, at the very least.

I tend to make and use unsafe setters rather than doing direct field access for most of my types anyway, so sometimes I forget that field access is always safe :stuck_out_tongue:


The way I've always thought of partial initialization is that the compiler treats them as distinct fields until the full place is initialized. So to use the common example:

let tuple: (T, U);
// do some work
tuple.0 = make_t();
// do some work with tuple.0
tuple.1 = make_u();
// do some work with tuple.1
return tuple;

This would become, effectively:

// do some work
let tuple.0 = make_t();
// do some work with tuple.0
let tuple.1 = make_u();
// do some work with tuple.1
return (tuple.0, tuple.1);

with the additional guarantee that tuple.0 and tuple.1 are arranged in memory such that tuple is just the memory place including both tuple.0 and tuple.1, and is valid once both tuple.0 and tuple.1 is valid.

So from that, we can derive that partial initialization of a partially uninhabited^1 place is allowed, just that it is impossible for the place to be fully initialized. The valid subset of the place can be initialized but the uninhabited subset cannot be validly initialized.

3 Likes

I like this idea. It is a way to get around the problematic

let t: (i32,!);
t.0=10;
t.1=abort();

Right now, it causes problem because (i32,!) was implemented as ZST, and so t.0 point to invalid memory. But with your proposal it will be desugar to

let t:(i32,!);
let __t0 = 10;
let __t1 = abort();
let t = (__t0,__t1);

even with (i32,!) being ZST, the above desugar will work.

But I would expect that, until in a static analysis shows that a value t is fully initialized, we should not allow it being sent to or return from other functions, even in unsafe code. If we change type of t to (i32, &!) in unsafe code should be allowed then.

1 Like

Your own example had unsafe { self.0 = 0; self.1 = 0; }.

And I don't believe I am just picking on a strawman. Applying your arguments, the implementation of Vec should never modify len outside of a unsafe block, even though it does not actually require unsafe.

I took a shortcut, and I failed to remember that safe code can break safety invariants within the same module. That is my bad. If I were writing Vec, I'd be using self.set_len(len) rather than self.len = len personally, because I like being reminded when I'm doing something potentially unsafe (especially around unwinds, which are invisible).


Good news, that's how it works! The compiler will complain about use of partially uninitialized / possibly uninitialized variables. The problem arises around unions/MaybeInitialized, and what parts are actually required to be valid when, which is the purview of the other thread, not this one. Let's not hijack this thread to talk about partial initialization :slight_smile:

Partial initialization is pretty in-topic as it relates to definitions about what is "valid" and what is "safe", and this is what the blog post is all about.

Partially; As ! is never initialized, the compiler should also apply the same rule; but we cannot because we want ! to be in the return position. For the parameter position though, I would say NO. If you want to write a function that receives uninhabited values, use indirection like &!.

(I am not saying you cannot declare a function accepts !; but such a function can never be called, and the compiler can always ignore such a function, even when deny(dead_code))

Howso? The only way to exit a function that returns an uninhabited type is to create a ! -- to diverge, panic, or call a subroutine that returns a !. How does this preclude the exact same initialization check as is done today?

The initialization check doesn't care about validity, safety, or any other measure of did you actually get a value of this type. It only cares about if every place has received a value. And if you call a diverging function, you can fully initialize an uninhabited type as far as the type checker is concerned. It's just that you cannot reach this (or, equivalently, reaching it is UB), as signified by having a value of type !.

It's perfectly allowed to take an uninhabited value as a parameter. It's just impossible to reach code that calls that function. (playground)

fn conjure<T>(never: !) -> T { never }

fn main() {
    let never = panic!();
    let it_came_from_outer_space: String = conjure(never);
    println!("{}", it_came_from_outer_space);
}

Oh, so we agree. There's nothing wrong about writing the function, it's just not callable. Nobody is arguing that. You can actually use a function that takes !, just not for anything useful. However, it should trigger the unreachable lint just like everything else that you don't use.

As a slight aside, there has been discussion of allowing fields to be marked unsafe as a reminder to the programmer that they're relied on by other unsafe code. len would be a perfect candidate for such a thing.

That is what I am proposing, yes. The terminology of validity vs. safety I think is useful independent of what we decide for references, (a) to be able to even have this discussion and (b) because there will be other differences between validity and safety.

I do not think we want the extent of the unsafe block to have any direct consequences.

However, I think this distinction is useful to define what unsafe code is. It is essentially code that works with unsafe data (data that is valid, but not safe). This goes back to what I wrote two years ago about how far out unsafe "leaks".

All of these discussions, as far as I am concerned, are happening on the MIR -- so autoderef is just a method call like any other.

See what I wrote above about it being hard to define where unsafe code ends. :slight_smile:

Yes! Maybe I should clarify in the post :slight_smile:

I cannot think of any.

I have been sitting on these thoughts for quite a while and wished I had them already spelled out for that discussion -- but then, that discussion certainly helped me to sharpen my thoughts and make them more precise.

Agreed.

Notice, however, that I glossed over one issue in that post: When I said all data must always be valid, I was only referring to data the compiler considers initialized. In

let x : &'static i32;

Certainly x must not be valid.

It is quite a burden. Unsafe code does things like calling size_of_val on uninitialized references -- I found an instance of this in Arc::drop_slow and I am sure I would have found more if I would have went on looking. See the PR implementing MaybeUninit for a whole bunch of examples where passing &mut T pointing to uninitialized data to known safe functions is very useful.

I am a fan of saying that a safe function must only be called with safe data, ever -- but first of all we still cannot make violations of this UB (because safety cannot be checked), and secondly this is surprising to lot of people.

That is totally the case. You can only move a value if the compiler thinks it is initialized, which means at this point is must be valid or else you have UB.

If you want to write a function that receives uninhabited values, stop what you are doing.

If you want to write a function that receives uninitialized values, e.g. to initialize them, use &mut T. This will usually be generic code. (That is assuming we adapt my proposal for validity, so your &mut T must be valid but that does not require you to find a valid T.)

I consider this the most beautiful part of the whole proposal.

4 Likes

How does unchecked_get and the likes fit into this model? In the standard usage of them, there is no unsafe data involved.

Excellent! This is the first solid answer I’ve seen to a question I’ve been wondering about: Is it okay for this code to mutate the memory behind an &mut str such that it is temporarily not UTF-8?

Under this model, I think this code can be correct if a non-UTF-8 str is valid but not safe.

5 Likes

The main reason of having a split between safety and validity is that whether an execution of a program is defined is only controlled by validity.

We very much want the question of "is this execution well-defined" to be answerable (and decidable),

However, it is possible (and in fact, had been proposed) to have a "tootsie pop" model with 2 separate notions of validity - one for safe code and one for unsafe code, but that is not what this post is talkin about.

To be more precise, an &mut str pointing to non-UTF-8 is valid but not safe.

I think str itself would have being UTF-8 as validity requirement. Being unsized, that's not extremely relevant, but would be relevant for unsized locals, for example.

And tail is always safe, right? So graphemes is only ever called on safe data? Yeah then I think this is fine under my proposal.

Continuing a discussion from Zulip, I think we may want to phrase both of these invariants as a kind of “range”. In other words, we might want to specify two things:

  • Things that your unsafe code must ensure is true
  • Things that your unsafe code can rely on being true
    • this should be a subset of the first one

The idea is that there are some validity invariants that we require now but which we might not always want to require. For example, right now we require that &T is aligned. Unsafe code might therefore rely on this by taking some random &T, casting it to a usize, and packing things in the low bits. If we decided to drop the requirement that &T is aligned – we could adjust our own codegen, but we can’t change that unsafe code.

Put another way, if all unsafe code implicitly has “validity requirements are met” as a precondition, we are not free to make more things valid without breaking that unsafe code.

Now, I’m not sure if there are any things we might consider changing in the future, but I think this is something we have to keep in mind.

5 Likes

This article is both rigorous and accessible at the same time - a great achievement!!

Notice that the “boundary” is not necessarily where the unsafe block ends. The boundary occurs where the unsafe code provides a public API that safe code is intended to use – that might be at the module boundary, or it might even be at the crate level.

(and more discussion in the comments)

I think that even if the model doesn't insist on the 'correct' placement of unsafe, it's still worth encouraging authors to do so. If you had a function like

fn change_vec_len(v: &mut Vec) {
  unsafe {
    v.set_len(v.len() + 10);
  }
}

that you know is safe because of the module/crate visibility boundary, I would still consider this bad practice - the function should be marked unsafe.

2 Likes

RalfJung, after reading your arguments on the MaybeUninit RFC and in your blog post “Two Kinds of Invariants”, I think you’re right that &mut T should be UB for uninitialized T. But, as you mentioned, there is already a lot of code that relies on this behaving as naively expected. All of this code could be converted to use *mut T, but the only way I’m aware of to get struct/enum member offsets (in general) is to create two &mut T's to uninitialized T, cast them to pointers, and then subtract. So at the very least, an intrinsic needs to be provided to get struct/enum member offsets before exploiting &mut T being UB for uninitialized T.

Even better would be to provide type or compiler-level support for partial initialization. I wrote a blog post recently about one approach, but to make it truly usable (i.e. efficient), a high-level optimization needs to be added to rustc. It would be amazing if someone intimately familiar with rustc and compiler optimizations could comment on the feasibility/difficulty of implementing such an optimization.

In the Reddit discussion for my blog post, we came up with an alternative approach using an &uninit T type that is linear (exactly single use) and write-only. This approach would be more ergonomic and more deeply engrained into the compiler. I plan to write a blog post exploring this latter idea a bit more, but it seems like it would be much more involved to implement, and so should likely be de-prioritized in favor of a quicker solution; but again, I would love to get input from someone intimately familiar with rustc.

That's funny, because I never argued for this. :slight_smile: I brought it up as a possibility, but my own thinking is actually that &mut T is only UB for NULL/unaligned references, and (through the aliasing model) for dangling pointers, but makes no statement about the pointee being initialized. The next topic of discussion in the unsafe-code-guidelines WG will be covering this.

It is true that we would be in a more type-safe world if people used some kind of &out instead of &mut when data is still to-be initialized -- but it is not at all clear to me that all that extra complexity would be worth the benefit.

1 Like

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.