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

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added inline comments.


================
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:
> > 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?
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.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D78457