On Mon, 2024-01-08 at 11:51 -0800, Yonghong Song wrote: [...] > > In case if check_stack_read_var_off() would be modified to check not > > only for STACK_ZERO, but also for zero spills, I think that all such > > spills would have to be marked precise at the time of read, > > as backtracking would not be able to find those later. > > I don't understand the above. If the code pattern looks like > r1 = ...; /* r1 range [-32, -16); > *(u8 *)(r10 + r1) = r2; > ... > r3 = *(u8 *)(r10 + r1); > r3 needs to be marked as precise. > > Conservatively marking r2 in '*(u8 *)(r10 + r1) = r2' as precise > should be the correct way to do. > > Or you are thinking even more complex code pattern like > *(u64 *)(r10 - 32) = r4; > *(u64 *)(r10 - 24) = r5; > ... > r1 = ...; /* r1 range [-32, -16) */ > r3 = *(u8 *)(r10 + r1); > r3 needs to be marked as precise. > > In this case, we should proactively mark r4 and r5 as precise. > But currently we did not do it, right? Yes, I'm thinking about the latter scenario. There would be zero spills for fp-32 and fp-24. If check_stack_read_var_off() is modified to handle zero spills, then it would conclude that r3 is zero. But if r3 is later marked precise, there would be no info for backtracking to mark fp-32, fp-24, r4, r5 as precise: - either backtracking info would have to be supplemented with a list of stack locations that were spilled zeros at time of check_stack_read_var_off(); - or check_stack_read_var_off() would need to conservatively mark all spilled zeros as precise. Nothing like that is needed now, because check_stack_read_var_off() would return unbound scalar for r3 upon seeing zero spill. > I think this later case is a very unlikely case. But it is possible and verifier has to be conservative.
