Is there a way to use the stacked borrows model to make pointers just integers by keeping the provenance information in the memory rather than the pointer value, then on converting a *T to a &T checking that there is an appropriate borrow, and that the T value being pointed to all has the same provenance? This would deal with the example from the blog post:

  let mut x = false;
  let mut y = false;
  if (&x as usize + 1) == (&y as usize) {
    let z: *mut bool = (&mut x as *mut bool as usize + 1) as *mut bool;
    let z: &mut bool = unsafe { &mut *z };
    *z = true;
  }
  y // can be optimized to false

since there's an implicit freezing of y, so the unsafe block is UB since there is no "appropriate" borrow of &mut y.

Er, lots of hand-waving there about what an "appropriate" borrow is.

Provenance #52

Description

asajeffreyopenedon Nov 29, 2018

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

asajeffrey
openedon Nov 29, 2018