Pointers Are Complicated, or: What's in a Byte?

[RalfJung]

@canndrew

Does this work? It seems to match my mental model, allow a lot of safe ways of generating valid addresses while still permitting optimizations.

Wow, this gets mighty complicated. It reminds me a bit of this memory model based on symbolic values. They are using a different algebra though.

One issue I think with your algebra is IIRC, arithmetic operations like multiplication become very complex on bit patterns. You very quickly end up in a situation where you need a SAT solver to test if two elements of the algebra are equal.

I hope we can find something less complicated.

@canndrew

There is a set of memory allocations. These could refer to allocations on the heap or on the stack, whatever. An allocation consists of a base address and a type, the base address however is purely abstract - it is represented as a free variable of type usize , not as some specific value.

What do you mean by "type"? A Rust type? I strongly believe that memory should be untyped. CompCert originally had typed memory but moved away from it. LLVM has untyped memory. C... is somewhat unclear, but it does allow type punning when "done right", and C with -fno-strict-aliasing has untyped memory (I would argue).

---

@mcy

do you think there’s value in trying to write down a fictional struct or enum representation of a pointer?

I do. The one I described in the post is very simple:

pub struct Pointer {
    pub alloc_id: AllocId,
    pub offset: Size,
}