Thresher
| Autor: | Sam Blackshear, Bor-Yuh Evan Chang, Manu Sridharan |
|---|---|
| Rok vydání: | 2013 |
| Předmět: |
Theoretical computer science
Computer science Programming language computer.software_genre Symbolic execution Computer Graphics and Computer-Aided Design Memory leak Reachability TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Pointer (computer programming) Binary heap computer Software Binomial heap Heap (data structure) |
| Zdroj: | PLDI |
| Popis: | 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 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|