mikhail.ramalho updated this revision to Diff 148828.
mikhail.ramalho retitled this revision from "[analyzer] WIP: False positive
refutation with Z3" to "[analyzer] False positive refutation with Z3".
mikhail.ramalho added a comment.
Added test cases and updated the analyzer-config tests with the new crosscheck
flag.
Currently, there is one test failing that does not fail when building without
the crosscheck:
llvm/tools/clang/test/Driver/response-file.c:18:10: error: expected string
not found in input
// LONG: extern int it_works;
^
<stdin>:1:1: note: scanning from here
clang version 7.0.0 (trunk 333352) (llvm/trunk 333374)
^
<stdin>:8:3: note: possible intended match here
Selected GCC installation: /usr/lib/gcc/x86_64-redhat-linux/6.4.1
^
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,41 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+// expected-no-diagnostics
+
+int foo(int x)
+{
+ int *z = 0;
+ if ((x & 1) && ((x & 1) ^ 1))
+ return *z; // no-warning
+ return 0;
+}
+
+void g(int d);
+
+void f(int *a, int *b) {
+ int c = 5;
+ if ((a - b) == 0)
+ c = 0;
+ if (a != b)
+ g(3 / c); // no-warning
+}
+
+_Bool nondet_bool();
+
+void h(int d) {
+ int x, y, k, z = 1;
+ // FIXME: Should warn about 'k' being a garbage value
+ while (z < k) { // no-warning
+ 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 (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+ SymbolRef Sym = I.getKey();
+
+ if (OnlyPurged && SuccCR.contains(Sym))
+ continue;
+
+ Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+ 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);
+
+ 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,35 @@
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();
+
+ if (FirstNodeVisited) {
+ RefutationMgr.reset();
+ RefutationMgr.addRangeConstraints(PrevCR, SuccCR, /*OnlyPurged=*/false);
+ FirstNodeVisited = false;
+ }
+
+ auto K = Succ->getLocation().getKind();
+ if (K == ProgramPoint::PreStmtPurgeDeadSymbolsKind ||
+ K == ProgramPoint::PostStmtPurgeDeadSymbolsKind) {
+ RefutationMgr.addRangeConstraints(PrevCR, SuccCR, /*OnlyPurged=*/true);
+ }
+
+ if (Prev->pred_size() == 0 && !RefutationMgr.isModelFeasible()) {
+ const LocationContext *LC = Succ->getLocationContext();
+ BR.markInvalid("Infeasible constraints", LC);
+ }
+
+ 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().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,25 @@
BugReport &BR) override;
};
+class FalsePositiveRefutationBRVisitor final
+ : public BugReporterVisitorImpl<FalsePositiveRefutationBRVisitor> {
+ // Flag first node as seen by the visitor.
+ bool FirstNodeVisited = true;
+
+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 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
