[PATCH] D12358: [Analyzer] Widening loops which do not exit

[Sean Eveson via cfe-commits]

seaneveson marked 3 inline comments as done.
seaneveson added a comment.

In http://reviews.llvm.org/D12358#266391, @dcoughlin wrote:

> I think this is an acceptable loss of precision because, in general, it is unlikely that a concrete-bounded loop will be executed *exactly* maxBlockVisitOnPath times. You could add special syntactic checks to try to detect this, but I think it is unlikely to make much different in practice.


I agree.

The problem can be solved by executing the widened state after the last iteration, rather than instead of it. This can only really be done by changing the max block visit approach. This needs to be done in the future in order to support nested loops. This precision issue could also be resolved at that time.


================
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/CoreEngine.h:84
@@ +83,3 @@
+  /// The blocks that have been visited during analysis
+  llvm::DenseSet<const CFGBlock *> blocksVisited;
+
----------------
The BlockCount is specific to the path of analysis, so it can't be used to check if a loop has been exited before. I've added this set to store and identify previously visited blocks. Is there a better way this can/could be done?

================
Comment at: lib/StaticAnalyzer/Core/LoopWidening.cpp:65
@@ +64,3 @@
+  if (FalseBranch)
+    return FalseBranch;
+  // If there isn't a false branch we still have to check for break points
----------------
Perfect, thanks.

Perhaps it could be changed back to false when the invalidation is better? Then it could catch true positives e.g.
```
int *a = new int[10]
for (int i = 0; i < 100; ++i) {
  if (i > 90) 
    ++a;
  ...
}
```

================
Comment at: test/Analysis/loop-widening.c:159
@@ +158,3 @@
+
+void variable_bound_exiting_loops_not_widened(int x) {
+  int i = 0;
----------------
Thank you for the example tests.

When an inner loop is widened, any outer loops are widened 'coincidentally' since everything is invalidated. This means the second example test passes. When an inner loop is not widened the outer loop will not be widened. This is because a sink is generated when the max block count is reached the second time through the outer loop. i.e.
```
for (i = 0; i < 10; i++) {
  for (j = 0; j < 2; j++) {
    // A sink is generated here on the second iteration of the outer loop,
    // since this block was already visited twice (when i == 0).
    ...
  }
}
// Never reach here
```
This means the first example test does not pass. I’ve added the tests with a FIXME comment.



http://reviews.llvm.org/D12358