On Thu, Jun 1, 2023 at 11:52 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > On Thu, 2023-06-01 at 10:13 -0700, Alexei Starovoitov wrote: > > On Thu, Jun 1, 2023 at 9:57 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > > > > > On Wed, 2023-05-31 at 19:05 -0700, Alexei Starovoitov wrote: > > > > [...] > > > > > Suppose that current verification path is 1-7: > > > > > - On a way down 1-6 r7 will not be marked as precise, because > > > > > condition (r7 > X) is not predictable (see check_cond_jmp_op()); > > > > > - When (7) is reached mark_chain_precision() will start moving up > > > > > marking the following registers as precise: > > > > > > > > > > 4: if (r6 > r7) goto +1 ; r6, r7 > > > > > 5: r7 = r6 ; r6 > > > > > 6: if (r7 > X) goto ... ; r6 > > > > > 7: r9 += r6 ; r6 > > > > > > > > > > - Thus, if checkpoint is created for (6) r7 would be marked as read, > > > > > but will not be marked as precise. > > > > > > > > > > Next, suppose that jump from 4 to 6 is verified and checkpoint for (6) > > > > > is considered: > > > > > - r6 is not precise, so check_ids() is not called for it and it is not > > > > > added to idmap; > > > > > - r7 is precise, so check_ids() is called for it, but it is a sole > > > > > register in the idmap; > > > > > > > > typos in above? > > > > r6 is precise and r7 is not precise. > > > > > > Yes, it should be the other way around in the description: > > > r6 precise, r7 not precise. Sorry for confusion. > > > > > > > > - States are considered equal. > > > > > > > > > > Here is the log (I added a few prints for states cache comparison): > > > > > > > > > > from 10 to 13: safe > > > > > steq hit 10, cur: > > > > > R0=scalar(id=2) R6=scalar(id=2) R7=scalar(id=1) R9=fp-8 R10=fp0 fp-8=00000000 > > > > > steq hit 10, old: > > > > > R6_rD=Pscalar(id=2) R7_rwD=scalar(id=2) R9_rD=fp-8 R10=fp0 fp-8_rD=00000000 > > > > > > > > the log is correct, thouhg. > > > > r6_old = Pscalar which will go through check_ids() successfully and both are unbounded. > > > > r7_old is not precise. different id-s don't matter and different ranges don't matter. > > > > > > > > As another potential fix... > > > > can we mark_chain_precision() right at the time of R1 = R2 when we do > > > > src_reg->id = ++env->id_gen > > > > and copy_register_state(); > > > > for both regs? > > > > > > This won't help, e.g. for the original example precise markings would be: > > > > > > 4: if (r6 > r7) goto +1 ; r6, r7 > > > 5: r7 = r6 ; r6, r7 > > > 6: if (r7 > X) goto ... ; r6 <-- mark for r7 is still missing > > > 7: r9 += r6 ; r6 > > > > Because 6 is a new state and we do mark_all_scalars_imprecise() after 5 ? > > Yes, precision marks are not inherited by child states. > > > > > > What might help is to call mark_chain_precision() from > > > find_equal_scalars(), but I expect this to be very expensive. > > > > maybe worth giving it a shot? > > Sure, will report a bit later today. > > > > > I think > > > > if (rold->precise && !check_ids(rold->id, rcur->id, idmap)) > > > > would be good property to have. > > > > I don't like u32_hashset either. > > > > It's more or less saying that scalar id-s are incompatible with precision. > > > > > > > > I hope we don't need to do: > > > > + u32 reg_ids[MAX_CALL_FRAMES]; > > > > for backtracking either. > > > > Hacking id-s into jmp history is equally bad. > > > > > > > > Let's figure out a minimal fix. > > > > > > Solution discussed with Andrii yesterday seems to work. > > > > The thread is long. Could you please describe it again in pseudo code? > > - Add a function mark_precise_scalar_ids(struct bpf_verifier_env *env, > struct bpf_verifier_state *st) > such that it: > - collect PRECISE_IDS: a set of IDs of all registers marked in env->bt > - visit all registers with ids from PRECISE_IDS and make sure > that these registers are marked in env->bt > - Call mark_precise_scalar_ids() from __mark_chain_precision() > for each state 'st' visited by states chain processing loop, > so that: > - mark_precise_scalar_ids() is called for current state when > __mark_chain_precision() is entered, reusing id assignments in > current state; > - mark_precise_scalar_ids() is called for each parent state, reusing > id assignments valid at 'last_idx' instruction of that state. > > The idea is that in situations like below: > > 4: if (r6 > r7) goto +1 > 5: r7 = r6 > --- checkpoint #1 --- > 6: <something> > 7: if (r7 > X) goto ... > 8: r7 = 0 > 9: r9 += r6 > > The mark_precise_scalar_ids() would be called at: > - (9) and current id assignments would be used. > - (6) and id assignments saved in checkpoint #1 would be used. > > If <something> is the code that modifies r6/r7 the link would be > broken and we would overestimate the set of precise registers. > To avoid this we need to recalculate these IDs on each new parent state, based on requested precision marks. If we keep a simple and small array of IDs and do a quick linear search over them for each SCALAR register, I suspect it should be very fast. I don't think in practice we'll have more than 1-2 IDs in that array, right?
