M. Eichberg
F. Kübler
M. Mezini
ABSTRACT
Static analyses which compute conceptually independent information, e.g., class immutability or method purity are typically developed as standalone, closed analyses. Complementary information that could improve the analyses is either ignored by making a sound over-approximation or it is also computed by the analyses, but at a rudimentary level. For example, an immutability analysis requires field mutability information, alias/escape information, and information about the concurrent behavior of methods to correctly classify classes like java.lang.String or java.util.BigDecimal. As a result, without properly supporting the integration of independently developed, mutually benefiting analysis, many analyses will not correctly classify relevant entities.
We propose to use explicitly reified lattices that encode the information about a source code element's properties (e.g., a method's purity or a class' immutability) as the sole interface between mutually dependent analyses. This enables the composition of multiple analyses. Our case study shows that using such an approach enables highly scalable, lightweight implementations of modularized static analyses.
- S. Arzt, S. Rasthofer, C. Fritz, E. Bodden, A. Bartel, J. Klein, Y. Le Traon, D. Octeau, and P. McDaniel. 2014. FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps (PLDI). Google Scholar
Digital Library
- M. Bravenboer and Y. Smaragdakis. 2009. Strictly Declarative Specification of Sophisticated Points-to Analyses (OOPSLA). Google ScholarDigital Library
- J.-D. Choi, M. Gupta, M. Serrano, V. C. Sreedhar, and S. Midkiff. 1999. Escape Analysis for Java. In OOPSLA. Google ScholarDigital Library
- P. Cousot and R. Cousot. 2014. Abstract Interpretation: Past, Present and Future (CSL-LICS). Google ScholarDigital Library
- M. Eichberg, M. Kahl, D. Saha, M. Mezini, and K. Ostermann. 2007. Automatic Incrementalization of Prolog Based Static Analyses (PADL). Google ScholarDigital Library
- M. Eichberg, M. Mezini, S. Kloppenburg, K. Ostermann, and B. Rank. 2006. Integrating and Scheduling an Open Set of Static Analyses. (ASE). Google ScholarDigital Library
- Torbjörn Ekman and Görel Hedin. 2007. The Jastadd Extensible Java Compiler (OOPSLA). Google ScholarDigital Library
- M. Finifter, A. Mettler, N. Sastry, and D. Wagner. 2008. Verifiable functional purity in Java (CCS). Google ScholarDigital Library
- P. Haller, S. Geries, M. Eichberg, and G. Salvaneschi. 2016. Reactive Async: expressive deterministic concurrency (SCALA). Google ScholarDigital Library
- W. Huang and A. Milanova. 2012. ReImInfer: Method purity inference for Java (FSE). Google ScholarDigital Library
- W. Huang, A. Milanova, W. Dietl, and M. D. Ernst. 2012. ReIm & ReImInfer: Checking and inference of reference immutability and method purity (OOPSLA). Google ScholarDigital Library
- P. Klint, T. van der Storm, and J. J. Vinju. 2009. RASCAL: A Domain Specific Language for Source Code Analysis and Manipulation (SCAM). Google ScholarDigital Library
- T. Kotzmann and H. Mössenböck. 2005. Escape Analysis in the Context of Dynamic Compilation and Deoptimization (VEE). Google ScholarDigital Library
- Sorin Lerner, David Grove, and Craig Chambers. 2002. Composing dataflow analyses and transformations (POPL). Google ScholarDigital Library
- Ralf M. 2014. Scalable Automated Incrementalization for Real-Time Static Analyses. Ph.D. Dissertation. Technische Universität Darmstadt.Google Scholar
- F. Nielson, H. Nielson, and C. Hankin. 2005. Principles of Program Analysis. Google ScholarDigital Library
- D. Pearce. 2011. JPure: a modular purity system for Java (CC). Google ScholarDigital Library
- T. Reps, S. Horwitz, and M. Sagiv. 1995. Precise Interprocedural Dataflow Analysis via Graph Reachability (POPL). Google ScholarDigital Library
- J. Rodriguez and O. Lhoták. 2011. Actor-based parallel dataflow analysis (CC). Google ScholarDigital Library
- Mooly Sagiv, Thomas Reps, and Susan Horwitz. 1996. Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science 167 (1996). Google ScholarDigital Library
- J. Späth, L. Nguyen Quang Do, K. Ali, and E. Bodden. 2016. Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java (ECOOP).Google Scholar
Recommendations
Improving static analyses of C programs with conditional predicates
Static code analysis is increasingly used to guarantee the absence of undesirable behaviors in industrial programs. Designing sound analyses is a continuing trade-off between precision and complexity. Notably, dataflow analyses often perform overly wide ...
Numerical static analysis with Soot
SOAP '13: Proceedings of the 2nd ACM SIGPLAN International Workshop on State Of the Art in Java Program analysisNumerical static analysis computes an approximation of all the possible values that a numeric variable may assume, in any execution of the program. Many numerical static analyses have been proposed exploiting the theory of abstract interpretation, which ...
Design and implementation of sparse global analyses for C-like languages
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and ImplementationIn this article we present a general method for achieving global static analyzers that are precise, sound, yet also scalable. Our method generalizes the sparse analysis techniques on top of the abstract interpretation framework to support relational as ...
Comments