rnkovacs updated this revision to Diff 143287.
rnkovacs edited the summary of this revision.
rnkovacs added a comment.
Fixed logical operator in the
`Z3ConstraintManager::checkRangedStateConstraints()` function.
https://reviews.llvm.org/D45517
Files:
include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/BugReporter.cpp
lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
lib/StaticAnalyzer/Core/ProgramState.cpp
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
lib/StaticAnalyzer/Core/RangedConstraintManager.h
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -7,6 +7,7 @@
//
//===----------------------------------------------------------------------===//
+#include "RangedConstraintManager.h"
#include "clang/Basic/TargetInfo.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
@@ -915,6 +916,8 @@
void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
const char *sep) override;
+ bool checkRangedStateConstraints(ProgramStateRef State) override;
+
//===------------------------------------------------------------------===//
// Implementation for interface from SimpleConstraintManager.
//===------------------------------------------------------------------===//
@@ -1235,6 +1238,47 @@
return State->set<ConstraintZ3>(CZ);
}
+bool Z3ConstraintManager::checkRangedStateConstraints(ProgramStateRef State) {
+ Solver.reset();
+ ConstraintRangeTy CR = State->get<ConstraintRange>();
+
+ for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+ SymbolRef Sym = I.getKey();
+
+ for (const auto &Range : I.getData()) {
+ const llvm::APSInt &From = Range.From();
+ const llvm::APSInt &To = Range.To();
+
+ assert((getAPSIntType(From) == getAPSIntType(To)) &&
+ "Range values have different types!");
+ QualType RangeTy = getAPSIntType(From);
+ // Skip ranges whose endpoints cannot be converted to APSInts with
+ // a valid APSIntType.
+ if (RangeTy.isNull())
+ continue;
+
+ QualType SymTy;
+ Z3Expr Exp = getZ3Expr(Sym, &SymTy);
+ bool isSignedTy = SymTy->isSignedIntegerOrEnumerationType();
+
+ Z3Expr FromExp = Z3Expr::fromAPSInt(From);
+ Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+
+ if (From == To) {
+ Z3Expr Eq = getZ3BinExpr(Exp, SymTy, BO_EQ, FromExp, RangeTy, nullptr);
+ Solver.addConstraint(Eq);
+ } else {
+ Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr);
+ Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
+ Solver.addConstraint(Z3Expr::fromBinOp(LHS, BO_LOr, RHS, isSignedTy));
+ }
+ }
+ }
+ // If Z3 timeouts, Z3_L_UNDEF is returned, and we assume that the state
+ // is feasible.
+ return Solver.check() != Z3_L_FALSE;
+}
+
//===------------------------------------------------------------------===//
// Internal implementation.
//===------------------------------------------------------------------===//
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.h
===================================================================
--- lib/StaticAnalyzer/Core/RangedConstraintManager.h
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.h
@@ -15,12 +15,124 @@
#define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
namespace clang {
namespace ento {
+/// A Range represents the closed range [from, to]. The caller must
+/// guarantee that from <= to. Note that Range is immutable, so as not
+/// to subvert RangeSet's immutability.
+class Range : public std::pair<const llvm::APSInt *, const llvm::APSInt *> {
+public:
+ Range(const llvm::APSInt &from, const llvm::APSInt &to)
+ : std::pair<const llvm::APSInt *, const llvm::APSInt *>(&from, &to) {
+ assert(from <= to);
+ }
+ bool Includes(const llvm::APSInt &v) const {
+ return *first <= v && v <= *second;
+ }
+ const llvm::APSInt &From() const { return *first; }
+ const llvm::APSInt &To() const { return *second; }
+ const llvm::APSInt *getConcreteValue() const {
+ return &From() == &To() ? &From() : nullptr;
+ }
+
+ void Profile(llvm::FoldingSetNodeID &ID) const {
+ ID.AddPointer(&From());
+ ID.AddPointer(&To());
+ }
+};
+
+class RangeTrait : public llvm::ImutContainerInfo<Range> {
+public:
+ // When comparing if one Range is less than another, we should compare
+ // the actual APSInt values instead of their pointers. This keeps the order
+ // consistent (instead of comparing by pointer values) and can potentially
+ // be used to speed up some of the operations in RangeSet.
+ static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
+ return *lhs.first < *rhs.first ||
+ (!(*rhs.first < *lhs.first) && *lhs.second < *rhs.second);
+ }
+};
+
+/// RangeSet contains a set of ranges. If the set is empty, then
+/// there the value of a symbol is overly constrained and there are no
+/// possible values for that symbol.
+class RangeSet {
+ typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
+ PrimRangeSet ranges; // no need to make const, since it is an
+ // ImmutableSet - this allows default operator=
+ // to work.
+public:
+ typedef PrimRangeSet::Factory Factory;
+ typedef PrimRangeSet::iterator iterator;
+
+ RangeSet(PrimRangeSet RS) : ranges(RS) {}
+
+ /// Create a new set with all ranges of this set and RS.
+ /// Possible intersections are not checked here.
+ RangeSet addRange(Factory &F, const RangeSet &RS) {
+ PrimRangeSet Ranges(RS.ranges);
+ for (const auto &range : ranges)
+ Ranges = F.add(Ranges, range);
+ return RangeSet(Ranges);
+ }
+
+ iterator begin() const { return ranges.begin(); }
+ iterator end() const { return ranges.end(); }
+
+ bool isEmpty() const { return ranges.isEmpty(); }
+
+ /// Construct a new RangeSet representing '{ [from, to] }'.
+ RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
+ : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
+
+ /// Profile - Generates a hash profile of this RangeSet for use
+ /// by FoldingSet.
+ void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
+
+ /// getConcreteValue - If a symbol is contrained to equal a specific integer
+ /// constant then this method returns that value. Otherwise, it returns
+ /// NULL.
+ const llvm::APSInt *getConcreteValue() const {
+ return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
+ }
+
+private:
+ void IntersectInRange(BasicValueFactory &BV, Factory &F,
+ const llvm::APSInt &Lower, const llvm::APSInt &Upper,
+ PrimRangeSet &newRanges, PrimRangeSet::iterator &i,
+ PrimRangeSet::iterator &e) const;
+
+ const llvm::APSInt &getMinValue() const;
+
+ bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const;
+
+public:
+ RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower,
+ llvm::APSInt Upper) const;
+
+ void print(raw_ostream &os) const;
+
+ bool operator==(const RangeSet &other) const {
+ return ranges == other.ranges;
+ }
+};
+
+
+class ConstraintRange {};
+using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;
+
+template <>
+struct ProgramStateTrait<ConstraintRange>
+ : public ProgramStatePartialTrait<ConstraintRangeTy> {
+ static void *GDMIndex() { static int Index; return &Index; }
+};
+
+
class RangedConstraintManager : public SimpleConstraintManager {
public:
RangedConstraintManager(SubEngine *SE, SValBuilder &SB)
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -23,263 +23,171 @@
using namespace clang;
using namespace ento;
-/// A Range represents the closed range [from, to]. The caller must
-/// guarantee that from <= to. Note that Range is immutable, so as not
-/// to subvert RangeSet's immutability.
-namespace {
-class Range : public std::pair<const llvm::APSInt *, const llvm::APSInt *> {
-public:
- Range(const llvm::APSInt &from, const llvm::APSInt &to)
- : std::pair<const llvm::APSInt *, const llvm::APSInt *>(&from, &to) {
- assert(from <= to);
- }
- bool Includes(const llvm::APSInt &v) const {
- return *first <= v && v <= *second;
- }
- const llvm::APSInt &From() const { return *first; }
- const llvm::APSInt &To() const { return *second; }
- const llvm::APSInt *getConcreteValue() const {
- return &From() == &To() ? &From() : nullptr;
- }
-
- void Profile(llvm::FoldingSetNodeID &ID) const {
- ID.AddPointer(&From());
- ID.AddPointer(&To());
- }
-};
-
-class RangeTrait : public llvm::ImutContainerInfo<Range> {
-public:
- // When comparing if one Range is less than another, we should compare
- // the actual APSInt values instead of their pointers. This keeps the order
- // consistent (instead of comparing by pointer values) and can potentially
- // be used to speed up some of the operations in RangeSet.
- static inline bool isLess(key_type_ref lhs, key_type_ref rhs) {
- return *lhs.first < *rhs.first ||
- (!(*rhs.first < *lhs.first) && *lhs.second < *rhs.second);
- }
-};
-
-/// RangeSet contains a set of ranges. If the set is empty, then
-/// there the value of a symbol is overly constrained and there are no
-/// possible values for that symbol.
-class RangeSet {
- typedef llvm::ImmutableSet<Range, RangeTrait> PrimRangeSet;
- PrimRangeSet ranges; // no need to make const, since it is an
- // ImmutableSet - this allows default operator=
- // to work.
-public:
- typedef PrimRangeSet::Factory Factory;
- typedef PrimRangeSet::iterator iterator;
-
- RangeSet(PrimRangeSet RS) : ranges(RS) {}
-
- /// Create a new set with all ranges of this set and RS.
- /// Possible intersections are not checked here.
- RangeSet addRange(Factory &F, const RangeSet &RS) {
- PrimRangeSet Ranges(RS.ranges);
- for (const auto &range : ranges)
- Ranges = F.add(Ranges, range);
- return RangeSet(Ranges);
- }
-
- iterator begin() const { return ranges.begin(); }
- iterator end() const { return ranges.end(); }
-
- bool isEmpty() const { return ranges.isEmpty(); }
-
- /// Construct a new RangeSet representing '{ [from, to] }'.
- RangeSet(Factory &F, const llvm::APSInt &from, const llvm::APSInt &to)
- : ranges(F.add(F.getEmptySet(), Range(from, to))) {}
-
- /// Profile - Generates a hash profile of this RangeSet for use
- /// by FoldingSet.
- void Profile(llvm::FoldingSetNodeID &ID) const { ranges.Profile(ID); }
-
- /// getConcreteValue - If a symbol is contrained to equal a specific integer
- /// constant then this method returns that value. Otherwise, it returns
- /// NULL.
- const llvm::APSInt *getConcreteValue() const {
- return ranges.isSingleton() ? ranges.begin()->getConcreteValue() : nullptr;
- }
+void RangeSet::IntersectInRange(BasicValueFactory &BV, Factory &F,
+ const llvm::APSInt &Lower, const llvm::APSInt &Upper,
+ PrimRangeSet &newRanges, PrimRangeSet::iterator &i,
+ PrimRangeSet::iterator &e) const {
+ // There are six cases for each range R in the set:
+ // 1. R is entirely before the intersection range.
+ // 2. R is entirely after the intersection range.
+ // 3. R contains the entire intersection range.
+ // 4. R starts before the intersection range and ends in the middle.
+ // 5. R starts in the middle of the intersection range and ends after it.
+ // 6. R is entirely contained in the intersection range.
+ // These correspond to each of the conditions below.
+ for (/* i = begin(), e = end() */; i != e; ++i) {
+ if (i->To() < Lower) {
+ continue;
+ }
+ if (i->From() > Upper) {
+ break;
+ }
-private:
- void IntersectInRange(BasicValueFactory &BV, Factory &F,
- const llvm::APSInt &Lower, const llvm::APSInt &Upper,
- PrimRangeSet &newRanges, PrimRangeSet::iterator &i,
- PrimRangeSet::iterator &e) const {
- // There are six cases for each range R in the set:
- // 1. R is entirely before the intersection range.
- // 2. R is entirely after the intersection range.
- // 3. R contains the entire intersection range.
- // 4. R starts before the intersection range and ends in the middle.
- // 5. R starts in the middle of the intersection range and ends after it.
- // 6. R is entirely contained in the intersection range.
- // These correspond to each of the conditions below.
- for (/* i = begin(), e = end() */; i != e; ++i) {
- if (i->To() < Lower) {
- continue;
- }
- if (i->From() > Upper) {
+ if (i->Includes(Lower)) {
+ if (i->Includes(Upper)) {
+ newRanges =
+ F.add(newRanges, Range(BV.getValue(Lower), BV.getValue(Upper)));
break;
- }
-
- if (i->Includes(Lower)) {
- if (i->Includes(Upper)) {
- newRanges =
- F.add(newRanges, Range(BV.getValue(Lower), BV.getValue(Upper)));
- break;
- } else
- newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
- } else {
- if (i->Includes(Upper)) {
- newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
- break;
- } else
- newRanges = F.add(newRanges, *i);
- }
+ } else
+ newRanges = F.add(newRanges, Range(BV.getValue(Lower), i->To()));
+ } else {
+ if (i->Includes(Upper)) {
+ newRanges = F.add(newRanges, Range(i->From(), BV.getValue(Upper)));
+ break;
+ } else
+ newRanges = F.add(newRanges, *i);
}
}
+}
- const llvm::APSInt &getMinValue() const {
- assert(!isEmpty());
- return ranges.begin()->From();
- }
+const llvm::APSInt &RangeSet::getMinValue() const {
+ assert(!isEmpty());
+ return ranges.begin()->From();
+}
- bool pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
- // This function has nine cases, the cartesian product of range-testing
- // both the upper and lower bounds against the symbol's type.
- // Each case requires a different pinning operation.
- // The function returns false if the described range is entirely outside
- // the range of values for the associated symbol.
- APSIntType Type(getMinValue());
- APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower, true);
- APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper, true);
-
- switch (LowerTest) {
+bool RangeSet::pin(llvm::APSInt &Lower, llvm::APSInt &Upper) const {
+ // This function has nine cases, the cartesian product of range-testing
+ // both the upper and lower bounds against the symbol's type.
+ // Each case requires a different pinning operation.
+ // The function returns false if the described range is entirely outside
+ // the range of values for the associated symbol.
+ APSIntType Type(getMinValue());
+ APSIntType::RangeTestResultKind LowerTest = Type.testInRange(Lower, true);
+ APSIntType::RangeTestResultKind UpperTest = Type.testInRange(Upper, true);
+
+ switch (LowerTest) {
+ case APSIntType::RTR_Below:
+ switch (UpperTest) {
case APSIntType::RTR_Below:
- switch (UpperTest) {
- case APSIntType::RTR_Below:
- // The entire range is outside the symbol's set of possible values.
- // If this is a conventionally-ordered range, the state is infeasible.
- if (Lower <= Upper)
- return false;
-
- // However, if the range wraps around, it spans all possible values.
- Lower = Type.getMinValue();
- Upper = Type.getMaxValue();
- break;
- case APSIntType::RTR_Within:
- // The range starts below what's possible but ends within it. Pin.
- Lower = Type.getMinValue();
- Type.apply(Upper);
- break;
- case APSIntType::RTR_Above:
- // The range spans all possible values for the symbol. Pin.
- Lower = Type.getMinValue();
- Upper = Type.getMaxValue();
- break;
- }
+ // The entire range is outside the symbol's set of possible values.
+ // If this is a conventionally-ordered range, the state is infeasible.
+ if (Lower <= Upper)
+ return false;
+
+ // However, if the range wraps around, it spans all possible values.
+ Lower = Type.getMinValue();
+ Upper = Type.getMaxValue();
break;
case APSIntType::RTR_Within:
- switch (UpperTest) {
- case APSIntType::RTR_Below:
- // The range wraps around, but all lower values are not possible.
- Type.apply(Lower);
- Upper = Type.getMaxValue();
- break;
- case APSIntType::RTR_Within:
- // The range may or may not wrap around, but both limits are valid.
- Type.apply(Lower);
- Type.apply(Upper);
- break;
- case APSIntType::RTR_Above:
- // The range starts within what's possible but ends above it. Pin.
- Type.apply(Lower);
- Upper = Type.getMaxValue();
- break;
- }
+ // The range starts below what's possible but ends within it. Pin.
+ Lower = Type.getMinValue();
+ Type.apply(Upper);
break;
case APSIntType::RTR_Above:
- switch (UpperTest) {
- case APSIntType::RTR_Below:
- // The range wraps but is outside the symbol's set of possible values.
- return false;
- case APSIntType::RTR_Within:
- // The range starts above what's possible but ends within it (wrap).
- Lower = Type.getMinValue();
- Type.apply(Upper);
- break;
- case APSIntType::RTR_Above:
- // The entire range is outside the symbol's set of possible values.
- // If this is a conventionally-ordered range, the state is infeasible.
- if (Lower <= Upper)
- return false;
-
- // However, if the range wraps around, it spans all possible values.
- Lower = Type.getMinValue();
- Upper = Type.getMaxValue();
- break;
- }
+ // The range spans all possible values for the symbol. Pin.
+ Lower = Type.getMinValue();
+ Upper = Type.getMaxValue();
+ break;
+ }
+ break;
+ case APSIntType::RTR_Within:
+ switch (UpperTest) {
+ case APSIntType::RTR_Below:
+ // The range wraps around, but all lower values are not possible.
+ Type.apply(Lower);
+ Upper = Type.getMaxValue();
+ break;
+ case APSIntType::RTR_Within:
+ // The range may or may not wrap around, but both limits are valid.
+ Type.apply(Lower);
+ Type.apply(Upper);
+ break;
+ case APSIntType::RTR_Above:
+ // The range starts within what's possible but ends above it. Pin.
+ Type.apply(Lower);
+ Upper = Type.getMaxValue();
break;
}
+ break;
+ case APSIntType::RTR_Above:
+ switch (UpperTest) {
+ case APSIntType::RTR_Below:
+ // The range wraps but is outside the symbol's set of possible values.
+ return false;
+ case APSIntType::RTR_Within:
+ // The range starts above what's possible but ends within it (wrap).
+ Lower = Type.getMinValue();
+ Type.apply(Upper);
+ break;
+ case APSIntType::RTR_Above:
+ // The entire range is outside the symbol's set of possible values.
+ // If this is a conventionally-ordered range, the state is infeasible.
+ if (Lower <= Upper)
+ return false;
- return true;
+ // However, if the range wraps around, it spans all possible values.
+ Lower = Type.getMinValue();
+ Upper = Type.getMaxValue();
+ break;
+ }
+ break;
}
-public:
- // Returns a set containing the values in the receiving set, intersected with
- // the closed range [Lower, Upper]. Unlike the Range type, this range uses
- // modular arithmetic, corresponding to the common treatment of C integer
- // overflow. Thus, if the Lower bound is greater than the Upper bound, the
- // range is taken to wrap around. This is equivalent to taking the
- // intersection with the two ranges [Min, Upper] and [Lower, Max],
- // or, alternatively, /removing/ all integers between Upper and Lower.
- RangeSet Intersect(BasicValueFactory &BV, Factory &F, llvm::APSInt Lower,
- llvm::APSInt Upper) const {
- if (!pin(Lower, Upper))
- return F.getEmptySet();
-
- PrimRangeSet newRanges = F.getEmptySet();
-
- PrimRangeSet::iterator i = begin(), e = end();
- if (Lower <= Upper)
- IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
- else {
- // The order of the next two statements is important!
- // IntersectInRange() does not reset the iteration state for i and e.
- // Therefore, the lower range most be handled first.
- IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
- IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
- }
+ return true;
+}
- return newRanges;
- }
+// Returns a set containing the values in the receiving set, intersected with
+// the closed range [Lower, Upper]. Unlike the Range type, this range uses
+// modular arithmetic, corresponding to the common treatment of C integer
+// overflow. Thus, if the Lower bound is greater than the Upper bound, the
+// range is taken to wrap around. This is equivalent to taking the
+// intersection with the two ranges [Min, Upper] and [Lower, Max],
+// or, alternatively, /removing/ all integers between Upper and Lower.
+RangeSet RangeSet::Intersect(BasicValueFactory &BV, Factory &F,
+ llvm::APSInt Lower, llvm::APSInt Upper) const {
+ if (!pin(Lower, Upper))
+ return F.getEmptySet();
- void print(raw_ostream &os) const {
- bool isFirst = true;
- os << "{ ";
- for (iterator i = begin(), e = end(); i != e; ++i) {
- if (isFirst)
- isFirst = false;
- else
- os << ", ";
-
- os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
- << ']';
- }
- os << " }";
+ PrimRangeSet newRanges = F.getEmptySet();
+
+ PrimRangeSet::iterator i = begin(), e = end();
+ if (Lower <= Upper)
+ IntersectInRange(BV, F, Lower, Upper, newRanges, i, e);
+ else {
+ // The order of the next two statements is important!
+ // IntersectInRange() does not reset the iteration state for i and e.
+ // Therefore, the lower range most be handled first.
+ IntersectInRange(BV, F, BV.getMinValue(Upper), Upper, newRanges, i, e);
+ IntersectInRange(BV, F, Lower, BV.getMaxValue(Lower), newRanges, i, e);
}
- bool operator==(const RangeSet &other) const {
- return ranges == other.ranges;
- }
-};
-} // end anonymous namespace
+ return newRanges;
+}
-REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintRange,
- CLANG_ENTO_PROGRAMSTATE_MAP(SymbolRef,
- RangeSet))
+void RangeSet::print(raw_ostream &os) const {
+ bool isFirst = true;
+ os << "{ ";
+ for (iterator i = begin(), e = end(); i != e; ++i) {
+ if (isFirst)
+ isFirst = false;
+ else
+ os << ", ";
+
+ os << '[' << i->From().toString(10) << ", " << i->To().toString(10)
+ << ']';
+ }
+ os << " }";
+}
namespace {
class RangeConstraintManager : public RangedConstraintManager {
Index: lib/StaticAnalyzer/Core/ProgramState.cpp
===================================================================
--- lib/StaticAnalyzer/Core/ProgramState.cpp
+++ lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -13,6 +13,8 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/Analysis/CFG.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
@@ -78,6 +80,10 @@
CallEventMgr(new CallEventManager(alloc)), Alloc(alloc) {
StoreMgr = (*CreateSMgr)(*this);
ConstraintMgr = (*CreateCMgr)(*this, SubEng);
+ AnalyzerOptions &Opts = SubEng->getAnalysisManager().getAnalyzerOptions();
+ RefutationMgr = Opts.shouldPostProcessBugReports()
+ ? CreateZ3ConstraintManager(*this, SubEng)
+ : nullptr;
}
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2333,3 +2333,26 @@
return std::move(Piece);
}
+
+std::shared_ptr<PathDiagnosticPiece>
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *Succ,
+ const ExplodedNode *Prev,
+ BugReporterContext &BRC,
+ BugReport &BR) {
+ if (isInvalidated)
+ return nullptr;
+
+ if (Succ->getLocation().getKind() != ProgramPoint::BlockEdgeKind)
+ return nullptr;
+
+ ConstraintManager &RefutationMgr =
+ BRC.getStateManager().getRefutationManager();
+
+ if (!RefutationMgr.checkRangedStateConstraints(Succ->getState())) {
+ const LocationContext *LC = Succ->getLocationContext();
+ BR.markInvalid("Infeasible constraints", LC);
+ isInvalidated = true;
+ }
+
+ return nullptr;
+}
Index: lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporter.cpp
+++ lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -3149,6 +3149,9 @@
R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>());
R->addVisitor(llvm::make_unique<CXXSelfAssignmentBRVisitor>());
+ if (getAnalyzerOptions().shouldPostProcessBugReports())
+ R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
+
BugReport::VisitorList visitors;
unsigned origReportConfigToken, finalReportConfigToken;
LocationContextMap LCM;
Index: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
===================================================================
--- lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
+++ lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
@@ -296,6 +296,12 @@
/* Default = */ true);
}
+bool AnalyzerOptions::shouldPostProcessBugReports() {
+ return getBooleanOption(PostProcessBugReports,
+ "postprocess-reports",
+ /* Default = */ false);
+}
+
bool AnalyzerOptions::shouldReportIssuesInMainSourceFile() {
return getBooleanOption(ReportIssuesInMainSourceFile,
"report-in-main-source-file",
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h
@@ -475,6 +475,7 @@
EnvironmentManager EnvMgr;
std::unique_ptr<StoreManager> StoreMgr;
std::unique_ptr<ConstraintManager> ConstraintMgr;
+ std::unique_ptr<ConstraintManager> RefutationMgr;
ProgramState::GenericDataMap::Factory GDMFactory;
TaintedSubRegions::Factory TSRFactory;
@@ -540,6 +541,7 @@
StoreManager& getStoreManager() { return *StoreMgr; }
ConstraintManager& getConstraintManager() { return *ConstraintMgr; }
+ ConstraintManager& getRefutationManager() { return *RefutationMgr; }
SubEngine* getOwningEngine() { return Eng; }
ProgramStateRef removeDeadBindings(ProgramStateRef St,
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -175,6 +175,10 @@
return checkNull(State, Sym);
}
+ virtual bool checkRangedStateConstraints(ProgramStateRef State) {
+ return true;
+ }
+
protected:
/// A flag to indicate that clients should be notified of assumptions.
/// By default this is the case, but sometimes this needs to be restricted
Index: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
===================================================================
--- include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -343,6 +343,24 @@
BugReport &BR) override;
};
+class FalsePositiveRefutationBRVisitor final
+ : public BugReporterVisitorImpl<FalsePositiveRefutationBRVisitor> {
+ bool isInvalidated = false;
+
+public:
+ FalsePositiveRefutationBRVisitor() = default;
+
+ void Profile(llvm::FoldingSetNodeID &ID) const override {
+ static int Tag = 0;
+ ID.AddPointer(&Tag);
+ }
+
+ std::shared_ptr<PathDiagnosticPiece> VisitNode(const ExplodedNode *Succ,
+ const ExplodedNode *Prev,
+ BugReporterContext &BRC,
+ BugReport &BR) override;
+};
+
namespace bugreporter {
/// Attempts to add visitors to trace a null or undefined value back to its
Index: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
===================================================================
--- include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
+++ include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
@@ -280,6 +280,9 @@
/// \sa shouldSuppressFromCXXStandardLibrary
Optional<bool> SuppressFromCXXStandardLibrary;
+ /// \sa shouldPostProcessBugReports
+ Optional<bool> PostProcessBugReports;
+
/// \sa reportIssuesInMainSourceFile
Optional<bool> ReportIssuesInMainSourceFile;
@@ -575,6 +578,13 @@
/// which accepts the values "true" and "false".
bool shouldSuppressFromCXXStandardLibrary();
+ /// Returns whether bug reports should be postprocessed using the Z3
+ /// constraint manager backend.
+ ///
+ /// This is controlled by the 'postprocess-reports' config option,
+ /// which accepts the values "true" and "false".
+ bool shouldPostProcessBugReports();
+
/// Returns whether or not the diagnostic report should be always reported
/// in the main source file and not the headers.
///
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
