Summary:
This fixes (if in a hackish way) an inherently quadratic behaviour in
the disjunctive domain when analysing loops: If you start with some
disjuncts `D1 \/ ... \/ Dn` and go once around the loop, you will end up
with disjuncts `(D1 \/ ... \/ Dn) \/ (D1' \/ ... \/ Dn')` assuming that
for all `i`, `{ Di } body of loop { Di' }` (in practice there is the
added difficulty that the post of the body of the loop can be a
disjunction too instead of a single abstract state). Assuming this isn't
a fixpoint, we would then go around the loop again from `D1`, ..., `Dn`,
`D1'`, ..., `Dn'`. However we already know what the posts of `D1` to `Dn`
are!
This attempts to curb duplicate work by marking the disjuncts in `prev`
as "visited" and instructing symbolic execution to skip visited states.
Then, once convergence is detected (from within `widen` for now) we mark
again all states as unvisited so that whatever is after the loop gets
symbolically executed.
This is a hack because ideally the AI scheduler would know about
disjunctive domain and schedule individual disjuncts for analysis.
However that would be a much bigger change. Let's see if the hack is
enough for now.
Reviewed By: mbouaziz
Differential Revision: D14258491
fbshipit-source-id: 21454398c
Jules Villard
a49645ed61