基于共享溯因与双向溯因循环加速的组合形状分析

《ACM Transactions on Programming Languages and Systems》：Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration

　　

摘要AI 摘要

要查看此 AI 生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

基于双向反演的形状分析是一种组合式验证与分析技术，能够在存在复杂链接数据结构的情况下证明内存安全性。尽管该技术非常有用，但此类分析仍存在若干未解决的问题；本文针对其中两个问题进行了研究。一方面，原始分析虽然具有路径敏感性，但无法将相关分支的安全要求进行合并。这导致分析需要额外的可靠性检查，并降低了分析的精确度。我们扩展了底层的符号执行机制，并提出了一种"共享反演"框架，在该框架中为相关计算分支维护一个公共的前置条件。

另一方面，先前的实现方法将循环加速技术从正向分析移植到双向反演分析中，方法是分别对前置条件和后置条件应用这些技术，这可能导致不精确甚至不可靠的加速结果，且无法构成循环不变量。与此不同，我们提出了"双向反演循环加速"方法，该方法显式地构造并检查候选循环不变量。为此，我们还引入了一种新颖的启发式方法，称为"形状外推"。该启发式方法利用了链表类数据结构处理中的局部性特征（链表类数据结构是底层代码中最常见的数据结构），并通过外推相关形状来联合加速前置条件和后置条件。

除了使分析更加精确之外，我们的技术还使双向反演分析更加高效，因为它们在一个分析阶段中即可保证可靠性。相比之下，先前技术总是需要两个阶段（因为第一阶段可能产生不可靠的合约，因此必须对其进行验证）。我们通过实验证实，与先前技术相比，我们的技术在精确度和运行时间方面均有改进。

本工作是对会议论文 [32] 的扩展。

AI 摘要

AI 生成的摘要（实验性）

此摘要由自动化工具生成，并非由文章作者撰写或审核。其目的是支持文献发现，帮助读者评估相关性，并协助相邻研究领域的读者理解本文工作。它旨在补充作者提供的摘要，后者仍然是论文的主要概述。全文仍然是权威的正式版本。 点击此处了解更多。

点击 此处 对此摘要的准确性、清晰度和实用性进行评论。这样做将有助于改进和优化未来重新生成的版本。

要查看此 AI 生成的通俗摘要，您必须具有高级访问权限。