[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

2871

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

2822

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

2871

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

197

x and y -> x and n.

200

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

2871

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

2869

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?

2871

@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

197

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

2871

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

2871

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:
   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;
+  void addConstraints(const ExplodedNode *N, bool OnlyForNewSymbols);
 };
 
 
 /// The visitor detects NoteTags and displays the event notes they contain.
 class TagVisitor : public BugReporterVisitor {
 public:
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 

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<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.
     PathSensitiveBugReport *R = BugPath->Report;
while (BugPathInfo *BugPath = BugGraph.getNextBugPath()) {
 
     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
+        // We don't overwrite the notes inserted by other visitors because the
         // refutation manager does not add any new note to the path
         generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
       }
 
       // Check if the bug is still valid
       if (R->isValid())
         return PathDiagnosticBuilder(
             std::move(BRC), std::move(BugPath->BugPath), BugPath->Report,

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

 //===----------------------------------------------------------------------===//
 
 FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
     : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
 
 void FalsePositiveRefutationBRVisitor::finalizeVisitor(
     BugReporterContext &BRC, const ExplodedNode *EndPathNode,
     PathSensitiveBugReport &BR) {
   // Collect new constraints
-  VisitNode(EndPathNode, BRC, BR);
+  addConstraints(EndPathNode, /*OnlyForNewSymbols=*/false);
 
   // 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(
+    llvm::SMTExprRef SMTConstraints = 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,
+      SMTConstraints = RefutationSolver->mkOr(
+          SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
                                                 RangeIt->From(), RangeIt->To(),
                                                 /*InRange=*/true));
     }
 
-    RefutationSolver->addConstraint(Constraints);
+    RefutationSolver->addConstraint(SMTConstraints);
   }
 
   // And check for satisfiability
-  Optional<bool> isSat = RefutationSolver->check();
-  if (!isSat.hasValue())
+  Optional<bool> IsSAT = RefutationSolver->check();
+  if (!IsSAT.hasValue())
     return;
 
-  if (!isSat.getValue())
+  if (!IsSAT.getValue())
     BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
 }
 
-PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
-    const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
+void FalsePositiveRefutationBRVisitor::addConstraints(const ExplodedNode *N,
+                                                      bool OnlyForNewSymbols) {
   // 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)) {
+      // This symbol is new, just add the constraint.
+      Constraints = CF.add(Constraints, Sym, C.second);
+    } else if (!OnlyForNewSymbols) {
+      // Overwrite the associated constraint of the Symbol.
+      Constraints = CF.remove(Constraints, Sym);
       Constraints = CF.add(Constraints, Sym, C.second);
     }
   }
+}
 
+PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
+    const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
+  addConstraints(N, /*OnlyForNewSymbols=*/true);
   return nullptr;
 }
 
 void FalsePositiveRefutationBRVisitor::Profile(
     llvm::FoldingSetNodeID &ID) const {
   static int Tag = 0;
   ID.AddPointer(&Tag);
 }

clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp

TEST(FalsePositiveRefutationBRVisitor, UnSatAtErrorNodeWithNewSymbolNoReport) {
   std::string Diags2;
   EXPECT_TRUE(runCheckerOnCodeWithArgs<addFalsePositiveGenerator>(
       Code, LazyAssumeArgs, Diags2));
   EXPECT_EQ(Diags2,
             "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n"
             "test.FalsePositiveGenerator:CAN_BE_TRUE\n");
 }
 
+TEST(FalsePositiveRefutationBRVisitor,
+     UnSatAtErrorNodeDueToRefinedConstraintNoReport) {
+  SKIP_WITHOUT_Z3;
+  constexpr auto Code = R"(
+    void reportIfCanBeTrue(bool);
+    void reachedWithNoContradiction();
+    void test(unsigned x, unsigned n) {
+      if (n >= 1 && n <= 2) {
+        if (x >= 3)
+          return;
+        // x: [0,2] and n: [1,2]
+        int y = x + n; // y: '(x+n)' Which is in approximately between 1 and 4.
+
+        // Registers the symbol 'y' with the constraint [1, MAX] in the true
+        // branch.
+        if (y > 0) {
+          // Since the x: [0,2] and n: [1,2], the 'y' is indeed greater than
+          // zero. If we emit a warning here, the constraints on the BugPath is
+          // SAT. Therefore that report is NOT invalidated.
+          reachedWithNoContradiction(); // 'y' can be greater than zero. OK
+
+          // If we ask the analyzer whether the 'y' can be 5. It won't know,
+          // therefore, the state will be created where the 'y' expression is 5.
+          // Although, this assumption is false!
+          // 'y' can not be 5 if the maximal value of both x and y is 2.
+          // The BugPath which become UnSAT in the ErrorNode with a refined
+          // constraint, should be invalidated.
+          reportIfCanBeTrue(y == 5);
+        }
+      }
+    })";
+
+  std::string Diags;
+  EXPECT_TRUE(runCheckerOnCodeWithArgs<addFalsePositiveGenerator>(
+      Code, LazyAssumeAndCrossCheckArgs, Diags));
+  EXPECT_EQ(Diags,
+            "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n");
+  // Single warning. The second report was invalidated by the visitor.
+
+  // Without enabling the crosscheck-with-z3 both reports are displayed.
+  std::string Diags2;
+  EXPECT_TRUE(runCheckerOnCodeWithArgs<addFalsePositiveGenerator>(
+      Code, LazyAssumeArgs, Diags2));
+  EXPECT_EQ(Diags2,
+            "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n"
+            "test.FalsePositiveGenerator:CAN_BE_TRUE\n");
+}
+
 } // namespace
 } // namespace ento
 } // namespace clang