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