On 23/02/18 22:27, John Fastabend wrote: > 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. So, I should mention that I _do_ have an idea for an optimisation that lets us avoid walking N times. Basically, after you walk the loop for the first time (and detect the loop presence & jump condition), you change the type of the register from SCALAR_VALUE to INDUCTION_VARIABLE, which the other code should treat basically like a pointer in terms of accumulating offsets when doing arithmetic, etc. Then when you get round the loop the second time, if the register still holds the INDUCTION_VARIABLE, you can look at the offsets and determine that the right thing is happening. And because you made it around the loop with the INDUCTION_VARIABLE there, you know that any accesses etc. you do in the loop body are safe (you'd feed in the constraints you have in the min/max values so that e.g. array indexing could be verified). So you do have to walk it twice, but not N times :-) However, the idea needs more work to turn it into an obviously-correct algorithm (issues like nested loops and popped branches make me worry a little). Also I feel a little safer knowing that if the verifier wrongly considers a loop bounded that actually isn't, it'll just walk round it until it hits the complexity limit and reject the program. That seems like a nice kind of belt-and-braces security to have.
-Ed
