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


Reply via email to