AI 中文总结
本文针对WebAssembly开发了融合分阶段、延续和快照技术的Concolic执行编译器GenWasym，相比WASP实现了最高44.9倍的加速，兼顾了Concolic执行的简洁性与高效性。
AI 中文摘要
符号化与 concretized 执行（Concolic执行）是符号执行的一种变体，它同时用 concrete 输入和符号输入运行程序，记录 concrete 执行路径上遇到的符号约束，随后求解这些约束以生成能探索新路径的输入。现有Concolic引擎通常遵循两种实现策略之一：基于解释器的系统构建相对简单，但会产生大量解释开销；而基于插桩的系统避免了这种开销，但通常会为每个新输入从头重新执行程序。在本文中，我们开发了一种新方法，融合两者的优势：从目标语言的 concrete 语义出发，首先开发一个定义式Concolic解释器，并对其进行分阶段处理以消除解释开销，同时保留基于解释器实现的简洁性；通过将分阶段解释器表示为延续传递风格，我们可以在分支点捕获执行快照，并在探索替代路径时从快照恢复，避免从程序入口重复执行。由于快照复用本身可能产生开销，我们进一步开发了一种启发式方法，仅在预期快照复用有益时才优先使用它。我们将该方法实例化到WebAssembly中，并在新的Concolic执行编译器GenWasym中实现。在184个基准测试中，仅使用分阶段技术的GenWasym相比基于解释器的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 alone achieves a $29.4\times$ average speedup over the interpreter-based WASP; heuristic snapshot-reuse further increases the speedup to $44.9\times$.
Comments29 pages; preprint of paper accepted at OOPSLA 2026
