[PATCH] D53701: [Analyzer] Record and process comparison of symbols instead of iterator positions in interator checkers
Balogh, Ádám via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Mon Nov 5 01:56:12 PST 2018
baloghadamsoftware added a comment.
Your suggestion sounds completely reasonable. We cannot rely entirely on inlining of comparison operators. However, there is an important side-effect of inlining: on iterator-adapters inlining ensures that we handle the comparison of the underlying iterator correctly. Without inlining, `evalCall()` only works on the outermost iterator which is not always correct: it may happen that the checker cannot conclude any useful relation between the two iterator-adapters but there are some relations stored about the inner iterators. Based on my experiments quite many of the false-positives are related to iterator-adapters. So I am afraid that we introduce even more false-positives by losing inlining.
I wonder whether the current "mixed" approach introduces additional paths because we do not do explicit state-splits and function `processComparison()` removes contradicting branches.
Comment at: lib/StaticAnalyzer/Checkers/IteratorChecker.cpp:2066
"Symbol comparison must be a comparison");
return assumeNoOverflow(NewState, cast<SymIntExpr>(CompSym)->getLHS(), 2);
> P.S. What was the idea here? Like, `CompSym` was just computed via `BO_EQ` and has type of a condition, i.e. `bool` because we are in C++. Is this code trying to say that the result of the comparison is bounded by `true/2`?
There is also a `->getLHS()` which means that we enforce the bound on the left-hand side of the rearranged comparison. Although both symbols are bounded by `max/4`, constraint manager does not imply that the sum/diff is the bounded by `max/2`. I have to enforce this manually to prevent `min` negated to `min` when the constraint manager negates the difference.
More information about the cfe-commits