baloghadamsoftware updated this revision to Diff 282675.
baloghadamsoftware added a comment.
Rebased.
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D76604/new/
https://reviews.llvm.org/D76604
Files:
clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp
clang/lib/StaticAnalyzer/Checkers/Iterator.cpp
clang/lib/StaticAnalyzer/Checkers/Iterator.h
clang/test/Analysis/container-modeling.cpp
Index: clang/test/Analysis/container-modeling.cpp
===================================================================
--- clang/test/Analysis/container-modeling.cpp
+++ clang/test/Analysis/container-modeling.cpp
@@ -96,6 +96,38 @@
// expected-note@-3 {{FALSE}}
}
+void size0(const std::vector<int>& V) {
+ assert(V.size() == 0); // expected-note{{'?' condition is true}}
+ // expected-note@-1{{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}}
+}
+
+void size1(const std::vector<int>& V) {
+ assert(V.size() == 1); // expected-note{{'?' condition is true}}
+ // expected-note@-1{{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}}
+}
+
+void size12(std::vector<int>& V) {
+ assert(V.size() == 1); // expected-note{{'?' condition is true}}
+ // expected-note@-1{{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}}
+}
+
////////////////////////////////////////////////////////////////////////////////
///
/// C O N T A I N E R M O D I F I E R S
Index: clang/lib/StaticAnalyzer/Checkers/Iterator.h
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/Iterator.h
+++ clang/lib/StaticAnalyzer/Checkers/Iterator.h
@@ -182,6 +182,8 @@
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,
Index: clang/lib/StaticAnalyzer/Checkers/Iterator.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/Iterator.cpp
+++ clang/lib/StaticAnalyzer/Checkers/Iterator.cpp
@@ -18,9 +18,6 @@
namespace ento {
namespace iterator {
-ProgramStateRef relateSymbols(ProgramStateRef State, SymbolRef Sym1,
- SymbolRef Sym2, bool Equal);
-
bool isIteratorType(const QualType &Type) {
if (Type->isPointerType())
return true;
Index: clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp
+++ clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp
@@ -47,6 +47,8 @@
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,
@@ -102,6 +104,7 @@
// Capacity
{{0, "empty", 0}, &ContainerModeling::handleEmpty},
+ {{0, "size", 0}, &ContainerModeling::handleSize},
// Modifiers
{{0, "clear", 0}, &ContainerModeling::handleClear},
@@ -170,6 +173,8 @@
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);
} // namespace
@@ -448,6 +453,72 @@
}
}
+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(EndSym),
+ nonloc::ConcreteInt(*RetSize), C.getASTContext().LongTy)
+ .getAsSymbol();
+ if (CalcEnd) {
+ State = relateSymbols(State, BeginSym, EndSym, 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 {
@@ -1131,6 +1202,40 @@
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;
+}
+
} // namespace
void ento::registerContainerModeling(CheckerManager &mgr) {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
