- Main
Practical Shape Analysis
- McCloskey, William Terrence
- Advisor(s): Brewer, Eric
Abstract
Shape analysis is a program analysis technique used to prove that
imperative programs using manual memory management will not crash. In
the past, shape analysis has been applied to data structures like
linked lists and binary trees. It has also been used on
simplified versions of Windows device drivers.
We describe techniques that allow us to apply shape analysis to data
structures that occur commonly in systems code. These data structures
often use arrays, hash tables, C strings, and buffers of a known
size. Sometimes, memory in these data structures is managed by manual
reference counting. Analyzing such code is difficult or impossible
with existing shape analyses. Most difficult of all, many data
structures use several of these patterns at the same time, such as a
hash table pointing to reference counted objects through which a
doubly linked list threads.
We describe an analysis capable of handling these data structures
easily and efficiently. Our technique uses abstract interpretation
over the combination of two abstract domains. One, based on
three-valued logic, is used for analyzing the heap. The other domain
reasons about integers and set cardinality. The key feature of the
combined domain is that quantified facts can be shared between the
integer and heap domains. The precision we achieve is significantly
greater than if either domain were used independently.
Besides improvements in precision, we also describe changes that make
both domains more scalable and efficient. We present the results of
experiments analyzing the cache data structure of the thttpd web
server, which uses a hash table, linked lists, and reference counting
in a single data structure. We successfully prove the absence of
memory errors in about two minutes.
Main Content
Enter the password to open this PDF file:
-
-
-
-
-
-
-
-
-
-
-
-
-
-