Specialized 3-valued logic shape analysis using structure-based refinement and loose embedding

Abstract

We consider a shape analysis framework based on 3-valued logic, and explore ways for improving its performance and scalability by means of reducing algorithmic overhead and restraining abstract state set inflation. First we propose a new approach to implementing a fast 3-valued logic analyzer, which replaces a general-purpose abstract heap refinement mechanism - accounting for most of the time spent by the reference implementation - with tailored structure-based refinement. We apply our framework to analyze a set of small Java programs manipulating singly- and doubly-linked lists, obtaining results that are comparable to those of the reference implementation, with a process 40-85 times faster and 2-11 times less memory consuming. We then propose a new definition for partial ordering of abstract heap descriptors (embedding), that trims abstract states representing "special cases" in the presence of a state representing a "general case". This extension deflates sets of abstract states by a combinatorial factor, resulting in 45-55% less structures for the same set of benchmarks. Despite its induced algorithmic overhead per operation, this modification further cuts the analysis time by 17-50%. We argue that improving on these two axes together yields a promise for greater applicability of specialized shape analysis to real-life programs. © Springer-Verlag Berlin Heidelberg 2006.