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

[Sean Eveson via cfe-commits]

seaneveson marked an inline comment as done.
seaneveson added a comment.

Hi Devin,

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


================
Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:266
@@ +265,3 @@
+  /// \sa shouldWidenLoops
+  bool WidenLoops;
+
----------------
dcoughlin wrote:
> Is this field used?
No. Thanks I'll fix that.

================
Comment at: lib/StaticAnalyzer/Core/ExprEngine.cpp:1407
@@ +1406,3 @@
+    const CFGBlock *Following = getBlockAfterLoop(L.getDst());
+    if (Following && nodeBuilder.getContext().Eng.blockWasVisited(Following))
+      return;
----------------
dcoughlin wrote:
> 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.
> 
> 
I was trying to avoid doing unnecessary invalidation, where the variable bound loop had already exited. I suppose this won’t be a concern when the invalidation is improved. If everyone is happy for loops that have already exited to be widened then I will remove the related changes.

================
Comment at: lib/StaticAnalyzer/Core/LoopWidening.cpp:98
@@ +97,3 @@
+  RegionAndSymbolInvalidationTraits ITraits;
+  for (int RegionIndex = 0; RegionIndex < NumRegions; ++ RegionIndex) {
+    ITraits.setTrait(Regions[RegionIndex],
----------------
dcoughlin wrote:
> 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) {
>     ...
>   }
> ```
Will do. Thanks.


http://reviews.llvm.org/D12358