mikhail.ramalho updated this revision to Diff 149524.
mikhail.ramalho added a comment.
- Simplified the API even further by constructing a Z3ConstraintManager object
directly.
- Update isModelFeasible to return a isModelFeasible
- Update code with the fix for 1-bit long integer
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/Z3ConstraintManager.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/BugReporter.cpp
lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
lib/StaticAnalyzer/Core/Z3ConstraintManager.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: 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<ConstraintZ3>(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: 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<PathDiagnosticEventPiece>(L, "Taint originated here");
}
+
+static bool
+check_constraints(BugReporterContext &BRC,
+ const llvm::SmallVector<ConstraintRangeTy, 32> &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<PathDiagnosticPiece>
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
+ const ExplodedNode *PrevN,
+ BugReporterContext &BRC,
+ BugReport &BR) {
+ const ConstraintRangeTy &CR = N->getState()->get<ConstraintRange>();
+ 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/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<LikelyFalsePositiveSuppressionBRVisitor>());
+ if (getAnalyzerOptions().shouldCrosscheckWithZ3())
+ R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
+
// Register additional node visitors.
R->addVisitor(llvm::make_unique<NilReceiverBRVisitor>());
R->addVisitor(llvm::make_unique<ConditionBRVisitor>());
- R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>());
R->addVisitor(llvm::make_unique<CXXSelfAssignmentBRVisitor>());
BugReport::VisitorList visitors;
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/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: 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;
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<FalsePositiveRefutationBRVisitor> {
+private:
+ /// Holds the constraints in a given path
+ // TODO: should we use a set?
+ llvm::SmallVector<ConstraintRangeTy, 32> Constraints;
+
+public:
+ FalsePositiveRefutationBRVisitor() = default;
+
+ void Profile(llvm::FoldingSetNodeID &ID) const override;
+
+ std::shared_ptr<PathDiagnosticPiece> 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/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
[email protected]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
