Sound Control-Flow Graph Extraction for Java Programs with Exceptions

A. Amighi, Pedro de Carvalho Gomes, Dilian Gurov, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Citations (Scopus)
31 Downloads (Pure)

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 \textsc{ConFlEx} tool. A number of test-cases show the efficiency and the utility of the implementation.
Original languageUndefined
Title of host publication10th International Conference on Software Engineering and Formal Methods (SEFM 2012)
EditorsGeorge Eleftherakis, Mike Hinchey, Mike Holcombe
Place of PublicationBerlin
PublisherSpringer
Pages33-47
Number of pages15
ISBN (Print)978-3-642-33825-0
DOIs
Publication statusPublished - Oct 2012
Event10th International Conference on Software Engineering and Formal Methods, SEFM 2012 - Thessaloniki, Greece
Duration: 1 Oct 20125 Oct 2012
Conference number: 10

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume7504
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference10th International Conference on Software Engineering and Formal Methods, SEFM 2012
Abbreviated titleSEFM
CountryGreece
CityThessaloniki
Period1/10/125/10/12

Keywords

  • METIS-289716
  • IR-82012
  • EWI-22311
  • Program model
  • Control flow graph
  • Program Analysis

Cite this

Amighi, A., de Carvalho Gomes, P., Gurov, D., & Huisman, M. (2012). Sound Control-Flow Graph Extraction for Java Programs with Exceptions. In G. Eleftherakis, M. Hinchey, & M. Holcombe (Eds.), 10th International Conference on Software Engineering and Formal Methods (SEFM 2012) (pp. 33-47). (Lecture Notes in Computer Science; Vol. 7504). Berlin: Springer. https://doi.org/10.1007/978-3-642-33826-7_3
Amighi, A. ; de Carvalho Gomes, Pedro ; Gurov, Dilian ; Huisman, Marieke. / Sound Control-Flow Graph Extraction for Java Programs with Exceptions. 10th International Conference on Software Engineering and Formal Methods (SEFM 2012). editor / George Eleftherakis ; Mike Hinchey ; Mike Holcombe. Berlin : Springer, 2012. pp. 33-47 (Lecture Notes in Computer Science).
@inproceedings{161fa67d48ec4d88894b4d1e76f44b44,
title = "Sound Control-Flow Graph Extraction for Java Programs with Exceptions",
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 \textsc{ConFlEx} tool. A number of test-cases show the efficiency and the utility of the implementation.",
keywords = "METIS-289716, IR-82012, EWI-22311, Program model, Control flow graph, Program Analysis",
author = "A. Amighi and {de Carvalho Gomes}, Pedro and Dilian Gurov and Marieke Huisman",
note = "10.1007/978-3-642-33826-7_3",
year = "2012",
month = "10",
doi = "10.1007/978-3-642-33826-7_3",
language = "Undefined",
isbn = "978-3-642-33825-0",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "33--47",
editor = "George Eleftherakis and Mike Hinchey and Mike Holcombe",
booktitle = "10th International Conference on Software Engineering and Formal Methods (SEFM 2012)",

}

Amighi, A, de Carvalho Gomes, P, Gurov, D & Huisman, M 2012, Sound Control-Flow Graph Extraction for Java Programs with Exceptions. in G Eleftherakis, M Hinchey & M Holcombe (eds), 10th International Conference on Software Engineering and Formal Methods (SEFM 2012). Lecture Notes in Computer Science, vol. 7504, Springer, Berlin, pp. 33-47, 10th International Conference on Software Engineering and Formal Methods, SEFM 2012, Thessaloniki, Greece, 1/10/12. https://doi.org/10.1007/978-3-642-33826-7_3

Sound Control-Flow Graph Extraction for Java Programs with Exceptions. / Amighi, A.; de Carvalho Gomes, Pedro; Gurov, Dilian; Huisman, Marieke.

10th International Conference on Software Engineering and Formal Methods (SEFM 2012). ed. / George Eleftherakis; Mike Hinchey; Mike Holcombe. Berlin : Springer, 2012. p. 33-47 (Lecture Notes in Computer Science; Vol. 7504).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Sound Control-Flow Graph Extraction for Java Programs with Exceptions

AU - Amighi, A.

AU - de Carvalho Gomes, Pedro

AU - Gurov, Dilian

AU - Huisman, Marieke

N1 - 10.1007/978-3-642-33826-7_3

PY - 2012/10

Y1 - 2012/10

N2 - 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 \textsc{ConFlEx} tool. A number of test-cases show the efficiency and the utility of the implementation.

AB - 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 \textsc{ConFlEx} tool. A number of test-cases show the efficiency and the utility of the implementation.

KW - METIS-289716

KW - IR-82012

KW - EWI-22311

KW - Program model

KW - Control flow graph

KW - Program Analysis

U2 - 10.1007/978-3-642-33826-7_3

DO - 10.1007/978-3-642-33826-7_3

M3 - Conference contribution

SN - 978-3-642-33825-0

T3 - Lecture Notes in Computer Science

SP - 33

EP - 47

BT - 10th International Conference on Software Engineering and Formal Methods (SEFM 2012)

A2 - Eleftherakis, George

A2 - Hinchey, Mike

A2 - Holcombe, Mike

PB - Springer

CY - Berlin

ER -

Amighi A, de Carvalho Gomes P, Gurov D, Huisman M. Sound Control-Flow Graph Extraction for Java Programs with Exceptions. In Eleftherakis G, Hinchey M, Holcombe M, editors, 10th International Conference on Software Engineering and Formal Methods (SEFM 2012). Berlin: Springer. 2012. p. 33-47. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-33826-7_3