fix(rt): handle SingletonArray+Field(0)+ConstantIndex(0) in traversal#988
fix(rt): handle SingletonArray+Field(0)+ConstantIndex(0) in traversal#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".
ca049dd to
d232a5f
Compare
…napshot Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
d232a5f to
72cb233
Compare
b057a45 to
490d167
Compare
Add a traversal rule that eliminates the three-element projection chain SingletonArray+Field(0)+ConstantIndex(0) on single-element Aggregates, reducing it to just Field(0). This pattern arises from pointer casts like `*const Pubkey as *mut [u8; 32]` in write_volatile calls. The three projections together mean "treat the struct as a one-element array, take field 0, index element 0" which is equivalent to just "take field 0". Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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.
Fixes stuck execution in
std::ptr::write_volatile::<[u8; 32]>caused by unhandledprojectionElemSingletonArrayin#traverseProjection.The pointer cast
*const Pubkey as *mut [u8; 32]produces the projection chainSingletonArray + Field(0) + ConstantIndex(0). This is semantically equivalent to justField(0), so a single traversal rule cancels the triplet on single-element Aggregates.