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: if (rold->precise && rold->id && !check_ids(idmap, rold, rcur)) is not fully 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.
