Types as Contracts: Implementation and Evaluation


#1

Some weeks ago, I described Types as Contracts as an approach for how to go about defining Rust’s aliasing-related undefined behavior. One key property of this approach is that it is executable, which means we can actually have a program (in this case, miri) tell us whether some particular Rust test case exhibits undefined behavior or not. I have since then spent most of my time completing and refining this implementation, and running it on miri’s test suite to exercise various bits of the standard library and see whether they are actually following the rules I have been suggesting.

This post is my report on what I found, and how the approach itself changed in response to these findings. It also explains how you can run miri yourself and have it check your code for undefined behavior according to this model. Finally, I discuss some of the things that I would like to look at going forward.

https://www.ralfj.de/blog/2017/08/11/types-as-contracts-evaluation.html


#2

Regarding the Arc::drop case, would it be legal in your model if the self.inner().weak was replaced by some unsafe pointer arithmetic that fetched the weak field without any intermediate partially invalid ArcInner value? (i.e., would removing the type also “remove the contract” that’s being violated?)


#3

Yes. Notice however that the call to Layout::for_value would still be UB and also needs to be fixed. Also, there is no need for literally using pointer arithmetic. I think the following should work (and I should really test that…):

    unsafe fn drop_slow(&mut self) {
        let old_weak = self.inner().weak.fetch_sub(1, Release);

        let ptr = self.ptr.as_ptr();
        let layout = Layout::for_value(&*ptr);

        // Destroy the data at this time, even though we may not free the box
        // allocation itself (there may still be weak pointers lying around).
        ptr::drop_in_place(&mut self.ptr.as_mut().data);

        if old_weak == 1 {
            atomic::fence(Acquire);
            Heap.dealloc(ptr as *mut u8, layout)
        }
    }

Note that this computes the layout even when that is not needed. But we are talking about a one-time cost per Arc, this is probably not significant (and would be fixed at the expense of some code duplication).

I think reordering the fetch_sub up to the beginning of the function is okay, but if it is not, this should also work:

    unsafe fn drop_slow(&mut self) {
        let ptr = self.ptr.as_ptr();

        let layout = Layout::for_value(&*ptr);

        // Destroy the data at this time, even though we may not free the box
        // allocation itself (there may still be weak pointers lying around).
        ptr::drop_in_place(&mut (*ptr).data);
        // We must not use the type &(mut) ArcInner from now on, because that
        //  type is actually no longer valid.

        if (*ptr).weak.fetch_sub(1, Release) == 1 {
            atomic::fence(Acquire);
            Heap.dealloc(ptr as *mut u8, layout)
        }
    }

I actually think not obtaining a pointer to the inner part three times makes the code overall more readable.


#4

I confirmed that the second version I presented above (now also shown in the post itself) indeed makes validation go through just fine – of course, this makes use of the “validation is relaxed around unsafe blocks” mode.


#5

Status update: I finally got around to implement a fix for the problem with suspended write locks hat I have been alluding to earlier. This made a bunch of additional test cases work in miri. Also, there’s an RFC on the way that will fix the problems I have been having around mem::uninitialized.

The only unexpected failure currently is that tests that panic trigger a validation error; I still have to investigate that problem.


#6

In implementing more validation for miri (namely, ruling out uninitialized data to be passed around at types like u8), I found at least one other contract violation in the standard library. Vec::extend can end up running the following code:

    fn spec_extend(&mut self, iterator: slice::Iter<'a, T>) {
        let slice = iterator.as_slice();
        self.reserve(slice.len());
        unsafe {
            let len = self.len();
            self.set_len(len + slice.len());
            self.get_unchecked_mut(len..).copy_from_slice(slice); // <-
        }
    }

The interesting line here is the get_unchecked_mut, which creates a slice covering uninitialized data. So this ends up calling copy_from_slice (a safe, public function) with a self argument that is not a valid reference to initialized data. T here can be arbitrary. Imagine T being an enum, then this would pass around (references to) data with an uninitialized discriminant.

None of the exceptions (concerning unsafe code, or private fields) that have been suggested so far would make this legal, nor does there seem to be a good way to fix this locally.


#7

It seems that you would want to have a function in std::slice, such as uninitialized_copy_from_slice:

pub unsafe fn uninitialized_copy_from_slice<'a, T>(p: *const T, len: usize, src: &[T]) -> &'a [T] {
    assert!(len == src.len(),
                "destination and source slices have different lengths");
    ptr::copy_nonoverlapping(src.as_ptr(), p, len);
    from_raw_parts(p, len)
}

This would then allow:

    fn spec_extend(&mut self, iterator: slice::Iter<'a, T>) {
        let slice = iterator.as_slice();
        self.reserve(slice.len());
        let len = self.len();
        unsafe {
            uninitialized_copy_from_slice(self.as_mut_ptr().offset(len as isize), slice.len(), slice);
            self.set_len(len + slice.len());
        }
    }

This actually does the same operations as it does currently but without ever forming a slice with uninitialized data. Note, setting the length after the data is initialized prevents the Vec from perceiving itself as having uninitialized data as well.


#8

@ahmedcharles There is no need for uninitialized_copy_from_slice to return anything then, and indeed spec_extend could just as well call copy_nonoverlapping directly. So it seems I was wrong, there is a good way to fix this locally. That’s great.

However, the really interesting question is: We now have at least two cases where programmers considered it fine to pass around uninitialized data behind a reference type, given that they knew that the code that is called here is actually able to cope with uninitialized data. IOW, the functions that were called Layout::for_value and copy_from_slice are “super-safe” in that they are safe to call with certain “bad” values. Given that, is it reasonable to eventually rule out this pattern in the future and always require uninitialized data to live behind a MaybeUninitialized (or a raw pointer) when crossing function boundaries? Or will that break too much existing code?


#9

From my POV from unsafe code guidelines project: I made references to uninitialized data defined behavior because that seemed like a fairly popular pattern, and it didn’t break the compiler as badly as directly uninitialized data. The compiler “crawling” through references deeply to cause UB seemed to be a very surprising behavior.


#10

I made references to uninitialized data defined behavior because that seemed like a fairly popular pattern, and it didn’t break the compiler as badly as directly uninitialized data. The compiler “crawling” through references deeply to cause UB seemed to be a very surprising behavior.

I can see that. For consistency, then, this shouldn’t be restricted to uninitialized data – passing a &bool to an out-of-range value, or an &&i32 where the inner reference is 0, should also not be “insta-UB” when crossing function boundaries, but only become UB at some later stage after the reference has been dereferenced.

What exactly that later stage is I suppose remains open; this then becomes one of these old discussions.


#11

The point of suggesting uninitialized_copy_from_slice is to create helper functions for dealing with uninitialized data, much like similar functions in the C++ STL. The reason it returns a slice is because algorithms should return information rather than throw it away and this function knows that the slice is initialized, so it’s in the best position to call from_raw_parts correctly.

And my preference would be to explicitly treat uninitialized data and have functions which help with common ways of initializing that data. One of the things I like about Rust is that safe references are always valid. I wouldn’t want to lose that.


#12

Right. Uninitialized data is just one kind of invalid data.


#13

Well, I think we all want to uphold the rule that they are properly aligned and point to allocated storage. But there’s a problem with enforcing things “behind the reference” to be initialized. After fixing extend_with, I now hit fmt::Display:

            let mut buf: [u8; 39] = unsafe { mem::uninitialized() };
            let mut curr = buf.len() as isize;
            let buf_ptr = buf.as_mut_ptr();

The call to len() is fixed easy enough by using a const LEN : usize = 39;, but buf_ptr is… more interesting.


@arielb1: One problem with not going “below” references is the interaction with other guarantees, e.g. shared references being read-only. Consider a function like

fn foo(x: &Result<Cell<i32>, i32>) {
  // ...
}

(I am using Result here just as a general sum type.) Assuming a 4-byte discriminant, the question now is: Does foo have a “lock” on the memory range [x+4, x+8[ or not? My model will just read the enum discriminant to determine whether the second half of *x is covered by an UnsafeCell or not. However, if we do not descend through references, then we cannot tell whether there is an UnsafeCell or not. What are your thoughts on this?


#14

Given that arrays are built in, it seems like the semantics of an uninitialized array should be that the content of the array is uninitialized but the address and length are valid (they can’t change anyways). So, why would the code, as written, be problematic? The uninitialized data doesn’t apply to the address or size of the array, only the data.

And what’s the problem with enforcing things behind a reference being valid? You can certainly check for it, even if it’s expensive. (On second thought, I see the point. In many cases you have to form a reference to something that’s uninitialized in order to initialize it. Though, that would only require &mut, since & alone can’t be used to initialize it. And obviously, arrays have to be special cased.)


#15

I’m beginning to realize that having write only references would be really nice. You could have functions like fn reset(&write self) which only write to the value. Obviously, some functions that do a ‘reset’ operation need to read and write, but then you could distinguish which ones require reading first. Note, you could have &write mean that any member needs to be written before being read, rather than requiring that it can only be written.


#16

The RMM model was “aliasing-based” - it only ever “locked” on an access, so it did not encounter that particular problem (as UnsafeCell is not Copy, not even when copying a complex structure).

However, I see why a validation-based model would encounter this problem. But it’s the “reference to garbage” problem from before. Maybe it’s interesting enough to lock down.


#17

Is the slice case different than the reference case? I thought there were quite a few “out of bounds” .get_unchecked_mut(i) for single indices i in the Vec code. There is for example one here, in a different extend function:

    fn extend_desugared<I: Iterator<Item = T>>(&mut self, mut iterator: I) {
        // This is the case for a general iterator.
        //
        // This function should be the moral equivalent of:
        //
        //      for item in iterator {
        //          self.push(item);
        //      }
        while let Some(element) = iterator.next() {
            let len = self.len();
            if len == self.capacity() {
                let (lower, _) = iterator.size_hint();
                self.reserve(lower.saturating_add(1));
            }
            unsafe {
                ptr::write(self.get_unchecked_mut(len), element);
                // NB can't overflow since we would have had to alloc the address space
                self.set_len(len + 1);
            }
        }
    }

#18

For exactly the same reason that extend_with was problematic – it passes &T to another function where T is not initialized. len and as_mut_ptr as both just methods that take &self and &mut self respectively.

Ah, that’s a good point. We could in principle require data behind & to be initialized and recursively follow shared references (which would also solve thenUnsafeCell problem above), but permit uninitialized data behind &mut and only do shallow validation of mutable references.

However, that would probably we a fairly surprising asymmetry.


Right. However, I think it would be preferrable to hold locks even for un-accessed data, at least under some circumstances.

However, it could well be Copy, and I think we should have a model compatible with that. There is no reason besides ergonomics for Cell not to be Copy.


No, not fundamentally. It is just another example. Thanks for adding yet another one!


#19

That’s my point, have the compiler treat len and as_mut_ptr on arrays as being special. No other type in the language has the same properties as arrays in this regard, by definition, so why wouldn’t treating them specially be ok?

Reading from a &mut would still require a deep check. It’s just that the check wouldn’t happen at function boundaries, but instead, happen at the location of the read operation. Normal &'s can be checked at the function boundary. So, there isn’t an asymmetry, they just get treated differently because they are different.


#20

I don’t think that’s a good idea – this looks fairly arbitrary to me. Many functions are fine to be called with some of their references being uninitialized, so I don’t see these two as being special in any way.