基于统一的指针分析
Unification-based Pointer Analysis without Oversharing
摘要：
指针分析对于有效地验证堆操作程序是必不可少的。尽管它已经被广泛研究，但没有公开可用的指针分析是适度精确的，同时可扩展到大型现实世界的程序。在本文中，我们表明，现有的上下文敏感的统一为基础的指针分析遭受过度共享的问题-传播太多的抽象对象在不同的程序的分析，这将阻止他们扩展到大型程序。我们提出了一个新的指针分析LLVM，称为TeaDsa，没有这样的过度共享。我们展示了如何进一步提高精度和速度的TeaDsa额外的上下文信息，如流的敏感性在调用和返回站点，和类型信息的内存访问。我们评估TeaDsa检测不安全的内存访问的验证问题，并比较它对两个国家的最先进的指针分析：SVF和SeaDsa。我们表明，TeaDsa是一个数量级的速度比SVF或SeaDsa，严格比SeaDsa更精确，令人惊讶的是，有时比SVF更精确。
英文摘要：
Pointer analysis is indispensable for effectively verifying heap-manipulating programs. Even though it has been studied extensively, there are no publicly available pointer analyses that are moderately precise while scalable to large real-world programs. In this paper, we show that existing context-sensitive unification-based pointer analyses suffer from the problem of oversharing -- propagating too many abstract objects across the analysis of different procedures, which prevents them from scaling to large programs. We present a new pointer analysis for LLVM, called TeaDsa, without such an oversharing. We show how to further improve precision and speed of TeaDsa with extra contextual information, such as flow-sensitivity at call- and return-sites, and type information about memory accesses. We evaluate TeaDsa on the verification problem of detecting unsafe memory accesses and compare it against two state-of-the-art pointer analyses: SVF and SeaDsa. We show that TeaDsa is one order of magnitude faster than either SVF or SeaDsa, strictly more precise than SeaDsa, and, surprisingly, sometimes more precise than SVF.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
