论文标题
内存有效的固定点计算
Memory-Efficient Fixpoint Computation
论文作者
论文摘要
静态分析的实际采用通常需要进行绩效交易精度。本文着重于提高抽象解释的记忆效率而不牺牲精度或时间效率。在计算上，抽象的解释减少了将程序不变性推断为计算一组方程的固定点的问题。本文提出了一种将Bourdoncle迭代策略中的内存足迹最小化，这是一种广泛使用的FIXPOINT计算技术。我们的技术对所使用的抽象领域不可知。我们证明，在计算相同结果的同时，您的技术是Bourdoncle迭代策略的最佳（即，它导致最低记忆足迹）。我们通过在称为Mikos的工具中实现技术的功效，该工具扩展了最先进的抽象解释器IKOS。在验证用户提供的断言时，与IKO相比，Mikos的峰值记忆使用量降低到平均为4.07％（24.57倍）。与IKO相比，在进行概要术缓冲流分析时，Mikos的峰值记忆使用量降低至平均43.7％（2.29倍）。
Practical adoption of static analysis often requires trading precision for performance. This paper focuses on improving the memory efficiency of abstract interpretation without sacrificing precision or time efficiency. Computationally, abstract interpretation reduces the problem of inferring program invariants to computing a fixpoint of a set of equations. This paper presents a method to minimize the memory footprint in Bourdoncle's iteration strategy, a widely-used technique for fixpoint computation. Our technique is agnostic to the abstract domain used. We prove that our technique is optimal (i.e., it results in minimum memory footprint) for Bourdoncle's iteration strategy while computing the same result. We evaluate the efficacy of our technique by implementing it in a tool called MIKOS, which extends the state-of-the-art abstract interpreter IKOS. When verifying user-provided assertions, MIKOS shows a decrease in peak-memory usage to 4.07% (24.57x) on average compared to IKOS. When performing interprocedural buffer-overflow analysis, MIKOS shows a decrease in peak-memory usage to 43.7% (2.29x) on average compared to IKOS.
