Re: [RFC PATCH bpf-next 07/12] bpf/verifier: allow bounded loops with JLT/true back-edge

[John Fastabend <john.fastabend@gmail.com>]

On 02/23/2018 09:41 AM, Edward Cree wrote:
> Where the register umin_value is increasing sufficiently fast, the loop
>  will terminate after a reasonable number of iterations, so we can allow
>  to keep walking it.

Continuing to walk the loop is problematic because we hit the complexity
limit. What we want to do is a static analysis step upfront on the basic
block containing the loop to ensure the loop is bounded.

We can do this by finding the induction variables (variables with form
cn+d) and ensuring the comparison register is an induction variable and
also increasing/decreasing correctly with respect to the comparison op.

This seems to be common in compilers to pull computation out of the
loop. So should be doable in the verifier.


> The semantics of prev_insn_idx are changed slightly: it now always refers
>  to the last jump insn walked, even when that jump was not taken.  Also it
>  is moved into env, alongside a new bool last_jump_taken that records
>  whether the jump was taken or not.  This is needed so that, when we detect
>  a loop, we can see how we ended up in the back-edge: what was the jump
>  condition, and is it the true- or the false-branch that ends up looping?
> We record in our explored_states whether they represent a conditional jump
>  and whether that jump produced a good loop bound.  This allows us to make
>  unconditional jumps "not responsible" for ensuring the loop is bounded, as
>  long as there is a conditional jump somewhere in the loop body; whereas a
>  conditional jump must ensure that there is a bounding conditional somewhere
>  in the loop body.
> Recursive calls have to remain forbidden because the calculation of maximum
>  stack depth assumes the call graph is acyclic, even though the loop
>  handling code could determine whether the recursion was bounded.
> 
> Signed-off-by: Edward Cree <ecree@solarflare.com>
> ---