On Fri, 2026-08-14 at 16:19 -0700, Vineet Gupta wrote: > The verifier's linked-scalar machinery tracks register equality only for the > full 64 bits (optionally with a constant delta). There is no way to record > "these two registers share just their low 32 bits", so a 32-bit mov from a > source with unknown high bits has to drop the relationship entirely, and a > later narrowing of the source never reaches the destination: > > > r6 = ... /* full 64-bit unknown */ > > w7 = w6 /* 32-bit zero-extending mov */ > > if w6 != 0 goto .Lxx /* not taken: r6's low 32 bits are 0 */ > > if w7 == 0 goto .Lok <-- not deduced today > > The same gap exists for the 32-bit sign extension and was the > motivation for this patchset. > > > 0: (61) r2 = *(u32 *)(r1 +24) > > 1: (bf) r0 = (s32)r2 > > 2: (56) if w2 != 0x0 goto pc+10 ; R2=0 (branch taken) > > ... > > 12: (95) exit
Note that ldx instructions have similar structure: one can either zero or sign extend on 32-bit load. I think this series should be expanded to cover these cases. Also, please drop RFC tag when submitting v2.
