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.
|Name||Karlsruhe Reports in Informatics|
|Publisher||Karlsruhe Institute of Technology|
|Conference||2nd International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2011|
|Period||5/10/11 → 7/10/11|
|Other||October 5-7, 2011|
- Control flow graph
- Static Analysis
- Java bytecode