[PATCH] D45517: [analyzer] WIP: False positive refutation with Z3

[Dávid Bolvanský via Phabricator via cfe-commits]

xbolva00 added inline comments.



Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1261
+
+  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+SymbolRef Sym = I.getKey();

for (auto I : CR)?


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] WIP: False positive refutation with Z3

[Dominic Chen via Phabricator via cfe-commits]

ddcc added a comment.

FYI the fix for the 1-bit APSInt issue is in 
https://reviews.llvm.org/D35450#change-ifYnQ3IlVso


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] WIP: False positive refutation with Z3

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

Commandeering the PR because of GSoC.


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] WIP: False positive refutation with Z3

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs added inline comments.



Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2342
+BugReport ) {
+  if (isInvalidated)
+return nullptr;

george.karpenkov wrote:
> Is this field actually necessary? Do we ever check the same bug report with 
> the same visitor multiple times?
I believe this function is called for each node on the bug path. I have a 
similar field to indicate the first visited node in the new version, but there 
may exist a better solution for that as well.



Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2351
+
+  if (!RefutationMgr.checkRangedStateConstraints(Succ->getState())) {
+const LocationContext *LC = Succ->getLocationContext();

george.karpenkov wrote:
> For the initial version I would just do all work in the visitor, but that's a 
> matter of taste.
I think that doing all the work in the visitor would need exposing even more of 
`Z3ConstraintManager`'s internals as of `RangedConstraintManager`. I tried to 
keep such changes minimal.



Comment at: lib/StaticAnalyzer/Core/ProgramState.cpp:86
+  ? CreateZ3ConstraintManager(*this, SubEng)
+  : nullptr;
 }

george.karpenkov wrote:
> Would then we crash on NPE if `getRefutationManager` is called? Getters 
> should preferably not cause crashes.
Um, currently yes, it will give a backend error if clang isn't built with Z3, 
but the option is on.


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] WIP: False positive refutation with Z3

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs updated this revision to Diff 145762.
rnkovacs marked 4 inline comments as done.
rnkovacs edited the summary of this revision.
rnkovacs added a comment.

Expression chaining is fixed. The visitor now collects constraints that are 
about to disappear along the bug path and checks them once in the end.


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

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,57 @@
   return State->set(CZ);
 }
 
+void Z3ConstraintManager::reset() { Solver.reset(); }
+
+bool Z3ConstraintManager::isModelFeasible() {
+  return Solver.check() != Z3_L_FALSE;
+}
+
+void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy PrevCR,
+  ConstraintRangeTy SuccCR,
+  bool OnlyPurged) {
+  if (OnlyPurged && PrevCR.isEmpty())
+return;
+  if (!OnlyPurged && SuccCR.isEmpty())
+return;
+  ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR;
+
+  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+SymbolRef Sym = I.getKey();
+
+if (OnlyPurged && SuccCR.contains(Sym))
+  continue;
+
+Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+for (const auto  : I.getData()) {
+  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.
+  if (RangeTy.isNull())
+continue;
+
+  QualType SymTy;
+  Z3Expr Exp = getZ3Expr(Sym, );
+  bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType();
+
+  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
+  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+
+  Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr);
+  Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
+  Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy);
+  Constraints = Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+}
+Solver.addConstraint(Constraints);
+  }
+}
+
 //===--===//
 // Internal implementation.
 //===--===//
Index: lib/StaticAnalyzer/Core/ProgramState.cpp
===
--- lib/StaticAnalyzer/Core/ProgramState.cpp
+++ lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -13,6 +13,8 @@
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/Analysis/CFG.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
@@ -78,6 +80,10 @@
 CallEventMgr(new CallEventManager(alloc)), Alloc(alloc) {
   StoreMgr = (*CreateSMgr)(*this);
   ConstraintMgr = (*CreateCMgr)(*this, SubEng);
+  AnalyzerOptions  = SubEng->getAnalysisManager().getAnalyzerOptions();
+  RefutationMgr = Opts.shouldCrosscheckWithZ3()
+  ? CreateZ3ConstraintManager(*this, SubEng)
+ 

[PATCH] D45517: [analyzer] WIP: False positive refutation with Z3

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

In https://reviews.llvm.org/D45517#1074422, @rnkovacs wrote:

> In https://reviews.llvm.org/D45517#1074057, @NoQ wrote:
>
> > So, yeah, that's a good optimization that we're not invoking the solver on 
> > every node. But i don't think we should focus on improving this 
> > optimization further; instead, i think the next obvious step here is to 
> > implement it in such a way that we only needed to call the solver //once// 
> > for every report. We could simply collect all constraints from all states 
> > along the path and put them into the solver all together. This will work 
> > because symbols are not mutable and they don't reincarnate.
>
>
> Won't collecting all constraints and solving a ~100ish equations at once take 
> a long time? Maybe the timeout limit for Z3 will need to be slightly 
> increased for refutation then.


Well, in the worst case we would still be able to split our full system of 
equations into smaller chunks, and it'd most likely still be better than 
solving roughly-the-same system of equations ~100ish times.


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] WIP: False positive refutation with Z3

[George Karpenkov via Phabricator via cfe-commits]

george.karpenkov added inline comments.



Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:284
+  /// \sa shouldPostProcessBugReports
+  Optional PostProcessBugReports;
+

The option name should be more self-explanatory, post-processing in general can 
mean anything



Comment at: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h:586
+  /// which accepts the values "true" and "false".
+  bool shouldPostProcessBugReports();
+

Same here



Comment at: 
include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h:348
+: public BugReporterVisitorImpl {
+  bool isInvalidated = false;
+

LLVM coding standart mandates capital case for field names.



Comment at: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp:301
+  return getBooleanOption(PostProcessBugReports,
+  "postprocess-reports",
+  /* Default = */ false);

Same for the option name. "crosscheck-with-z3"?



Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2342
+BugReport ) {
+  if (isInvalidated)
+return nullptr;

Is this field actually necessary? Do we ever check the same bug report with the 
same visitor multiple times?



Comment at: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2351
+
+  if (!RefutationMgr.checkRangedStateConstraints(Succ->getState())) {
+const LocationContext *LC = Succ->getLocationContext();

For the initial version I would just do all work in the visitor, but that's a 
matter of taste.



Comment at: lib/StaticAnalyzer/Core/ProgramState.cpp:86
+  ? CreateZ3ConstraintManager(*this, SubEng)
+  : nullptr;
 }

Would then we crash on NPE if `getRefutationManager` is called? Getters should 
preferably not cause crashes.



Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1268
+  if (From == To) {
+Z3Expr Eq = getZ3BinExpr(Exp, SymTy, BO_EQ, FromExp, RangeTy, nullptr);
+Solver.addConstraint(Eq);

I wouldn't even bother with this branch, but again, a matter of taste.



Comment at: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp:1273
+Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
+Solver.addConstraint(Z3Expr::fromBinOp(LHS, BO_LOr, RHS, isSignedTy));
+  }

Why `OR`? Shouldn't it be AND?


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] WIP: False positive refutation with Z3

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs added a comment.

In https://reviews.llvm.org/D45517#1074057, @NoQ wrote:

> > The visitor currently checks states appearing as block edges in the 
> > exploded graph. The first idea was to filter states based on the shape of 
> > the exploded graph, by checking the number of successors of the parent 
> > node, but surprisingly, both `succ_size()` and `pred_size()` seemed to 
> > return 1 for each node in the graph (except for the root), even if there 
> > clearly were branchings in the code (and on the `.dot` picture). To my 
> > understanding, the exploded graph is fully constructed at the stage where 
> > visitors are run, so I must be missing something.
>
> Aha, yep, that's probably because visitors are operating on the "trimmed" 
> exploded graph. You can paint it via the `-trim-egraph` flag or by calling 
> `ViewGraph(1)` in the debugger.


Oh, thanks! That explains a lot.

> So, yeah, that's a good optimization that we're not invoking the solver on 
> every node. But i don't think we should focus on improving this optimization 
> further; instead, i think the next obvious step here is to implement it in 
> such a way that we only needed to call the solver //once// for every report. 
> We could simply collect all constraints from all states along the path and 
> put them into the solver all together. This will work because symbols are not 
> mutable and they don't reincarnate.

Won't collecting all constraints and solving a ~100ish equations at once take a 
long time? Maybe the timeout limit for Z3 will need to be slightly increased 
for refutation then.

> Apart from that, the patch seems to be going in the right direction. It 
> should be possible to split up the `RangeSet` refactoring into a different 
> review, for easier reviewing and better commit history.

Done in https://reviews.llvm.org/D45920.

I'll update this patch shortly.


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] WIP: False positive refutation with Z3

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs added a comment.

In https://reviews.llvm.org/D45517#1074057, @NoQ wrote:

> > The visitor currently checks states appearing as block edges in the 
> > exploded graph. The first idea was to filter states based on the shape of 
> > the exploded graph, by checking the number of successors of the parent 
> > node, but surprisingly, both `succ_size()` and `pred_size()` seemed to 
> > return 1 for each node in the graph (except for the root), even if there 
> > clearly were branchings in the code (and on the `.dot` picture). To my 
> > understanding, the exploded graph is fully constructed at the stage where 
> > visitors are run, so I must be missing something.
>
> Aha, yep, that's probably because visitors are operating on the "trimmed" 
> exploded graph. You can paint it via the `-trim-egraph` flag or by calling 
> `ViewGraph(1)` in the debugger.


Oh, thanks! That explains a lot.

> So, yeah, that's a good optimization that we're not invoking the solver on 
> every node. But i don't think we should focus on improving this optimization 
> further; instead, i think the next obvious step here is to implement it in 
> such a way that we only needed to call the solver //once// for every report. 
> We could simply collect all constraints from all states along the path and 
> put them into the solver all together. This will work because symbols are not 
> mutable and they don't reincarnate.

Won't collecting all constraints and solving a ~100ish equations at once take a 
long time? Maybe the timeout limit for Z3 will need to be slightly increased 
for refutation then.

> Apart from that, the patch seems to be going in the right direction. It 
> should be possible to split up the `RangeSet` refactoring into a different 
> review, for easier reviewing and better commit history.

Done in https://reviews.llvm.org/D45920.

I'll update this patch shortly.


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] WIP: False positive refutation with Z3

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs updated this revision to Diff 143440.

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

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,8 @@
   void print(ProgramStateRef St, raw_ostream , const char *nl,
  const char *sep) override;
 
+  bool checkRangedStateConstraints(ProgramStateRef State) override;
+
   //===--===//
   // Implementation for interface from SimpleConstraintManager.
   //===--===//
@@ -1235,6 +1238,47 @@
   return State->set(CZ);
 }
 
+bool Z3ConstraintManager::checkRangedStateConstraints(ProgramStateRef State) {
+  Solver.reset();
+  ConstraintRangeTy CR = State->get();
+
+  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+SymbolRef Sym = I.getKey();
+
+for (const auto  : I.getData()) {
+  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.
+  if (RangeTy.isNull())
+continue;
+
+  QualType SymTy;
+  Z3Expr Exp = getZ3Expr(Sym, );
+  bool isSignedTy = SymTy->isSignedIntegerOrEnumerationType();
+
+  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
+  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+
+  if (From == To) {
+Z3Expr Eq = getZ3BinExpr(Exp, SymTy, BO_EQ, FromExp, RangeTy, nullptr);
+Solver.addConstraint(Eq);
+  } else {
+Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr);
+Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
+Solver.addConstraint(Z3Expr::fromBinOp(LHS, BO_LOr, RHS, isSignedTy));
+  }
+}
+  }
+  // If Z3 timeouts, Z3_L_UNDEF is returned, and we assume that the state
+  // is feasible.
+  return Solver.check() != Z3_L_FALSE;
+}
+
 //===--===//
 // Internal implementation.
 //===--===//
Index: lib/StaticAnalyzer/Core/ProgramState.cpp
===
--- lib/StaticAnalyzer/Core/ProgramState.cpp
+++ lib/StaticAnalyzer/Core/ProgramState.cpp
@@ -13,6 +13,8 @@
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/Analysis/CFG.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
@@ -78,6 +80,10 @@
 CallEventMgr(new CallEventManager(alloc)), Alloc(alloc) {
   StoreMgr = (*CreateSMgr)(*this);
   ConstraintMgr = (*CreateCMgr)(*this, SubEng);
+  AnalyzerOptions  = SubEng->getAnalysisManager().getAnalyzerOptions();
+  RefutationMgr = Opts.shouldPostProcessBugReports()
+  ? CreateZ3ConstraintManager(*this, SubEng)
+  : nullptr;
 }
 
 
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2333,3 +2333,26 @@
 
   return std::move(Piece);
 }
+
+std::shared_ptr
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *Succ,
+const ExplodedNode *Prev,
+BugReporterContext ,
+BugReport ) {
+  if (isInvalidated)
+return nullptr;
+
+  if (Succ->getLocation().getKind() != ProgramPoint::BlockEdgeKind)
+

[PATCH] D45517: [analyzer] WIP: False positive refutation with Z3

[Artem Dergachev via Phabricator via cfe-commits]

NoQ added a comment.

> The visitor currently checks states appearing as block edges in the exploded 
> graph. The first idea was to filter states based on the shape of the exploded 
> graph, by checking the number of successors of the parent node, but 
> surprisingly, both `succ_size()` and `pred_size()` seemed to return 1 for 
> each node in the graph (except for the root), even if there clearly were 
> branchings in the code (and on the `.dot` picture). To my understanding, the 
> exploded graph is fully constructed at the stage where visitors are run, so I 
> must be missing something.

Aha, yep, that's probably because visitors are operating on the "trimmed" 
exploded graph. You can paint it via the `-trim-egraph` flag or by calling 
`ViewGraph(1)` in the debugger.

So, yeah, that's a good optimization that we're not invoking the solver on 
every node. But i don't think we should focus on improving this optimization 
further; instead, i think the next obvious step here is to implement it in such 
a way that we only needed to call the solver //once// for every report. We 
could simply collect all constraints from all states along the path and put 
them into the solver all together. This will work because symbols are not 
mutable and they don't reincarnate.

Apart from that, the patch seems to be going in the right direction. It should 
be possible to split up the `RangeSet` refactoring into a different review, for 
easier reviewing and better commit history.


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] WIP: False positive refutation with Z3

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs updated this revision to Diff 143287.
rnkovacs edited the summary of this revision.
rnkovacs added a comment.

Fixed logical operator in the 
`Z3ConstraintManager::checkRangedStateConstraints()` function.


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/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.h
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

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,8 @@
   void print(ProgramStateRef St, raw_ostream , const char *nl,
  const char *sep) override;
 
+  bool checkRangedStateConstraints(ProgramStateRef State) override;
+
   //===--===//
   // Implementation for interface from SimpleConstraintManager.
   //===--===//
@@ -1235,6 +1238,47 @@
   return State->set(CZ);
 }
 
+bool Z3ConstraintManager::checkRangedStateConstraints(ProgramStateRef State) {
+  Solver.reset();
+  ConstraintRangeTy CR = State->get();
+
+  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+SymbolRef Sym = I.getKey();
+
+for (const auto  : I.getData()) {
+  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.
+  if (RangeTy.isNull())
+continue;
+
+  QualType SymTy;
+  Z3Expr Exp = getZ3Expr(Sym, );
+  bool isSignedTy = SymTy->isSignedIntegerOrEnumerationType();
+
+  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
+  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+
+  if (From == To) {
+Z3Expr Eq = getZ3BinExpr(Exp, SymTy, BO_EQ, FromExp, RangeTy, nullptr);
+Solver.addConstraint(Eq);
+  } else {
+Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr);
+Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
+Solver.addConstraint(Z3Expr::fromBinOp(LHS, BO_LOr, RHS, isSignedTy));
+  }
+}
+  }
+  // If Z3 timeouts, Z3_L_UNDEF is returned, and we assume that the state
+  // is feasible.
+  return Solver.check() != Z3_L_FALSE;
+}
+
 //===--===//
 // Internal implementation.
 //===--===//
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.h
===
--- lib/StaticAnalyzer/Core/RangedConstraintManager.h
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.h
@@ -15,12 +15,124 @@
 #define LLVM_CLANG_LIB_STATICANALYZER_CORE_RANGEDCONSTRAINTMANAGER_H
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
 
 namespace clang {
 
 namespace ento {
 
+/// A Range represents the closed range [from, to].  The caller must
+/// guarantee that from <= to.  Note that Range is immutable, so as not
+/// to subvert RangeSet's immutability.
+class Range : public std::pair {
+public:
+  Range(const llvm::APSInt , const llvm::APSInt )
+  : std::pair(, ) {
+assert(from <= to);
+  }
+  bool Includes(const llvm::APSInt ) const {
+return *first <= v && v <= *second;
+  }
+  const llvm::APSInt () const { return *first; }
+  const llvm::APSInt () const { return *second; }
+  const llvm::APSInt *getConcreteValue() const {
+return () == () ? () : nullptr;
+  }
+
+  void Profile(llvm::FoldingSetNodeID ) const {
+ID.AddPointer(());
+ID.AddPointer(());
+  }
+};
+
+class RangeTrait : public llvm::ImutContainerInfo {
+public:
+  // When comparing if one Range is less than another, we should compare
+  // the 

[PATCH] D45517: [analyzer] WIP: False positive refutation with Z3

[Reka Kovacs via Phabricator via cfe-commits]

rnkovacs created this revision.
rnkovacs added reviewers: george.karpenkov, NoQ, dcoughlin.
Herald added subscribers: a.sidorin, szepet, baloghadamsoftware, whisperity, 
fhahn.

This is a prototype of a bug reporter visitor that invalidates bug reports by 
re-checking constraints of certain states on the bug path using the Z3 
constraint manager backend. The functionality is available under the 
`postprocess-reports` analyzer config flag.

Results of analysis runs on a few open-source projects with this option turned 
on can be explored here .

This work is preliminary and any comments are appreciated. A few remarks:

- In order to work with constraints generated by the range-based constraint 
manager outside its own file, much of the `Range`, `RangeTrait` and `RangeSet` 
classes have been moved to the corresponding header file.

- The visitor currently checks states appearing as block edges in the exploded 
graph. The first idea was to filter states based on the shape of the exploded 
graph, by checking the number of successors of the parent node, but 
surprisingly, both `succ_size()` and `pred_size()` seemed to return 1 for each 
node in the graph (except for the root), even if there clearly were branchings 
in the code (and on the `.dot` picture). To my understanding, the exploded 
graph is fully constructed at the stage where visitors are run, so I must be 
missing something.

- 1-bit APSInts obtained from ranged constraints crashed when 
`isSignedIntegerOrEnumerationType()` was called on them inside 
`Z3ConstraintManager`'s methods. This issue is currently sidestepped, but they 
might be converted to a valid built-in type at some point.


Repository:
  rC Clang

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/RangeConstraintManager.cpp
  lib/StaticAnalyzer/Core/RangedConstraintManager.h
  lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

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,8 @@
   void print(ProgramStateRef St, raw_ostream , const char *nl,
  const char *sep) override;
 
+  bool checkRangedStateConstraints(ProgramStateRef State) override;
+
   //===--===//
   // Implementation for interface from SimpleConstraintManager.
   //===--===//
@@ -1235,6 +1238,47 @@
   return State->set(CZ);
 }
 
+bool Z3ConstraintManager::checkRangedStateConstraints(ProgramStateRef State) {
+  Solver.reset();
+  ConstraintRangeTy CR = State->get();
+
+  for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) {
+SymbolRef Sym = I.getKey();
+
+for (const auto  : I.getData()) {
+  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.
+  if (RangeTy.isNull())
+continue;
+
+  QualType SymTy;
+  Z3Expr Exp = getZ3Expr(Sym, );
+  bool isSignedTy = SymTy->isSignedIntegerOrEnumerationType();
+
+  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
+  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+
+  if (From == To) {
+Z3Expr Eq = getZ3BinExpr(Exp, SymTy, BO_EQ, FromExp, RangeTy, nullptr);
+Solver.addConstraint(Eq);
+  } else {
+Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr);
+Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
+Solver.addConstraint(Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, isSignedTy));
+  }
+}
+  }
+  // If Z3 timeouts, Z3_L_UNDEF is returned, and we assume that the state
+  // is feasible.
+  return Solver.check() != Z3_L_FALSE;
+}
+
 //===--===//
 // Internal implementation.