Verified just-in-time compiler on x86
This page contains supporting material for a POPL paper:The verified x86 machine code, C wrapper file and the C implementation of GCD, to which we compare the JIT compiler, are included in the following ZIP file:
Note: the C wrapper file makes a few calls to the operating system and might, as a result, only work on Mac OS X 10.5. The C wrapper interfaces correctly with the operating system and the JIT compiler when built using the following version of GCC:The HOL4 proofs, which are currently undocumented, are compressed into the following zip-file.$ gcc --version i686-apple-darwin9-gcc-4.0.1 (GCC) 4.0.1 (Apple Inc. build 5490) Copyright (C) 2005 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.