[PATCH] D131645: [clang][dataflow] Allow user-provided lattices to provide a widen operator

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

xazax.hun accepted this revision.
xazax.hun added a comment.

Very cool! Thanks for investing into fixing the soundness issues!

A couple of ideas for the future (probably you are already aware of most of this, but open communication can help other members of the community to jump in):

- Some frameworks have the option to delay widening. I.e., only invoke the widening operator when the analysis of a loop did not converge after a certain number of iterations.
- Some frameworks implement narrowing. In the narrowing phase, we would do a couple more iterations but using the regular join instead of the widening operator. Sometimes doing multiple narrow/widen phases can be beneficial.
- Writing a widening operator can be tricky. It would be nice to add some guidance to the documentation. E.g., listing some of the algebraic properties that we expect a widening operator to have can be a lot of help for newcommers (like `bottom.widen(lat) == lat`).


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D131645