Fix 5800 soundness rust aliasing

[MikaelMayer]

Fixes #5800

Description

class A {
  var x: uint8
  method Test(other: A) modifies this requires this == other {
    x := 0;
    other.x := 1;
    if this.x == 1 == other.x {
      print "ok";
    }
  }
}

used to be translated to

struct A {
  pub x: u8
}
impl A {
  fn Test(&mut self, other: &Object<A>) {
    self.x = 0;
    md!(other).x == 1;
    if self.x == 1 && 1 == rd!(other).x {
      print "ok";
    }
  }
}

but the &mut self is a long-lived mutable borrow, so anything else that could mutate "this" during the duration of this long-lived mutable borrow could end up being moved around by the compiler. Therefore, given the Dafny semantics, it's not sound to have long-term mutable borrows as Dafny references are never exclusive.
Now, the above code is rewritten to

pub use ::dafny_runtime::{Field, read_field, modify_field}

struct A {
  pub x: Field<u8>
}
impl A {
  fn Test(&self, other: &Object<A>) { // Note the abandon of the &mut because it was not sound.
    modify_field!(self.x, 0);
    modify_field!(rd!(other).x), 1); // Note the rd, we don't need md anymore
    if read_field!(self.c) == 1 && 1 == read_field!(rd!(other).x) {
      print "ok";
    }
  }
}

In short, here are the breaking fixes

• Field read is now read_field!(rd!(ref).field)
• Field mutation is now modify_field!(rd!(ref).field, value)
• Mutable fields are now wrapped with Field<_>, a type synonym of UnsafeCell
• Methods no longer accept &mut self as first parameter, only &self so that the compiler won't assume there is only one mutable borrow at a time.
• Same for trait methods

How has this been tested?

A new test (avoid_soundness_mut) that was emitting at least one "Soundness Issue" now emits "Correct" with this fix.

Considerations.

I think it's worth piggy-backing on this soundness issue to revisiting the concept of "object" with this. Indeed, it used to be that the struct was wrapped in UnsafeCell because of potential mutation, but this soundness issue demonstrated that this is not sufficient. Hence, the new type of object could be simply:

pub struct Object<T: ?Sized>(pub Option<Rc<T>>) // No more UnsafeCell
pub struct Ptr<T: ?Sized>(pub Option<NonNull<T>>) // No more UnsafeCell

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

I can't perform the change for Object and Ptr as intented, for the simple reason that these pointers are also used for arrays, and we are not changing Arrays to be arrays of UnsafeCells since it's not needed.

[ssomayyajula]

Actual changes to the ->Rust compiler are benign, trusting the field read / modify macros in the Rust runtime.