Abstract
We present an algorithm to extract control-flow graphs from Java bytecode, considering exceptional flows. We then establish its correctness: the behavior of the extracted graphs is shown to be a sound over-approximation of the behavior of the original programs. Thus, any temporal safety property that holds for the extracted control-flow graph also holds for the original program. This makes the extracted graphs suitable for performing various static analyses, in particular model checking. The extraction proceeds in two phases. First, we translate Java bytecode into BIR, a stack-less intermediate representation. The BIR transformation is developed as a module of Sawja, a novel static analysis framework for Java bytecode. Besides Sawja’s efficiency, the resulting intermediate representation is more compact than the original bytecode and provides an explicit representation of exceptions. These features make BIR a natural starting point for sound control-flow graph extraction. Next, we formally define the transformation from BIR to control-flow graphs, which (among other features) considers the propagation of uncaught exceptions within method calls. We prove the correctness of the two-phase extraction by suitably combining the properties of the two transformations with those of an idealized control-flow graph extraction algorithm, whose correctness has been proved directly. The control-flow graph extraction algorithm is implemented in the ConFlEx tool. A number of test-cases show the efficiency and the utility of the implementation.
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.
References
Amighi, A.: Flow Graph Extraction for Modular Verification of Java Programs. Master’s thesis, KTH Royal Institute of Technology, Stockholm, Sweden (February 2011), http://www.nada.kth.se/utbildning/grukth/exjobb/rapportlistor/2011/rapporter11/amighi_afshin_11038.pdf , Ref.: TRITA-CSC-E 2011:038
Amighi, A., de Carvalho Gomes, P., Gurov, D., Huisman, M.: Provably correct control-flow graphs from Java programs with exceptions. Tech. rep., KTH Royal Institute of Technology (2012), http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-61188
Bacon, D.F., Sweeney, P.F.: Fast static analysis of C++ virtual function calls. In: OOPSLA, pp. 324–341 (1996)
Barre, N., Demange, D., Hubert, L., Monfort, V., Pichardie, D.: SAWJA API documentation (June 2011), http://javalib.gforge.inria.fr/doc/sawja-api/sawja-1.3-doc/api/index.html
Besson, F., Jensen, T., Le Métayer, D., Thorn, T.: Model checking security properties of control flow graphs. J. of Computer Security 9(3), 217–250 (2001)
Burke, M.G., Choi, J.D., 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: Proceedings of the ACM 1999 conference on Java Grande, JAVA 1999, pp. 129–141. ACM, New York (1999)
Choi, J.D., Grove, D., Hind, M., Sarkar, V.: Efficient and precise modeling of exceptions for the analysis of Java programs. SIGSOFT Softw. Eng. Notes 24, 21–31 (1999)
Demange, D., Jensen, T., Pichardie, D.: A provably correct stackless intermediate representation for Java bytecode. Tech. Rep. 7021, Inria Rennes (2009), http://www.irisa.fr/celtique/demange/bir/rr7021-3.pdf , version 3 (November 2010)
Gurov, D., Huisman, M., Sprenger, C.: Compositional verification of sequential programs with procedures. Information and Computation 206(7), 840–868 (2008)
Hubert, L., Barré, N., Besson, F., Demange, D., Jensen, T., Monfort, V., Pichardie, D., Turpin, T.: Sawja: Static Analysis Workshop for Java. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 92–106. Springer, Heidelberg (2011)
Huisman, M., Aktug, I., Gurov, D.: Program Models for Compositional Verification. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 147–166. Springer, Heidelberg (2008)
Huisman, M., Gurov, D.: CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 107–121. Springer, Heidelberg (2011)
IBM: T.J. Watson Libraries for Analysis (Wala). http://wala.sourceforge.net/
Jiang, S., Jiang, Y.: An analysis approach for testing exception handling programs. SIGPLAN Not. 42, 3–8 (2007)
Jo, J.-W., Chang, B.-M.: Constructing Control Flow Graph for Java by Decoupling Exception Flow from Normal Flow. In: Laganá, A., Gavrilova, M.L., Kumar, V., Mun, Y., Tan, C.J.K., Gervasi, O. (eds.) ICCSA 2004. LNCS, vol. 3043, pp. 106–113. Springer, Heidelberg (2004)
Milner, R.: Communicating and mobile systems: the π-calculus, ch. 6, pp. 52–53. Cambridge University Press, New York (1999)
Sinha, S., Harrold, M.J.: Criteria for testing exception-handling constructs in Java programs. In: Proceedings of the IEEE International Conference on Software Maintenance, ICSM 1999, pp. 265–276. IEEE Computer Society (1999)
Sinha, S., Harrold, M.J.: Analysis and testing of programs with exception handling constructs. IEEE Trans. Softw. Eng. 26, 849–871 (2000)
Soleimanifard, S., Gurov, D., Huisman, M.: ProMoVer: Modular Verification of Temporal Safety Properties. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 366–381. Springer, Heidelberg (2011)
Sundaresan, V., Hendren, L., Razafimahefa, C., Vallée-Rai, R., Lam, P., Gagnon, E., Godin, C.: Practical virtual method call resolution for java. In: Proceedings of the 15th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2000, pp. 264–280. ACM, New York (2000), http://doi.acm.org/10.1145/353171.353189
Vallée-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a Java Optimization Framework. In: CASCON 1999, pp. 125–135 (1999), http://www.sable.mcgill.ca/soot/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amighi, A., de C. Gomes, P., Gurov, D., Huisman, M. (2012). Sound Control-Flow Graph Extraction for Java Programs with Exceptions. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds) Software Engineering and Formal Methods. SEFM 2012. Lecture Notes in Computer Science, vol 7504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33826-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-33826-7_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33825-0
Online ISBN: 978-3-642-33826-7
eBook Packages: Computer ScienceComputer Science (R0)