基于图的数据结构的形状中性分析
Shape Neutral Analysis of Graph-based Data-structures
摘要：
格式错误的数据结构可能导致运行时错误，如任意内存访问或损坏。尽管如此，低级别堆操作程序的数据结构属性推理仍然具有挑战性。在本文中，我们提出了一个基于约束的程序分析，检查数据结构的完整性，w.r.t.给定目标数据结构属性，因为堆由程序操纵。我们的方法是使用来自目标程序的类型定义自动生成属性的求解器。生成的求解器是使用内置堆、整数和等式求解器的约束处理规则（Constraint Handling Rules，简称CLR）扩展实现的。我们的程序分析的一个关键属性是目标数据结构属性是形状中性的，即，该分析不检查与给定数据结构图形形状相关的属性，例如双链表与树。尽管如此，分析可以检测到错误的数据结构操作程序，包括那些使用列表，树，DAG，图形等，我们提出了一个实现，使用的可满足性模约束处理规则（SMESTO）系统。实验结果表明，我们的方法可以很好地为现实世界的C程序。
英文摘要：
Malformed data-structures can lead to runtime errors such as arbitrary memory access or corruption. Despite this, reasoning over data-structure properties for low-level heap manipulating programs remains challenging. In this paper we present a constraint-based program analysis that checks data-structure integrity, w.r.t. given target data-structure properties, as the heap is manipulated by the program. Our approach is to automatically generate a solver for properties using the type definitions from the target program. The generated solver is implemented using a Constraint Handling Rules (CHR) extension of built-in heap, integer and equality solvers. A key property of our program analysis is that the target data-structure properties are shape neutral, i.e., the analysis does not check for properties relating to a given data-structure graph shape, such as doubly-linked-lists versus trees. Nevertheless, the analysis can detect errors in a wide range of data-structure manipulating programs, including those that use lists, trees, DAGs, graphs, etc. We present an implementation that uses the Satisfiability Modulo Constraint Handling Rules (SMCHR) system. Experimental results show that our approach works well for real-world C programs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
