Struct vstd::simple_pptr::PPtr

PPtr (which stands for “permissioned pointer”) is a wrapper around a raw pointer to a heap-allocated V. This is designed to be simpler to use that Verus’s more general pointer support, but also to serve as a better introductory point. Historically, PPtr was positioned as a “trusted primitive” of Verus, but now, it is implemented and verified from the more general pointer support, which operates on similar principles, but which is much precise to Rust’s pointer semantics.

A PPtr is equvialent to its usize-based address. The type paramter V technically doesn’t matter, and you can freely convert between PPtr<V> and PPtr<W> by casting to and from the usize address. What really matters is the type paramter of the PointsTo<V>.

In order to access (read or write) the value behind the pointer, the user needs a special ghost permission token, PointsTo<V>. This object is tracked, which means that it is “only a proof construct” that does not appear in compiled code, but its uses are checked by the borrow-checker. This ensures memory safety, data-race-freedom, prohibits use-after-free, etc.

PointsTo objects.

The PointsTo object represents both the ability to access (read or write) the data behind the pointer and the ability to free it (return it to the memory allocator).

The perm: PointsTo<V> object tracks two pieces of data:

• perm.pptr() is the pointer that the permission is associated to.
• perm.mem_contents() is the memory contents, which is one of either:
  • MemContents::Uninit if the memory pointed-to by by the pointer is uninitialized.
  • MemContents::Init(v) if the memory points-to the the value v.

Your access to the PointsTo object determines what operations you can safely perform with the pointer:

• You can read from the pointer as long as you have read access to the PointsTo object, e.g., &PointsTo<V>.
• You can write to the pointer as long as you have mutable access to the PointsTo object, e.g., &mut PointsTo<V>
• You can call free to deallocate the memory as long as you have full onwership of the PointsTo object (i.e., the ability to move it).

For those familiar with separation logic, the PointsTo object plays a role similar to that of the “points-to” operator, ptr ↦ value.

Example

fn main() {
    unsafe {
        // ALLOCATE
        // p: PPtr<u64>, points_to: PointsTo<u64>
        let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();

        assert(points_to.mem_contents() === MemContents::Uninit);
        assert(points_to.pptr() == p);

        // unsafe { *p = 5; }
        p.write(Tracked(&mut points_to), 5);

        assert(points_to.mem_contents() === MemContents::Init(5));
        assert(points_to.pptr() == p);

        // let x = unsafe { *p };
        let x = p.read(Tracked(&points_to));

        assert(x == 5);

        // DEALLOCATE
        let y = p.into_inner(Tracked(points_to));

        assert(y == 5);
    }
}

Examples of incorrect usage

The following code has a use-after-free bug, and it is rejected by Verus because it fails to satisfy Rust’s ownership-checker.

fn main() {
    unsafe {
        // ALLOCATE
        // p: PPtr<u64>, points_to: PointsTo<u64>
        let (p, Tracked(mut points_to)) = PPtr::<u64>::empty();

        // unsafe { *p = 5; }
        p.write(Tracked(&mut points_to), 5);

        // let x = unsafe { *p };
        let x = p.read(Tracked(&points_to));

        // DEALLOCATE
        p.free(Tracked(points_to));                 // `points_to` is moved here

        // READ-AFTER-FREE
        let x2 = p.read(Tracked(&mut points_to));   // so it can't be used here
    }
}

The following doesn’t violate Rust’s ownership-checking, but it “mixes up” the PointsTo objects, attempting to use the wrong PointsTo for the given pointer. This violates the precondition on p.read().

fn main() {
    unsafe {
        // ALLOCATE p
        let (p, Tracked(mut perm_p)) = PPtr::<u64>::empty();

        // ALLOCATE q
        let (q, Tracked(mut perm_q)) = PPtr::<u64>::empty();

        // DEALLOCATE p
        p.free(Tracked(perm_p));

        // READ-AFTER-FREE (read from p, try to use q's permission object)
        let x = p.read(Tracked(&mut perm_q));
    }
}

Differences from PCell.

PPtr is similar to cell::PCell, but has a few key differences:

• In PCell<V>, the type V is placed internally to the PCell, whereas with PPtr, the type V is placed at some location on the heap.
• Since PPtr is just a pointer (represented by an integer), it can be Copy.
• The ptr::PointsTo token represents not just the permission to read/write the contents, but also to deallocate.

Simplifications relative to more general pointer API

• Pointers are only represented by addresses and don’t have a general notion of provenance
• Pointers are untyped (only PointsTo is typed).
• The PointsTo also encapsulates the permission to free a pointer.
• PointsTo tokens are non-fungible. They can’t be broken up or made variable-sized.