知乎上有一篇对符号执行近些年的前沿研究较为详细的综述：
近些年学术界符号执行引擎优化的主要思路大体可以分为以下两类：
- 解释型：在程序执行过程中，对程序代码（通常是中间语言（IR）或机器指令）进行解释来构建这种映射关系。一般而言，对程序指令进行这类解释执行，相比直接执行程序速度会变慢。故有些符号执行引擎会区分指令操作数是否包含符号值，如果包含，则解释执行；否则直接执行源程序代码。
- 编译型：在程序编译过程中，将这种映射过程编译到程序代码中，在程序执行时进行符号表达式的构建。相较于解释型，这种方法将“解释”过程移动到编译时，只解释程序代码一次。由于在执行过程中速度接近原始代码，这种设计显著提高了速度。
我们比较熟悉的Angr，KLEE都属于解释型，但编译型才是前沿的主流关注点
SymCC
把 QSYM 解释执行 LLVM IR 的函数，通过动态链接库，链接进来，到 binary 层去执行。
SymQEMU
借用并扩展了 QEMU 中的 TCG (Tiny Code Generator)，以支持 Symbolic Execution。对比 SymCC，这次插桩的是 QEMU 的 TCG 而不是 LLVM IR；对比 S2E (也用了 TCG)，把符号执行的 runtime 也 compile 进 QEMU 去执行了从而加速（思路和 SymCC 是一样的）。
SymSAN
SymSAN 在SymCC的基础上，将符号执行看作是数据流分析的一种特殊形式，结合基于LLVM的数据流分析框架DFSAN，对符号表达式的管理进行优化，提高了执行速度
SymFusion
SymFusion 分析了编译型（编译时插桩）和解释型（执行时插桩）两类技术的优缺点：
解释型：
优点：
- 不需要重新编译程序
- 现代DBT（动态二进制转换工具）工具会生成架构依赖的IR来进行插桩，很容易支持大规模指令集
- 在二进制层面，程序语言设计的高维度概念被简化了，如在pointer、unsigned value、unsigned struct field之间并无区别
缺点：
- 插桩代码效率低下，通常在指令级或基本块级；DBT在JIT（即时编译）过程中优化能力有限；DBT会差异如一些无分支代码，当触发条件时让executor去调用helpers执行
- DBT使用内存中的virtual CPU来跟踪原始程序状态，需要额外内存访问来更新
- DBT的IR并不显示支持专用指令，而是在运行时去调用helper函数处理，如QEMU在处理x86的division operations、vectorized instructions和floating-point operations时。KLEE使用function models，比如klee-clibc，很容易编写但容易出错；S2E 将helper函数也转换成LLVM IR并使用KLEE去解释执行
- 即使executor能够对专用指令进行插桩，生成的符号表达式可能非常复杂以至于SMT solver无法求解
编译型：
优点：
- 执行时无插桩带来的开销
- 针对IR进行插桩，不仅能进行更复杂的代码转化，而且能够受益于原有的编译优化手段
- 支持跨架构
缺点：
- 需要引入自定义的编译工具链
- 新增编译工具链在原始编译过程中放置的位置难以确定。放到前面能够受益于之后的优化，但最终代码与之前差异过大，如替换一些call为inline code，可能导致它们不被插桩而影响符号执行分析
- 当一个函数未插桩时，需要创建一个函数模型来模仿这个函数的行为
- IR继承了很多复杂专用的数据类型，如array、vector、struct，增大了编写pass的复杂度
SymFusion结合两类技术，对不同的代码使用不同的插桩方式，如下图。internal code主要是用户程序代码，而external code时其他编译时未插桩的、采用动态链接的代码
SymFusion的执行流程，核心问题是如何协调两种插桩代码的执行（包括程序执行的具体数据、DBT需要的virtual CPU状态以及生成的符号表达式）