Skip to content

Are raw pointers fully equivalent to the place they are created from? #591

@RalfJung

Description

@RalfJung

In Tree Borrows, &raw const/mut expressions don't do anything -- the raw pointer created by this expression just has whatever tag the place they point to has. This makes code like the following legal:

let mut a = 0;
let ptr = &raw mut a;
a = 1;
*ptr = 2;

*ptr and a are allowed to freely alias.

I think this best reflects programmer expectations. In the early days of Stacked Borrows, this came up as a surprise for multiple people, and one c2rust translation tool had to change the code they generate to deal with this. This also simplifies the model since we no longer have to (somewhat awkwardly) identify when a raw pointer is created from a "safe" place (reference/local/Box), and only retag those. This is in contrast to references which we can just always retag no matter where we encounter them.

This somewhat relates to the following questions:

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-SB-vs-TBTopic: Design questions where SB and TB are opposite sides of the design axisA-aliasing-modelTopic: Related to the aliasing model (e.g. Stacked/Tree Borrows)

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions