seaneveson marked 4 inline comments as done.
seaneveson added a comment.
There are some issues which haven't been resolved yet:
- There is a loss of precision for loops that need to be executed exactly
maxBlockVisitOnPath times, as the loop body is executed with the widened state
**instead**
seaneveson updated this revision to Diff 36739.
seaneveson added a comment.
Updated to latest revision.
Change patch to widen all loops which do not exit.
Changed to widen on block entrance so the guard condition is accounted for
(thanks for the suggestion).
Updated tests to reflect changes.
seaneveson added a comment.
My initial approach was for the analyzer to have as much information as
possible after the loop. This means there are cases where the information is
incorrect. Future work would be to reduce these cases.
I believe your preferred approach is to have no inaccuracies
seaneveson added a comment.
Thank you for your comments.
@zaks.anna wrote:
> What do you mean by "approximate"?
I think @dcoughlin gave a perfect example in the following comment:
@dcoughlin wrote:
> This doesn't seem quite right. Consider:
>
> int i;
> for (i = 0; i < 21; i += 3) {}
>
zaks.anna added inline comments.
Comment at: lib/StaticAnalyzer/Core/ExprEngine.cpp:1616
@@ +1615,3 @@
+builder.isFeasible(false) && !StFalse &&
+BldCtx.blockCount() == AMgr.options.maxBlockVisitOnPath - 1) {
+
seaneveson wrote:
> zaks.anna
dcoughlin added inline comments.
Comment at: lib/StaticAnalyzer/Core/LoopWidening.cpp:149
@@ +148,3 @@
+ break;
+}
+
This doesn't seem quite right. Consider:
```
int i;
for (i = 0; i < 21; i += 3) {}
clang_analyzer_eval(i == 23);
```
The value of `i`
zaks.anna added a comment.
nit: Please, use proper punctuation in the comments.
Comment at: lib/StaticAnalyzer/Core/ExprEngine.cpp:1616
@@ +1615,3 @@
+builder.isFeasible(false) && !StFalse &&
+BldCtx.blockCount() == AMgr.options.maxBlockVisitOnPath - 1) {
+
seaneveson updated this revision to Diff 35216.
seaneveson added a comment.
The TK_EntireMemSpace trait is now used when invalidating. The trait was added
in http://reviews.llvm.org/D12993, thank you Devin for that patch.
Updated to the latest trunk.
http://reviews.llvm.org/D12358
Files:
dcoughlin added a comment.
There is a patch to add memspace region invalidation in
http://reviews.llvm.org/D12993.
http://reviews.llvm.org/D12358
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
dcoughlin added a comment.
I looked at the behavior of invalidateRegions() under the patch. It looks like
MemSpaceRegions //are// being added to the worklist but these regions don't
have clusters associated with them so invalidating the regions themselves
doesn't remove any bindings.
Ted:
seaneveson added a comment.
In http://reviews.llvm.org/D12358#241631, @cfe-commits wrote:
> Hi Sean,
>
> Ted provided more details off-list. He suspects that the problem is that we
> likely don't add MemSpaceRegions to the worklist because every region is a
> subregion of a MemSpaceRegion, and
dcoughlin added a comment.
I'll look at this today. Thanks for your patience!
http://reviews.llvm.org/D12358
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Hi Sean,
Ted provided more details off-list. He suspects that the problem is that we
likely don't add MemSpaceRegions to the worklist because every region is a
subregion of a MemSpaceRegion, and thus we would invalidate, by default, all
regions that were in the same MemSpace as the regions we
krememek added a comment.
In http://reviews.llvm.org/D12358#238303, @seaneveson wrote:
> In http://reviews.llvm.org/D12358#237099, @krememek wrote:
>
> > To get the conservative invalidation that Anna suggests (actually, a little
> > less conservative), I think you can just pass in a two
seaneveson updated this revision to Diff 33906.
seaneveson added a comment.
Refactored into a new file: LoopWidening.cpp (and LoopWidening.h).
Added an analyzer-config option, which defaults to false:
widen-constant-bound-loops=false
Modified analyzer-config tests to check for the new option.
seaneveson added a comment.
In http://reviews.llvm.org/D12358#237099, @krememek wrote:
> To get the conservative invalidation that Anna suggests (actually, a little
> less conservative), I think you can just pass in a two MemRegions as the
> input to that method and get a new ProgramState with
krememek added a comment.
In http://reviews.llvm.org/D12358#234949, @zaks.anna wrote:
I accept that my current patch is not a comprehensive solution to the
problem and that it may introduce false positives, however I do think it
is an improvement, where it is preferable to have false
krememek added a comment.
I think the functionality started here by doing something clever with loops is
complex enough to warrant putting this into a separate .cpp file. We can keep
this here for now, but this seems like complexity that is going to naturally
creep up and make this file even
krememek added a comment.
In http://reviews.llvm.org/D12358#234975, @krememek wrote:
1. We need to consult the number of times a loop has been executed to
determine when to apply this widening. We can look at the basic block
counts, which are already used to cull off too many
Hi Sean,
I responded with some more feedback. Conceptually the patch is quite simple,
but I think Anna’s points are all spot on. I think we’d all be quite amendable
for this work to go in under a flag, with further improvements going in on top
of that. That way we can all collectively start
seaneveson added a comment.
In http://reviews.llvm.org/D12358#233983, @zaks.anna wrote:
This will leave us in a state that is wrong and will likely lead to false
positives and inconsistencies, avoiding which is extremely important.
I accept that my current patch is not a comprehensive
zaks.anna added a comment.
I accept that my current patch is not a comprehensive solution to the problem
and that it may introduce false positives, however I do think it is an
improvement, where it is preferable to have false positives
over doing no analysis after the loop.
We try to
zaks.anna requested changes to this revision.
zaks.anna added a comment.
This revision now requires changes to proceed.
I agree that the way the static analyzer handles loops with known bounds is
quite bad and we loose coverage because of it, so this is definitely an
important problem to solve!
krememek added a comment.
One thing about the tests passing: that's great, but that's obviously
insufficient. We probably have fewer tests showing that the analyzer can't
handle something than tests that show it does handle something.
When a patch like this lands, which expands the analysis
krememek added a comment.
In http://reviews.llvm.org/D12358#233983, @zaks.anna wrote:
A way this could be improved is by invalidating all the values that the loops
effects, both the values on the stack and on the heap. (We could even start
overly conservative and invalidate all the values
xazax.hun added a comment.
A conservative solution should work.
But if we want to preserve some precision I think it should be possible to not
to invalidate those values on the stack that are not effected by the loop. The
hard problem here is that, it is impossible to reason about the heap
On Aug 26, 2015, at 3:59 AM, Sean Eveson via cfe-commits
cfe-commits@lists.llvm.org wrote:
We have been looking at the following problem, where any code after the
constant bound loop is not analyzed because of the limit on how many times
the same block is visited, as described in
krememek added a comment.
FWIW, I do think this is a great problem to work on. It is easy to come up
with solutions that work for specific examples but fall over on general code.
I completely agree that failing to analyzing code after the loop is a major
hole and lost opportunity to find
28 matches
Mail list logo
