我试图了解符号执行引擎的工作原理。本文调查了使用 C 的技术。他们提到了符号记忆：
3.1 全符号记忆
在最高级别的通用性上，引擎可以将内存地址视为完全符号...
以紧凑的形式表示内存。这种方法在 [32] 中采用，它将符号（而不是具体）地址表达式映射到数据，表示使用紧凑、隐式形式的符号地址引用内存所产生的可能替代状态
本文还对 Java 的符号堆进行了一些探讨：
4.1 符号状态表示
符号状态 s 由符号堆 H、原始类型字段的估值、路径条件 PC 和程序计数器组成。
我想知道这在实践中意味着什么，这个符号堆。对我来说，这意味着符号执行中使用的所有数据结构都将使用符号内存而不是实际内存。这意味着像数组这样的结构需要有符号模型。我想知道这些模型是什么样的。我看不到您如何“对数组长度进行符号建模”。在我看来，它是一个整数，所以它将是一个整数值。但作为一个象征性的价值，想知道这意味着什么。我还没有看到。想知道是否可以从高层次上解释如何对一些数据结构（如数组或具有一些不同字段值的结构）进行符号建模，因此它在符号执行中很有用。
这篇较旧的论文提到：
还可以为不需要使用真实数据对象但可以用任意符号表示的编程语言定义另一种“符号执行”语义。
不知道这看起来如何。