一句话：将具体语义分阶段编译为 CPS 混合执行器，并用快照复用避免重复执行，在 WebAssembly 上平均加速 44.9 倍。
混合执行（concolic execution）同时用具体与符号输入运行程序，记录路径约束并求解以探索新路径。现有引擎要么基于解释器，实现简单但解释开销大；要么基于插桩，虽避免解释开销却常常为新输入从头重新执行程序。本文提出一种兼取两者优点的方法：从目标语言的具体语义出发，先构造定义式混合解释器，再通过分阶段（staging）编译消除解释开销，同时保留解释器式实现的简洁性。作者将分阶段解释器写成续延传递风格（CPS），从而在分支点捕获执行快照，并在探索其他路径时从快照恢复，避免重复执行。针对快照复用本身可能带来的开销，论文还提出启发式策略，仅在预期有益时复用快照。该方法在 WebAssembly 上实例化为混合执行编译器 GenWasym。在 184 个基准测试上，仅使用分阶段即比基于解释器的 WASP 平均加速 29.4 倍，启发式快照复用进一步提升至 44.9 倍。
Concolic execution is a variant of symbolic execution that runs a program simultaneously with concrete and symbolic inputs. It records the symbolic constraints encountered along a concrete execution path, then solves those constraints to generate inputs that explore new paths. Existing concolic engines generally follow one of two implementation strategies: Interpreter-based systems are comparatively simple to build but incur substantial interpretation overhead, while instrumentation-based systems avoid this overhead but typically re-execute the program from the beginning for each new input. In this paper, we develop a new approach that achieves the best of both worlds. Starting from the concrete semantics of the target language, we first develop a definitional concolic interpreter and stage it to compile away interpretation overhead while retaining the simplicity of an interpretation-based implementation. By expressing the staged interpreter in continuation-passing style, we can capture execution snapshots at branch points and resume from them when exploring alternative paths, avoiding repeated execution from the program entry. Because snapshot-reuse can itself incur overhead, we further develop a heuristic that favors snapshot-reuse only when it is expected to be beneficial. We instantiate this approach for WebAssembly and implement it in a new concolic-execution compiler GenWasym. Across 184 benchmarks, GenWasym with staging along achieves a 29.4X average speedup over the interpreter-based WASP; heuristic snapshot-reuse further increases the speedup to 44.9X.
@article{paperbot12083,
title = {Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots},
author = {Dinghong Zhong and Alexander Y. Bai and Mikail Khan and Guannan Wei},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839498}
}