On Fri, 2023-06-02 at 13:03 -0700, Alexei Starovoitov wrote: > On Fri, Jun 2, 2023 at 12:51 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > > > On Fri, 2023-06-02 at 12:43 -0700, Alexei Starovoitov wrote: > > > On Fri, Jun 2, 2023 at 12:37 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > > > > > - do a check as follows: > > > > > > if (rold->precise && rold->id && !check_ids(idmap, rold, rcur)) > > > > > > > > > > Ignoring rcur->id > 0 ? Is it safe? > > > > > > > > Well, I thought about it a bit and arrived to the following reasoning: > > > > - suppose checkpoint C exists, is proven safe and has > > > > registers r6=Pscalar(range1),id=0 and r7=Pscalar(range2),id=0 > > > > - this means that C is proven safe for any value of > > > > r6 in range1 and any value of r7 in range2 > > > > - having same id on r6 and r7 means that r6 and r7 share same value > > > > - so this is just a special case of what's already proven. > > > > > > > > But having written this down, it looks like I also need to verify > > > > that range1 and range2 overlap :( > > > > > > I'm lost. > > > id==0 means there is no relationship between regs. > > > with > > > if (rold->precise && rold->id && !check_ids(idmap, rold, rcur)) > > > > > > and r6_old->precise > > > we will only do range_within(rold, rcur) && tnum_in() check > > > and will ignore r6_cur->id and its relationship with some other reg in cur. > > > It could be ok. > > > > Yes, but I just realized that for the following case: > > > > Old Cur > > r6=Pscalar(range1),id=0 r6=Pscalar(range1),id=1 > > r7=Pscalar(range2),id=0 r7=Pscalar(range2),id=1 > > > > For 'Cur' to be a subset of 'Old' ranges range1 and range2 > > have to have non-empty overlap, so my new check: > > In theory. yes. and most likely that _was_ the case for 'old', > but 'cur' doesn't need to do that check. > 'old' was successful already and 'cur' ranges just need to be within. > > so > > > if (rold->precise && rold->id && !check_ids(idmap, rold, rcur)) > > > > is not fully correct. > > still looks correct. Ok, that's the last piece, if Cur[r6.id=1] and Cur[r7.id=1] they share the same range. So as long as this range is within range1, range2 it is all good. And the range is checked downstream of regsafe. So, yes '(rold->precise && rold->id && !check_ids(idmap, rold, rcur))' is fine. > > > > > It was a "clever" attempt to ignore solo scalar IDs in Cur without modifying Cur. > > I'll think a bit more, sorry for a lot of noise.
