[PATCH] D53701: [Analyzer] Record and process comparison of symbols instead of iterator positions in interator checkers

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In https://reviews.llvm.org/D53701#1287007, @baloghadamsoftware wrote:

> ...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.


Mmm, is it possible to detect adapters and inline them as an exception from the rule? You can foresee a pretty complicated system of rules and exceptions if we go down this path, but i believe that it is still much easier and more reliable than the system that tries to synchronize two different models of iterators, so i really encourage you to at least give it a try somehow.

> I  wonder whether the current "mixed" approach introduces additional paths because we do not do explicit state-splits and function `processComparison()` removes contradicting branches.

I believe that the effect of eager state splits is going to be roughly similar to the actual -analyzer-eagerly-assume:

1. Split paths earlier than it is absolutely necessary, which may slow down the analysis and duplicate some work, but most of the time it'll be just a few nodes before the actual check in the code would have caused a split anyway.
2. Simplify constraint solving on each of the new paths, which will indeed help with refuting some invalid paths, especially those in which new constraints over the symbols are introduced after the check, but that's due to pecularities of our constraint solver, i.e. rather accidentally than intentionally.



================
Comment at: lib/StaticAnalyzer/Checkers/IteratorChecker.cpp:1197-1199
   while (const auto *CBOR = Cont->getAs<CXXBaseObjectRegion>()) {
     Cont = CBOR->getSuperRegion();
   }
----------------
Szelethus wrote:
> You will have to excuse me for commenting on something totally unrelated, but I'm afraid this may cause a crash, if the region returned by `getSuperRegion` is symbolic. I encountered this error when doing the exact same thing in my checker: D50892. Can something like this occur with this checker?
Hmm, had a look at the crash you mention here. Your code crashed because you additionally did `getAs<TypedValueRegion>`, which would turn your pointer into a null when a symbolic region is encountered. So the final code ended up a bit weird: there's no need to check that it's a `TypedValueRegion` before you check that it's a `CXXBaseObjectRegion`; just check for the latter directly. This code looks correct in this sense.

Also, since this code keeps copied around, do we need a better helper function for this unwrap idiom? I.e., something like `MemRegion::StripCasts()` that only unwraps derived-to-base casts?


================
Comment at: lib/StaticAnalyzer/Checkers/IteratorChecker.cpp:2066
            "Symbol comparison must be a comparison");
     return assumeNoOverflow(NewState, cast<SymIntExpr>(CompSym)->getLHS(), 2);
   }
----------------
baloghadamsoftware wrote:
> NoQ wrote:
> > 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.
Ouch, right, didn't notice `getLHS()`, sorry!


Repository:
  rC Clang

https://reviews.llvm.org/D53701