baloghadamsoftware updated this revision to Diff 293183.
baloghadamsoftware added a comment.
New test cases added.
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
@@ -14,6 +14,7 @@
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,
@@ -104,6 +105,125 @@
// 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
Index: clang/lib/StaticAnalyzer/Checkers/Iterator.h
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/Iterator.h
+++ clang/lib/StaticAnalyzer/Checkers/Iterator.h
@@ -187,6 +187,8 @@
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,10 @@
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
@@ -446,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(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 {
@@ -932,7 +1005,8 @@
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);
@@ -955,7 +1029,8 @@
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);
@@ -1129,6 +1204,63 @@
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) {
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
