-
Notifications
You must be signed in to change notification settings - Fork 13.6k
[analyzer] Don't assume third iteration in loops #119388
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
This commit ensures that if the loop condition is opaque (the analyzer cannot determine whether it's true or false) and there were at least two iterations, then the analyzer doesn't make the unjustified assumption that it can enter yet another iteration. Note that the presence of a loop suggests that the developer thought that two iterations can happen (otherwise an `if` would've been sufficient), but it does not imply that the developer expected three or four iterations -- and in fact there are many false positives where a loop iterates over a two-element (or three-element) data structure, but the analyzer cannot understand the loop condition and blindly assumes that there may be three or more iterations. (In particular, analyzing the FFMPEG project produces 100+ such false positives.) Moreover, this provides some performance improvements in the sense that the analyzer won't waste time on traversing the execution paths with 3 or 4 iterations in a loop (which are very similar to the paths with 2 iterations) and therefore will be able to traverse more branches elsewhere on the `ExplodedGraph`. This logic is disabled if the user enables the widen-loops analyzer option (which is disabled by default), because the "simulate one final iteration after the invalidation" execution path would be suppressed by the "exit the loop if the loop condition is opaque and there were at least two iterations" logic. If we want to support loop widening, we would need to create a follow-up commit which ensures that it "plays nicely" with this logic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
This comment was marked as off-topic.
The difference between this PR and my earlier PR #109804 "Suppress out of bounds reports after weak loop assumptions" is:
Slightly offtopic remark: I'm planning to create a separate commit to filter out branches where the analyzer assumes that 0 iterations happen in a loop (with an opaque condition). I'll probably put that logic behind an analyzer option (e.g. These follow-up ideas can be discussed at the umbrella discourse thread for my loop handling improvement plans. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you for the ping. I'm really busy lately with stabilizing Z3 refutation.
I really liked the extensive evaluation, which helped a lot forming my opinion here.
The diffs look all right. I only spotchecked some places the reports. I agree with your evaluation.
The content of the patch looks also correct. I only found a couple Grammarly spellings, but that's it.
I wonder how you found out that loop widening may conflict with this heuristic, were any tests broken that raised your awareness?
I have one concern with didEagerlyAssumeBifurcateAt
, that it is bound and overwritten at the most recent eager split - which to my knowledge may not be the loop condition if we have something like this:
while (coin()) {
if (coin()) { // #inner_coin
++num;
}
}
Each time the inner_coin
would spoil the LastEagerlyAssumeBifurcationAt
trait between the loop iterations, right?
Storing const Expr *
pointers is brittle for recursive functions too, where the same expression could appear in different LocationContexts. I wonder if we could make an example where it would confuse this heuristic.
I'm also not entirely convinced about nested loops - if this heuristic would kick in. This is basically a variant of the coin
case I showed an example.
I don't have a counter example just yet, but I'm not sure I can spare the time to craft one.
Once again, big kudos for the extensive data. And I have no objections overall, I only have these minor questions before I'd approve this.
Thanks for the review, I'll fix the minor remarks soon.
Yes, some (IIRC three) testcases fail in
These situations do not cause problems for my goals, because I only intend to use However, it's nice that you highlighted this question, because now I realized that my implementation is buggy (does not do what I wanted). For example in void foo(int x) {
while (x == 0) {
// body that does not change x and does not trigger any EagerlyAssume
}
} EagerlyAssume would succeed at the beginning of the first iteration, and this would set To fix this problem, it would be sufficient to e.g. ensure that
|
Co-authored-by: Balazs Benics <[email protected]>
Sounds good to me. Let's zero it out after it's "used"/"consumed".
Yes, it could get messy. For instance if we have multiple parent nodes due to a merge. Let's not do traversals. I'm good with the change once the last remark is fixed. |
I took a different approach (which was already mostly implemented when I've seen this suggestion): I'm setting the stored
OK, if you say so, I'm very happy to avoid it 😀
I didn't expect running time implications, because as we discard these execution paths, the analyzer will traverse other execution paths instead of them -- so any performance gains should appear as "more results" instead of "faster analysis". Unfortunately the improvements that I hoped didn't appear in the experimental results: the "final" version of this commit doesn't produce significantly more results compared to the "intermediate" version which just suppresses the results (after "wasting time" on traversing the unjustified paths). I think we don't see visible performance improvements because my observation that "difference between 2 or 3 iterations is irrelevant on the later parts of the execution path" does not imply that we can save a significant amount of calculations by driving each of those paths through 2 iterations (instead of roughly half 2 iterations, half 3 iterations) -- because those paths differ in many assumptions, so we cannot merge them even if we ignore the iteration count in that particular loop. Additionally, my measurements are on stable open source projects, where real results are much rarer than false positives (even on stable checkers), so the number of results that we get is an imperfect and somewhat noisy proxy of the actual improvements. |
Do you expect any changes for less obvious ways of looping?
Would be nice to have some tests for those as well. |
The logic that I added only affects the handling of the condition part of loop statements, so it has absolutely no effect on the handling of code that implements similar looping behavior with different language features. I added a testcase to document this (and as an example, show the behavior of |
If I understand correctly, I handled every review suggestion. @steakhal If there are no additional suggestions, I'd be grateful for an approval. (My follow-up commit is mostly ready, I'll release it soon after merging this.) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If I understand correctly, I handled every review suggestion.
@steakhal If there are no additional suggestions, I'd be grateful for an approval. (My follow-up commit is mostly ready, I'll release it soon after merging this.)
My bad. I thought I already approved this one.
I checked again the PR and still looks good.
Thank you for your hard work for fixing loops.
One more thing. Please mention this in the release notes. |
Co-authored-by: Balazs Benics <[email protected]>
No problem, I didn't intend to merge this during the Christmas period (when I was on vacation and didn't want to monitor the effects of the change).
I added a paragraph to the release notes. Is it OK (= not too short, not too long, clear enough) ? |
LLVM Buildbot has detected a new failure on builder Full details are available at: https://lab.llvm.org/buildbot/#/builders/88/builds/6318 Here is the relevant piece of the build log for the reference
|
The LLVM Buildbot failure is clearly unrelated to this commit -- it seems to be a straightforward flakiness on a completely unrelated part of the project. |
This reverts commit bb27d5e. DO NOT MERGE, this is only for comparison.
This commit ensures that if the loop condition is opaque (the analyzer cannot determine whether it's true or false) and there were at least two iterations, then the analyzer doesn't make the unjustified assumption that it can enter yet another iteration.
Note that the presence of a loop suggests that the developer thought that two iterations can happen (otherwise an
if
would've been sufficient), but it does not imply that the developer expected three or four iterations -- and in fact there are many false positives where a loop iterates over a two-element (or three-element) data structure, but the analyzer cannot understand the loop condition and blindly assumes that there may be three or more iterations. (In particular, analyzing the FFMPEG project produces 100+ such false positives.)Moreover, this provides some performance improvements in the sense that the analyzer won't waste time on traversing the execution paths with 3 or 4 iterations in a loop (which are very similar to the paths with 2 iterations) and therefore will be able to traverse more branches elsewhere on the
ExplodedGraph
.This logic is disabled if the user enables the widen-loops analyzer option (which is disabled by default), because the "simulate one final iteration after the invalidation" execution path would be suppressed by the "exit the loop if the loop condition is opaque and there were at least two iterations" logic. If we want to support loop widening, we would need to create a follow-up commit which ensures that it "plays nicely" with this logic.
To evaluate the effects of this commit, I also implemented an intermediate version which doesn't change the traversal of the exploded graph and instead of discarding the "assumes a third iteration" code paths eagerly, it analyzes them (wasting some time) and then discards the results found on them.
I analyzed our usual set open source projects these three version (upstream, intermediate, this commit) and the checker groups core, cplusplus, deadcode, nullability, security, unix and valist, plus the checker
alpha.security.ArrayBoundV2
.Comparison between upstream (a few weeks old main revision) and the intermediate version:
Note that it's not surprising that most of the eliminated false positives are coming from the alpha checker
alpha.security.ArrayBoundV2
: as the analyzer engine was always making these unjustified assumptions, any checker that was affected by this was stuck in alpha -- and only checkers that are less dependent on values manipulated in loops were brought out of the alpha state.Comparison between intermediate and this commit:
These differences are just random perturbations: as we don't waste time on analyzing the discarded execution paths, the "smart" graph traversal algorithms pick different branches and finds different results. As this perturbation is negligible compared to the total number of reports (among the largest projects: 1.8% on qtbase, 0.4% on postgres, 0.3% on ffmpeg), I think it's completely fine if this number of random results is replaced by the approximately same amount of other random results. (This perturbation would happen only once, when the user upgrades to a clang version that includes this commit.)