Specialized 3-Valued Logic Shape Analysis using Structure-Based Refinement and Loose Embedding
Gilad Arnold (University of California, Berkeley)
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 abstraction 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), such 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 which is exponentially correlated with the number of summary nodes in the general case, 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.