rnkovacs updated this revision to Diff 143440.
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/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/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
