[Analyzer] Model `size()` member function of containers

[baloghadamsoftware]

Summary

After empty(), also model size() to further improve existing checkers and enable more future checkers for iterators and containers.

[baloghadamsoftware]

Supersedes D62724.

[martong]

clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp

458

Just out of curiosity: How do we handle containers that do not have a contiguous memory region? Balanced trees, bucketed hash-maps, etc.

484–485

How? I don't see how does it access the size.

494

What if we have both RetSize and CalcSize? Should we check their values for consistency? (And perhaps adding another sink node if we have inconsistency?)

[Szelethus]

clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp

458

I suspect that this is referring to the memory address of the container object, not the storage of the elements.

[baloghadamsoftware]

Rebased.

[baloghadamsoftware]

Fixes.

[baloghadamsoftware]

clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp

458

Yes. The region just serves to identify the container. It is not necessarily the region where the data is stored.

484–485

As explained between the parenthesis, the actual size of the container is the difference between its begin() and its end(). If we have this difference, then we know the actual size. The other value we may have is the return value of the size() function. We either have one of them, both or none. If we have one, then we adjust the other. If we have both, then we check for consistency, and generated a sink if they are inconsistent. If we have none, then we do nothing.

494

This is handled in the if branch: having CalcSize means that we know the difference between the begin() and the end(), thus inconsistency between RetSize and CalcSize is the same as inconstistency between CalcEnd and EndSym. The comment above explains that if there is such inconsistency, then relateSymbols() returns a null pointer which we assign to State. At the end of this functions we generate a sink whenever State is a null pointer.

[martong]

This basically looks good to me.

clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp

484–485

Ok, makes sense.

494

Ok. Perhpas we could move the relevant comment just right about the call of relateSymbols().

[baloghadamsoftware]

New test cases added.

clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp

class ContainerModeling
   // - Iter (or Iter1 and Iter2): Iterator parameters
 
   void handleBegin(CheckerContext &C, const Expr *CE, const Expr *ContE,
                    SVal Cont, SVal RetVal) const;
   void handleEnd(CheckerContext &C, const Expr *CE, const Expr *ContE,
                  SVal Cont, SVal RetVal) const;
   void handleEmpty(CheckerContext &C, const Expr *CE, const Expr *ContE,
                    SVal Cont, SVal RetVal) const;
+  void handleSize(CheckerContext &C, const Expr *CE, const Expr *ContE,
+                  SVal Cont, SVal RetVal) const;
   void handleAssign(CheckerContext &C, const Expr *CE, const Expr *ContE,
                     SVal Cont, SVal RetVal) const;
   void handleClear(CheckerContext &C, const Expr *CE, const Expr *ContE,
                    SVal Cont, SVal RetVal) const;
   void handlePushBack(CheckerContext &C, const Expr *CE, const Expr *ContE,
                       SVal Cont, SVal RetVal) const;
   void handlePopBack(CheckerContext &C, const Expr *CE, const Expr *ContE,
                      SVal Cont, SVal RetVal) const;
CallDescriptionMap<ZeroItParamFn> ZeroIterParamFunctions = {
     // Iterators
     {{0, "cbegin", 0}, &ContainerModeling::handleBegin},
     {{0, "cend", 0}, &ContainerModeling::handleEnd},
     {{0, "begin", 0}, &ContainerModeling::handleBegin},
     {{0, "end", 0}, &ContainerModeling::handleEnd},
 
     // Capacity
     {{0, "empty", 0}, &ContainerModeling::handleEmpty},
+    {{0, "size", 0}, &ContainerModeling::handleSize},
 
     // Modifiers
     {{0, "clear", 0}, &ContainerModeling::handleClear},
     {{0, "assign", 2}, &ContainerModeling::handleAssign},
     {{0, "push_back", 1}, &ContainerModeling::handlePushBack},
     {{0, "emplace_back", 1}, &ContainerModeling::handlePushBack},
     {{0, "pop_back", 0}, &ContainerModeling::handlePopBack},
     {{0, "push_front", 1}, &ContainerModeling::handlePushFront},
ProgramStateRef reassignAllIteratorPositionsUnless(ProgramStateRef State,
                                                    SymbolRef Offset,
                                                    BinaryOperator::Opcode Opc);
 ProgramStateRef rebaseSymbolInIteratorPositionsIf(
     ProgramStateRef State, SValBuilder &SVB, SymbolRef OldSym,
     SymbolRef NewSym, SymbolRef CondSym, BinaryOperator::Opcode Opc);
 SymbolRef rebaseSymbol(ProgramStateRef State, SValBuilder &SVB, SymbolRef Expr,
                         SymbolRef OldSym, SymbolRef NewSym);
 bool hasLiveIterators(ProgramStateRef State, const MemRegion *Cont);
+const llvm::APSInt* calculateSize(ProgramStateRef State, SymbolRef Begin,
+                                  SymbolRef End);
+ProgramStateRef ensureNonNegativeSize(ProgramStateRef State,
+                                      const MemRegion *Cont);
 
 } // namespace
 
 void ContainerModeling::checkPostCall(const CallEvent &Call,
                                      CheckerContext &C) const {
   const auto *Func = dyn_cast_or_null<FunctionDecl>(Call.getDecl());
   if (!Func)
     return;
if (const auto DefRetVal = RetVal.getAs<DefinedSVal>()) {
     if (StateEmpty)
       C.addTransition(StateEmpty);
 
     if (StateNonEmpty)
       C.addTransition(StateNonEmpty);
   }
 }
 
+void ContainerModeling::handleSize(CheckerContext &C, const Expr *CE,
+                                   const Expr *, SVal Cont, SVal RetVal) const {
+  const auto *ContReg = Cont.getAsRegion();
+  if (!ContReg)
+    return;
+
+  ContReg = ContReg->getMostDerivedObjectRegion();
+
+  auto State = C.getState();
+
+  State = createContainerBegin(State, ContReg, CE, C.getASTContext().LongTy,
+                               C.getLocationContext(), C.blockCount());
+  auto BeginSym = getContainerBegin(State, ContReg);
+  State = createContainerEnd(State, ContReg, CE, C.getASTContext().LongTy,
+                             C.getLocationContext(), C.blockCount());
+  auto EndSym = getContainerEnd(State, ContReg);
+  const llvm::APSInt *CalcSize = calculateSize(State, BeginSym, EndSym);
+
+  auto &SVB = C.getSValBuilder();
+  auto &BVF = State->getBasicVals();
+  const llvm::APSInt *RetSize = nullptr;
+  if (const auto *KnownSize = SVB.getKnownValue(State, RetVal)) {
+    RetSize = &BVF.Convert(C.getASTContext().LongTy, *KnownSize);
+  }
+
+  if (RetSize) {
+    // If the return value is a concrete integer, then try to adjust the size
+    // of the container (the difference between its `begin()` and `end()` to
+    // this size. Function `relateSymbols()` returns null if it contradits
+    // the current size.
+    const auto CalcEnd =
+      SVB.evalBinOp(State, BO_Add, nonloc::SymbolVal(BeginSym),
+                    nonloc::ConcreteInt(*RetSize), C.getASTContext().LongTy)
+      .getAsSymbol();
+    if (CalcEnd) {
+      State = relateSymbols(State, EndSym, CalcEnd, true);
+    }
+  } else {
+    if (CalcSize) {
+      // If the current size is a concrete integer, bind this to the return
+      // value of the function instead of the current one.
+      auto CSize = nonloc::ConcreteInt(BVF.Convert(CE->getType(), *CalcSize));
+      State = State->BindExpr(CE, C.getLocationContext(), CSize);
+    } else {
+      // If neither the returned nor the current size is a concrete integer,
+      // replace the return value with the symbolic difference of the
+      // container's `begin()` and `end()` symbols.
+      auto Size = SVB.evalBinOp(State, BO_Sub, nonloc::SymbolVal(EndSym),
+                                nonloc::SymbolVal(BeginSym),
+                                C.getASTContext().LongTy);
+      if (Size.isUnknown())
+        return;
+
+      auto CastedSize = SVB.evalCast(Size, CE->getType(),
+                                     C.getASTContext().LongTy);
+      State = State->BindExpr(CE, C.getLocationContext(), CastedSize);
+    }
+  }
+
+  if (State) {
+    C.addTransition(State);
+  } else {
+    C.generateSink(State, C.getPredecessor());
+  }
+}
+
 void ContainerModeling::handleAssign(CheckerContext &C, const Expr *CE,
                                      const Expr *, SVal Cont,
                                      SVal RetVal) const {
   const auto *ContReg = Cont.getAsRegion();
   if (!ContReg)
     return;
 
   ContReg = ContReg->getMostDerivedObjectRegion();
ProgramStateRef createContainerBegin(ProgramStateRef State,
 
   auto &SymMgr = State->getSymbolManager();
   const SymbolConjured *Sym = SymMgr.conjureSymbol(E, LCtx, T, BlockCount,
                                                    "begin");
   State = assumeNoOverflow(State, Sym, 4);
 
   if (CDataPtr) {
     const auto CData = CDataPtr->newBegin(Sym);
-    return setContainerData(State, Cont, CData);
+    State = setContainerData(State, Cont, CData);
+    return ensureNonNegativeSize(State, Cont);
   }
 
   const auto CData = ContainerData::fromBegin(Sym);
   return setContainerData(State, Cont, CData);
 }
 
 ProgramStateRef createContainerEnd(ProgramStateRef State, 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 && CDataPtr->getEnd())
     return State;
 
   auto &SymMgr = State->getSymbolManager();
   const SymbolConjured *Sym = SymMgr.conjureSymbol(E, LCtx, T, BlockCount,
                                                   "end");
   State = assumeNoOverflow(State, Sym, 4);
 
   if (CDataPtr) {
     const auto CData = CDataPtr->newEnd(Sym);
-    return setContainerData(State, Cont, CData);
+    State = setContainerData(State, Cont, CData);
+    return ensureNonNegativeSize(State, Cont);
   }
 
   const auto CData = ContainerData::fromEnd(Sym);
   return setContainerData(State, Cont, CData);
 }
 
 ProgramStateRef setContainerData(ProgramStateRef State, const MemRegion *Cont,
                                  const ContainerData &CData) {
bool hasLiveIterators(ProgramStateRef State, const MemRegion *Cont) {
   for (const auto &Sym : SymbolMap) {
     if (Sym.second.getContainer() == Cont)
       return true;
   }
 
   return false;
 }
 
+const llvm::APSInt* calculateSize(ProgramStateRef State, SymbolRef Begin,
+                                  SymbolRef End) {
+  if (!Begin || !End)
+    return nullptr;
+
+  auto &SVB = State->getStateManager().getSValBuilder();
+  auto &SymMgr = State->getSymbolManager();
+  auto Size = SVB.evalBinOp(State, BO_Sub, nonloc::SymbolVal(End),
+                            nonloc::SymbolVal(Begin),
+                            SymMgr.getType(End)).getAsSymbol();
+  if (!Size)
+    return nullptr;
+
+  llvm::APSInt Diff = llvm::APSInt::get(0);
+  if (const auto *SizeExpr = dyn_cast<SymIntExpr>(Size)) {
+    assert(BinaryOperator::isAdditiveOp(SizeExpr->getOpcode()) &&
+           "Symbolic positions must be additive expressions");
+    if (SizeExpr->getOpcode() == BO_Add) {
+      Diff = SizeExpr->getRHS();
+    } else {
+      Diff = -SizeExpr->getRHS();
+    }
+    Size = SizeExpr->getLHS();
+  }
+
+  auto &CM = State->getConstraintManager();
+  if (const auto *SizeInt = CM.getSymVal(State, Size)) {
+    auto &BVF = SymMgr.getBasicVals();
+    return &BVF.getValue(Diff + *SizeInt);
+  }
+
+  return nullptr;
+}
+
+ProgramStateRef ensureNonNegativeSize(ProgramStateRef State,
+                                      const MemRegion *Cont) {
+  const auto *CData = getContainerData(State, Cont);
+  if (!CData)
+    return State;
+
+  SymbolRef BeginSym = CData->getBegin();
+  SymbolRef EndSym = CData->getEnd();
+  if (!BeginSym || !EndSym)
+    return State;
+
+  auto &SVB = State->getStateManager().getSValBuilder();
+  auto NonNegativeSize = SVB.evalBinOp(State, BO_GE,
+                                       nonloc::SymbolVal(EndSym),
+                                       nonloc::SymbolVal(BeginSym),
+                                       SVB.getConditionType())
+    .getAs<DefinedSVal>();
+  assert(NonNegativeSize);
+  State = State->assume(*NonNegativeSize, true);
+  assert(State && "Container size must not be negative.");
+  return State;
+}
+
 } // namespace
 
 void ento::registerContainerModeling(CheckerManager &mgr) {
   mgr.registerChecker<ContainerModeling>();
 }
 
 bool ento::shouldRegisterContainerModeling(const CheckerManager &mgr) {
   if (!mgr.getLangOpts().CPlusPlus)

clang/lib/StaticAnalyzer/Checkers/Iterator.h

 
 // Returns states with comparison results assumed to `true` and `false`. If
 // only one of them is possible then the second value of the pair is `nullptr`.
 // If none is possible then both values are `nullptr`.
 std::pair<ProgramStateRef, ProgramStateRef>
 assumeComparison(ProgramStateRef State, SymbolRef Sym1, SymbolRef Sym2,
                  DefinedSVal RetVal, OverloadedOperatorKind Op);
 
+ProgramStateRef relateSymbols(ProgramStateRef State, SymbolRef Sym1,
+                              SymbolRef Sym2, bool Equal);
 bool compare(ProgramStateRef State, SymbolRef Sym1, SymbolRef Sym2,
              BinaryOperator::Opcode Opc);
 bool compare(ProgramStateRef State, NonLoc NL1, NonLoc NL2,
              BinaryOperator::Opcode Opc);
 
 // Returns the value of the iterator argument if it non-class value (a pointer
 // or a reference). Otherwise it returns the iterator parameter location (see
 // CallEvent::getParameterLocation()).

clang/lib/StaticAnalyzer/Checkers/Iterator.cpp

 #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
 
 #include "Iterator.h"
 
 namespace clang {
 namespace ento {
 namespace iterator {
 
-ProgramStateRef relateSymbols(ProgramStateRef State, SymbolRef Sym1,
-                              SymbolRef Sym2, bool Equal);
-
 bool isIteratorType(const QualType &Type) {
   if (Type->isPointerType())
     return true;
 
   const auto *CRD = Type->getUnqualifiedDesugaredType()->getAsCXXRecordDecl();
   return isIterator(CRD);
 }
 

clang/test/Analysis/container-modeling.cpp

 // RUN: %clang_analyze_cc1 -std=c++11 -analyzer-checker=core,cplusplus,debug.DebugIteratorModeling,debug.ExprInspection -analyzer-config aggressive-binary-operation-simplification=true -analyzer-config c++-container-inlining=false %s -analyzer-output=text -verify
 
 // RUN: %clang_analyze_cc1 -std=c++11 -analyzer-checker=core,cplusplus,debug.DebugIteratorModeling,debug.ExprInspection -analyzer-config aggressive-binary-operation-simplification=true -analyzer-config c++-container-inlining=true -DINLINE=1 %s -analyzer-output=text -verify
 
 // RUN: %clang_analyze_cc1 -std=c++11 -analyzer-checker=core,cplusplus,alpha.cplusplus.IteratorModeling,debug.ExprInspection -analyzer-config aggressive-binary-operation-simplification=true %s 2>&1 | FileCheck %s
 
 #include "Inputs/system-header-simulator-cxx.h"
 
 template <typename Container>
 long clang_analyzer_container_begin(const Container&);
 template <typename Container>
 long clang_analyzer_container_end(const Container&);
 
 void clang_analyzer_denote(long, const char*);
 void clang_analyzer_express(long);
 void clang_analyzer_eval(bool);
+void clang_analyzer_dump(std::size_t);
 void clang_analyzer_warnIfReached();
 
 extern void __assert_fail (__const char *__assertion, __const char *__file,
     unsigned int __line, __const char *__function)
      __attribute__ ((__noreturn__));
 #define assert(expr) \
   ((expr)  ? (void)(0)  : __assert_fail (#expr, __FILE__, __LINE__, __func__))
 
void non_empty2(const std::vector<int> &V) {
   for (auto n: V) {}
   assert(!V.empty()); // expected-note{{'?' condition is true}}
   clang_analyzer_eval(clang_analyzer_container_begin(V) ==
                       clang_analyzer_container_end(V));
   // expected-warning@-2{{FALSE}}
   // expected-note@-3   {{FALSE}}
 }
 
+// size()
+
+void size0(const std::vector<int>& V) {
+  assert(V.size() == 0); // expected-note 2{{'?' condition is true}}
+                         // expected-note@-1 2{{Assuming the condition is true}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{TRUE}}
+  // expected-note@-3   {{TRUE}}
+
+  clang_analyzer_dump(V.size()); // expected-warning{{0}}
+                                 // expected-note@-1{{0}}
+}
+
+void size1(const std::vector<int>& V) {
+  assert(V.size() == 1); // expected-note 2{{'?' condition is true}}
+                         // expected-note@-1 2{{Assuming the condition is true}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 1);
+  // expected-warning@-2{{TRUE}}
+  // expected-note@-3   {{TRUE}}
+
+  clang_analyzer_dump(V.size()); // expected-warning{{1}}
+                                 // expected-note@-1{{1}}
+}
+
+void size2(std::vector<int>& V) {
+  assert(V.size() == 1); // expected-note 2{{'?' condition is true}}
+                         // expected-note@-1 2{{Assuming the condition is true}}
+
+  V.push_back(1);
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 2);
+  // expected-warning@-2{{TRUE}}
+  // expected-note@-3   {{TRUE}}
+
+  clang_analyzer_dump(V.size()); // expected-warning{{2}}
+                                 // expected-note@-1{{2}}
+}
+
+void size3(std::vector<int>& V) {
+  assert(V.size() <= 10); // expected-note 6{{'?' condition is true}}
+                         // expected-note@-1 6{{Assuming the condition is true}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) + 1 ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{FALSE}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{TRUE}} expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{TRUE}} expected-note@-3   {{FALSE}}
+  // expected-note@-4  {{Assuming the condition is true}}
+  // expected-note@-5 4{{Assuming the condition is false}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 10);
+  // expected-warning@-2{{TRUE}} expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{TRUE}} expected-note@-3   {{FALSE}}
+  // expected-note@-4  {{Assuming the condition is true}}
+  // expected-note@-5 2{{Assuming the condition is false}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 11);
+  // expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{FALSE}}
+}
+
+void size4(std::vector<int>& V) {
+  assert(V.size() >= 10); // expected-note 6{{'?' condition is true}}
+                         // expected-note@-1 6{{Assuming the condition is true}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) + 1 ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{FALSE}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{FALSE}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 10);
+  // expected-warning@-2{{TRUE}} expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{TRUE}} expected-note@-3   {{FALSE}}
+  // expected-note@-4  {{Assuming the condition is true}}
+  // expected-note@-5 3{{Assuming the condition is false}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 11);
+  // expected-warning@-2{{TRUE}} expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{TRUE}} expected-note@-3   {{FALSE}}
+  // expected-note@-4{{Assuming the condition is true}}
+  // expected-note@-5{{Assuming the condition is false}}
+}
+
+void size5(std::vector<int>& V) {
+  long s = V.size();
+
+  clang_analyzer_denote(clang_analyzer_container_begin(V), "$V.begin()");
+  clang_analyzer_denote(clang_analyzer_container_end(V), "$V.end()");
+  
+  V.push_back(1);
+
+  clang_analyzer_express(V.size());
+  // expected-warning@-1{{$V.end() - $V.begin() + 1}}
+  // expected-note@-2   {{$V.end() - $V.begin() + 1}}
+  clang_analyzer_express(s + 1);
+  // expected-warning@-1{{$V.end() - $V.begin() + 1}}
+  // expected-note@-2   {{$V.end() - $V.begin() + 1}}
+  clang_analyzer_eval(V.size() == s + 1); // expected-warning{{TRUE}}
+                                          // expected-note@-1{{TRUE}}
+}
+
 ////////////////////////////////////////////////////////////////////////////////
 ///
 /// C O N T A I N E R   M O D I F I E R S
 ///
 ////////////////////////////////////////////////////////////////////////////////
 
 /// push_back()
 ///