[Analyzer] Refactor begin and end symbol creation

[baloghadamsoftware]

Summary

This patch refactors begin and end symbol creation by moving symbol conjuration into the create... functions. This way the functions' responsibilities are clearer and makes possible to add more functions handling these symbols (e.g. functions for handling the container's size) without code multiplication.

[NoQ]

Aha, yup, thx!

Do you plan to centralize other code paths on which you conjure symbols?

'Cause i still believe that given that we now support C++ (our prvalues are now properly materialized) (most of the time), you should be able to remove support for symbol-like iterators, and then replace your position symbols with SymbolMetadata.

lib/StaticAnalyzer/Checkers/IteratorChecker.cpp

1929–1930

This is a bit more auto than allowed by our coding standards (it pretty much disallows auto unless it's some sort of dyn_cast (getAs) or an iterator.

2247

This looks like a new feature. Is it testable?

[baloghadamsoftware]

In D61136#1479454, @NoQ wrote:

Aha, yup, thx!

Do you plan to centralize other code paths on which you conjure symbols?

Only in a small rework of handleAssign() because that is a place where we conjure a symbol for a new end(). I only plan to centralize conjuration of begin() and end() symbols of containers.

'Cause i still believe that given that we now support C++ (our prvalues are now properly materialized) (most of the time), you should be able to remove support for symbol-like iterators, and then replace your position symbols with SymbolMetadata.

Abstract iterator positions are represented by symbolic expressions because we must be able to do simple calculations with them. This has nothing to do with iterator objects represented as symbols. Or what do you mean exactly by "replacing position symbols with SymbolMetadata"?

[baloghadamsoftware]

lib/StaticAnalyzer/Checkers/IteratorChecker.cpp

1929–1930

I can add the type, of course. However, until now I understood and it is also in the coding standard that "other places where the type is already obvious from the context". For me it is obvious that conjureSymbol() returns a SymbolRef. Even more obvious is the getSymbolManager() returns a SymbolManager.

2247

I am not sure I can test it alone. Maybe I should leave it for now and add it in another patch together with modelling of empty() or size(). Then I should also rename this patch which remains pure refactoring.

[NoQ]

In D61136#1480023, @baloghadamsoftware wrote:

Abstract iterator positions are represented by symbolic expressions because we must be able to do simple calculations with them. This has nothing to do with iterator objects represented as symbols. Or what do you mean exactly by "replacing position symbols with SymbolMetadata"?

I mean, use SymbolMetadata wherever you use SymbolConjured. Because metadata is attached to objects (i.e., it takes a region as part of its identity), it's problematic to use with iterators represented as symbols.

Though i'd also consider the opposite direction which seems to be even more promising: re-do SymbolMetadata so that it took a symbol instead of a region as part of its identity, and then attach "identity symbols" to all C++ objects, so that we didn't ever have to track iterators by their regions, but instead we could make IteratorChecker operate more like SimpleStreamChecker. This still requires re-doing all the conjuring, so keeping all the conjuring in one place is still a good idea.

lib/StaticAnalyzer/Checkers/IteratorChecker.cpp

1929–1930

Here is a discussion on this matter that i had recently. It was hard enough to convince people that the code below follows the coding standards:

auto DV = V.getAs<DefinedOrUnknownSVal>();

Also, conjuredSymbol() in fact returns a const SymbolConjured *, which is a more specialized type. This probably deserves at least a const auto *.

2247

Yup, i think it's good to keep NFC commits and features apart.

[Szelethus]

lib/StaticAnalyzer/Checkers/IteratorChecker.cpp

1929–1930

+1, I strongly disagree with the overuse of auto. I think project-wide things like the one you mentioned (SVal::getAs) are fine, because after googleing it once of twice it genuinely makes the code far more readable. However, where the scope of the type (like in many cases in this file) is very small, line breaks aren't a concern, or the function just simply isn't widely used (and conjureSymbol really isn't) we shouldn't use auto.

In general, I'd be just far more conservative: whenever in doubt, just don't use it. Whenever it's anything but super-super obvious, don't use it.

[baloghadamsoftware]

SymbolConjured * written, feature removed, just refactoring.

[NoQ]

Thx!

lib/StaticAnalyzer/Checkers/IteratorChecker.cpp

 bool isDecrementOperator(OverloadedOperatorKind OK);
 bool isRandomIncrOrDecrOperator(OverloadedOperatorKind OK);
 bool hasSubscriptOperator(ProgramStateRef State, const MemRegion *Reg);
 bool frontModifiable(ProgramStateRef State, const MemRegion *Reg);
 bool backModifiable(ProgramStateRef State, const MemRegion *Reg);
 SymbolRef getContainerBegin(ProgramStateRef State, const MemRegion *Cont);
 SymbolRef getContainerEnd(ProgramStateRef State, const MemRegion *Cont);
 ProgramStateRef createContainerBegin(ProgramStateRef State,
-                                     const MemRegion *Cont,
-                                     const SymbolRef Sym);
+                                     const MemRegion *Cont, const Expr *E,
+                                     QualType T, const LocationContext *LCtx,
+                                     unsigned BlockCount);
 ProgramStateRef createContainerEnd(ProgramStateRef State, const MemRegion *Cont,
-                                   const SymbolRef Sym);
+                                   const Expr *E, QualType T,
+                                   const LocationContext *LCtx,
+                                   unsigned BlockCount);
 const IteratorPosition *getIteratorPosition(ProgramStateRef State,
                                             const SVal &Val);
 ProgramStateRef setIteratorPosition(ProgramStateRef State, const SVal &Val,
                                     const IteratorPosition &Pos);
 ProgramStateRef removeIteratorPosition(ProgramStateRef State, const SVal &Val);
 ProgramStateRef assumeNoOverflow(ProgramStateRef State, SymbolRef Sym,
                                  long Scale);
 ProgramStateRef invalidateAllIteratorPositions(ProgramStateRef State,
void IteratorChecker::handleBegin(CheckerContext &C, const Expr *CE,
 
   ContReg = ContReg->getMostDerivedObjectRegion();
 
   // If the container already has a begin symbol then use it. Otherwise first
   // create a new one.
   auto State = C.getState();
   auto BeginSym = getContainerBegin(State, ContReg);
   if (!BeginSym) {
-    auto &SymMgr = C.getSymbolManager();
-    BeginSym = SymMgr.conjureSymbol(CE, C.getLocationContext(),
-                                    C.getASTContext().LongTy, C.blockCount());
-    State = assumeNoOverflow(State, BeginSym, 4);
-    State = createContainerBegin(State, ContReg, BeginSym);
+    State = createContainerBegin(State, ContReg, CE, C.getASTContext().LongTy,
+                                 C.getLocationContext(), C.blockCount());
+    BeginSym = getContainerBegin(State, ContReg);
   }
   State = setIteratorPosition(State, RetVal,
                               IteratorPosition::getPosition(ContReg, BeginSym));
   C.addTransition(State);
 }
 
 void IteratorChecker::handleEnd(CheckerContext &C, const Expr *CE,
                                 const SVal &RetVal, const SVal &Cont) const {
   const auto *ContReg = Cont.getAsRegion();
   if (!ContReg)
     return;
 
   ContReg = ContReg->getMostDerivedObjectRegion();
 
   // If the container already has an end symbol then use it. Otherwise first
   // create a new one.
   auto State = C.getState();
   auto EndSym = getContainerEnd(State, ContReg);
   if (!EndSym) {
-    auto &SymMgr = C.getSymbolManager();
-    EndSym = SymMgr.conjureSymbol(CE, C.getLocationContext(),
-                                  C.getASTContext().LongTy, C.blockCount());
-    State = assumeNoOverflow(State, EndSym, 4);
-    State = createContainerEnd(State, ContReg, EndSym);
+    State = createContainerEnd(State, ContReg, CE, C.getASTContext().LongTy,
+                               C.getLocationContext(), C.blockCount());
+    EndSym = getContainerEnd(State, ContReg);
   }
   State = setIteratorPosition(State, RetVal,
                               IteratorPosition::getPosition(ContReg, EndSym));
   C.addTransition(State);
 }
 
 void IteratorChecker::assignToContainer(CheckerContext &C, const Expr *CE,
                                         const SVal &RetVal,

 bool compare(ProgramStateRef State, SymbolRef Sym1, SymbolRef Sym2,
              BinaryOperator::Opcode Opc);
 bool compare(ProgramStateRef State, NonLoc NL1, NonLoc NL2,
              BinaryOperator::Opcode Opc);
 const CXXRecordDecl *getCXXRecordDecl(ProgramStateRef State,
                                       const MemRegion *Reg);
 SymbolRef rebaseSymbol(ProgramStateRef State, SValBuilder &SVB, SymbolRef Expr,
                         SymbolRef OldSym, SymbolRef NewSym);
+ProgramStateRef ensureNonNegativeDiff(ProgramStateRef State, SymbolRef Sym1,
+                                      SymbolRef Sym2);
 
 bool isIteratorType(const QualType &Type) {
   if (Type->isPointerType())
     return true;
 
   const auto *CRD = Type->getUnqualifiedDesugaredType()->getAsCXXRecordDecl();
   return isIterator(CRD);
 }
SymbolRef getContainerEnd(ProgramStateRef State, const MemRegion *Cont) {
   const auto *CDataPtr = getContainerData(State, Cont);
   if (!CDataPtr)
     return nullptr;
 
   return CDataPtr->getEnd();
 }
 
 ProgramStateRef createContainerBegin(ProgramStateRef State,
-                                     const MemRegion *Cont,
-                                     const SymbolRef Sym) {
+                                     const MemRegion *Cont, const Expr *E,
+                                     QualType T, const LocationContext *LCtx,
+                                     unsigned BlockCount) {
   // Only create if it does not exist
   const auto *CDataPtr = getContainerData(State, Cont);
-  if (CDataPtr) {
-    if (CDataPtr->getBegin()) {
-      return State;
-    }
+  if (CDataPtr && CDataPtr->getBegin())
+
+  auto &SymMgr = State->getSymbolManager();
+  auto Sym = SymMgr.conjureSymbol(E, LCtx, T, BlockCount, "begin");
+  State = assumeNoOverflow(State, Sym, 4);
+
+  if (CDataPtr) {
     const auto CData = CDataPtr->newBegin(Sym);
+    if (auto EndSym = CDataPtr->getEnd()) {
+      State = ensureNonNegativeDiff(State, EndSym, Sym);
+    }
     return setContainerData(State, Cont, CData);
   }
+
   const auto CData = ContainerData::fromBegin(Sym);
   return setContainerData(State, Cont, CData);
 }
 
 ProgramStateRef createContainerEnd(ProgramStateRef State, const MemRegion *Cont,
-                                   const SymbolRef Sym) {
+                                   const Expr *E, QualType T,
+                                   const LocationContext *LCtx,
+                                   unsigned BlockCount) {
   // Only create if it does not exist
   const auto *CDataPtr = getContainerData(State, Cont);
-  if (CDataPtr) {
-    if (CDataPtr->getEnd()) {
-      return State;
-    }
+  if (CDataPtr && CDataPtr->getEnd())
+
+  auto &SymMgr = State->getSymbolManager();
+  auto Sym = SymMgr.conjureSymbol(E, LCtx, T, BlockCount, "end");
+  State = assumeNoOverflow(State, Sym, 4);
+
+  if (CDataPtr) {
     const auto CData = CDataPtr->newEnd(Sym);
+    if (auto BeginSym = CDataPtr->getBegin()) {
+      State = ensureNonNegativeDiff(State, Sym, BeginSym);
+    }
     return setContainerData(State, Cont, CData);
   }
+
   const auto CData = ContainerData::fromEnd(Sym);
   return setContainerData(State, Cont, CData);
 }
 
 const ContainerData *getContainerData(ProgramStateRef State,
                                       const MemRegion *Cont) {
   return State->get<ContainerMap>(Cont);
 }

 
 bool isZero(ProgramStateRef State, const NonLoc &Val) {
   auto &BVF = State->getBasicVals();
   return compare(State, Val,
                  nonloc::ConcreteInt(BVF.getValue(llvm::APSInt::get(0))),
                  BO_EQ);
 }
 
+ProgramStateRef ensureNonNegativeDiff(ProgramStateRef State, SymbolRef Sym1,
+                                      SymbolRef Sym2) {
+  // First Try to compare them and get a defined value
+  auto &SVB = State->getStateManager().getSValBuilder();
+
+  auto nonNeg =
+    SVB.evalBinOp(State, BO_GE, nonloc::SymbolVal(Sym1),
+                  nonloc::SymbolVal(Sym2), SVB.getConditionType())
+          .getAs<DefinedSVal>();
+
+  if (nonNeg) {
+    return State->assume(*nonNeg, true);
+  }
+
+  return State;
+}
+
 bool isPastTheEnd(ProgramStateRef State, const IteratorPosition &Pos) {
   const auto *Cont = Pos.getContainer();
   const auto *CData = getContainerData(State, Cont);
   if (!CData)
     return false;
 
   const auto End = CData->getEnd();
   if (End) {