Skip to content

Add support for rawptrs#164

Merged
zgrannan merged 46 commits into
prusti:mainfrom
ThomasMayerl:rawptr
May 19, 2026
Merged

Add support for rawptrs#164
zgrannan merged 46 commits into
prusti:mainfrom
ThomasMayerl:rawptr

Conversation

@ThomasMayerl
Copy link
Copy Markdown
Contributor

This PR adds support for rawptrs by adding Delegation Edges that connect rawptrs to their derived from places when this fact is known. Applying an action to a rawptr deref degelates that PCG action to the derived from place. This PR also adds RawPtrDeref edges that work similar to normal Deref edges - just that we do not have a lifetime projection when we do not know where the rawptr was derived from.
Note: The borrow checker does not check if rawptrs can be accessed. Nor does the PCG. However, this PR should show how capabilities change for references/places once rawptrs are involved.

@ThomasMayerl ThomasMayerl requested a review from zgrannan May 6, 2026 08:59
@zgrannan
Copy link
Copy Markdown
Collaborator

zgrannan commented May 6, 2026

@ThomasMayerl The code changes themselves look reasonable, but before merging please fix the failing test. It looks like the error is: Place (**node).next projects a shared ref, but has capability E. I haven't looked at the test case, but I suspect that node is a shared reference, *node is a *mut pointer, and therefore **node has exclusive capability. If that's the case, then it may simply be a matter of refining the validity check.

Copy link
Copy Markdown
Collaborator

@zgrannan zgrannan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ThomasMayerl This mostly looks good; the capability fix is a bit of a workaround for some other underlying issue: namely, the capability for the blocked places should already be correctly set via AbsExpander.expand_to_places. However, since the workaround doesn't seem to be breaking anything, I'll leave it in for now. At some point, I'm going to revisit the loop implementation to address #162 so hopefully the underlying issue can be fixed at that time.

@zgrannan zgrannan merged commit 22a805f into prusti:main May 19, 2026
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants