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 <ec...@solarflare.com>