[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:2822
     PathSensitiveBugReport &BR) {
   // Collect new constraints
+  addConstraints(EndPathNode, /*OnlyForNewSymbols=*/false);
----------------
Probably you wanted to use `hasContradictionUsingZ3` starting from here. (?)


================
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);
----------------
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)


================
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
----------------
`x and y` -> `x and n`.


================
Comment at: clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp:197
+          // of the bugpath are UnSAT.
+          reportIfCanBeZero(y - 5);
+        }
----------------
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`


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D78457