This is an archive of the discontinued LLVM Phabricator instance.

[clang][dataflow] Allow user-provided lattices to provide a widen operator
AcceptedPublic

Authored by li.zhe.hua on Aug 10 2022, 9:57 PM.

Details

Summary

In order to better support convergence in a sound way, we allow users
to provide a widen operator for their lattice type. This can be
implemented for lattices of infinite (or sufficiently large) height in
order to reach convergence in loops.

If not provided, this defaults to the existing join operation that
is required to be defined. This is a sound default, as join would be
at least more precise than a theoretical widen.

Tracking issue: #56931

Depends on D131644

Diff Detail

Event Timeline

li.zhe.hua created this revision.Aug 10 2022, 9:57 PM
Herald added a project: Restricted Project. · View Herald Transcript
li.zhe.hua requested review of this revision.Aug 10 2022, 9:57 PM
Herald added a project: Restricted Project. · View Herald TranscriptAug 10 2022, 9:57 PM
Herald added a subscriber: cfe-commits. · View Herald Transcript
li.zhe.hua edited the summary of this revision. (Show Details)Aug 10 2022, 10:05 PM
li.zhe.hua added reviewers: ymandel, xazax.hun.
ymandel added a subscriber: gribozavr.
ymandel accepted this revision.Aug 11 2022, 5:50 AM
ymandel added inline comments.
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
119

nit: why c++11 (vs something later)?

This revision is now accepted and ready to land.Aug 11 2022, 5:50 AM
li.zhe.hua marked an inline comment as done.Aug 11 2022, 7:52 AM
li.zhe.hua added inline comments.
clang/unittests/Analysis/FlowSensitive/TypeErasedDataflowAnalysisTest.cpp
119

Consistency with runAnalysis defined above. FWIW, I don't think int x = 0; is materially different in any standard, and all I really want out of this is an ASTContext to pass to TypeErasedDataflowAnalysis to satisfy its constructor.

sgatev accepted this revision.Aug 11 2022, 9:11 AM
xazax.hun accepted this revision.Aug 11 2022, 9:24 AM

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).
li.zhe.hua marked an inline comment as done.

Add FIXME

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

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 (I'm still struggling through Chapter 3!).

That is a really great book, I liked it a lot :) I implemented a small interpreter + static analysis framework for the graphical language in the book: https://github.com/Xazax-hun/domains
It is still half-baked, but it is doing something and can generate some ugly graphics.

gribozavr2 accepted this revision.Aug 11 2022, 1:06 PM