Statically Inferring Complex Heap, Array, and Numeric Invariants
Bill McCloskey, Thomas Reps, and Mooly Sagiv
We describe DESKCHECK, a parametric static analyzer that is able to
establish properties of programs that manipulate dynamically allocated
memory, arrays, and integers. DESKCHECK can verify
quantified invariants over mixed abstract domains, e.g.,
heap and numeric domains. These domains need only minor
extensions to work with our domain combination framework.
The technique used for managing the communication
between domains is reminiscent of the Nelson-Oppen technique
for combining decision procedures, in that the two domains share a
common predicate language to exchange shared facts. However,
whereas the Nelson-Oppen technique is limited to a common
predicate language of shared equalities, the technique described
in this paper uses a common predicate language in which shared facts
can be quantified predicates expressed in first-order logic with transitive
closure.
We explain how we used DESKCHECK to establish memory
safety of the thttpd web server's cache data structure, which
uses linked lists, a hash table, and reference counting in a single
composite data structure.
Our work
addresses some of the most complex data-structure invariants considered
in the shape-analysis literature.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)
University of Wisconsin