[PATCH] D45517: [analyzer] False positive refutation with Z3
This revision was automatically updated to reflect the committed changes.
Closed by commit rC333903: [analyzer] False positive refutation with Z3
(authored by mramalho, committed by ).
Changed prior to commit:
https://reviews.llvm.org/D45517?vs=149664=149764#toc
Repository:
rC Clang
https://reviews.llvm.org/D45517
Files:
include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/BugReporter.cpp
lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
test/Analysis/z3-crosscheck.c
Index: test/Analysis/z3-crosscheck.c
===
--- test/Analysis/z3-crosscheck.c
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,51 @@
+// 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
+
+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
+ while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#endif
+z = 2 * z;
+ }
+}
+
+void i() {
+ _Bool c = nondet_bool();
+ if (c) {
+h(1);
+ } else {
+h(2);
+ }
+}
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, );
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/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/BugReporterVisitors.cpp
===
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -44,6 +44,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/None.h"
#include "llvm/ADT/Optional.h"
@@ -2354,3 +2355,46 @@
return std::make_shared(L, "Taint originated here");
}
+
+static bool
+areConstraintsUnfeasible(BugReporterContext ,
+ const llvm::SmallVector ) {
+ // Create a refutation manager
+ std::unique_ptr RefutationMgr = CreateZ3ConstraintManager(
+ BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
+
+ SMTConstraintManager *SMTRefutationMgr =
+ static_cast(RefutationMgr.get());
+
+ // Add constraints to the solver
+ for (const auto : Cs)
+SMTRefutationMgr->addRangeConstraints(C);
+
+ // And check for satisfiability
+ return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
+}
+
+std::shared_ptr
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
+const ExplodedNode *PrevN,
+BugReporterContext ,
+
Re: [PATCH] D45517: [analyzer] False positive refutation with Z3
> > > Awesome! Does it mean that the optimization for adding less constraints > was in fact buggy? > > I pretty sure it was not related to the optimizations, I removed them days ago (in the previous version of this patch) and the bug was still there. > > 2. Could it be something unrelated to your changes? Any given trunk > version can be buggy, but usually those are resolved very fast, so if you > update now the issue can go away. > > Watching cfe-commits mailing list might be helpful there. > > I update my repo every other day and it's been happening for the past two/three weeks :/ The compiler shows the following error: posix_spawn failed: Argument list too long There are some discussions in several places about it. -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
mikhail.ramalho updated this revision to Diff 149664.
mikhail.ramalho edited the summary of this revision.
mikhail.ramalho added a comment.
Fix naming issue.
https://reviews.llvm.org/D45517
Files:
include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/BugReporter.cpp
lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
test/Analysis/z3-crosscheck.c
Index: test/Analysis/z3-crosscheck.c
===
--- /dev/null
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,51 @@
+// 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
+
+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
+ while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#endif
+z = 2 * z;
+ }
+}
+
+void i() {
+ _Bool c = nondet_bool();
+ if (c) {
+h(1);
+ } else {
+h(2);
+ }
+}
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -44,6 +44,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/None.h"
#include "llvm/ADT/Optional.h"
@@ -2354,3 +2355,46 @@
return std::make_shared(L, "Taint originated here");
}
+
+static bool
+areConstraintsUnfeasible(BugReporterContext ,
+ const llvm::SmallVector ) {
+ // Create a refutation manager
+ std::unique_ptr RefutationMgr = CreateZ3ConstraintManager(
+ BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
+
+ SMTConstraintManager *SMTRefutationMgr =
+ static_cast(RefutationMgr.get());
+
+ // Add constraints to the solver
+ for (const auto : Cs)
+SMTRefutationMgr->addRangeConstraints(C);
+
+ // And check for satisfiability
+ return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
+}
+
+std::shared_ptr
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
+const ExplodedNode *PrevN,
+BugReporterContext ,
+BugReport ) {
+ // Collect the constraint for the current state
+ const ConstraintRangeTy = 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 && areConstraintsUnfeasible(BRC, Constraints)) {
+BR.markInvalid("Infeasible constraints", N->getLocationContext());
+ }
+
+ return nullptr;
+}
+
+void FalsePositiveRefutationBRVisitor::Profile(
+llvm::FoldingSetNodeID ) const {
+ static int Tag = 0;
+ ID.AddPointer();
+}
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, );
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/AnalyzerOptions.cpp
===
---
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added a comment. > I pretty sure it was not related to the optimizations, I removed them days ago (in the previous version of this patch) and the bug was still there. OK so any idea what the change could have been? Clearly the bug was there but not now. Anyway, should be OK to commit now. > I update my repo every other day and it's been happening for the past two/three weeks :/ If it happens with your patch reverted as well, then it's unrelated, and we should just commit. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
mikhail.ramalho added a subscriber: rnkovacs. mikhail.ramalho added a comment. > Awesome! Does it mean that the optimization for adding less constraints > was in fact buggy? I pretty sure it was not related to the optimizations, I removed them days ago (in the previous version of this patch) and the bug was still there. > > > 2. Could it be something unrelated to your changes? Any given trunk version > can be buggy, but usually those are resolved very fast, so if you update now > the issue can go away. > > Watching cfe-commits mailing list might be helpful there. I update my repo every other day and it's been happening for the past two/three weeks :/ The compiler shows the following error: posix_spawn failed: Argument list too long There are some discussions in several places about it. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov requested changes to this revision.
george.karpenkov added a comment.
This revision now requires changes to proceed.
> I updated the test case as the cross check is not marking the true bug as
> invalid anymore.
Awesome! Does it mean that the optimization for adding less constraints was in
fact buggy?
> My make clang-test is still failing Driver/response-file.c whenever I compile
> clang with Z3. I'll update the patch as soon as I find the reason why.
1. You shouldn't use `make`, use `ninja` (also make sure you use `gold` linker,
default linker takes forever on Linux)
2. Could it be something unrelated to your changes? Any given trunk version can
be buggy, but usually those are resolved very fast, so if you update now the
issue can go away.
Watching cfe-commits mailing list might be helpful there.
Otherwise looks good apart from minor naming nit! I guess we could figure out
the casting issue later.
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2360
+static bool
+check_constraints(BugReporterContext ,
+ const llvm::SmallVector ) {
we would need a more descriptive name, e.g. `isUnfeasible` or similar.
from `bool check_constraints` it's unclear when `false` is returned.
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2366
+
+ SMTConstraintManager *SMTRefutationMgr =
+ static_cast(RefutationMgr.get());
mikhail.ramalho wrote:
> I'm not happy about this cast. Suggestions are welcome.
well yeah, `CreateZ3ConstraintManager` should return an `SMTConstraintManager`.
I don't fully understand the problem there, I'll try to take a look.
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
mikhail.ramalho added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2366 + + SMTConstraintManager *SMTRefutationMgr = + static_cast(RefutationMgr.get()); I'm not happy about this cast. Suggestions are welcome. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
mikhail.ramalho updated this revision to Diff 149653.
mikhail.ramalho added a comment.
Update patch based on https://reviews.llvm.org/D47640 and
https://reviews.llvm.org/D47689.
I updated the test case as the cross check is not marking the true bug as
invalid anymore.
My `make clang-test` is still failing `Driver/response-file.c` whenever I
compile clang with Z3. I'll update the patch as soon as I find the reason why.
https://reviews.llvm.org/D45517
Files:
include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/BugReporter.cpp
lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
test/Analysis/z3-crosscheck.c
Index: test/Analysis/z3-crosscheck.c
===
--- /dev/null
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,51 @@
+// 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
+
+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
+ while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#endif
+z = 2 * z;
+ }
+}
+
+void i() {
+ _Bool c = nondet_bool();
+ if (c) {
+h(1);
+ } else {
+h(2);
+ }
+}
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -44,6 +44,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/None.h"
#include "llvm/ADT/Optional.h"
@@ -2354,3 +2355,46 @@
return std::make_shared(L, "Taint originated here");
}
+
+static bool
+check_constraints(BugReporterContext ,
+ const llvm::SmallVector ) {
+ // Create a refutation manager
+ std::unique_ptr RefutationMgr = CreateZ3ConstraintManager(
+ BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
+
+ SMTConstraintManager *SMTRefutationMgr =
+ static_cast(RefutationMgr.get());
+
+ // Add constraints to the solver
+ for (const auto : Cs)
+SMTRefutationMgr->addRangeConstraints(C);
+
+ // And check for satisfiability
+ return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
+}
+
+std::shared_ptr
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
+const ExplodedNode *PrevN,
+BugReporterContext ,
+BugReport ) {
+ // Collect the constraint for the current state
+ const ConstraintRangeTy = 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 ) const {
+ static int Tag = 0;
+ ID.AddPointer();
+}
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, );
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());
-
[PATCH] D45517: [analyzer] False positive refutation with Z3
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(CZ);
}
+void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+ for (const auto : CR) {
+SymbolRef Sym = I.first;
+
+Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+for (const auto : I.second) {
+ const llvm::APSInt = Range.From();
+ const llvm::APSInt = Range.To();
+
+ QualType FromTy;
+ llvm::APSInt NewFromInt;
+ std::tie(NewFromInt, FromTy) = fixAPSInt(From);
+ Z3Expr FromExp = Z3Expr::fromAPSInt(NewFromInt);
+
+ QualType SymTy;
+ Z3Expr Exp = getZ3Expr(Sym, );
+ 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
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added a comment. @mikhail.ramalho I assume you know it, but just in case, you can mark dependencies in phabricator by adding "parent" revisions. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Re: [PATCH] D45517: [analyzer] False positive refutation with Z3
Hi, > Just a bit of context and to have some expectation management regarding > this patch. The main purpose of this implementation was to back a thesis. > It was made under a very serious time pressure and the main goal was to be > able to measure on real world projects as soon as possible and in the > meantime to be flexible so we can measure multiple configurations (like > incremental solving). > > So the goal was a flexible proof of concept that is sensible to measure in > the shortest possible time. After the thesis was done, Reka started to work > an another GSoC project, so she had no time to review the code with the > requirements of upstreaming in mind. Nevertheless we found that sharing the > proof of concept could be useful for the community. So it is perfectly > reasonable if you disagree with some design decisions behind this patch, > because the requirements for the thesis (in the short time frame) was very > different from the requirements of upstreaming this work. In a different > context these decisions made perfect sense. > > Just want to comment here and give thanks again for the first version of the refutation code. It's being really helpful to develop the approach this code as a base; things would definitely be slower if I had to start it from scratch. Thanks! -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
mikhail.ramalho added inline comments.
Comment at:
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183
+ virtual void reset() {}
+ virtual bool isModelFeasible() { return true; }
+ virtual void addRangeConstraints(ConstraintRangeTy) {}
george.karpenkov wrote:
> mikhail.ramalho wrote:
> > george.karpenkov wrote:
> > > Making those virtual does not make much sense to me.
> > > Returning `true` by default is not correct.
> > > When we are using the visitor, we should already know we have a
> > > `Z3ConstraintsManager`, why can't we just use methods of that class?
> > Z3ConstraintManager is fully contained inside a .cpp file, so we need
> > isModelFeasible and addRangeConstraints to be exposed via its base class.
> >
> > Another solution is to split Z3ConstraintManager into a .h and a .cpp file
> > and include the header. We would then be able to use it directly, instead
> > of through a ConstraintManager object.
> >
> > I honestly prefer the latter. What do you think?
> Yeah, I think we would need a header here.
> In general we try to avoid inheritance and virtual functions unless they are
> very beneficial, and here they are not.
Cool, I'll create a separate patch for that then.
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added inline comments.
Comment at:
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183
+ virtual void reset() {}
+ virtual bool isModelFeasible() { return true; }
+ virtual void addRangeConstraints(ConstraintRangeTy) {}
mikhail.ramalho wrote:
> george.karpenkov wrote:
> > Making those virtual does not make much sense to me.
> > Returning `true` by default is not correct.
> > When we are using the visitor, we should already know we have a
> > `Z3ConstraintsManager`, why can't we just use methods of that class?
> Z3ConstraintManager is fully contained inside a .cpp file, so we need
> isModelFeasible and addRangeConstraints to be exposed via its base class.
>
> Another solution is to split Z3ConstraintManager into a .h and a .cpp file
> and include the header. We would then be able to use it directly, instead of
> through a ConstraintManager object.
>
> I honestly prefer the latter. What do you think?
Yeah, I think we would need a header here.
In general we try to avoid inheritance and virtual functions unless they are
very beneficial, and here they are not.
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2391
+if (!RefutationMgr->isModelFeasible())
+ BR.markInvalid("Infeasible constraints", N->getLocationContext());
+ }
mikhail.ramalho wrote:
> george.karpenkov wrote:
> > That would be checking all constraints in all nodes one by one. I thought
> > the idea was to encode all constraints from the entire path and then check
> > all of it.
> All the constraints are being added in the previous for loop, isModelFeasible
> only calls check().
Ah right, I see we are inside of the branch when `pred_size() == 0`.
Sorry, I was wrong -- but could we move out this code to a private function
(could also simply use static function to avoid polluting the header)?
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
mikhail.ramalho added inline comments.
Comment at:
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183
+ virtual void reset() {}
+ virtual bool isModelFeasible() { return true; }
+ virtual void addRangeConstraints(ConstraintRangeTy) {}
george.karpenkov wrote:
> Making those virtual does not make much sense to me.
> Returning `true` by default is not correct.
> When we are using the visitor, we should already know we have a
> `Z3ConstraintsManager`, why can't we just use methods of that class?
Z3ConstraintManager is fully contained inside a .cpp file, so we need
isModelFeasible and addRangeConstraints to be exposed via its base class.
Another solution is to split Z3ConstraintManager into a .h and a .cpp file and
include the header. We would then be able to use it directly, instead of
through a ConstraintManager object.
I honestly prefer the latter. What do you think?
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added inline comments.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:925
+ void reset() override { Solver.reset(); }
+
mikhail.ramalho wrote:
> george.karpenkov wrote:
> > We don't need `reset` anymore.
> We don't need it but there's no reason to remove it, right? I might be useful
> in the future.
We try to keep the code as small and as simple as possible so that it still
achieves the task -- under that logic, unused methods should not be added.
I dislike `reset` in particular as it encourages stateful approach where the
same instance is used for all queries, which increases the likelihood of bugs.
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
mikhail.ramalho added inline comments.
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2391
+if (!RefutationMgr->isModelFeasible())
+ BR.markInvalid("Infeasible constraints", N->getLocationContext());
+ }
george.karpenkov wrote:
> That would be checking all constraints in all nodes one by one. I thought the
> idea was to encode all constraints from the entire path and then check all of
> it.
All the constraints are being added in the previous for loop, isModelFeasible
only calls check().
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:925
+ void reset() override { Solver.reset(); }
+
george.karpenkov wrote:
> We don't need `reset` anymore.
We don't need it but there's no reason to remove it, right? I might be useful
in the future.
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added inline comments.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:928
+ bool isModelFeasible() override {
+return Solver.check() != Z3_L_FALSE;
+ }
george.karpenkov wrote:
> The semantics of this method is incorrect. It should return a tri-value
> somehow (e.g. `Optional`, and then higher-level logic in visitor should
> decide what to do with it.)
We could also use `ConditionTruthVal` for this purpose.
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov requested changes to this revision.
george.karpenkov added a comment.
This revision now requires changes to proceed.
Thanks, this is going in the right direction!
Comment at:
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:182
+ virtual void reset() {}
+ virtual bool isModelFeasible() { return true; }
We don't need reset anymore.
Comment at:
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:183
+ virtual void reset() {}
+ virtual bool isModelFeasible() { return true; }
+ virtual void addRangeConstraints(ConstraintRangeTy) {}
Making those virtual does not make much sense to me.
Returning `true` by default is not correct.
When we are using the visitor, we should already know we have a
`Z3ConstraintsManager`, why can't we just use methods of that class?
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2377
+// Try to create the refutation manager, using Z3
+std::unique_ptr RefutationMgr =
+Opts.shouldCrosscheckWithZ3()
1. RefutationMgr should be created in the visitor constructor.
2. At this point we should not check options; if the visitor is created, we are
assuming that the option is on.
3. Consequently, the subsequent assert should be dropped.
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2391
+if (!RefutationMgr->isModelFeasible())
+ BR.markInvalid("Infeasible constraints", N->getLocationContext());
+ }
That would be checking all constraints in all nodes one by one. I thought the
idea was to encode all constraints from the entire path and then check all of
it.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:889
+
+ LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Solver
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:925
+ void reset() override { Solver.reset(); }
+
We don't need `reset` anymore.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:928
+ bool isModelFeasible() override {
+return Solver.check() != Z3_L_FALSE;
+ }
The semantics of this method is incorrect. It should return a tri-value somehow
(e.g. `Optional`, and then higher-level logic in visitor should decide
what to do with it.)
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1272
+ // FIXME: fix available in D35450
+ if (RangeTy.isNull())
+continue;
Since https://reviews.llvm.org/D47603 has landed we should drop this branch.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1282
+
+ Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr);
+ Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
/*RetTy=*/nullptr
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
rnkovacs added a comment. In https://reviews.llvm.org/D45517#1117898, @mikhail.ramalho wrote: > Just want to comment here and give thanks again for the first version of > the refutation code. It's being really helpful to develop the approach this > code as a base; things would definitely be slower if I had to start it from > scratch. @mikhail.ramalho Thanks for this note, it's very nice of you :) I'm glad if it saves a bit of time, but it's only a rough sketch, so please feel free to tailor it to your liking (and the reviewers' of course). https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
mikhail.ramalho added subscribers: dcoughlin, george.karpenkov, NoQ. mikhail.ramalho added a comment. Hi, > Just a bit of context and to have some expectation management regarding > this patch. The main purpose of this implementation was to back a thesis. > It was made under a very serious time pressure and the main goal was to be > able to measure on real world projects as soon as possible and in the > meantime to be flexible so we can measure multiple configurations (like > incremental solving). > > So the goal was a flexible proof of concept that is sensible to measure in > the shortest possible time. After the thesis was done, Reka started to work > an another GSoC project, so she had no time to review the code with the > requirements of upstreaming in mind. Nevertheless we found that sharing the > proof of concept could be useful for the community. So it is perfectly > reasonable if you disagree with some design decisions behind this patch, > because the requirements for the thesis (in the short time frame) was very > different from the requirements of upstreaming this work. In a different > context these decisions made perfect sense. Just want to comment here and give thanks again for the first version of the refutation code. It's being really helpful to develop the approach this code as a base; things would definitely be slower if I had to start it from scratch. Thanks! https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
mikhail.ramalho updated this revision to Diff 149317.
mikhail.ramalho marked 6 inline comments as not done.
mikhail.ramalho added a comment.
- Simplified refutation process: it now collects all the constraints in a given
path and, only when it reaches the root node, the refutation manager is created
and the constraints are checked for reachability. All the optimizations were
removed.
- Moved RangedConstraintManager.h to include/
- Moved refutation check to be the first in the list of BugVisitors
- Added dump method to Z3Solver (to print the formula)
- Added more documentation/comments
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/RangedConstraintManager.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/BugReporter.cpp
lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
lib/StaticAnalyzer/Core/RangedConstraintManager.h
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
@@ -10,6 +10,7 @@
#include "clang/Basic/TargetInfo.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
#include "clang/Config/config.h"
@@ -880,6 +881,12 @@
/// Reset the solver and remove all constraints.
void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
+
+ void print(raw_ostream ) const {
+OS << Z3_solver_to_string(Z3Context::ZC, Solver);
+ }
+
+ LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Solver
void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
@@ -915,6 +922,17 @@
void print(ProgramStateRef St, raw_ostream , const char *nl,
const char *sep) override;
+ void reset() override { Solver.reset(); }
+
+ bool isModelFeasible() override {
+return Solver.check() != Z3_L_FALSE;
+ }
+
+ /// Converts the ranged constraints of a set of symbols to SMT
+ ///
+ /// \param CR The set of constraints.
+ void addRangeConstraints(ConstraintRangeTy CR) override;
+
//===--===//
// Implementation for interface from SimpleConstraintManager.
//===--===//
@@ -1235,6 +1253,42 @@
return State->set(CZ);
}
+void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+ for (const auto : CR) {
+SymbolRef Sym = I.first;
+
+Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+for (const auto : I.second) {
+ const llvm::APSInt = Range.From();
+ const llvm::APSInt = 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.
+ // FIXME: fix available in D35450
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added a comment. @xazax.hun > So strictly speaking it is not a deduplication on the constraint level but on > the symbol level. Right, apologies, I was initially mistaken then. That's not even deduplication, I would call it using the interval solver to guide the constraint selection for the SMT solver. That makes sense, but I'm worried about tight coupling between different features, and classes of bugs which may arise due to that. It would be great to have it in a separate patch then. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
xazax.hun added a comment.
In https://reviews.llvm.org/D45517#1116770, @george.karpenkov wrote:
> > I am not not sure that I got the idea what are you suggesting here. If we
> > have the constraint of for example a symbol s > 10 and later on a path we
> > discover s > 20, will we also deduplicate this that way?
>
> No. But I thought in your optimization atoms inside the constraints would be
> the same?
> Could you give an example where they are not?
So the logic in the current patch would be the following. When the symbol s
dies it will be cleaned up from the state. For each symbol we will find the
state where it was cleaned up. We will add the constraint for that symbol from
the state before the cleanup which will contain the constraint `s > 20`. This
is the only point where we add the constraints regarding the symbol `s`, so `s
> 10` later on while we are traversing the path backwards will not be added.
Code to trigger this behavior:
void f(int s) {
if (s > 10) {
// ...
if (s > 20) {
// trigger a warning
}
}
}
So the point of this optimization is to only add the ranges of a symbol once,
where we have the most information about it. So strictly speaking it is not a
deduplication on the constraint level but on the symbol level.
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added a comment. > I am not not sure that I got the idea what are you suggesting here. If we > have the constraint of for example a symbol s > 10 and later on a path we > discover s > 20, will we also deduplicate this that way? No. But I thought in your optimization atoms inside the constraints would be the same? Could you give an example where they are not? https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
xazax.hun added a comment. In https://reviews.llvm.org/D45517#1116734, @george.karpenkov wrote: > @xazax.hun (I'll reply here to avoid scattering the conversation across many > subtrees) > > I was thinking about the optimization for not adding redundant constraints > some more, and I've decided I'm still against it --- > we are creating a higher potential for bugs, and we are tightly coupling the > visitor to an internal implementation detail (all formulas are eventually > purged at purge locations), > which creates a more fragile code. > > The proper way to do this would be to have a set of constraints, and then add > all constraints there as we iterate through the states (and through > constraints inside the state). > If we use the hashing function provided by Z3, the simple act of > construction of a set would implicitly drop all redundant constraints. I am not not sure that I got the idea what are you suggesting here. If we have the constraint of for example a symbol s > 10 and later on a path we discover s > 20, will we also deduplicate this that way? (Since the visitor is running backward we will add s > 20 constraint first, but this should be irrelevant for the deduplication I guess.) > @mikhail.ramalho In any case, the discussion here just further highlights > that this optimization should be dropped from the initial patch, and if > anything applied in a subsequent revision. Seams reasonable. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added a comment. @xazax.hun (I'll reply here to avoid scattering the conversation across many subtrees) I was thinking about the optimization for not adding redundant constraints some more, and I've decided I'm still against it --- we are creating a higher potential for bugs, and we are tightly coupling the visitor to an internal implementation detail (all formulas are eventually purged at purge locations), which creates a more fragile code. The proper way to do this would be to have a set of constraints, and then add all constraints there as we iterate through the states (and through constraints inside the state). If we use the hashing function provided by Z3, the simple act of construction of a set would implicitly drop all redundant constraints. @mikhail.ramalho In any case, the discussion here just further highlights that this optimization should be dropped from the initial patch, and if anything applied in a subsequent revision. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382 +// Reset the solver +RefutationMgr.reset(); + } xazax.hun wrote: > george.karpenkov wrote: > > xazax.hun wrote: > > > george.karpenkov wrote: > > > > george.karpenkov wrote: > > > > > (apologies in advance for nitpicking not on your code). > > > > > > > > > > Currently, this is written in a stateful way: we have a solver, at > > > > > each iteration we add constraints, and at the end we reset it. To me > > > > > it would make considerably more sense to write the code in a > > > > > functional style: as we go, generate a vector of formulas, then once > > > > > we reach the path end, create the solver object, check > > > > > satisfiability, and then destroy the entire solver. > > > > Elaborating more: we are already forced to have visitor object state, > > > > let's use that. `RefutationMgr` is essentially a wrapper around a Z3 > > > > solver object, let's just create one when visitor is constructed > > > > (directly or in unique_ptr) and then rely on the destructor to destroy > > > > it. > > > > Then no `reset` is necessary. > > > Note that while constructing the constraint solver here might make > > > perfect sense now, it also inhibits incremental solving. If we do not > > > plan to experiment with incremental solvers anytime soon I am fine with > > > this direction as well. > > @xazax.hun Right, I see. > > However, we should not optimize prematurely --- IF we decide to have > > incremental solving, then we would change our design to support it. > > > > Now I don't think incremental solving would help, and I don't think that > > having a global solver object would be helpful for it. > Just a bit of context and to have some expectation management regarding this > patch. The main purpose of this implementation was to back a thesis. It was > made under a very serious time pressure and the main goal was to be able to > measure on real world projects as soon as possible and in the meantime to be > flexible so we can measure multiple configurations (like incremental solving). > > So the goal was a flexible proof of concept that is sensible to measure in > the shortest possible time. After the thesis was done, Reka started to work > an another GSoC project, so she had no time to review the code with the > requirements of upstreaming in mind. Nevertheless we found that sharing the > proof of concept could be useful for the community. So it is perfectly > reasonable if you disagree with some design decisions behind this patch, > because the requirements for the thesis (in the short time frame) was very > different from the requirements of upstreaming this work. In a different > context these decisions made perfect sense. @xazax.hun of course. My comments are for @mikhail.ramalho who is now working on this patch. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1259 +return; + ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR; + xazax.hun wrote: > george.karpenkov wrote: > > rnkovacs wrote: > > > george.karpenkov wrote: > > > > TBH I'm really confused here. Why does the method take two constraint > > > > ranges? What's `OnlyPurged`? From reading the code it seems it's set by > > > > seeing whether the program point only purges dead symbols, but at least > > > > a comment should be added as to why this affects behavior. > > > The logic was: > > > - add every constraint from the last node (first visited), > > > - for other nodes on the path, only add those that disappear in the > > > next step. > > > > > > So `OnlyPurged` is meant to signal that we only want to add those symbols > > > to the solver that are getting purged from the program state. > > @rnkovacs right, so that's an optimization not to add extra constraints? > > > > 1. I would not do it at all, all formulas in Z3 are hash-consed, so a new > > formula would not even be *constructed* if it's already asserted in the > > solver. > > > > 2. Even if we do do it (which we shouldn't), this logic does not belong to > > Z3ConstraintManager. The method should have simple semantics: take a state, > > add all constraints to solver. > We would not just add the very same constraints over and over again. We would > first add the strongest possible constraint that the analyzer could infer > first and later on add weaker and weaker ones. Does Z3 do some special > handling for that as well? @xazax.hun Since all subformulas are hash-consed, I would be extremely surprised if this heuristic affected performance in a large way. However, your approach could be still useful in order to get readable dumps from the solver. I would still argue it should be done in a visitor, so something along the lines of: ``` // a comment explaining the logic if (State.succ_size() == 0 || State.getLocation().isPurged())
[PATCH] D45517: [analyzer] False positive refutation with Z3
xazax.hun added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382 +// Reset the solver +RefutationMgr.reset(); + } george.karpenkov wrote: > xazax.hun wrote: > > george.karpenkov wrote: > > > george.karpenkov wrote: > > > > (apologies in advance for nitpicking not on your code). > > > > > > > > Currently, this is written in a stateful way: we have a solver, at each > > > > iteration we add constraints, and at the end we reset it. To me it > > > > would make considerably more sense to write the code in a functional > > > > style: as we go, generate a vector of formulas, then once we reach the > > > > path end, create the solver object, check satisfiability, and then > > > > destroy the entire solver. > > > Elaborating more: we are already forced to have visitor object state, > > > let's use that. `RefutationMgr` is essentially a wrapper around a Z3 > > > solver object, let's just create one when visitor is constructed > > > (directly or in unique_ptr) and then rely on the destructor to destroy it. > > > Then no `reset` is necessary. > > Note that while constructing the constraint solver here might make perfect > > sense now, it also inhibits incremental solving. If we do not plan to > > experiment with incremental solvers anytime soon I am fine with this > > direction as well. > @xazax.hun Right, I see. > However, we should not optimize prematurely --- IF we decide to have > incremental solving, then we would change our design to support it. > > Now I don't think incremental solving would help, and I don't think that > having a global solver object would be helpful for it. Just a bit of context and to have some expectation management regarding this patch. The main purpose of this implementation was to back a thesis. It was made under a very serious time pressure and the main goal was to be able to measure on real world projects as soon as possible and in the meantime to be flexible so we can measure multiple configurations (like incremental solving). So the goal was a flexible proof of concept that is sensible to measure in the shortest possible time. After the thesis was done, Reka started to work an another GSoC project, so she had no time to review the code with the requirements of upstreaming in mind. Nevertheless we found that sharing the proof of concept could be useful for the community. So it is perfectly reasonable if you disagree with some design decisions behind this patch, because the requirements for the thesis (in the short time frame) was very different from the requirements of upstreaming this work. In a different context these decisions made perfect sense. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1259 +return; + ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR; + george.karpenkov wrote: > rnkovacs wrote: > > george.karpenkov wrote: > > > TBH I'm really confused here. Why does the method take two constraint > > > ranges? What's `OnlyPurged`? From reading the code it seems it's set by > > > seeing whether the program point only purges dead symbols, but at least a > > > comment should be added as to why this affects behavior. > > The logic was: > > - add every constraint from the last node (first visited), > > - for other nodes on the path, only add those that disappear in the next > > step. > > > > So `OnlyPurged` is meant to signal that we only want to add those symbols > > to the solver that are getting purged from the program state. > @rnkovacs right, so that's an optimization not to add extra constraints? > > 1. I would not do it at all, all formulas in Z3 are hash-consed, so a new > formula would not even be *constructed* if it's already asserted in the > solver. > > 2. Even if we do do it (which we shouldn't), this logic does not belong to > Z3ConstraintManager. The method should have simple semantics: take a state, > add all constraints to solver. We would not just add the very same constraints over and over again. We would first add the strongest possible constraint that the analyzer could infer first and later on add weaker and weaker ones. Does Z3 do some special handling for that as well? Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1264 + +if (OnlyPurged && SuccCR.contains(Sym)) + continue; george.karpenkov wrote: > xazax.hun wrote: > > george.karpenkov wrote: > > > I would guess that this is an optimization done in order not to re-add > > > the constraints we already have. > > > I think we should really not bother doing that, as Z3 will do a much > > > better job here then we can. > > Note that we are using lots of domain knowledge here like we have the most > > info about a symbol just before it dies. Also This optimization is a single > > lookup on the symbol level. I am not sure if Z3 could deal with this on the > > symbol
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added inline comments.
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382
+// Reset the solver
+RefutationMgr.reset();
+ }
xazax.hun wrote:
> george.karpenkov wrote:
> > george.karpenkov wrote:
> > > (apologies in advance for nitpicking not on your code).
> > >
> > > Currently, this is written in a stateful way: we have a solver, at each
> > > iteration we add constraints, and at the end we reset it. To me it would
> > > make considerably more sense to write the code in a functional style: as
> > > we go, generate a vector of formulas, then once we reach the path end,
> > > create the solver object, check satisfiability, and then destroy the
> > > entire solver.
> > Elaborating more: we are already forced to have visitor object state, let's
> > use that. `RefutationMgr` is essentially a wrapper around a Z3 solver
> > object, let's just create one when visitor is constructed (directly or in
> > unique_ptr) and then rely on the destructor to destroy it.
> > Then no `reset` is necessary.
> Note that while constructing the constraint solver here might make perfect
> sense now, it also inhibits incremental solving. If we do not plan to
> experiment with incremental solvers anytime soon I am fine with this
> direction as well.
@xazax.hun Right, I see.
However, we should not optimize prematurely --- IF we decide to have
incremental solving, then we would change our design to support it.
Now I don't think incremental solving would help, and I don't think that having
a global solver object would be helpful for it.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1249
+bool Z3ConstraintManager::isModelFeasible() {
+ return Solver.check() != Z3_L_FALSE;
+}
rnkovacs wrote:
> george.karpenkov wrote:
> > solver can also return "unknown", what happens then?
> If it returns `Z3_L_UNDEF`, e.g. in case of a timeout, this assumes that the
> state was feasible because we couldn't prove the opposite. In that case the
> report won't be invalidated.
@rnkovacs that's possibly valid (though the exact behavior might need to be
behind an option), but the current implementation is wrong and the decision
should be made at a different stack level.
This method is responsible for "whether the model is valid", and it should not
say "yes" when the solver returns "unknown". We could return an
`Optional` here, or a tri-value logic type (IIRC LLVM had one, which
could represent true/false/unknown)
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1259
+return;
+ ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR;
+
rnkovacs wrote:
> george.karpenkov wrote:
> > TBH I'm really confused here. Why does the method take two constraint
> > ranges? What's `OnlyPurged`? From reading the code it seems it's set by
> > seeing whether the program point only purges dead symbols, but at least a
> > comment should be added as to why this affects behavior.
> The logic was:
> - add every constraint from the last node (first visited),
> - for other nodes on the path, only add those that disappear in the next
> step.
>
> So `OnlyPurged` is meant to signal that we only want to add those symbols to
> the solver that are getting purged from the program state.
@rnkovacs right, so that's an optimization not to add extra constraints?
1. I would not do it at all, all formulas in Z3 are hash-consed, so a new
formula would not even be *constructed* if it's already asserted in the solver.
2. Even if we do do it (which we shouldn't), this logic does not belong to
Z3ConstraintManager. The method should have simple semantics: take a state, add
all constraints to solver.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1264
+
+if (OnlyPurged && SuccCR.contains(Sym))
+ continue;
xazax.hun wrote:
> george.karpenkov wrote:
> > I would guess that this is an optimization done in order not to re-add the
> > constraints we already have.
> > I think we should really not bother doing that, as Z3 will do a much better
> > job here then we can.
> Note that we are using lots of domain knowledge here like we have the most
> info about a symbol just before it dies. Also This optimization is a single
> lookup on the symbol level. I am not sure if Z3 could deal with this on the
> symbol level. It might need to do this on the constraint level.
> My point is, I am perfectly fine removing this optimization but I would like
> to see some performance numbers first either on a project that exercises
> refutation quite a bit or on some synthetic test cases.
>
> This optimization is a single lookup on the symbol level. I am not sure if Z3
> could deal with this on the symbol level
What do you mean? I'm positive adding redundant constraints to Z3 would not
slow solving down.
> I would like to see some performance numbers
[PATCH] D45517: [analyzer] False positive refutation with Z3
xazax.hun added inline comments. Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382 +// Reset the solver +RefutationMgr.reset(); + } george.karpenkov wrote: > george.karpenkov wrote: > > (apologies in advance for nitpicking not on your code). > > > > Currently, this is written in a stateful way: we have a solver, at each > > iteration we add constraints, and at the end we reset it. To me it would > > make considerably more sense to write the code in a functional style: as we > > go, generate a vector of formulas, then once we reach the path end, create > > the solver object, check satisfiability, and then destroy the entire solver. > Elaborating more: we are already forced to have visitor object state, let's > use that. `RefutationMgr` is essentially a wrapper around a Z3 solver object, > let's just create one when visitor is constructed (directly or in unique_ptr) > and then rely on the destructor to destroy it. > Then no `reset` is necessary. Note that while constructing the constraint solver here might make perfect sense now, it also inhibits incremental solving. If we do not plan to experiment with incremental solvers anytime soon I am fine with this direction as well. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1264 + +if (OnlyPurged && SuccCR.contains(Sym)) + continue; george.karpenkov wrote: > I would guess that this is an optimization done in order not to re-add the > constraints we already have. > I think we should really not bother doing that, as Z3 will do a much better > job here then we can. Note that we are using lots of domain knowledge here like we have the most info about a symbol just before it dies. Also This optimization is a single lookup on the symbol level. I am not sure if Z3 could deal with this on the symbol level. It might need to do this on the constraint level. My point is, I am perfectly fine removing this optimization but I would like to see some performance numbers first either on a project that exercises refutation quite a bit or on some synthetic test cases. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
rnkovacs added inline comments.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1249
+bool Z3ConstraintManager::isModelFeasible() {
+ return Solver.check() != Z3_L_FALSE;
+}
george.karpenkov wrote:
> solver can also return "unknown", what happens then?
If it returns `Z3_L_UNDEF`, e.g. in case of a timeout, this assumes that the
state was feasible because we couldn't prove the opposite. In that case the
report won't be invalidated.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1259
+return;
+ ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR;
+
george.karpenkov wrote:
> TBH I'm really confused here. Why does the method take two constraint ranges?
> What's `OnlyPurged`? From reading the code it seems it's set by seeing
> whether the program point only purges dead symbols, but at least a comment
> should be added as to why this affects behavior.
The logic was:
- add every constraint from the last node (first visited),
- for other nodes on the path, only add those that disappear in the next step.
So `OnlyPurged` is meant to signal that we only want to add those symbols to
the solver that are getting purged from the program state.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1278
+ // a valid APSIntType.
+ if (RangeTy.isNull())
+continue;
george.karpenkov wrote:
> I'm really curious where does it happen and why.
I encountered some 1-bit `APSInt`s that wouldn't work together with any other
integer-handling logic. As @ddcc mentioned, he has a fix for that in D35450
(`Z3ConstraintManager::fixAPSInt()`).
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added inline comments. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1267 + +Z3Expr Constraints = Z3Expr::fromBoolean(false); + george.karpenkov wrote: > almost certainly a bug, we shouldn't default to unfeasible when the list of > constraints is empty. Ooops, sorry, now I see how the code is supposed to work. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1292 + Constraints = + Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy); +} NoQ wrote: > george.karpenkov wrote: > > I'm very confused as to why are we doing disjunctions here. > I think this corresponds to RangeSet being a union of Ranges. Ah, thanks, right! Then my previous comment regarding `false` is wrong. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
NoQ added inline comments. Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1292 + Constraints = + Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy); +} george.karpenkov wrote: > I'm very confused as to why are we doing disjunctions here. I think this corresponds to RangeSet being a union of Ranges. https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added inline comments.
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:496
std::unique_ptr ConstraintMgr;
+ std::unique_ptr RefutationMgr;
See the comment below, I think we should not have this manager here. Just
create one in the visitor constructor.
Comment at: include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h:563
+
+ ConstraintManager& getRefutationManager() {
+return *RefutationMgr;
This should be deleted as well (see the comment above)
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382
+// Reset the solver
+RefutationMgr.reset();
+ }
george.karpenkov wrote:
> (apologies in advance for nitpicking not on your code).
>
> Currently, this is written in a stateful way: we have a solver, at each
> iteration we add constraints, and at the end we reset it. To me it would make
> considerably more sense to write the code in a functional style: as we go,
> generate a vector of formulas, then once we reach the path end, create the
> solver object, check satisfiability, and then destroy the entire solver.
Elaborating more: we are already forced to have visitor object state, let's use
that. `RefutationMgr` is essentially a wrapper around a Z3 solver object, let's
just create one when visitor is constructed (directly or in unique_ptr) and
then rely on the destructor to destroy it.
Then no `reset` is necessary.
Comment at: lib/StaticAnalyzer/Core/ProgramState.cpp:83
ConstraintMgr = (*CreateCMgr)(*this, SubEng);
+ AnalyzerOptions = SubEng->getAnalysisManager().getAnalyzerOptions();
+ RefutationMgr = Opts.shouldCrosscheckWithZ3()
This could be removed as well (see the comment above)
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:919
+ void reset() override;
+
`reset` should be removed, see comments above.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1246
+void Z3ConstraintManager::reset() { Solver.reset(); }
+
I would remove this, see comments above.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1292
+ Constraints =
+ Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+}
I'm very confused as to why are we doing disjunctions here.
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added inline comments.
Comment at: lib/StaticAnalyzer/Core/BugReporter.cpp:3153
+if (getAnalyzerOptions().shouldCrosscheckWithZ3())
+ R->addVisitor(llvm::make_unique());
+
Unless I'm mistaken, visitors are run in the order they are being declared.
It seems to me we would want to register our visitor first, as it does not make
sense to run diagnostics-visitors if we have already deemed the path to be
unfeasible.
Probably `LikelyFalsePositiveSuppressionBRVisitor` should be even before that.
Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2382
+// Reset the solver
+RefutationMgr.reset();
+ }
(apologies in advance for nitpicking not on your code).
Currently, this is written in a stateful way: we have a solver, at each
iteration we add constraints, and at the end we reset it. To me it would make
considerably more sense to write the code in a functional style: as we go,
generate a vector of formulas, then once we reach the path end, create the
solver object, check satisfiability, and then destroy the entire solver.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:923
+
+ void addRangeConstraints(ConstraintRangeTy PrevCR, ConstraintRangeTy SuccCR,
+ bool OnlyPurged) override;
@mikhail.ramalho I know the first version was not yours, but could you write a
doxygen comment explaining the semantics of all parameters? (I know we are
guilty for not writing those often).
I am also quite confused by the semantics of `OnlyPurged` variable.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1249
+bool Z3ConstraintManager::isModelFeasible() {
+ return Solver.check() != Z3_L_FALSE;
+}
solver can also return "unknown", what happens then?
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1259
+return;
+ ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR;
+
TBH I'm really confused here. Why does the method take two constraint ranges?
What's `OnlyPurged`? From reading the code it seems it's set by seeing whether
the program point only purges dead symbols, but at least a comment should be
added as to why this affects behavior.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1264
+
+if (OnlyPurged && SuccCR.contains(Sym))
+ continue;
I would guess that this is an optimization done in order not to re-add the
constraints we already have.
I think we should really not bother doing that, as Z3 will do a much better job
here then we can.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1267
+
+Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
almost certainly a bug, we shouldn't default to unfeasible when the list of
constraints is empty.
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1278
+ // a valid APSIntType.
+ if (RangeTy.isNull())
+continue;
I'm really curious where does it happen and why.
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
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 , 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
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added inline comments. Comment at: test/Analysis/z3-crosscheck.c:2 +// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s +// REQUIRES: z3 +// expected-no-diagnostics Could we also have a second RUN line without Z3, and then use ifdef's to differentiate between the two in tests? https://reviews.llvm.org/D45517 ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
george.karpenkov added a comment.
Please resubmit with -U999 diff flag (or using arc)
Comment at:
include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h:362
+class FalsePositiveRefutationBRVisitor final
+: public BugReporterVisitorImpl {
Can we have the whole class inside the `.cpp` file? It's annoying to recompile
half of the analyzer when an internal implementation detail changes
Comment at:
include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h:365
+ // Flag first node as seen by the visitor.
+ bool FirstNodeVisited = true;
+
I'm really not convinced we need this boolean field
Comment at:
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h:21
#include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h"
+#include "llvm/ADT/ImmutableMap.h"
#include "llvm/ADT/Optional.h"
NB: diff should be resubmitted with -U999, as phabricator shows "context not
available"
Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1261
+
+ for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+SymbolRef Sym = I.getKey();
xbolva00 wrote:
> for (auto I : CR)?
@mikhail.ramalho yes please do fix this one
https://reviews.llvm.org/D45517
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
[PATCH] D45517: [analyzer] False positive refutation with Z3
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;
^
:1:1: note: scanning from here
clang version 7.0.0 (trunk 52) (llvm/trunk 74)
^
: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 , 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(CZ);
}
+void Z3ConstraintManager::reset() { Solver.reset(); }
+
+bool Z3ConstraintManager::isModelFeasible() {
+ return Solver.check() != Z3_L_FALSE;
+}
+
+void
