A low-level memory model and an accompanying reachability predicate

• Published in: International journal on software tools for technology transfer 2009-04, Vol.11 (2), p.105-116
• Main Authors: Chatterjee, Shaunak, Lahiri, Shuvendu K., Qadeer, Shaz, Rakamarić, Zvonimir
• Format: Article
• Language: English
• Subjects: Computer memory; Computer Science; Information processing; Software Engineering; Software Engineering/Programming and Operating Systems; Special Section on TACAS07; Theory of Computation
• ISSN: 1433-2779; 1433-2787
• DOI: 10.1007/s10009-009-0098-1

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.