Types as Contracts

language design Unsafe Code Guidelines
41

I brought up a similar example in an earlier post, and the reaction was that out-of-bounds get_unchecked should just be UB, regardless of what it ends up accessing. (Of course, this is easy to check in sanitizing mode.)

Of course, UB can cause arbitrary negative effects, but this isn't about malicious code; it's about honest code making a contract with the compiler. With "unchecked", you (the code author) would promise not to request out-of-bounds indices, and the compiler would guarantee that no other types of UB can occur.

So the split is viable - but I still find it fairly dissatisfying, as it only improves things for a subset of use cases. For other use cases, the dilemma remains. Either:

  • Using, e.g., FFI (or other non-unchecked unsafe stuff) anywhere in a module penalizes the entire module, which could be the whole codebase for small programs.

or

  • Refactoring a function by moving some code into a separate function can create undefined behavior where there was none before.

They're both spooky action at a distance, affecting performance and correctness, respectively.

But... I'm really starting to lean towards a relatively UB-maximalist policy, personally. A lot of the original Tootsie Pop discussion boiled down to what code people are likely to write. In that regard, I suggest a simple principle.

Real code rarely commits aliasing violations conditionally.

That is, if the faulty code is reached, chances are it'll always commit a violation, rather than only doing so with certain inputs. This is very different from other types of UB, like integer overflow in C, which are usually input-dependent.

There may be some exceptions. I'll give you one up front: suppose some code takes array: &[Foo], idx1: usize, idx2: usize; accesses the idx1'th and idx2'th items of array; and on each, calls get on an UnsafeCell and converts the result to &mut, keeping both references alive at the same time. Then an aliasing violation will only occur if idx1 == idx2, obviously. But (a) deoptimizing unsafe code won't necessarily fix that case, e.g. if the code passes the two &muts as parameters to some unrelated safe function; and (b) most cases are not like that.

Therefore, with respect to aliasing, the sanitizer is almost as good as a static compiler check. We accept (empirically) counterintuitive aliasing rules when the borrow checker can enforce them; why not when the sanitizer can enforce them?

What's more important is ensuring that people actually run the sanitizer, and heed the output. Suggestions:

  • Take performance seriously. I have a lot to say about potential implementation strategies, but it's off topic here :slight_smile:
  • Have cargo test default to using it (when unsafe code is present?)
  • From experience with C, people are always tempted to dismiss sanitizer warnings as "false alarms" or "harmless". Minimize their motivation to do so:
    • Make the warnings kinda scary.
    • Ensure there's always a trivial patch that will make the errors go away, even in cases where a 'proper' fix would require more refactoring. For example, have a block attribute to just disable all aliasing assumptions in the block.
1 Like
42

Intuitively, it seems to me that the back-channel access to *x should be illegal, depending on how exactly foo() got access to it. This may very well wind up having an effect like locks in many cases, but it may not need to take the specific form developed here. For example, I believe that the (draft) proposal posted earlier by @strega-nil may allow this optimization, depending on how foo() gets access. Let's say x_foo: &usize is a reference to *x that was obtained by correctly guessing its address "ex nihilo" (to pick an example that should certainly be UB). In her terminology, and assuming I understand correctly, we would have !(*x_foo $ *x). Then the access to *x_foo in foo() is UB because there was a previous write through *x.

Again this is highly dependent on how foo() gets access to the pointer, but this is a feature, not a bug. We should not do the optimization if x escapes in a legitimate manner—and indeed the contract model also has ways in which this might happen (e.g., anything that reborrows x for a lifetime covering the call, or the presence of unsafe code if a tootsie-pop-/Sachertorte-ish approach to unsafe blocks is adopted).

The question (which is far from new, of course) is then what such a "legitimate" means of smuggling the reference might include and what not. For example, suppose the caller converts a short-lived (lifetime not covering the foo() call) &*x to a raw pointer, stashes it away in a thread local, and during the call foo retrieves it and casts it back to a reference.

  • IIUC this would be legitimate under the access-based models (I'm including @strega-nil's most recent propsal here, not sure if that's entirely correct), as long as the dance by which you transport the pointer stays within the boundaries of what the model considers "derived" (or equivalent).
  • A types-as-contracts-ish model would presumably either make it UB or deoptimize quite a bit of surrounding code. In the Sachertorte model, this would chiefly depend on whether the "escape" in the caller involves unsafe operations (releasing the lock on *x) or only safe and unchecked ones (keeping the lock).

In this example, I'm not even sure which version I prefer. Which almost makes me want to err on the side of caution (i.e., permitting it with an access-based model) to avoid breaking subtle unsafe code.

43

Indeed this matches the violations I have seen so far (running the miri test suite with the MIR validation statements emitted everywhere, even for unsafe code). These include:

  • AtomicBool::get_mut briefly holds on to two overlapping mutable references to the same data
  • mem::swap passes raw ptrs on to copy_nonoverlapping, so mem::swap keeps the write lock
  • RawVec::into_box has a slice: &mut [T] and a output: Box<[T]> to the same memory

Another thing these all have in common is that the problem is mutable references sticking around after having been converted to raw pointers. So maybe there is a way to make that conversion meaningful -- releasing the locks and not acquiring them again. (I keep wishing that raw pointers had lifetimes -- even if they would not themselves be used for validation, they would steer borrowck to suspend the mutable references for the right amount of time in all examples I have seen so far.)

slice::as_mut_ptr (as called by split_at_mut) is an interesting case in this contexts because it hides the ref-to-raw-ptr-conversion -- so e.g. just doing something special at the cast operation does not suffice. (And again, if only raw ptrs had lifetimes... split_at_mut would just work.)

However, what this would not allow us to do is the following:

let x: &mut usize;
foo();
*x += 1; // can we move this up across the call to foo?

Access-based models that do not use any form of "proactive" locking will always have the problem that if you cannot prove that a program used some particular data, then you cannot assume that data is valid in any way; this includes all aliasing guarantees. I feel like the meaning of types should not depend on whether the variable that has that type is actually used or not.

(Also, @strega-nil does not yet handle raw pointer casts or ptr-int-conversions, so it is hard to guess what exactly will and will not be permitted. I am looking forward to these details being fleshed out.)

"Pure" Types-as-Contacts has a pretty clear answer to such questions -- there is no smuggling. If there's something you own exclusively (i.e., you have it in a &mut), then the only way anyone can access this memory is if you pass the reference to them, at reference type. I like this rule for its simplicity.

Of course, the problem is, it looks like unsafe code wants to do some amount of smuggling. My personal stanza on this is that if we want to permit this (and it seems we do not have another option), then we should be cautious about second-guessing the programmer concerning which smuggling does or does not happen. My worry with access-based models is that they will permit some smuggling and rule out other smuggling; can we make it so that it is clear to the programmers what is and is not permitted?

44

So, coming back to this noalias discussion... I am still not sure I entirely understand how the scoping is supposed to work here. I brainstormed some ideas with @aturon to model Unique, and now that I realize its flaws, I realize I do not understand noalias and the intended effect of Unique enough. When I call Vec::index_mut and that gets inlined, just for how long is that pointer supposed to be unique? As with &mut, I'd like to encode uniqueness by validating things, so actually this would even be asserting that the target of the pointer is valid for whatever scope we are talking about. My first hypothesis was that this scope would be "until the Unique itself gets modified, but then I realized that pop may end up just decrementing the length -- invalidating the index_mut of the previously last index, but not changing the Unique pointer itself. Do you think that no_alias's scope should extend beyond a non-shrinking inlined pop?

So maybe the problem is in the approximation of noalias by validation; validation is "deep" and also asserts that the pointer-to memory is valid, while noalias is very "shallow" and just says that this is the only way to reach that pointer. But even then, there are some interesting scoping questions. For example: What if we have a RefCell<Vec<T>>? The scope of uniqueness of borrow_mut().index_mut() must somehow be restricted to the lifetime of the RefMut. How does that happen?

@Gankra it would be interesting to hear your thoughts on this; IIRC you had some pretty clear ideas about Unique.

45

Correct. And I would say, obviously we should be allowed to do that in this case, but there's always going to be some desirable optimizations we can't do. Drawing the line here seems okay (at a glance, more realistic case studies would be needed of course) since it's not a particularly interesting optimization and the alternatives that would allow it don't (currently) seem more appealing.

Why is that particular example seems rather uninteresting (unprofitable) to me? Precisely because there are only accesses after the call. I can't think of much motivation for moving it up in that case (not even cache locality, which goes beyond the scope of typical compiler optimizations).

Yes, this is a good point. However, despite how unsatisfying that may be from a "types mean things, god damn it" perspective (more on this below), it seems pretty okay from a "don't break unsafe code that's a bit wobbly but basically okay" perspective.

I can empathize with that, but I also feel the meaning of types shouldn't vary depending on how close I am to an unsafe block. This isn't an entirely fair characterization of the type-contract model, but what I am trying to get across is: yes, the model is a slam-dunk for safe code, but unsafe code is playing fast and loose with the semantics of those types anyway (and often by design). For example, if I have a raw pointer and somehow know nobody else is accessing it currently, then I should be able to just access it, no questions asked. I shouldn't have to worry about what types I have in the function signature, or the precise placement of the unsafe keyword, except insofar is necessary to ensure that my assumption (about no one else accessing the memory location) is correct. Of course, this desire is incompatible with other nice properties I want, my point is that access-based models are quite appealing to the unsafe code author in me.

Hm, this is an interesting perspective, because I would have argued the opposite: that the access-based models are very liberal and allow any "sensible" kind of smuggling, as long as the actual accesses (which are more central to the function of the unsafe code than the precise means of smuggling) are well-behaved. Meanwhile, types-as-contracts appears to make the smuggling legal if and only if certain correlated (but not necessarily 100% accurate) language features are used "around" the location of the smuggling. I see what you mean, though. An access-based model could just as easily be overly strict. The ones discussed so far seem to be rather liberal, though (without being trivial—e.g., @strega-nil's model still makes it UB to turn a &mut into a raw pointer and create and use two distinct &muts from this raw pointer).

46

Now that's funny, because I fully agree with this. :wink: It is exactly this kind of thinking which lead me to a model that uses no provenance tracking, a model where a pointer really is just a location in memory and does not also carry some "magic" meta-data about how it was computed. For example, I think unsafe code authors will expect the following two snippets should be contextually equivalent, meaning that snippet A can be replaced by snippet B no matter the surrounding code:

// ptr1, ptr2: *mut i32
// A
if (ptr1 as usize == ptr2 as usize) {
  *ptr1 = 42;
}
// B
if (ptr1 as usize == ptr2 as usize) {
  *ptr2 = 42;
}

So, what is your (and any other unsafe code author reading this) thinking here? Is it expected/acceptable/a catastrophe for a model to ever make a distinction between the two programs above?

My problem with this is that I do not think alias-based models provide that. They typically involve some form of provenance tracking, which means whether it is okay for you to use a pointer or not depends on how the pointer was computed. The two snippets I gave above are generally not equivalent in models that track how pointers are computed. (E.g., to use @strega-nil notation, it may be that for some third pointer ptr3, we have ptr3 $ ptr1 but not ptr3 $ ptr2, so one snippet may be allowed while the other is not.)

2 Likes
47

I would like it to just work, but I also know that this is impossible to achieve while having the kind of alias analysis LLVM does, and which raw pointers should probably have regardless of the higher-level issues discussed in this thread [1]. So it depends on when exactly the model makes a difference. For example, it would really suck if it mattered whether the two pointers came from borrows with different lifetimes.

I'll have to sleep over this more realistic case, though:

Going off the negative example in the gist, one case where that might happen in @strega-nil's model if ptr1 and ptr2 are derived from two different aliasing mutable references (i.e., both are derived from separate instances of &mut *some_raw_pointer and thus !(ptr1 $ ptr2)). ptr3 would be derived from ptr1. This is indeed something that should Just Work if pointers are "just a location in memory", but I'd have to play around a bit to decide whether this is an acceptable concession or too error prone in real code.

[1] For example, I would like to be able to conclude that the parameter does not alias x, which C does achieve:

unsafe fn optimize_this(p: *mut i32) -> i32 {
  let x = 1;
  *p = 2;
  return x;
}

Without such capabilities, I fear big regressions in alias analysis precision in unsafe code, even compared to the relatively conservative baseline of C w/ -fno-strict-aliasing. And code like the above should not be defined even if the caller happens to correctly guess the address of x. It's Just Plain Wrong.

Also, I don't know how to turn that behavior off in LLVM.

48

Sorry, I'm getting sloppy. What I mean is it should be UB if the parameter is made up ex nihilo and just so happens to be bitwise equal to the address of x. So in this setup, if ptr1 = p and ptr2 = &x, then I am affirmative that your two snippets should be treated differently.

1 Like
49

I was actually referring to the same case, but whatever. :wink:

This particular example is actually easy as x does not have an address. Where it would get interesting is if you force x to have a guessable address:

unsafe fn optimize_this(p: *mut i32) -> i32 {
  let x = 1;
  let _make_me_guessable = &x as *const _ as usize;
  *p = 2;
  return x;
}

Now it seems to me that you need provenance tracking to enforce p and x not to alias.

50

Wow, that's surprising to me. Interesting, and thanks for the feedback!

51

Ah, sure, I was thinking a bit too much in LLVM IR (which doesn't do the "objects don't have addresses until they need one" thing).

Yes, I agree and I intended something like that. (And indeed C compilers still optimize that.)

I feel compelled to point out that my compiler background most likely affects my judgement here. I'd like to hear what other people think about it.

52

Fair enough. :wink: I am also very much influenced by my formal methods background, and the fact that I do not know of a single model that would justify this optimization (as in, something that would let you prove this optimization correct). OTOH, I would think that losing this optimization would not be too bad either, because after all, hardly ever do functions turn the address of a local into an integer.

Well, I suppose you could try to argue that the integer has not been leaked to anyone, so we can just make it different by adapting the layout of the stack frame accordingly -- but then you'd have to actually make sure that is the case, which compilers also do not do. Funny enough, they do not optimize away the equality test, but still assume it fails as far as aliasing is concerned: Compiler Explorer. I am not even sure that there is a clause in the C standard which permits this...

53

Hm, turning it into an integer does not seem necessary here. (It may be necessary to confuse the formal models you're referring to, though.) In particular, without some kind of provenance rule, I'd expect that both versions of this function are well-defined and occasionally return 42:

fn foo(p: *mut i32) -> i32 {
    let mut x: i32 = 0;
    if (&mut x as *mut i32) == p {
        // Version 1
        unsafe { *p = 42; }
        // Version 2
        unsafe { x = 42; }
    }
    x
}

(edit: fixed mutability)

I want version 1 to optimized to return 0 (and not access memory) as the C equivalent would be, while my gut feeling about version 2 is that it should not be UB, though it definitely has unspecified behavior (may return 42 or 0, depending on optimizer details).

While the example discussed here is obviously quite artificial, the underlying idea—that you can't legitimately create a pointer to a local before the local exists—seems extremely important to have for alias analysis, because it kicks in in basically any any time you have local variables and pointer arguments. For example, without a rule to that effect a memcpy implementation (accepting raw pointers, not slices or other types with more invariants) would have to be optimized under the assumption that the source or destination of the memcpy potentially aliases local bookkeeping variables, greatly constraining the optimizer. I think it may not even be valid to store the locals in registers instead of the stack.

The definition of yp is wrong, you casted the value y instead of a pointer to it. Once you do that, the comparison is optimized out: Compiler Explorer

And indeed this optimization doesn't depend on casting any pointers to integers: Compiler Explorer

54

I should clarify that there are almost certainly other ways to justify optimizing this (e.g., noting that the address of x is never made concrete, as some formal models of C do IIUC) but my understanding is that the types-as-contract work isn't doing that, and there's no planned extension that would do it. (I also struggle to imagine a language rule that could justify this but would not fall under "provenance rule".)

As I understand it, because let mut x; is a local variable and not borrowed, we hold the lock for it for basically the entire function, and because we hold the lock, the write through p is perfectly valid, regardless of what black magic the caller may have performed to pass in the "right" pointer.

55

Sorry I haven't had time to read through this whole thread (probably won't ever :crying_cat_face:), just popping in to reply to this request.

The intended model for Unique -- which may very well be meaningless trash -- is that it should behave "as if" the pointed-to memory was actually stored inline, in the place of the pointer. Which is to say:

Vec<u32> { ptr: 0xdeadbeef, len: 3, cap: 6 }

should be treated/analyzed/optimized "as if" it was actually:

Vec<u32> { ptr: [x, y, z, uninit, uninit, uninit], len: 3, cap: 6 }

56

Pointers that are never casted to integers or otherwise subject to operations that can leak their integer value (like potentially overflowing arithmetic) can typically be handled as "abstract pointers" (the way miri currently handles all pointers). Abstract pointers are unforgeable and hence a new allocation (like this fresh stack slot) is guaranteed to be at an abstract pointer that is not already existing anywhere in the program. So, I can see a formal model that justifies this optimization if the ptr is never casted to an integer.

Notice that this does not violate the principle that my two snippets A and B should always be equivalent: When testing for pointer equality, abstract pointers are not equal to any integer.

Hm, now that I think about this in more detail, there is actually something subtle going on here -- the model as I have been implicitly using it here has the interesting quirk that equality is not stable. The pointers can compare inequal while one of them is still abstract, but then once the abstract pointer is casted to an integer and becomes "concrete" (this is the intptrcast model), it would actually compare equal if the right integer was picked. Once again, pointer equality strikes back...

Notice that I do not see any fundamental difference here between locals and fresh allocations obtained via malloc. Indeed malloc is marked as noalias, which I assume also has the effect that its address is not pre-guessable?

Every model I can think of gives you this property for locals that never have their address taken. If the address is ever taken, things become interesting. This is entirely unrelated to Rust's fancy types or restrict/noalias -- it is just about reconciling integer-pointer-casts with freshness guarantees for new allocations with pointer equality tests.

Ah, nice catch. :smiley:

Casting pointer to integers makes optimizations harder, so this is not surprising.

Types-as-contracts is orthogonal to the underlying memory model and pointer representation. The current implementation in miri represents pointers to valid allocations abstractly (as pairs of an "allocation ID" and an offset), which provides only extremely limited support for arithmetic on pointers casted to integers. This combination leads the optimization you are asking for, in all versions we have considered.

There are plans to change miri to use the intptrcast model instead, providing full support for arithmetic on integers obtained from pointers. This combination disallows the optimization in the version where the pointer to the local has been casted to an integer. For the version where the address is taken and compared, we can either tune the model to allow the optimization (at the cost of making pointer equality tests unstable), or to not allow it (but having stable pointer equality -- in this variant, comparing an abstract pointer to an integer would "concretize" that pointer with all the same effects as casting it to an integer). In this last version (intptrcast with stable ptr equality), if the address of the local is taken but never compared to anything else, the optimization would still be permitted. In terms of the state of the art of formal models for C-like languages, that currently seems to be the best we have.

Notice that while this discussion about formal models justifying optimizations sounds fairly academic, I still think it is important. In particular, I am not yet convinced that there even exists a formal semantics that provides full integer-pointer-arithmetic while also providing the freshness guarantees you are asking for (i.e., permitting the optimization even if the pointers are casted to an integer). It could well be that it is impossible to reconcile these two features, making any semantics that claims to have them both inconsistent. (It wouldn't be the first time that happens -- the first version of Java's memory model for concurrency was inconsistent in the sense that the conjunction of all their axioms implies false. Unfortunately, I cannot find a source for this right now.)

1 Like
57

Thanks for popping in. :slight_smile: I have not previously seen it described like that.

Of course, this means the "meaning" of Unique in RawVec magically depends on the two adjacent integer values. That seems... rather specifically hard-coded for this one case. Wasn't Unique supposed to be more generally useful?

58

That sounds hard to implement with LLVM. First, LLVM's optimizer reduces inttoptr(ptrtoint(ptr_in)) to ptr_in. Second, it assumes alloca-ed pointers do not equal any other pointers, without any special metadata provided by the frontend (so rustc can't easily override this assumption).

Concretely, this IR:

define i1 @test(i64 %compare_int) {
  %allocaed = alloca i32
  %allocaed_as_int = ptrtoint i32* %allocaed to i64
  %allocaed_as_ptr_again = inttoptr i64 %allocaed_as_int to i32*
  %compare_ptr = inttoptr i64 %compare_int to i32*
  %out = icmp eq i32* %allocaed_as_ptr_again, %compare_ptr
  ret i1 %out
}

optimizes to:

define i1 @test(i64 %compare_int) local_unnamed_addr #0 {
  ret i1 false
}

I suppose rustc could have pointer-to-integer conversions pass the pointer through an opaque-to-LLVM identity function, but that sounds quite unfortunate from an optimization perspective.

Edit: And that wouldn't even be enough, because you can do ptr-to-int via 'back door' by memcpying the bytes of the pointer.

1 Like
59

It's a specification that's only intended for optimizers (which don't need to know the bounds of an allocation, and may forget what is or isn't initialized), and not the verifiers you're pursuing. All that matters is it knows that the ptr doesn't point to another field of the Vec, or another local variable.

60

Yeah, the trouble is that the function could have all sorts of other side-effects and hence is hard to reorder. OTOH, ptr-int-casts are effectful in the intptrcast model as they make addresses guessable.

On first reading, I somehow missed the significance of this. Since optimization may not change program behavior, I would translate what you are saying to the formal world by saying that the pointer comparison is non-deterministic -- it can either return true or false. This gives the optimizer the option to fix the behavior either way, or to leave it to where the stack frame happens to be put. That's interesting because pointer comparison in Rust is already non-deterministic on other cases. For example. when you turn a Box into a raw ptr and drop it, and then create a new box, and compare the two box's addresses.

At least, I would think that the optimizer is allowed to claim that these two pointers compare inequal, and I am pretty sure I saw it optimizing based on that, but now I can't get it do do that... I can make it reorder loads and stores, or short-circuit loads, but not change comparisons: Rust Playground. Clang is happy to do similar optimizations: Compiler Explorer

So, if the model would make comparison of abstract pointers and concrete pointers non-deterministic rather than either forcing "concretization" or always making them unequal, that would also permit the optimization (if the ptr is never casted to an integer). However, either way, non-deterministic pointer comparison could result in the same two pointers first comparing unequal and later comparing equal, or vice versa.