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

[Eric Li via Phabricator via cfe-commits]

li.zhe.hua added a comment.

In D131645#3716464 <https://reviews.llvm.org/D131645#3716464>, @xazax.hun wrote:

> probably you are already aware of most of this

Actually, more likely than not I don't! I don't have a strong background in PL (or, really any background), so I'm really just learning as I go, mostly from talking to @ymandel and reading through Introduction to Static Analysis <https://mitpress.mit.edu/9780262043410/> (I'm still struggling through Chapter 3!).

> - 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.

There's a `FIXME` in D131646 <https://reviews.llvm.org/D131646> that talks about unrolling, which sounds like this.

> - 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.

Good to know. I'll keep this in mind and try to dig up some more about this.

> - 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`).

Agreed. FWIW, I'm still struggling to grok this in the abstract, and don't have a concrete example readily available that makes sense to me.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D131645