[PATCH] D105436: [analyzer][solver] Use all sources of constraints

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp:908
+        // into subexpressions of Sym.
+        Visit(Sym));
   }
----------------
martong wrote:
> vsavchenko wrote:
> > martong wrote:
> > > Alright. So, this is correct because `Visit` boils down finally to either `infer(Sym->getType)` or to `VisitBinaryOperator`. And both of them do a correct over-approximation of the ranges. Please confirm. 
> > > 
> > > First, I was a bit concerned b/c it is not immediate and not documented here. And it is easy to think by the first look that this might be faulty if we take the approximation of one operand of a binop that might not be true for the whole binop expression. Again, that is not the case because we approximate only in case of such ops where we can do a correct over-approximation (i.e. `|`, `&` and `%`). 
> > > 
> > > My point is, I'd like to see more explanatory comments here.
> > I'm sorry, but I don't really understand your point here.
> > 
> > Everything that this solver provides is conservative ranges, from whatever source it comes.  If you intersect two conservative ranges, you get a conservative range.
> > It doesn't matter what we do in `Visit` as long as it is correct.  If `Visit` is incorrect then the previous version of this code that gave preference to some sources over the other ones was also incorrect.
> Thanks for your reply.  So, with other words, I didn't see why it is immediate that a range for a sub-expression is a good approximation for the whole expression. Maybe it's just me, but that's not obvious until one checks that what exactly happens in `Visit`.
Oh, I mean, it's not correct.  Symbolic expressions are N-ary operators, and if we know constraints for at least some of these N operands, we can provide a conservative range for the whole symbol using some knowledge of the operator.  It doesn't say anywhere that we use a range for a sub-expression as an approximation for the whole range.

Actually I want to move some of these other sources inside of `Visit` as well because they trigger only to very specific kinds of symbolic expressions (e.g. binary minus, equality/disequality, comparisons).


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D105436/new/

https://reviews.llvm.org/D105436