符号模型是什么样的

What a Symbolic Model Looks Like

我正在尝试了解符号执行引擎的工作原理。 This paper 使用 C 调查技术。他们提到符号记忆：

3.1 Fully Symbolic Memory

At the highest level of generality, an engine may treat memory addresses as fully symbolic...

Representing memory in a compact form. This approach was taken in [32], which maps symbolic – rather than concrete – address expressions to data, representing the possible alternative states resulting from referencing memory using symbolic addresses in a compact, implicit form

This paper 也稍微进入了 Java:

的符号堆

4.1 Symbolic State Representation

A symbolic state s consists of a symbolic heap H, the valuation of the primitive typed fields, the path condition PC and the program counter.

我想知道实际上这意味着什么，这个符号堆。对我来说，这意味着符号执行中使用的所有数据结构都将使用符号内存而不是实际内存。这意味着像数组这样的结构需要有 符号模型 。我在高层次上想知道这些模型是什么样的。我不明白你怎么能 "symbolically model the array length"。在我看来，它是一个整数，因此它将是一个整数值。但是作为一个象征性的价值，想知道这意味着什么。我还没有看到。想知道是否可以在较高层次上解释如何对一些数据结构进行符号建模，例如数组或具有一些不同字段值的结构，因此它在符号执行中很有用。

This older paper 提及：

One can also define an alternative "symbolic execution" semantics for a programming language where the real data objects need not be used but can be represented by arbitrary symbols.

不确定这看起来如何。

"The array X has size 100, and the element in position 5 has value 7"是数组的符号表示。 符号表示的关键点是你只关注明确重要的事情。

如果你想表示一个更通用的数组，你也可以通过说 "X has size L" 使它的大小成为符号，在你的分析过程中你可能会发现 L=100 或 L>90。

您捕获多少不同的数据结构取决于您想要做什么。链表是一堆内存区域还是更多？

符号执行引擎的完整文档化开源示例是 JPF - Symbolic Pathfinder。它在 Java 虚拟机级别执行。它也应该回答您关于更复杂的数据结构（如数组或对象数组）的问题。

这里有一篇非常好的出版物： “Symbolic PathFinder：将符号执行与模型检查集成以进行 Java 字节码分析”，自动化软件工程杂志 20(3) 2013 https://ti.arc.nasa.gov/publications/5269/download/

在这里你可以看到一个详细的例子（第4.9节）具体代码是如何"rewritten"并转化为符号代码的。特别是如何处理堆栈和堆内存以及取决于此符号内存的代码条件（图 6+7）。您不能简单地将内存与条件路径执行分开。

非常简单：条件被所有 "symbolic" 分支的循环所取代（非确定性选择）。内存被符号值替换（就像你提到的那样 - 通过所谓的属性在此处传播）和根据分支循环对这些值的约束。约束求解器用于进一步减少不可能的分支（回溯）并最终求解约束。

.Net 代码的另一个很好的实践示例是 运行 Microsoft SpecExplorer (XRTs) 在完全符号模式下使用 "Combination.KeepUnexpanded"。在生成的探索遍历路径图中，您可以看到一个很好的示例，说明如何表示符号内存和约束。不幸的是，XRTs 不是开源的。

P.S.: 事实上，符号变量的表示是一大挑战。这里有一些非常好的出版物：