Track lifetimes of type parameters as lifetime projections by rgwohlbold · Pull Request #195 · prusti/pcg

rgwohlbold · 2026-11-02T17:04:27Z

This PR adds tracking of lifetimes of type parameters as lifetime projections. Take the following example:

fn take<T>(v: &mut Vec<T>) -> T { ... }

fn f<T>(mut v: Vec<T>) -> T {
    take(&mut v)
}

Callers of f may substitute T with a type containing regions, e.g. &'a mut i32. We would like to track these (unknown) regions through the generalized lifetime RegionsIn(T) in the body of f.

The codebase already supports the right data structures with the GeneralizedLifetime type. This PR makes the following steps:

switch the (default) Kind in LifetimeProjection and a couple other structs/enums to Generalized and thread this change through the codebase
implement functions that decide when a GeneralizedLifetime outlives another one. This is the area where this PR deserves the most scrutiny

AI Usage

Claude Code was used to help with creating the PR. All the code has been manually reviewed.
Note that I am not very familiar with the codebase.

rgwohlbold · 2026-11-02T18:36:34Z

Ran the top 50 crates and the selected_crates functions with validity checks on, against this branch and main. 118/136 pass on both, 13 fail on both, and nothing fails only on main. 5 fail only on this branch, all because type parameters now have lifetime projections and hit existing bugs:

Loop abstraction creates a borrow flow edge from a lifetime projection to itself #194: rand_core (BlockRng::fill_bytes), rand (sample_efraimidis_spirakis), regex-syntax (IntervalSet::intersect)
Placeholder assertion when a raw pointer is copied while a mutable borrow through it is live #193: linked-hash-map (LinkedHashMap::get_refresh), strsim (GrowingHashmapChar::grow)

zgrannan

this is a good start and is mostly on track I think. Let me know if any of comments need claraification

Body lifetime projections and call shapes now index into the generalized lifetime list, so places of opaque types get `RegionsIn(T)` projections. Outlives and liveness checks involving `RegionsIn` conservatively answer `true`. Work in progress: test files 025, 041, 069, 163 and 174 fail (all pass on main). Prusti does not build against this yet.

A constant argument has no place, so its post-call version cannot be observed. With `RegionsIn` projections, call shapes could select such an argument as an output and hit the `todo!()` in `expect_place`.

A borrow can only be stored in a value of type `X` if its region outlives some region in `X`. Regions hidden inside an opaque type are chosen by the caller and outlive the function body, so a region flows into `RegionsIn(X)` only if it outlives some universal region, or a region written in `X`. Previously such flows were always assumed, so e.g. the result of a call taking `&mut v` kept `v` blocked although the borrow checker allows it.

The maps from call-site lifetimes to the callee's identity signature are now keyed by generalized lifetimes, so `RegionsIn` at the call site is translated like a region and decided in the signature (e.g. `RegionsIn(I)` vs `RegionsIn(I::Item)` in `collect` becomes `RegionsIn(Self)` vs `RegionsIn(B)`). This fixes 041. Known regressions: 247 and 069 now fail. 247 hits the existing special case for a returned type parameter, which also fails on main for `take::<&'static u32>(&mut v)`.

A defined call's shape now requires both that the callee's signature allows a flow and that the borrow checker allows it at the call site. The signature alone has to account for every instantiation of the callee's type parameters, so e.g. `take::<&'static i32>(&mut v)` used to get an edge from the local `&mut` borrow into the `'static` result. Fixes 069, 247 and the new test 248 (which also fails on main).

`introduce_initial_borrows` iterated over the regions of an argument's type but created projections indexed by its generalized lifetimes. For an associated type with a lifetime argument (`<T as Tr<'a>>::Out`), the region `'a` is part of `RegionsIn(..)` and has no projection of its own, so the lookup failed and the PCG panicked.

Mirrors `Place::regions` and replaces direct calls to `extract_generalized_lifetimes` on a place's type.

Find the universal regions for 'static and the function body from the borrow checker facts, and use them instead of a hardcoded vid.

Keep the signature check in `outlives` as on main to keep the diff small, and add a test where the signature alone would allow cross edges.

rgwohlbold · 2026-11-03T20:52:05Z

I removed test-files/174_linked_hashmap_refresh.rs since it fails on this branch. Fixing #193 should fix this test

rgwohlbold · 2026-11-03T21:07:08Z

I worked in the feedback, thank you very much! Most importantly, I changed the way outlives is handled for generalized lifetimes, hope it's correct now.
One incompleteness is documented in test #248 where we don't look inside opaque types, even if we could know what they resolve to

…ive`

…rusti#193)

zgrannan

Looks good! I can merge it if you aren't able to for some reason

rgwohlbold · 2026-11-05T17:03:30Z

It doesn't seem like I can merge it

zgrannan requested changes Nov 2, 2026

View reviewed changes

rgwohlbold added 21 commits November 3, 2026 15:31

Skip call outputs on constant arguments

07af8b0

A constant argument has no place, so its post-call version cannot be observed. With `RegionsIn` projections, call shapes could select such an argument as an output and hit the `todo!()` in `expect_place`.

Remove 174_linked_hashmap_refresh (blocked by prusti#193)

e82c5f3

Add Place::generalized_lifetimes

a56c3c4

Mirrors `Place::regions` and replaces direct calls to `extract_generalized_lifetimes` on a place's type.

Remove unused code and format

adcbda8

Rename outlives_region to signature_allows_flow

53bba1e

Do not let borrows flow between different type parameters

d0e0ff8

Compare alias types up to renumbered regions in outlives_generalized

7354832

Erase regions with a toolchain-dependent helper

4ab1e06

A region outlives RegionsIn only if it outlives 'static

b0af381

RegionsIn outlives a region only if the function body outlives it

d6866d1

Find the universal regions for 'static and the function body from the borrow checker facts, and use them instead of a hardcoded vid.

Reorganize and annotate RegionsIn tests

1755c44

Make code in is_live more concise

521773d

Check outlives at the call site inline in DefinedFnCallShapeDataSource

b54cf8c

Keep the signature check in `outlives` as on main to keep the diff small, and add a test where the signature alone would allow cross edges.

Fix formatting, clippy warnings and rustc_middle imports

68e280b

Remove unnecessary comments

ad05c27

Explain why both call-shape checks are needed and test it

2506577

rgwohlbold force-pushed the generalized-lifetime-default branch from 6f3a30d to 2506577 Compare November 3, 2026 14:34

rgwohlbold added 5 commits November 3, 2026 16:11

Use place liveness for RegionsIn in the Polonius is_live

0c1b9a4

Try to make diff smaller

f7dbcd7

Assert more edges in test #250

a8e96e7

Add alias cases and a negative edge to test #251

5114b66

Clarify comment

0e4b690

Move test #248 into the region flow test and renumber

88a7736

rgwohlbold requested a review from zgrannan November 3, 2026 21:07

rgwohlbold changed the title ~~Draft: Track lifetimes of type parameters as lifetime projections~~ Track lifetimes of type parameters as lifetime projections Nov 4, 2026

zgrannan requested changes Nov 4, 2026

View reviewed changes

rgwohlbold added 3 commits November 5, 2026 13:29

Clarify fr_static and fr_fn_body

803bdfd

Reason about places instead of locals in `PoloniusBorrowChecker::is_l…

43b27eb

…ive`

Disable linked-hash-map get_refresh selected crate test (blocked by p…

6e19a50

…rusti#193)

rgwohlbold requested a review from zgrannan November 5, 2026 14:34

zgrannan approved these changes Nov 5, 2026

View reviewed changes

rgwohlbold marked this pull request as ready for review November 5, 2026 17:02

zgrannan merged commit fa397ae into prusti:main Nov 5, 2026
24 checks passed

rgwohlbold deleted the generalized-lifetime-default branch November 5, 2026 18:34

Conversation

rgwohlbold commented Nov 2, 2026

AI Usage

Uh oh!

rgwohlbold commented Nov 2, 2026

Uh oh!

zgrannan left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

rgwohlbold commented Nov 3, 2026

Uh oh!

rgwohlbold commented Nov 3, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zgrannan left a comment

Choose a reason for hiding this comment

Uh oh!

rgwohlbold commented Nov 5, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants