Translation validation for javascript JIT compiler

Abstract

We present TurboTV, a translation validator for the JavaScript (JS) just-in-time (JIT) compiler of Chromium. While JS engines have become a crucial part of various software systems, their emerging adaption of JIT compilation makes it increasingly challenging to ensure their correctness. We tackle this problem with an SMT-based translation validation that checks whether a specific compilation is semantically correct. We formally define the semantics of IR of TurboFan (JIT compiler of Chromium) and its SMT encoding. Furthermore, we propose two novel techniques to effectively apply translation validation to TurboFan. First, we design a staged strategy by carefully assuming that JS does not have undefined behaviors. This allows us to decompose the whole correctness checking into simpler ones. Second, we propose a generation-based strategy for translation validation of JIT compilers. Due to its dynamic nature, it is hard to apply translation validation in a traditional way. Thus, we generate a large program corpus curated to cover diverse optimization passes and validate their compilation. We evaluate TurboTV on various sets of JS programs and demonstrate the effectiveness of our approach.