Shape Analysis of Low-Level C with Overlapping Structures

Abstract. Device drivers often keep data in multiple data structures simultaneously while embedding list or tree related records into the records containing the actual data; this results in overlapping structures. Shape analyses have traditionally relied on a graph-based representation of memory where a node corresponds to a whole record and edges to pointers. As this is ill-suited for encoding overlapping structures, we propose and formally relate two refined memory models. We demonstrate the appropriateness of these models by implementing shape analyses based on them within the TVLA framework. The implementation is exemplified using code extracted from cache managing kernel modules.

• Type: Conference
• Year: 2010
• Where: VMCAI
• Authors: Jörg Kreiker, Helmut Seidl, Vesal Vojdani
• Keywords: Multiple Data Structures, Refined Memory Models, Shape Analyses, Software Engineering, VMCAI 2010