defined as xenc inc capjbs: a relation which states that byte list bs, at machine ..... [18], and foun- dational PCC (FP
Verified Just-In-Time Compiler on x86 Magnus O. Myreen Computer Laboratory, University of Cambridge
[email protected]
Abstract This paper presents a method for creating formally correct just-intime (JIT) compilers. The tractability of our approach is demonstrated through, what we believe is the first, verification of a JIT compiler with respect to a realistic semantics of self-modifying x86 machine code. Our semantics includes a model of the instruction cache. Two versions of the verified JIT compiler are presented: one generates all of the machine code at once, the other one is incremental i.e. produces code on-demand. All proofs have been performed inside the HOL4 theorem prover. General Terms software verification, formal methods Keywords self-modifying code, compiler verification, just in time
1.
Introduction
Just-in-time (JIT) compilation is an effective technique for boosting the speed of program interpreters. The idea of JIT compilation, i.e. to dynamically translate input programs into native machine code, then execute only native code, is an old invention which dates back to 1960 [15]. However, the concept is still relevant today as JIT compilation is considered vital for competitive interpreter-based implementations of modern languages, Java, C# and ML etc. To date, there seems to be no publications on verification of a full JIT compiler. The reasons for this is likely to lie in the fact that verification of JIT compilers poses a number of challenges that are generally considered hard: 1. Compiler verification. A JIT compiler needs to correctly map its input programs down to concrete machine code. In this case the target must be real machine code (numbers), not assembly code or intermediate code which most other verified compilers seem to output. 2. Non-static code. Conventional static compilers can treat generated code purely as
