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** of
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.
ht
dcoughlin added a comment.
> What do people think about me creating a new patch based on your feedback?
I don't think you need to create a new review -- we can update this one and
keep the history.
> The aim would be to widen any non-exiting loops by invalidation. The initial
> patch would
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 af
dcoughlin added a comment.
Sean,
One important difference between what you are proposing and what Cousot and
Cousot describe in the paper you cite is that they don't drop coverage. They
widen for termination on infinite-height lattices and their narrowing still
maintains an over-approximation
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 wrote:
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) {}
>
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` sho
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:
inc
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
http://lists.llvm.org/cgi-bin/mailman/listinfo
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: What
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
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
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 w
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.
Add
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 MemRegi
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#235142, @seaneveson wrote:
> If I refactor this patch in its current state into a separate file and put it
> behind a flag, would it then be acceptable? I would then like to take some
> time to look at the invalidation improvements as
seaneveson added a comment.
In http://reviews.llvm.org/D12358#234949, @zaks.anna wrote:
> We try to avoid false positives as much as possible. They are very painful
> for users to deal with.
> You should develop this feature behind a flag. This would allow for
> incremental development and
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 ma
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
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 m
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 fa
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
> On Aug 27, 2015, at 8:57 AM, Sean Eveson 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 positives over doing no
> analysi
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 solu
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 sc
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 bugs
> On Aug 26, 2015, at 3:59 AM, Sean Eveson via cfe-commits
> 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 bugzillas #7638 and #23438.
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 with
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!
seaneveson created this revision.
seaneveson added a subscriber: cfe-commits.
Dear All,
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 bugzillas #7638 a
34 matches
Mail list logo
