On Tue, Nov 01, 2022 at 11:22:16PM -0700, Andrii Nakryiko wrote: > When processing ALU/ALU64 operations (apart from BPF_MOV, which is > handled correctly already; and BPF_NEG and BPF_END are special and don't > have source register), if destination register is already marked > precise, this causes problem with potentially missing precision tracking > for the source register. E.g., when we have r1 >>= r5 and r1 is marked > precise, but r5 isn't, this will lead to r5 staying as imprecise. This > is due to the precision backtracking logic stopping early when it sees > r1 is already marked precise. If r1 wasn't precise, we'd keep > backtracking and would add r5 to the set of registers that need to be > marked precise. So there is a discrepancy here which can lead to invalid > and incompatible states matched due to lack of precision marking on r5. > If r1 wasn't precise, precision backtracking would correctly mark both > r1 and r5 as precise. > > This is simple to fix, luckily. If destination register is already > precise, we need to propagate precision to source register (if it is > SCALAR). This is similar to `reg += scalar` handling case, so nothing > conceptually new here. Could you rephrase the above paragraph to make it clear that the fix is not in backtracking logic, but in nomral forward simulating part of the verifier. After reading the 1st paragraph it sounds that backtracking is wrong, but it's the normal pass that is missing precisions propagation. Also instead of "similar to `reg += scalar`" could you explicitly mention that pointer += scalar and scalar += pointer correctly propagate precisions of scalars. It's the scalar += scalar case that was incomplete. Other than that it's a great fix!
