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