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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
