mikhail.ramalho updated this revision to Diff 148969.
mikhail.ramalho marked 6 inline comments as done.
mikhail.ramalho added a comment.
1. Moved FalsePositiveRefutationBRVisitor::Profile definition to
BugReporterVisitor.cpp
2. Update test cases two run twice, with and without the crosscheck
3. Removed the FirstNodeVisited flag (the solver is being reset after checking
the bug reachability)
4. Use ranged loop when adding the constraints
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
test/Analysis/analyzer-config.c
test/Analysis/analyzer-config.cpp
test/Analysis/z3-crosscheck.c
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);
+ }
+}
+
Index: test/Analysis/analyzer-config.cpp
===================================================================
--- test/Analysis/analyzer-config.cpp
+++ test/Analysis/analyzer-config.cpp
@@ -32,6 +32,7 @@
// CHECK-NEXT: cfg-rich-constructors = true
// CHECK-NEXT: cfg-scopes = false
// CHECK-NEXT: cfg-temporary-dtors = true
+// CHECK-NEXT: crosscheck-with-z3 = false
// CHECK-NEXT: experimental-enable-naive-ctu-analysis = false
// CHECK-NEXT: exploration_strategy = unexplored_first_queue
// CHECK-NEXT: faux-bodies = true
@@ -50,4 +51,4 @@
// CHECK-NEXT: unroll-loops = false
// CHECK-NEXT: widen-loops = false
// CHECK-NEXT: [stats]
-// CHECK-NEXT: num-entries = 30
+// CHECK-NEXT: num-entries = 31
Index: test/Analysis/analyzer-config.c
===================================================================
--- test/Analysis/analyzer-config.c
+++ test/Analysis/analyzer-config.c
@@ -18,6 +18,7 @@
// CHECK-NEXT: cfg-rich-constructors = true
// CHECK-NEXT: cfg-scopes = false
// CHECK-NEXT: cfg-temporary-dtors = true
+// CHECK-NEXT: crosscheck-with-z3 = false
// CHECK-NEXT: exploration_strategy = unexplored_first_queue
// CHECK-NEXT: faux-bodies = true
// CHECK-NEXT: graph-trim-interval = 1000
@@ -35,4 +36,4 @@
// CHECK-NEXT: unroll-loops = false
// CHECK-NEXT: widen-loops = false
// CHECK-NEXT: [stats]
-// CHECK-NEXT: num-entries = 23
+// CHECK-NEXT: num-entries = 24
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,13 @@
void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
const char *sep) override;
+ void reset() override;
+
+ bool isModelFeasible() override;
+
+ void addRangeConstraints(ConstraintRangeTy PrevCR, ConstraintRangeTy SuccCR,
+ bool OnlyPurged) override;
+
//===------------------------------------------------------------------===//
// Implementation for interface from SimpleConstraintManager.
//===------------------------------------------------------------------===//
@@ -1235,6 +1243,58 @@
return State->set<ConstraintZ3>(CZ);
}
+void Z3ConstraintManager::reset() { Solver.reset(); }
+
+bool Z3ConstraintManager::isModelFeasible() {
+ return Solver.check() != Z3_L_FALSE;
+}
+
+void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy PrevCR,
+ ConstraintRangeTy SuccCR,
+ bool OnlyPurged) {
+ if (OnlyPurged && PrevCR.isEmpty())
+ return;
+ if (!OnlyPurged && SuccCR.isEmpty())
+ return;
+ ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR;
+
+ for (auto const &I : CR) {
+ SymbolRef Sym = I.first;
+
+ if (OnlyPurged && SuccCR.contains(Sym))
+ continue;
+
+ Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+ for (const auto &Range : I.second) {
+ 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);
+
+ Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr);
+ Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
+ Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy);
+ Constraints =
+ Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+ }
+ Solver.addConstraint(Constraints);
+ }
+}
+
//===------------------------------------------------------------------===//
// 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.shouldCrosscheckWithZ3()
+ ? CreateZ3ConstraintManager(*this, SubEng)
+ : nullptr;
}
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 "RangedConstraintManager.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,38 @@
return std::make_shared<PathDiagnosticEventPiece>(L, "Taint originated here");
}
+
+std::shared_ptr<PathDiagnosticPiece>
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *Succ,
+ const ExplodedNode *Prev,
+ BugReporterContext &BRC,
+ BugReport &BR) {
+
+ const ConstraintRangeTy SuccCR = Succ->getState()->get<ConstraintRange>();
+ const ConstraintRangeTy PrevCR = Prev->getState()->get<ConstraintRange>();
+
+ ConstraintManager &RefutationMgr =
+ BRC.getStateManager().getRefutationManager();
+
+ RefutationMgr.addRangeConstraints(PrevCR, SuccCR,
+ Succ->getLocation().isPurgeKind());
+
+ // Reached root node, encode the path and check for satisfatiability
+ if (Prev->pred_size() == 0) {
+ if (!RefutationMgr.isModelFeasible()) {
+ // If the bug is not reachable, mark it as invalid
+ BR.markInvalid("Infeasible constraints", Succ->getLocationContext());
+ }
+
+ // Reset the solver
+ RefutationMgr.reset();
+ }
+
+ return nullptr;
+}
+
+void FalsePositiveRefutationBRVisitor::Profile(
+ llvm::FoldingSetNodeID &ID) const {
+ static int Tag = 0;
+ ID.AddPointer(&Tag);
+}
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().shouldCrosscheckWithZ3())
+ 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::shouldCrosscheckWithZ3() {
+ return getBooleanOption(CrosscheckWithZ3,
+ "crosscheck-with-z3",
+ /* 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
@@ -493,6 +493,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;
@@ -558,6 +559,11 @@
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
@@ -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 <memory>
@@ -33,9 +34,12 @@
namespace ento {
class ProgramStateManager;
+class RangeSet;
class SubEngine;
class SymbolReaper;
+using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;
+
class ConditionTruthVal {
Optional<bool> Val;
@@ -175,6 +179,12 @@
return checkNull(State, Sym);
}
+ virtual void reset() {}
+ virtual bool isModelFeasible() { return true; }
+ virtual void addRangeConstraints(ConstraintRangeTy PrevCR,
+ ConstraintRangeTy SuccCR,
+ bool OnlyPurged) {}
+
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
@@ -359,6 +359,20 @@
BugReport &BR) override;
};
+class FalsePositiveRefutationBRVisitor final
+ : public BugReporterVisitorImpl<FalsePositiveRefutationBRVisitor> {
+
+public:
+ FalsePositiveRefutationBRVisitor() = default;
+
+ void Profile(llvm::FoldingSetNodeID &ID) const override;
+
+ 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 shouldCrosscheckWithZ3
+ Optional<bool> CrosscheckWithZ3;
+
/// \sa reportIssuesInMainSourceFile
Optional<bool> 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.
///
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
