[analyzer][Z3-refutation] Fix a refutation BugReporterVisitor bug

[steakhal]

Summary

FalsePositiveRefutationBRVisitor had a bug where the constraints were not
properly collected thus crosschecked with Z3.
This patch demonstratest and fixes that bug.

Bug:
The visitor wanted to collect all the constraints on a BugPath.
Since it is a visitor, it stated the visitation of the BugPath with the node
before the ErrorNode. As a final step, it visited the ErrorNode explicitly,
before it processed the collected constraints.

In principle, the ErrorNode should have visited before every other node.
Since the constraints were collected into a map, mapping each symbol to its
RangeSet, if the map already had a mapping with the symbol, then it was skipped.

This behavior was flawed if:
We already had a constraint on a symbol, but az the end in the ErrorNode we have
a stricter constraint on that. Therefore, this visitor would not utilize that
stricter constraint during the crosscheck validation.

[xazax.hun]

As turned out we don't even need a BugReporterVisitor for doing the crosscheck.
We should simply use the constraints of the ErrorNode since that has all the necessary information.

This should not be true. But we should definitely have a test case that proves this. The main idea is that unused symbols can be garbage collected. The problem is that the ErrorNode does not have any information about the symbols that were garbage collected earlier. This is why we need the visitor.

[steakhal]

In D78457#1991288, @xazax.hun wrote:

As turned out we don't even need a BugReporterVisitor for doing the crosscheck.
We should simply use the constraints of the ErrorNode since that has all the necessary information.

This should not be true. But we should definitely have a test case that proves this. The main idea is that unused symbols can be garbage collected. The problem is that the ErrorNode does not have any information about the symbols that were garbage collected earlier. This is why we need the visitor.

You might be right. Could you give a short example to a garbage-collected symbol?
Either way, we need to fix the bug which I stated earlier.

I tried to create a unit-test for the bug, but I miserably failed.
To call the visitor::finalizeVisitor you would need almost the entire world. (A ExprEngine, a CompilerInstance, etc.)
I also considered a lit-test, though I really doubt that is the right tool for testing this.
Since we are constantly improving the checkers, we should not bake in a false-positive bugreport which is then invalidated by the Z3 visitor...

[martong]

In D78457#1991288, @xazax.hun wrote:

As turned out we don't even need a BugReporterVisitor for doing the crosscheck.
We should simply use the constraints of the ErrorNode since that has all the necessary information.

This should not be true. But we should definitely have a test case that proves this. The main idea is that unused symbols can be garbage collected. The problem is that the ErrorNode does not have any information about the symbols that were garbage collected earlier. This is why we need the visitor.

If a symbol is unused and garbage collected then that is not part of the path constraint that leads to the ErrorNode, is it? So why should we care about constraints on an unused symbol?

[xazax.hun]

In D78457#1991780, @martong wrote:

If a symbol is unused and garbage collected then that is not part of the path constraint that leads to the ErrorNode, is it? So why should we care about constraints on an unused symbol?

Unused means it is unused at a program point.
For example:

void f(int sym1, int sym2) {
  int sym3 = sym1 * sym2;
  if (!sym1)
    return;
  // Here sym1 is no longer used, it is garbage collected from the state.
  if (sym3) {
    sym2 / 0; // This is a false positive. sym1 is 0 -> sym3 should be 0 as well, this branch is never taken. But to refute this path we need the info about sym1, that is not available in the ErrorNode state. It was garbage collected earlier.
  } 
}

I did not try this specific example. The constraint manager might be smart enough to not to report a false positive, but I hope it makes the idea clear why do we need the garbage collected symbols.

[xazax.hun]

One way to test this change would be to add a statistic that is bumped each time a path is refuted (a report to be refuted we need all of the paths refuted, so using refuted reports might not be fine-grained enough). We can test on some big projects if the refuted paths increase or decrease after the change.

[NoQ]

Yup, just take a symbol that is completely unrelated to the bug report, make an impossible constraint on it that our normal constraint manager can't refute, forget about it. That'll be the example.

[NoQ]

If a symbol is unused and garbage collected then that is not part of the path constraint that leads to the ErrorNode, is it?

It is part of the path, it's just no longer accessible in the program, so it can't be observed at the end of the path. But it did play an important role at some point in the path.

[NoQ]

(sry for the noise, just keep thinking of new things to reply)

To call the visitor::finalizeVisitor you would need almost the entire world. (A ExprEngine, a CompilerInstance, etc.)

We already have unittests that mock these objects, cf. ExprEngineConsumer (feel free to extend as necessary).

[steakhal]

• keep the visitor
• fix the bug
• add test demonstrating the bug and the fix

[steakhal]

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

2816

How can we simplify this?

[xazax.hun]

clang/lib/StaticAnalyzer/Core/BugReporter.cpp

2751

Is this function used anywhere?

[martong]

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

2811–2812

Probably you wanted to use hasContradictionUsingZ3 starting from here. (?)

2816

Could we change the visitation logic to start with the EndPathNode? I mean could we exercise FalsePositiveRefutationBRVisitor to start the visitation from EndPathNode? If that was possible then this whole patch would be way simpler.
In BugReporter.cpp:

// Run visitors on all nodes starting from the node *before* the last one.
// The last node is reserved for notes generated with {@code getEndPath}.
const ExplodedNode *NextNode = ErrorNode->getFirstPred();
while (NextNode) {

Why can't we have a different visitation order implemented specifically for the refutation visitor? (@NoQ, @xazax.hun)

clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp

194 ↗

(On Diff #259532)

x and y -> x and n.

197 ↗

(On Diff #259532)

Perhaps reportIfTrue(y > 4) would be easier to understand here. But then probably you also need a rename: ZERO_STATE_SHOULD_NOT_EXIST -> STATE_SHOULD_NOT_EXIST

[martong]

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

2816

Hmm, to answer my own question, then we would visit the ErrorNode twice. So then perhaps we should not allow any constraints in the ErrorNodes, right? What if we'd split all such ErrorNodes into a PrevNode with the constraints and a simple ErrorNode without the constraints?

[steakhal]

I'm really embarrassed that I uploaded the wrong diff.
I appologize.

Most of the comments are done :)

[xazax.hun]

LGTM, thanks!

[whisperity]

@steakhal You might want to update the patch summary before committing this to the upstream (it still mentions "not needing a visitor" 😄)

[martong]

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

2814

If there is really no other way (see my comments below) then perhaps OverwriteConstraintsOnExistingSyms would be a better naming than OnlyForNewSymbols because it expresses what exactly is happening.
In either case, could you add some documentation (comments) to addConstraints? What it does, and what is the exact meaning of the param?

2816

@xazax.hun, and others: Any thoughts on my comments above? What do you think, would it be possible to split the error node into two nodes? A PrevNode with the constraints and a simple ErrorNode without the constraints?

clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp

194 ↗

(On Diff #259532)

It's not done. It is still x and y but should be x and n, isn't it?

[xazax.hun]

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

2816

I think this would make a lot of sense in the context of this visitor. But we would need to check if it also makes sense in the context of the other parts of the analyzer (other visitors and mechanisms like bug report generation). I'd prefer such a change to be a separate patch so we can assess it easier whether it makes things easier or more complicated. I think it might be worth to experiment with.

[steakhal]

• fix patch summary
• fix patch title
• renamed function parameter to OverwriteConstraintsOnExistingSyms
• fixed x+y to x+n in the test comment

[martong]

LGTM! Thanks for addressing the comments!

[steakhal]

I'm planning to measure how impactful this patch is using the CodeChecker.
Stay tuned if you are interested!

[mikhail.ramalho]

Nice work, @steakhal!

I remember discussing with @NoQ a way of going backward on the bug report, from the error node, and never add constraints of symbols that were already collected; that way we would always have the tighter constraints.

I don't quite remember if I ever implemented it that way though.

[NoQ]

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

2816

We could add a new visitor callback, like VisitErrorNode or something, and call it before visiting all other nodes. It won't affect other visitors because they don't subscribe to it. Then drop the update in finalizeVisitor in this visitor. Visitor callbacks are currently messy; it's hard to understand what exactly they're doing by looking at their name. A cleanup is super welcome.

clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h

public:
   /// to make all PathDiagnosticPieces created by this visitor.
   static const char *getTag();
 
   PathDiagnosticPieceRef VisitNode(const ExplodedNode *Succ,
                                    BugReporterContext &BRC,
                                    PathSensitiveBugReport &BR) override;
 };
 
-/// The bug visitor will walk all the nodes in a path and collect all the
-/// constraints. When it reaches the root node, will create a refutation
-/// manager and check if the constraints are satisfiable
-class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
-private:
-  /// Holds the constraints in a given path
-  ConstraintRangeTy Constraints;
-
-public:
-  FalsePositiveRefutationBRVisitor();
-
-  void Profile(llvm::FoldingSetNodeID &ID) const override;
-
-  PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
-                                   BugReporterContext &BRC,
-                                   PathSensitiveBugReport &BR) override;
-
-  void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
-                       PathSensitiveBugReport &BR) override;
-};
-
-
 /// The visitor detects NoteTags and displays the event notes they contain.
 class TagVisitor : public BugReporterVisitor {
 public:
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 
   PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
                                    BugReporterContext &BRC,
                                    PathSensitiveBugReport &R) override;
 };
 
 } // namespace ento
 
 } // namespace clang
 
 #endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_BUGREPORTERVISITORS_H

clang/lib/StaticAnalyzer/Core/BugReporter.cpp

 #include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
 #include "clang/StaticAnalyzer/Core/Checker.h"
 #include "clang/StaticAnalyzer/Core/CheckerManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/None.h"
 #include "llvm/ADT/Optional.h"
if (!R->isValid())
       break;
 
     NextNode = Pred;
   }
 
   return Notes;
 }
 
+Optional<bool> hasContradictionUsingZ3(BugReporterContext &BRC,
+                                       const ExplodedNode *EndPathNode) {
+  // Create a refutation manager
+  llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
+  ASTContext &Ctx = BRC.getASTContext();
+  ConstraintRangeTy Constraints =
+      EndPathNode->getState()->get<ConstraintRange>();
+
+  // Add constraints to the solver
+  for (const auto &I : Constraints) {
+    const SymbolRef Sym = I.first;
+    auto RangeIt = I.second.begin();
+
+    llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
+        RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
+        /*InRange=*/true);
+    while ((++RangeIt) != I.second.end()) {
+      SMTConstraints = RefutationSolver->mkOr(
+          SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
+                                                RangeIt->From(), RangeIt->To(),
+                                                /*InRange=*/true));
+    }
+
+    RefutationSolver->addConstraint(SMTConstraints);
+  }
+
+  return RefutationSolver->check();
+}
+
 Optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
     ArrayRef<PathSensitiveBugReport *> &bugReports,
     PathSensitiveBugReporter &Reporter) {
 
   BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);
 
   while (BugPathInfo *BugPath = BugGraph.getNextBugPath()) {
     // Find the BugReport with the original location.
while (BugPathInfo *BugPath = BugGraph.getNextBugPath()) {
     BugReporterContext BRC(Reporter);
 
     // Run all visitors on a given graph, once.
     std::unique_ptr<VisitorsDiagnosticsTy> visitorNotes =
         generateVisitorsDiagnostics(R, ErrorNode, BRC);
 
     if (R->isValid()) {
       if (Reporter.getAnalyzerOptions().ShouldCrosscheckWithZ3) {
-        // If crosscheck is enabled, remove all visitors, add the refutation
-        // visitor and check again
-        R->clearVisitors();
-        R->addVisitor(std::make_unique<FalsePositiveRefutationBRVisitor>());
-
-        // We don't overrite the notes inserted by other visitors because the
-        // refutation manager does not add any new note to the path
-        generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
+        Optional<bool> IsSAT = hasContradictionUsingZ3(BRC, ErrorNode);
+        if (IsSAT.hasValue() && !IsSAT.getValue())
+          R->markInvalid("Infeasible constraints",
+                         ErrorNode->getLocationContext());
       }
 
       // Check if the bug is still valid
       if (R->isValid())
         return PathDiagnosticBuilder(
             std::move(BRC), std::move(BugPath->BugPath), BugPath->Report,
             BugPath->ErrorNode, std::move(visitorNotes));
     }

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

for (const auto ParamDecl : parms) {
     SVal BoundVal = State->getSVal(R);
     if (BoundVal.isUndef() || BoundVal.isZeroConstant()) {
       BR.markInteresting(CEnter->getCalleeContext());
       return nullptr;
     }
   }
   return nullptr;
 }
 
 //===----------------------------------------------------------------------===//
-// Implementation of FalsePositiveRefutationBRVisitor.
-//===----------------------------------------------------------------------===//
-
-FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
-    : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
-
-void FalsePositiveRefutationBRVisitor::finalizeVisitor(
-    BugReporterContext &BRC, const ExplodedNode *EndPathNode,
-    PathSensitiveBugReport &BR) {
-  // Collect new constraints
-  VisitNode(EndPathNode, BRC, BR);
-
-  // Create a refutation manager
-  llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
-  ASTContext &Ctx = BRC.getASTContext();
-
-  // Add constraints to the solver
-  for (const auto &I : Constraints) {
-    const SymbolRef Sym = I.first;
-    auto RangeIt = I.second.begin();
-
-    llvm::SMTExprRef Constraints = SMTConv::getRangeExpr(
-        RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
-        /*InRange=*/true);
-    while ((++RangeIt) != I.second.end()) {
-      Constraints = RefutationSolver->mkOr(
-          Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
-                                             RangeIt->From(), RangeIt->To(),
-                                             /*InRange=*/true));
-    }
-
-    RefutationSolver->addConstraint(Constraints);
-  }
-
-  // And check for satisfiability
-  Optional<bool> isSat = RefutationSolver->check();
-  if (!isSat.hasValue())
-    return;
-
-  if (!isSat.getValue())
-    BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
-}
-
-PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
-    const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
-  // Collect new constraints
-  const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>();
-  ConstraintRangeTy::Factory &CF =
-      N->getState()->get_context<ConstraintRange>();
-
-  // Add constraints if we don't have them yet
-  for (auto const &C : NewCs) {
-    const SymbolRef &Sym = C.first;
-    if (!Constraints.contains(Sym)) {
-      Constraints = CF.add(Constraints, Sym, C.second);
-    }
-  }
-
-  return nullptr;
-}
-
-void FalsePositiveRefutationBRVisitor::Profile(
-    llvm::FoldingSetNodeID &ID) const {
-  static int Tag = 0;
-  ID.AddPointer(&Tag);
-}
-
-//===----------------------------------------------------------------------===//
 // Implementation of TagVisitor.
 //===----------------------------------------------------------------------===//
 
 int NoteTag::Kind = 0;
 
 void TagVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
   static int Tag = 0;
   ID.AddPointer(&Tag);
 }
 
 PathDiagnosticPieceRef TagVisitor::VisitNode(const ExplodedNode *N,
                                              BugReporterContext &BRC,