fix(types): make #pointeeProjection confluent with source-first unwrapping strategy#988
fix(types): make #pointeeProjection confluent with source-first unwrapping strategy#988
Conversation
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: beef218f11
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
d232a5f to
72cb233
Compare
490d167 to
9afd294
Compare
dkcumming
left a comment
There was a problem hiding this comment.
This feels like it is addressing the symptom of a problem and not the problem itself. The description given does not fill me with much confidence that the problem is being accurately understood or addressed. It feels to me the problem is the projection chain is being built incorrect, and this dismisses a particular bad projection chain. But really we want to construct correct projection chains so everything is fixed for the general case and not this particular instance of a bad chain.
I tried looking the example you provided but it adds a lot of noise, I think something like this is much better to analyse and has the same problem and everything goes wrong within the first basic block:
struct Wrapper([u8; 2]);
fn main() {
let w = Wrapper([11, 22]);
let arr: [u8; 2] = unsafe { *((&w) as *const Wrapper as *const [u8; 2]) };
assert_eq!(arr, [11, 22]);
}
This proof gets stuck on Node 72 (Statement: _3 <- Use(cp((*_4)))) with stuck state:
#traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ListItem (Integer ( 11 , 8 , false ))
ListItem (Integer ( 22 , 8 , false ))
))
) , projectionElemSingletonArray projectionElemField ( fieldIdx ( 0 ) , ty ( 80 ) ) projectionElemConstantIndex ( ... offset: 0 , minLength: 0 , fromEnd: false ) .ProjectionElems , .Contexts )
Which shows there is projectionElemSingletonArray then projectionElemField(0, ...) then projectionElemConstantIndex(0, ...). The first thing that comes to mind is the rules @jberthold added that should cancel the projections out types.md:65-67, but they don't apply when the projectionElemField is intersected.
// special cancellation rules with higher priority
rule maybeConcatProj(projectionElemSingletonArray, projectionElemConstantIndex(0, 0, false) REST:ProjectionElems) => REST [priority(40)]
rule maybeConcatProj(projectionElemConstantIndex(0, 0, false), projectionElemSingletonArray REST:ProjectionElems) => REST [priority(40)]
So is that field projection the problem, or are the array projections the problem? The projections are first introduced at Node 64 (Statement: _4 <- Cast-PtrToPtr mv(5)) which is the result of casting ty(81)/*const Wrapper to ty(76)/*const [u8; 2]:
#cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , castKindPtrToPtr , ty ( 81 ) , ty ( 76 ) )
giving:
PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: projectionElemSingletonArray projectionElemField ( fieldIdx ( 0 ) , ty ( 80 ) ) projectionElemConstantIndex ( ... offset: 0 , minLength: 0 , fromEnd: false ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 2 ) , 0 , noMetadataSize ) )
So this looks wrong, it shouldn't have these array projections, just the field access.
This projection chain is built from data.md:1458,1469 which appends projections by #typeProjection. If you follow the logic through, what you find is that #pointeeProjection for typeInfoArrayType is being matched:
rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2)
=> maybeConcatProj(
projectionElemConstantIndex(0, 0, false),
#pointeeProjection(lookupTy(TY1), TY2)
)
rule #pointeeProjection(TY1, typeInfoArrayType(TY2, _))
=> maybeConcatProj(
projectionElemSingletonArray,
#pointeeProjection(TY1, lookupTy(TY2))
)
The comment and the PR that introduces the rule #936 would indicate this is for casts of the form T -> [T; N] or [T; N] -> T, however there is no appropriate guard on the rule, or restriction for the rule to only match for casts of that case. The approach to solve this is to choose an appropriate guard (no easy I imagine because the guard will rely on context that the casts is of the form T -> [T; N] or [T; N] -> T. So problem the flow of rules needs to change.
As hacky tests I added [priority(55)] on the rules, and tried a contrived restrictive guard. Both approaches resulted in the minimised test passing, with node 64 only having the projectionFieldElem(0, ...) as expected:
PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 80 ) ) .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 2 ) , 0 , noMetadataSize ) )
I personally would change the test to be the minimised one I provided, but that is not strictly necessary. However I think any rule being suggested to solve this issue should be argued with thorough evidence that they are addressing the problem and not a symptom of the problem.
Demonstrates stuck #traverseProjection caused by incorrect projection chain SingletonArray+Field(0)+ConstantIndex(0) from #pointeeProjection when casting *const Wrapper to *const [u8; 2]. Minimal reproducer from @dkcumming's review comment on PR #988.
9afd294 to
deb736c
Compare
Demonstrates stuck #traverseProjection caused by incorrect projection chain SingletonArray+Field(0)+ConstantIndex(0) from #pointeeProjection when casting *const Wrapper to *const [u8; 2]. Minimal reproducer from @dkcumming's review comment on PR #988.
This fixes ptr-cast-wrapper-to-array by ensuring struct unwrapping takes precedence over array unwrapping. However, it REGRESSES iter_next_2 (renamed to iter_next_2-fail) because that test needs the opposite priority (array first for [Thing;3] → Thing). This commit demonstrates why priority alone cannot fix the non-deterministic overlap — the two cases need conflicting priorities.
deb736c to
18334d1
Compare
Revert the priority approach (which regressed iter_next_2) and instead refactor #pointeeProjection to always unwrap the source type first. Target-side unwrapping is deferred to #pointeeProjectionTarget, only reached when source cannot be unwrapped further. This eliminates the non-deterministic overlap because a type cannot be both a struct and an array simultaneously. Both ptr-cast-wrapper-to-array and iter_next_2 now pass.
18334d1 to
aeefea2
Compare
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: aeefea2a3b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
The proof now passes with just #EndProgram, no interesting show output.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0877ae1791
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
The reverse cast *const [u8; 2] → *const Wrapper([u8; 2]) gets stuck on both master and with the source-first strategy. This is a pre-existing limitation of #pointeeProjection: source-first unwraps the array before considering the target struct, producing an uncancelable SingletonArray in the projection chain.
When source is an array and target is a transparent struct wrapping that same array type (e.g., *const [u8;2] → *const Wrapper([u8;2])), the source-first strategy incorrectly unwraps the array first, producing an uncancelable SingletonArray in the projection chain. Add a prioritized rule that detects this case (lookupTy(FIELD) ==K SRC) and directly produces WrapStruct, deferring to target-side wrapping. The expected output for ptr-cast-array-to-wrapper-fail now shows node 7 reaching #EndProgram (was previously stuck on #traverseProjection). The test still fails overall due to an unrelated alignment assertion on the other proof branch.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c22c881c74
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Summary
#pointeeProjection[priority(45)]alone doesn't work (it fixes one case but regresses the other)#pointeeProjectionTargetWrapper([u8; 2])cast)Test plan
ptr-cast-wrapper-to-arraypasses (new reproducer)iter_next_2still passes (regression test for opposite overlap:[Thing;3] → Thing)