Transforming Low-level Languages Using FermaT and WSL.
Doni Pracner, Zoran Budimac · 2013
One of the serious problems of modern software engineering is the perceived ageing of software. Although an application correctly written 20 years ago should still work as designed, maybe the underlying system is no longer available, making the application useless, or on the other hand maybe the user now needs a different result due to changes in the “real” world. The problems of integrating legacy libraries, often available just as assembly code, into modern software/hardware systems can be tackled in different manners. One of the most efficient approaches, especially in the short term, is to encapsulate the functionality of reliable software[Sneed 2000]. Sometimes this is not really applicable – like in situations where new features need to be added to the system or, even worse, when there are bugs in the original software, in which cases it is necessary to understand and improve the original code. The focus of this paper is on presenting two tools for working with low level code, that could help with understanding the logic behind the code and also potentially enable automatic restructuring of the code. One tool uses a subset of x86 assembly as its input, while the other one works with MicroJava bytecode. Both of the tools translate the programs into the high level language WSL that enables formally proven transformations on the source code, resulting in semantically equivalent code that should be much easier to understand. The rest of the paper is organised as follows. Section 2 presents the existing transformation system that was used in this work. Section 3 shows the main steps and principles of the assembly translation and transformation process, as well as the tools created during this research. Following is an example