A Shape Neutral Analysis for Graph Data-structures
G. Duck, J. Jaffar and R. Yap
Abstract
Malformed data-structures can lead to runtime errors such
as arbitrary memory access or corruption. Low level languages
make it easy to have bugs which can lead to malformed
data structures as they allow direct pointer manipulation
-- making reasoning over data-structure properties
challenging. In this paper we present a constraint-based
program analysis that checks data-structure integrity, w.r.t.
given target data-structure properties, suitable for detecting
data-structure bugs in low level code. A key property of
our analysis is that it is 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. As a
result, the analysis can be applied to a wide range of datastructure
manipulating programs, including those that use
lists, trees, DAGs, etc., all of which are speci c kinds of
graph data-structures. Furthermore, the analysis is powerful
enough to detect certain classes of critical memory errors
that can lead to data corruption or information leaks. Our
analysis is modular and can be used to analyze code in libraries
and components without requiring whole programs.
Experimental results show that our approach works well in
practice.