baloghadamsoftware added inline comments.
================
Comment at: lib/StaticAnalyzer/Checkers/IteratorPastEndChecker.cpp:423
+
+void IteratorPastEndChecker::handleComparison(CheckerContext &C,
+ const SVal &LVal,
----------------
baloghadamsoftware wrote:
> NoQ wrote:
> > baloghadamsoftware wrote:
> > > NoQ wrote:
> > > > a.sidorin wrote:
> > > > > What will happen if we write something like this:
> > > > > ```
> > > > > bool Eq1 = it1 == it2;
> > > > > bool Eq2 = it3 == it4;
> > > > > if (Eq1) {...}?
> > > > > ```
> > > > >
> > > > > As I understand, we'll assume the second condition instead of first.
> > > > Had a look. So the problem is, we obtain the result of the comparison
> > > > as a symbol, from which it is too hard to recover the operands in order
> > > > to move iterator position data from one value to another.
> > > >
> > > > Normally we obtain a simple SymbolConjured for the return value of the
> > > > `operator==()` call (or, similarly, `operator!=()`). For plain-value
> > > > iterators (eg. `typedef T *iterator`) we might be obtaining an actual
> > > > binary symbolic expression, but even then it's not quite clear how to
> > > > obtain operands (the structure of the expression might have changed due
> > > > to algebraic simplifications). Additionally, LHS and RHS aren't
> > > > necessarily symbols (they might be semi-concrete), so composing
> > > > symbolic expressions from them in general is problematic with our
> > > > symbol hierarchy, which is rarely a problem for numbers but for
> > > > structural symbols it'd be a mess.
> > > >
> > > > For now i suggest, instead of storing only the last LHS and RHS, to
> > > > save a map from symbols (which are results of comparisons) to (LHS
> > > > value, RHS value) pairs. This map should, apart from the obvious, be
> > > > cleaned up whenever one of the iterators in the pair gets mutated
> > > > (incremented or decremented). This should take care of the problem
> > > > Alexey points out, and should work with semi-concrete stuff.
> > > >
> > > > For the future i suggest to let users construct their own symbols and
> > > > symbolic expressions more easily. In fact, if only we had all iterators
> > > > as regions, we should have probably used SymbolMetadata for this
> > > > purpose: it's easy to both recover the parent region from it and use it
> > > > in symbolic expressions. We could also deprecate the confusing
> > > > structural symbols (provide default-bound lazy compound values for
> > > > conjured structures instead), and then it'd be possible to transition
> > > > to SymbolMetadata entirely.
> > > Thank you for the suggestion. I am not sure if I fully understand you. If
> > > I create a map where the key is the resulting symbol of the comparison,
> > > it will not work because evalAssume is called for the innermost
> > > comparison. So if the body of operator== (or operator!=) is inlined, then
> > > I get a binary symbolic expression in evalAssume, not the SymbolConjured.
> > > This binary Symbolic expression is a comparison of the internals of the
> > > iterators, e.g. the internal pointer. So the key will not match any LHS
> > > and RHS value pair in the map. I also thought on such solution earlier
> > > but I dismissed it because of this.
> > Well, even if the body of the comparison operator is inlined,
> > PreStmt/PostStmt callbacks should still work, and it doesn't really matter
> > if there's a `SymbolConjured` or not, we can still add the symbolic
> > expression to our map as a key.
> >
> > Essentially, you ignore whatever happens in the iterator's operator==()
> > when it's inlined (including any evalAssume events), then in PostStmt of
> > operator==() you map the return-value symbol of the operator to the
> > operator's arguments (operands), then whenever an assumption is being made
> > against the return-value symbol, you carry over this assumption to the
> > operands. I think it shouldn't really matter if the operator call was
> > inlined.
> >
> > The only unexpected thing that may happen due to inlining is if the inlined
> > operator returns a concrete value (plain true or plain false) instead of
> > the symbol, but in this case what we need to do is to just carry over the
> > assumption to the operands instantly.
> Maybe if I evaluate the operator==() call for iterators using evalCall()?
Sorry, maybe my phrasing was not accurate enough. The problem is that the
assumption is not being made against the return-value symbol of the
operator==(), but if inlined, against the internal == operator. So I do not
have the same key in evalAssume() thus I cannot access the operands from the
map I stored in checkPostCall(). The only solution I can imagine is that I
evalCall() the operator==() but then we lose the opportunity to check anything
inside the body of the operator.
https://reviews.llvm.org/D25660
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
