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> > ---