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. > > 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.
