Skip to content

Stacked Borrows: track raw pointers more precisely #248

Closed
@RalfJung

Description

@RalfJung

Currently, Stacked Borrows teats all raw pointers as identical -- if any raw pointer is allowed to access some memory, then all are. This does not reflect LLVM's pointer treatment though, and it leads to confusing behavior (e.g. rust-lang/miri#1526).

I have long planned to make tracking more precise, but there's a big open question in how to handle integer-pointer casts. We cannot (and do not want to) track integers, so we have to somehow mark memory as "integer-available" when casting to int, and then use that when casting back from an int.

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-aliasing-modelTopic: Related to the aliasing model (e.g. Stacked/Tree Borrows)C-open-questionCategory: An open question that we should revisit

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions