[PATCH] D78457: [analyzer][Z3-refutation] Fix refutation BugReporterVisitor bug and refactor

[Gabor Marton via Phabricator via cfe-commits]

martong added inline comments.


================
Comment at: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2869
+      Constraints = CF.add(Constraints, Sym, C.second);
+    } else if (!OnlyForNewSymbols) {
+      // Overwrite the associated constraint of the Symbol.
----------------
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?


================
Comment at: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp:2871
+      // Overwrite the associated constraint of the Symbol.
+      Constraints = CF.remove(Constraints, Sym);
       Constraints = CF.add(Constraints, Sym, C.second);
----------------
martong wrote:
> martong wrote:
> > steakhal wrote:
> > > How can we simplify this?
> > 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)
> 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?
@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?


================
Comment at: clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp:194
+          // This assumption is false!
+          // 'y' can not be 5 if the maximal value of both x and y is 2.
+          // This bugreport must be caught by the visitor, since the constraints
----------------
martong wrote:
> `x and y` -> `x and n`.
It's not done. It is still `x and y` but should be `x and n`, isn't it?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D78457/new/

https://reviews.llvm.org/D78457