Reference
Abstract
We present a precise, path-sensitive static analysis for reasoning about heap reachability; that is, whether an object can be reached from another variable or object via pointer dereferences. Precise reachability information is useful for a number of clients, including static detection of a class of Android memory leaks. For this client, we found that the heap reachability information computed by a state-of-the-art points-to analysis was too imprecise, leading to numerous false-positive leak reports. Our analysis combines a symbolic execution capable of path-sensitivity and strong updates with abstract heap information computed by an initial flow-insensitive points-to analysis. This novel mixed representation allows us to achieve both precision and scalability by leveraging the pre-computed points-to facts to guide execution and prune infeasible paths. We have evaluated our techniques in the Thresher tool, which we used to find several developer-confirmed leaks in Android applications.
BibTeX
@string{PLDI = "ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)"}
@inproceedings{thresher-pldi13,
author = {Sam Blackshear and Bor-Yuh Evan Chang and Manu Sridharan},
title = {Thresher: Precise Refutations for Heap Reachability},
booktitle = PLDI,
year = {2013},
pages = {275-286},
}