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