Abstract
Static analysis is a powerful technique for automatic verification of programs but raises major engineering challenges when developing a full-fledged analyzer for a realistic language such as Java. Efficiency and precision of such a tool rely partly on low level components which only depend on the syntactic structure of the language and therefore should not be redesigned for each implementation of a new static analysis. This paper describes the Sawja library: a static analysis workshop fully compliant with Java 6 which provides OCaml modules for efficiently manipulating Java bytecode programs. We present the main features of the library, including i) efficient functional data-structures for representing a program with implicit sharing and lazy parsing, ii) an intermediate stack-less representation, and iii) fast computation and manipulation of complete programs. We provide experimental evaluations of the different features with respect to time, memory and precision.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bacon, D.F., Sweeney, P.F.: Fast static analysis of C++ virtual function calls. In: Proc. of OOPSLA 1996, pp. 324–341 (1996)
Bicolano - web home, http://mobius.inria.fr/bicolano
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proc. of PLDI 2003, San Diego, California, USA, June 7–14, pp. 196–207. ACM Press, New York (2003)
Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. SIGPLAN Not. 44(10), 243–262 (2009)
Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Survey 24(3), 293–318 (1992)
Burke, M.G., Choi, J., Fink, S., Grove, D., Hind, M., Sarkar, V., Serrano, M.J., Sreedhar, V.C., Srinivasan, H., Whaley, J.: The Jalapeño dynamic optimizing compiler for Java. In: Proc. of JAVA 1999, pp. 129–141. ACM, New York (1999)
Clerc, X.: Barista, http://barista.x9c.fr/
The Coq Proof Assistant, http://coq.inria.fr/
Dean, J., Grove, D., Chambers, C.: Optimization of object-oriented programs using static class hierarchy analysis. In: Olthoff, W. (ed.) ECOOP 1995. LNCS, vol. 952, pp. 77–101. Springer, Heidelberg (1995)
Demange, D., Jensen, T., Pichardie, D.: A provably correct stackless intermediate representation for Java bytecode. Research Report 7021, INRIA (2009), http://www.irisa.fr/celtique/ext/bir/rr7021.pdf
Ershov, A.P.: On programming of arithmetic operations. Commun. ACM 1(8), 3–6 (1958)
Grove, D., Chambers, C.: A framework for call graph construction algorithms. Toplas 23(6), 685–746 (2001)
Hubert, L.: A Non-Null annotation inferencer for Java bytecode. In: Proc. of PASTE 2008, pp. 36–42. ACM, New York (November 2008)
Hubert, L., Jensen, T., Monfort, V., Pichardie, D.: Enforcing secure object initialization in java. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 101–115. Springer, Heidelberg (2010)
IBM: The T.J. Watson Libraries for Analysis (Wala), http://wala.sourceforge.net
Jensen, T., Pichardie, D.: Secure the clones: Static enforcement of policies for secure object copying. Technical report, INRIA (June 2010); Presented at OWASP (2010)
Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system, Inria (May 2007), http://caml.inria.fr/ocaml/
Lhoták, O., Hendren, L.: Scaling java points-to analysis using SPARK. In: Wang, H. (ed.) CC 2003. LNCS, vol. 2622, pp. 153–169. Springer, Heidelberg (2003)
Lhoták, O., Hendren, L.: Evaluating the benefits of context-sensitive points-to analysis using a BDD-based implementation. ACM Trans. Softw. Eng. Methodol. 18(1) (2008)
Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Prentice Hall PTR, Englewood Cliffs (1999)
Livshits, V.B., Whaley, J., Lam, M.S.: Reflection analysis for java. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 139–160. Springer, Heidelberg (2005)
Meyer, J., Downing, T.: Java Virtual Machine. O’Reilly Associates, Sebastopol (1997), http://jasmin.sourceforge.net
Morrison, D.R.: PATRICIA — Practical algorithm to retrieve information coded in alphanumeric. J. ACM 15(4) (1968)
Pagano, B., Andrieu, O., Moniot, T., Canou, B., Chailloux, E., Wang, P., Manoury, P., Colaço, J.L.: Experience report: using Objective Caml to develop safety-critical embedded tools in a certification framework. In: Proc. of ICFP, pp. 215–220. ACM, New York (2009)
Rose, E.: Lightweight bytecode verification. J. Autom. Reason. 31(3-4), 303–334 (2003)
Spoto, F.: Julia: A generic static analyser for the Java bytecode. In: Proc. of the Workshop FTfJP (2005)
Stata, R., Abadi, M.: A type system for Java bytecode subroutines. In: Proc. of POPL 1998, pp. 149–160. ACM Press, New York (1998)
Tip, F., Palsberg, J.: Scalable propagation-based call graph construction algorithms. In: Proc. of OOPSLA 2000, pp. 281–293. ACM Press, New York (October 2000)
Vallée-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - A Java bytecode optimization framework. In: Proc. of CASCON 1999 (1999)
Whaley, J.: Dynamic optimization through the use of automatic runtime specialization. Master’s thesis, Massachusetts Institute of Technology (May 1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hubert, L. et al. (2011). Sawja: Static Analysis Workshop for Java. In: Beckert, B., Marché, C. (eds) Formal Verification of Object-Oriented Software. FoVeOOS 2010. Lecture Notes in Computer Science, vol 6528. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18070-5_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-18070-5_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-18069-9
Online ISBN: 978-3-642-18070-5
eBook Packages: Computer ScienceComputer Science (R0)