[PATCH] D124758: [analyzer] Implement assume in terms of assumeDual

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

Thanks Balazs for the report.

Here is my analysis. Looks like during the recursive simplification, `reAssume`  produces `State`s that had been created by a previous `reAssume`. Before this change, to stop the recursion it was enough to to check if the `OldState` equals to the actual `State` in `reAssume`. Now, with this change, each `assume` call evaluates both the true and the false branches, thus it is not necessary that the subsequent `reAssume` could detect an already "visited" State.
So, the obvious solution would be to have a `State` cache in the `reAssume` machinery, though, implementation details are not clear yet.

There is another really important thing. We should not continue with `reAssume` if the `State` is `posteriorlyOverConstrained`.

   LLVM_NODISCARD ProgramStateRef reAssume(ProgramStateRef State,
                                           const RangeSet *Constraint,
                                           SVal TheValue) {
  +  if (State->isPosteriorlyOverconstrained())
  +    return nullptr;
     if (!Constraint)
       return State;

This change in itself reduced the run-time of the analysis to 16 seconds, on my machine. However, the repetition of States should still be addressed. I am going to upload the upper patch for a starter.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D124758