[PATCH] D12358: [Analyzer] Handling constant bound loops

[Devin Coughlin via cfe-commits]

dcoughlin added a comment.



> What do people think about me creating a new patch based on your feedback?


I don't think you need to create a new review -- we can update this one and keep the history.

> The aim would be to widen any non-exiting loops by invalidation. The initial patch would be behind a flag and would use the TK_EntireMemSpace trait to conservatively invalidate 'everything' when a loop does not exit. It would then run through the loop body in the invalidated state, resulting in the analysis of all possible paths. The loop would then exit from the (now possibly false) loop condition, or a (now reachable) break statement.


This sounds great to me. I think it shouldn't be too difficult to add coarse widening before the last iteration through the loop for both concrete-bounded loops and loops with symbolic bounds. This will be a very imprecise hammer. It will invalidate everything (heap, locals, globals). I think you can choose the widening location (i.e, a loop back edge) to make it possible to still learn from the guard condition. For example, for the following loop I think the analyzer should be able widen and still know that ‘j’ < ’N’ on the final, widened iteration through the loop and that ‘j’ >= ’N’ after the loop (assuming there is no ‘break’):

  for (int j = 0; j < N; j++) { .. }

This will let us evaluate what kinds of improvements in coverage you get from not generating a sink but will almost certainly be too imprecise to turn on by default. I think a slightly tricky challenge here will be to handle nested loops without unnecessary sinks.

You could then make the widening more precise by invalidating only memory regions that a pre-analysis indicates may be modified by the loop. This pre-analysis can be relatively simple — invalidating the cone of influence of the DeclRefExprs in the the loop (as Ted suggested above.) With this implemented, we can evaluate precision and performance to decide whether to turn this on by default — but the hope is yes. If not, we may need to play with unsound tricks that leave less invalidated.

> Loops that never exit regardless of any variables would be an exception; see my comment below for thoughts on handling infinite loops.


Generalized non-termination checking is a very hard problem and is not something analyzer is particularly well-suited for. While this would be an interesting avenue for the analyzer to pursue, I think it should be in separate checker.


http://reviews.llvm.org/D12358