[Discussion] Abstract heap

[izgzhen]

I think we need an abstract model of heap. What is on your mind? @hermanventer

Another question to clarify is how to abstract heap pointer values, a.k.a. Box<T>. Is there another wrapper of heap-allocated object in Rust?

I checked the source and there is only pub environment: &'a mut HashTrieMap<Path, AbstractValue>.

[hermanventer]

The Path -> AbstractValue map is my current guess of what is needed to model the heap, but you are probably right to question if this is going to be sufficient.

Two big questions that still need answering are:

1. Can we ensure that no two Path values correspond to the same heap location? If not, what needs to change?
2. How often do we need to do weak updates of collections of Path values and how big do we expect environments to become? I.e. can we live with O(n) complexity for such updates or do we need additional indices?

[izgzhen]

Can we ensure that no two Path values correspond to the same heap location? If not, what needs to change?

I'm suspicious that we can't, since it is valid that some variable on stack is a reference/clone of another (i.e. two pointer value alias).

I think instead of being Path -> AbstractValue, heap should be modeled as AllocationSite -> AbstractValue. AllocationSite is the allocation site, approximating addresses of all heap cells allocated at that site. Then, we could imagine abstracting Box-typed variable as a set of AllocationSite, meaning that this variable might points to cells allocated at any of this set.

In this abstraction, it is okay for two Path corresponds to the same AllocationSite, but not two AllocationSite sharing the actual cells.

[izgzhen]

How often do we need to do weak updates of collections of Path values and how big do we expect environments to become? I.e. can we live with O(n) complexity for such updates or do we need additional indices?

I am not sure about the frequency or the amount of computation needed, only guessing that this is minimal in user code. We can optimize that anyway in future I think.

[sblackshear]

Can we ensure that no two Path values correspond to the same heap location? If not, what needs to change?

There's at least one case where this is violated: RefCell. This is an interesting construct that lets you mutate the interior of a struct via a read-only reference. Apparently the borrow checking invariants are still enforced at runtime, but I'm not sure exactly what that means.

In any case, here's a program that uses RefCell that would cause two distinct Paths to correspond to the same concrete heap location. It compiles and runs without problems.

use std::cell::RefCell;

struct MutableOnTheInside {
    f: RefCell<u64>,
}

// if s1 and s2 alias, there will be two writes to the same memory via distinct access paths
// s1.f and s2.f
fn foo(s1: &MutableOnTheInside, s2: &MutableOnTheInside) {
    s1.f.replace(2);
    s2.f.replace(3);
}

fn main() {
    let s = MutableOnTheInside { f: RefCell::new(0) };
    foo(&s, &s);
    println!("{:?}", s.f);
}

[izgzhen]

Apparently the borrow checking invariants are still enforced at runtime, but I'm not sure exactly what that means.

You will need to enforce them explicitly, e.g.

use std::cell::RefCell;

struct MutableOnTheInside {
    f: RefCell<u64>,
}

// if s1 and s2 alias, there will be two writes to the same memory via distinct access paths
// s1.f and s2.f
fn foo(s1: &MutableOnTheInside, s2: &MutableOnTheInside) {
    let bor = s1.f.borrow_mut();
    *s2.f.borrow_mut() = 2;
    *bor = 3; // panics!
}

fn main() {
    let s = MutableOnTheInside { f: RefCell::new(0) };
    foo(&s, &s);
    println!("{:?}", s.f);
}

[hermanventer]

I suspect that the only reasonable way to deal with this is to check call sites for aliasing. So, at the call foo(&s, &s) one could use the summary to detect that s1 is actually modified and therefore complain if it is also aliased.

Looking at the implementation of replace, it seems likely that things will not work well (or at all) unless replace is custom summarized. Let's see how things pan out.