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
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
