A low-level memory model and an accompanying reachability predicate
A low-level memory model and an accompanying reachability predicate
复制标题
低级内存模型和附带的可达性谓词
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Zvonimir Rakamaric
中科院分区：
文献类型：
--
作者：
S. Chatterjee;Shuvendu K. Lahiri;S. Qadeer;Zvonimir Rakamaric
关于程序堆的推理，特别是如果它涉及处理无界的，动态堆分配的数据结构，如链表和数组，是具有挑战性的。此外，在系统软件中普遍存在低级指针操作的情况下，精确建模堆的合理分析变得更具挑战性。可达性谓词已经被证明对于类型安全语言中堆的推理是有用的，在类型安全语言中，内存是通过解引用对象字段来操纵的。在本文中，我们提出了一个适合推理低级指针操作的内存模型，并伴随着存在内部指针和指针算法的可达性谓词的形式化。我们已经为C程序设计了一种注释语言，它使用了新的谓词。这种语言使我们能够指定Windows内核中存在的许多有趣的数据结构的属性。我们提出了我们的经验与原型验证一组说明C基准。
Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software. The reachability predicate has already proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. In this paper, we present a memory model suitable for reasoning about low-level pointer operations that is accompanied by a formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present our experience with a prototype verifier on a set of illustrative C benchmarks.