rnkovacs created this revision.
rnkovacs added reviewers: george.karpenkov, NoQ, dcoughlin.
Herald added subscribers: a.sidorin, szepet, baloghadamsoftware, whisperity,
fhahn.
This is a prototype of a bug reporter visitor that invalidates bug reports by
re-checking constraints of certain states on the bug path using the Z3
constraint manager backend. The functionality is available under the
`postprocess-reports` analyzer config flag.
Results of analysis runs on a few open-source projects with this option turned
on can be explored here <http://cc.elte.hu/refutation.html>.
This work is preliminary and any comments are appreciated. A few remarks:
- In order to work with constraints generated by the range-based constraint
manager outside its own file, much of the `Range`, `RangeTrait` and `RangeSet`
classes have been moved to the corresponding header file.
- The visitor currently checks states appearing as block edges in the exploded
graph. The first idea was to filter states based on the shape of the exploded
graph, by checking the number of successors of the parent node, but
surprisingly, both `succ_size()` and `pred_size()` seemed to return 1 for each
node in the graph (except for the root), even if there clearly were branchings
in the code (and on the `.dot` picture). To my understanding, the exploded
graph is fully constructed at the stage where visitors are run, so I must be
missing something.
- 1-bit APSInts obtained from ranged constraints crashed when
`isSignedIntegerOrEnumerationType()` was called on them inside
`Z3ConstraintManager`'s methods. This issue is currently sidestepped, but they
might be converted to a valid built-in type at some point.
Repository:
rC Clang
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_LAnd, 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
