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

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to