Provably Correct Control-Flow Graphs from Java Programs with Exceptions

A. Amighi, Pedro de Carvalho Gomes, Marieke Huisman

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

36 Downloads (Pure)

Abstract

We present an algorithm to extract flow graphs from Java bytecode, focusing on exceptional control flows. We prove its correctness, meaning that the behaviour of the extracted control-flow graph is an over-approximation of the behaviour of the original program. Thus any safety property that holds for the extracted control-flow graph also holds for the original program. This makes control-flow graphs suitable for performing different static analyses. For precision and efficiency, the extraction is performed in two phases. In the first phase the program is transformed into a BIR program, where BIR is a stack-less intermediate representation of Java bytecode; in the second phase the control-flow graph is extracted from the BIR representation. To prove the correctness of the two-phase extraction, we also define a direct extraction algorithm, whose correctness can be proven immediately. Then we show that the behaviour of the control-flow graph extracted via the intermediate representation is an over-approximation of the behaviour of the directly extracted graphs, and thus of the original program.
Original languageUndefined
Title of host publicationPapers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11
Place of PublicationKarlsruhe
PublisherKarlsruhe Institute of Technology
Pages31-48
Number of pages18
ISBN (Print)2190-4782
Publication statusPublished - Oct 2011

Publication series

NameKarlsruhe Reports in Informatics
PublisherKarlsruhe Institute of Technology
Number26
Volume26
ISSN (Print)2190-4782

Keywords

  • METIS-285024
  • IR-79610
  • Control flow graph
  • EWI-21319
  • Static Analysis
  • CR-D.3.1
  • Java bytecode

Cite this

Amighi, A., de Carvalho Gomes, P., & Huisman, M. (2011). Provably Correct Control-Flow Graphs from Java Programs with Exceptions. In Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11 (pp. 31-48). (Karlsruhe Reports in Informatics; Vol. 26, No. 26). Karlsruhe: Karlsruhe Institute of Technology.
Amighi, A. ; de Carvalho Gomes, Pedro ; Huisman, Marieke. / Provably Correct Control-Flow Graphs from Java Programs with Exceptions. Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11. Karlsruhe : Karlsruhe Institute of Technology, 2011. pp. 31-48 (Karlsruhe Reports in Informatics; 26).
@inproceedings{ac3cd23e0a4c4da78d81e5e5b87bd713,
title = "Provably Correct Control-Flow Graphs from Java Programs with Exceptions",
abstract = "We present an algorithm to extract flow graphs from Java bytecode, focusing on exceptional control flows. We prove its correctness, meaning that the behaviour of the extracted control-flow graph is an over-approximation of the behaviour of the original program. Thus any safety property that holds for the extracted control-flow graph also holds for the original program. This makes control-flow graphs suitable for performing different static analyses. For precision and efficiency, the extraction is performed in two phases. In the first phase the program is transformed into a BIR program, where BIR is a stack-less intermediate representation of Java bytecode; in the second phase the control-flow graph is extracted from the BIR representation. To prove the correctness of the two-phase extraction, we also define a direct extraction algorithm, whose correctness can be proven immediately. Then we show that the behaviour of the control-flow graph extracted via the intermediate representation is an over-approximation of the behaviour of the directly extracted graphs, and thus of the original program.",
keywords = "METIS-285024, IR-79610, Control flow graph, EWI-21319, Static Analysis, CR-D.3.1, Java bytecode",
author = "A. Amighi and {de Carvalho Gomes}, Pedro and Marieke Huisman",
note = "eemcs-eprint-21319",
year = "2011",
month = "10",
language = "Undefined",
isbn = "2190-4782",
series = "Karlsruhe Reports in Informatics",
publisher = "Karlsruhe Institute of Technology",
number = "26",
pages = "31--48",
booktitle = "Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11",

}

Amighi, A, de Carvalho Gomes, P & Huisman, M 2011, Provably Correct Control-Flow Graphs from Java Programs with Exceptions. in Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11. Karlsruhe Reports in Informatics, no. 26, vol. 26, Karlsruhe Institute of Technology, Karlsruhe, pp. 31-48.

Provably Correct Control-Flow Graphs from Java Programs with Exceptions. / Amighi, A.; de Carvalho Gomes, Pedro; Huisman, Marieke.

Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11. Karlsruhe : Karlsruhe Institute of Technology, 2011. p. 31-48 (Karlsruhe Reports in Informatics; Vol. 26, No. 26).

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

TY - GEN

T1 - Provably Correct Control-Flow Graphs from Java Programs with Exceptions

AU - Amighi, A.

AU - de Carvalho Gomes, Pedro

AU - Huisman, Marieke

N1 - eemcs-eprint-21319

PY - 2011/10

Y1 - 2011/10

N2 - We present an algorithm to extract flow graphs from Java bytecode, focusing on exceptional control flows. We prove its correctness, meaning that the behaviour of the extracted control-flow graph is an over-approximation of the behaviour of the original program. Thus any safety property that holds for the extracted control-flow graph also holds for the original program. This makes control-flow graphs suitable for performing different static analyses. For precision and efficiency, the extraction is performed in two phases. In the first phase the program is transformed into a BIR program, where BIR is a stack-less intermediate representation of Java bytecode; in the second phase the control-flow graph is extracted from the BIR representation. To prove the correctness of the two-phase extraction, we also define a direct extraction algorithm, whose correctness can be proven immediately. Then we show that the behaviour of the control-flow graph extracted via the intermediate representation is an over-approximation of the behaviour of the directly extracted graphs, and thus of the original program.

AB - We present an algorithm to extract flow graphs from Java bytecode, focusing on exceptional control flows. We prove its correctness, meaning that the behaviour of the extracted control-flow graph is an over-approximation of the behaviour of the original program. Thus any safety property that holds for the extracted control-flow graph also holds for the original program. This makes control-flow graphs suitable for performing different static analyses. For precision and efficiency, the extraction is performed in two phases. In the first phase the program is transformed into a BIR program, where BIR is a stack-less intermediate representation of Java bytecode; in the second phase the control-flow graph is extracted from the BIR representation. To prove the correctness of the two-phase extraction, we also define a direct extraction algorithm, whose correctness can be proven immediately. Then we show that the behaviour of the control-flow graph extracted via the intermediate representation is an over-approximation of the behaviour of the directly extracted graphs, and thus of the original program.

KW - METIS-285024

KW - IR-79610

KW - Control flow graph

KW - EWI-21319

KW - Static Analysis

KW - CR-D.3.1

KW - Java bytecode

M3 - Conference contribution

SN - 2190-4782

T3 - Karlsruhe Reports in Informatics

SP - 31

EP - 48

BT - Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11

PB - Karlsruhe Institute of Technology

CY - Karlsruhe

ER -

Amighi A, de Carvalho Gomes P, Huisman M. Provably Correct Control-Flow Graphs from Java Programs with Exceptions. In Papers the of 2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS'11. Karlsruhe: Karlsruhe Institute of Technology. 2011. p. 31-48. (Karlsruhe Reports in Informatics; 26).