Shape Analysis of Low-Level C With Overlapping Structures

Date Added: Oct 2009
Format: PDF

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, the authors propose and formally relate two refined memory models. They 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.