WebAssembly is a modern low-level intermediate representation (IR) and a popular compilation target. The official specification of WebAssembly provides a small-step reduction semantics. Unlike other common low-level IRs, WebAssembly provides structured control-flow constructs, whose reduction rules are complicated by additional “administrative instructions” in the reference semantics. In light of Danvy’s functional correspondence constructed through defunctionalization and refunctionalization, I will present an alternative natural semantics for WebAssembly in continuation-passing style (CPS), which can be implemented as a concise, compositional, and tail-recursive definitional interpreter. Using continuations from the meta-language streamlines the semantics by eliminating the need for additional administrative instructions.

I will further talk about the application of such a CPS semantics for efficient test case generation of WebAssembly. We first derive a symbolic execution semantics of WebAssembly in CPS, then obtain a compiler from that by staging, where the generated code performs test case generation. Since our CPS semantics are compositional, they are amenable to two-level programming such as partial evaluation or staging. Therefore, we mix transformation and symbolic execution along with continuation for efficient test case generation of WebAssembly.