Symbolic execution (SE) tools often rely on intermediate languages (ILs) to support multiple programming languages, promising reusability and efficiency. In practice, this approach introduces trade-offs between performance, accuracy, and language feature support. We argue that building SE engines \emph{directly} for each source language is both simpler and more effective. We present Soteria, a lightweight OCaml library for writing SE engines in a functional style, without compromising on performance, accuracy or feature support. Soteria enables developers to construct SE engines that operate directly over source-language semantics, offering \emph{configurability}, compositional reasoning, and ease of implementation. Using Soteria, we develop Soteria$^{\text{Rust}}$, the \emph{first} Rust SE engine supporting Tree Borrows (the intricate aliasing model of Rust), and Soteria$^{\text{C}}$, a compositional SE engine for C. Both tools are competitive with or outperform state-of-the-art tools such as Kani, Pulse, CBMC and Gillian-C in performance and the number of bugs detected. We formalise the theoretical foundations of Soteria and prove its soundness, demonstrating that sound, efficient, accurate, and expressive SE can be achieved without the compromises of ILs.

翻译：符号执行（SE）工具常依赖中间语言（IL）以支持多种编程语言，旨在实现可复用性与效率。然而在实践中，该方法在性能、准确性和语言特性支持之间引入了权衡。我们认为，为每种源语言直接构建符号执行引擎既更简单也更有效。本文提出Soteria——一个轻量级OCaml库，用于以函数式风格编写符号执行引擎，且不牺牲性能、准确性或功能支持。Soteria使开发者能够构建直接基于源语言语义运行的符号执行引擎，提供可配置性、组合式推理及易于实现的特性。基于Soteria，我们开发了Soteria$^{\text{Rust}}$——首个支持Tree Borrows（Rust复杂别名模型）的Rust符号执行引擎，以及Soteria$^{\text{C}}$——面向C语言的组合式符号执行引擎。两者在性能和检测缺陷数量上均与Kani、Pulse、CBMC及Gillian-C等现有先进工具相当或更优。我们形式化了Soteria的理论基础并证明了其可靠性，表明无需依赖中间语言的妥协即可实现可靠、高效、准确且具表现力的符号执行。