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 SuppressFromCXXStandardLibrary; + /// \sa shouldCrosscheckWithZ3 + Optional CrosscheckWithZ3; + /// \sa reportIssuesInMainSourceFile Optional ReportIssuesInMainSourceFile; @@ -575,6 +578,13 @@ /// which accepts the values "true" and "false". bool shouldSuppressFromCXXStandardLibrary(); + /// Returns whether bug reports should be crosschecked with the Z3 + /// constraint manager backend. + /// + /// This is controlled by the 'crosscheck-with-z3' config option, + /// which accepts the values "true" and "false". + bool shouldCrosscheckWithZ3(); + /// Returns whether or not the diagnostic report should be always reported /// in the main source file and not the headers. /// Index: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h =================================================================== --- include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h +++ include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h @@ -17,6 +17,7 @@ #include "clang/Basic/LLVM.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" #include "llvm/ADT/FoldingSet.h" #include "llvm/ADT/STLExtras.h" #include "llvm/ADT/StringRef.h" @@ -359,6 +360,27 @@ BugReport &BR) override; }; +/// The bug visitor will walk all the nodes in a path and collect all the +/// constraints. When it reaches the root node, will encode the constraints +/// and check for satisfiability +class FalsePositiveRefutationBRVisitor final + : public BugReporterVisitorImpl { +private: + /// Holds the constraints in a given path + // TODO: should we use a set? + llvm::SmallVector Constraints; + +public: + FalsePositiveRefutationBRVisitor() = default; + + void Profile(llvm::FoldingSetNodeID &ID) const override; + + std::shared_ptr VisitNode(const ExplodedNode *N, + const ExplodedNode *PrevN, + 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/PathSensitive/ConstraintManager.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h @@ -18,6 +18,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h" +#include "llvm/ADT/ImmutableMap.h" #include "llvm/ADT/Optional.h" #include "llvm/Support/SaveAndRestore.h" #include @@ -33,9 +34,12 @@ namespace ento { class ProgramStateManager; +class RangeSet; class SubEngine; class SymbolReaper; +using ConstraintRangeTy = llvm::ImmutableMap; + class ConditionTruthVal { Optional Val; Index: include/clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h @@ -10,7 +10,7 @@ #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_Z3CONSTRAINTMANAGER_H #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_Z3CONSTRAINTMANAGER_H -#include "clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" #include "clang/Config/config.h" @@ -275,6 +275,14 @@ Z3ConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB); //===------------------------------------------------------------------===// + // Implementation for Refutation. + //===------------------------------------------------------------------===// + + void addRangeConstraints(clang::ento::ConstraintRangeTy CR); + + clang::ento::ConditionTruthVal isModelFeasible(); + + //===------------------------------------------------------------------===// // Implementation for interface from ConstraintManager. //===------------------------------------------------------------------===// Index: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp =================================================================== --- lib/StaticAnalyzer/Core/AnalyzerOptions.cpp +++ lib/StaticAnalyzer/Core/AnalyzerOptions.cpp @@ -296,6 +296,12 @@ /* Default = */ true); } +bool AnalyzerOptions::shouldCrosscheckWithZ3() { + return getBooleanOption(CrosscheckWithZ3, + "crosscheck-with-z3", + /* Default = */ false); +} + bool AnalyzerOptions::shouldReportIssuesInMainSourceFile() { return getBooleanOption(ReportIssuesInMainSourceFile, "report-in-main-source-file", Index: lib/StaticAnalyzer/Core/BugReporter.cpp =================================================================== --- lib/StaticAnalyzer/Core/BugReporter.cpp +++ lib/StaticAnalyzer/Core/BugReporter.cpp @@ -3143,10 +3143,15 @@ PathDiagnosticBuilder PDB(*this, R, ErrorGraph.BackMap, &PC); const ExplodedNode *N = ErrorGraph.ErrorNode; + // Register refutation visitors first, if they mark the bug invalid no + // further analysis is required + R->addVisitor(llvm::make_unique()); + if (getAnalyzerOptions().shouldCrosscheckWithZ3()) + R->addVisitor(llvm::make_unique()); + // Register additional node visitors. R->addVisitor(llvm::make_unique()); R->addVisitor(llvm::make_unique()); - R->addVisitor(llvm::make_unique()); R->addVisitor(llvm::make_unique()); BugReport::VisitorList visitors; Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp =================================================================== --- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -41,6 +41,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h" @@ -2354,3 +2355,42 @@ return std::make_shared(L, "Taint originated here"); } + +static bool +check_constraints(BugReporterContext &BRC, + const llvm::SmallVector &Cs) { + // Create a refutation manager + Z3ConstraintManager Z3RefutationMgr(BRC.getStateManager().getOwningEngine(), + BRC.getStateManager().getSValBuilder()); + + // Add constraints to the solver + for (const auto &C : Cs) + Z3RefutationMgr.addRangeConstraints(C); + + // And check for satisfiability + return Z3RefutationMgr.isModelFeasible().isConstrainedFalse(); +} + +std::shared_ptr +FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N, + const ExplodedNode *PrevN, + BugReporterContext &BRC, + BugReport &BR) { + const ConstraintRangeTy &CR = N->getState()->get(); + Constraints.push_back(CR); + + // If there are no predecessor, we reached the root node. In this point, + // a new refutation manager will be created and the path will be checked + // for reachability + if (PrevN->pred_size() == 0 && check_constraints(BRC, Constraints)) { + BR.markInvalid("Infeasible constraints", N->getLocationContext()); + } + + return nullptr; +} + +void FalsePositiveRefutationBRVisitor::Profile( + llvm::FoldingSetNodeID &ID) const { + static int Tag = 0; + ID.AddPointer(&Tag); +} Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -8,7 +8,7 @@ //===----------------------------------------------------------------------===// #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/Z3ConstraintManager.h" using namespace clang; @@ -1013,6 +1013,50 @@ return State->set(CZ); } +void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) { + for (const auto &I : CR) { + SymbolRef Sym = I.first; + + Z3Expr Constraints = Z3Expr::fromBoolean(false); + + for (const auto &Range : I.second) { + const llvm::APSInt &From = Range.From(); + const llvm::APSInt &To = Range.To(); + + QualType FromTy; + llvm::APSInt NewFromInt; + std::tie(NewFromInt, FromTy) = fixAPSInt(From); + Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt); + + QualType SymTy; + Z3Expr Exp = getZ3Expr(Sym, &SymTy); + bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType(); + + QualType ToTy; + llvm::APSInt NewToInt; + std::tie(NewToInt, ToTy) = fixAPSInt(To); + Z3Expr ToExp = Z3Expr::fromAPSInt(NewToInt); + assert(FromTy == ToTy && "Range values have different types!"); + + Z3Expr LHS = + getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, FromTy, /*RetTy=*/nullptr); + Z3Expr RHS = + getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, FromTy, /*RetTy=*/nullptr); + Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy); + Constraints = + Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy); + } + Solver.addConstraint(Constraints); + } +} + +clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() { + if(Solver.check() == Z3_L_FALSE) + return false; + + return ConditionTruthVal(); +} + //===------------------------------------------------------------------===// // Internal implementation. //===------------------------------------------------------------------===// Index: test/Analysis/z3-crosscheck.c =================================================================== --- /dev/null +++ test/Analysis/z3-crosscheck.c @@ -0,0 +1,57 @@ +// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s +// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s +// REQUIRES: z3 + +#ifndef NO_CROSSCHECK +// expected-no-diagnostics +#endif + +int foo(int x) +{ + int *z = 0; + if ((x & 1) && ((x & 1) ^ 1)) +#ifdef NO_CROSSCHECK + return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}} +#else + return *z; // no-warning +#endif + return 0; +} + +void g(int d); + +void f(int *a, int *b) { + int c = 5; + if ((a - b) == 0) + c = 0; + if (a != b) +#ifdef NO_CROSSCHECK + g(3 / c); // expected-warning {{Division by zero}} +#else + g(3 / c); // no-warning +#endif +} + +_Bool nondet_bool(); + +void h(int d) { + int x, y, k, z = 1; +#ifdef NO_CROSSCHECK + while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}} +#else + // FIXME: Should warn about 'k' being a garbage value + while (z < k) { // no-warning +#endif + z = 2 * z; + } +} + +void i() { + _Bool c = nondet_bool(); + if (c) { + h(1); + } else { + h(2); + } +} +