Java Bytecode Verification and Manipulation based on Model Driven Engineering

Abstract

Program transformations are frequently developed, e.g., to realize programming language extensions or dynamic program analyses such as profiling. They are typically implemented by manipulating bytecode as the availability of source code is not guaranteed. There are standard libraries such as ASM that are typically used for implementing Java bytecode manipulations. To check their correctness, they are usually tested by applying them to different programs, running the manipulated programs and observing their behaviors. As part of the second step, the Java virtual machine verifies the bytecode, which can uncover errors in the bytecode introduced by the manipulation. That approach uses different technologies that are not well linked making the process of developing and testing bytecode manipulations difficult.

In this talk, we intend to perform bytecode manipulation by using concepts and techniques of model-driven engineering. We are convinced that the declarative nature of model transformation rules allows the debugging and analyzing of bytecode manipulations in more details than classically done. Following this path, a meta-model for bytecode is needed including OCL constraints for bytecode verification. We show that basing bytecode manipulation on model transformation can provide more immediate guidance and feedback to the developer, especially when model transformation is formally based on graph transformation. Bytecode verification can take place directly in the manipulated model with the help of OCL checking, eliminating the need to use multiple technologies. In some cases, it is even possible to automatically determine application conditions under which bytecode manipulations are correct by construction; then bytecode verification after a bytecode manipulation can be avoided altogether.