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

[Devin Coughlin via cfe-commits]

dcoughlin added a comment.

Hi Sean,

Sorry it took me so long to get back to you.


================
Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:266
@@ +265,3 @@
+  /// \sa shouldWidenLoops
+  bool WidenLoops;
+
----------------
Is this field used?

================
Comment at: lib/StaticAnalyzer/Core/ExprEngine.cpp:1407
@@ +1406,3 @@
+    const CFGBlock *Following = getBlockAfterLoop(L.getDst());
+    if (Following && nodeBuilder.getContext().Eng.blockWasVisited(Following))
+      return;
----------------
What is the purpose of checking whether the block has already been visited by some other path?

If I understand correctly, this will stop the analyzer from widening before the "last" iteration through the loop and so will result in a sink after that iteration. What this means is that we will never explore the code beyond the loop in the widened state -- but isn't this the whole point of the widening?

So, for example, in your `variable_bound_exiting_loops_not_widened()` test, don't we want the clang_analyzer_eval() statement after the loop to be symbolically executed on 4 separate paths? That is, once when i is 0, once when i is 1, once when i is 2 and once when i is $conj_i$ + 1 where $conj_i$ is the value conjured for i when widening.

Also, in general, analysis of one path should not depend at all on whether another path has been explored. This is because we want the analyzer to be free choose different strategies about path exploration (e.g., BFS vs. DFS, prioritizing some paths over others, etc.) without changing the issues reported on along any given path. For this reason, I don't think we necessarily want to track and expose `blockWasVisited()` on CoreEngine or use this to determine when to permit a sink.



================
Comment at: lib/StaticAnalyzer/Core/LoopWidening.cpp:98
@@ +97,3 @@
+  RegionAndSymbolInvalidationTraits ITraits;
+  for (int RegionIndex = 0; RegionIndex < NumRegions; ++ RegionIndex) {
+    ITraits.setTrait(Regions[RegionIndex],
----------------
I get a warning here about comparing a signed int (RegionIndex) to an unsigned (NumRegions).

I think you can avoid this and simplify things by using a range-based for loop:
```
  const MemRegion *Regions[] = {
      ...
  };
  RegionAndSymbolInvalidationTraits ITraits;
  for (auto *Region : Regions) {
    ...
  }
```


http://reviews.llvm.org/D12358