[PATCH] D130306: [clang][dataflow] Analyze calls to in-TU functions

Gábor Horváth via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Mon Jul 25 09:47:28 PDT 2022


xazax.hun added a comment.

Thanks! Knowing the context, I am much happier with the direction overall. Is the plan to analyze a mock of std::optional instead of the actual code in the STL? How will that mock be shipped? Would that be embedded in the binary?

In D130306#3676475 <https://reviews.llvm.org/D130306#3676475>, @ymandel wrote:

> Gabor, I fully agree. We need to start paying down the debt on the unsoundness, reducing it where possible and otherwise giving users control over whether to incur it.

I'm glad that this is still on the roadmap. I am a bit worried about how hard it will be to make the current memory model sound. Generally, I saw some researchers arguing that the access path approach <https://www.youtube.com/watch?v=LTRykVVDfgE> approach is a better fit for dataflow analysis. See this paper <https://bodden.de/pubs/bodden18secret.pdf> as an example. Although admittedly, I do not fully agree with everything they claim, they focus on distributive problems in that paper, and I found that most actual problems that we want to solve are not distributive. But whatever model we end up using, to restore soundness we might need to introduce a way to summarize certain constructs in our memory model. There are some ideas in this <https://arxiv.org/pdf/1403.4910.pdf> survey paper.

> However, as Sam wrote, we did not expect to be incurring any new unsoundness here.

I fully agree that this patch itself will not introduce new unsoundness (after the fixme mentioned in the description is resolved). My main concerns were:

- The framework started to feel more similar to symbolic execution than abstract interpretation, see the answer to this <https://cstheory.stackexchange.com/questions/19708/symbolic-execution-is-a-case-of-abstract-interpretation> question on the differences.
- I was a bit worried that adding more features before fixing the soundness issues might make fixing those problems harder.
- I was not sure the current approach would scale to general context-sensitive analysis. But looks like that is a non-goal for now. Doing this to model certain types of interest makes sense to me and is a good first step.

Overall, I am excited for context-sensitive analysis, and some of my concerns are addressed. Looking forward to the follow-up patches :)


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D130306



More information about the cfe-commits mailing list