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.
