在 Z3 中表示内存缓冲区的最有效方法

Question

我想在 Z3 中对固定大小的内存缓冲区及其访问操作进行建模。缓冲区的大小可以从几个字节到数百个字节不等。几种现有工具（例如 KLEE）采用的标准方法是在位向量的域和范围内创建数组变量。每个内存缓冲区都获得这样一个数组，并且内存读取/写入使用select/store 操作进行编码。

唉，在我的基准测试中，使用这种方法时，Z3(*) 似乎始终比 STP 慢。在更详细地分析查询以弄清楚发生了什么之前，我想确保我使用“正确”的方法来编码 Z3 中的内存操作（因为，诚然，STP 专门设计用于数组和位向量)。

那么在 Z3 中表示内存缓冲区的最有效方式是什么？到目前为止，我正在考虑几种替代方案：

1. Use assertions 指定内存缓冲区的初始值，而不是使用嵌套的store-s。但是，在我的初步测试中，这似乎会进一步降低 Z3 的速度。
2. 使用位向量对缓冲区进行编码。但是，生成的位向量可能会变得非常大（约 1000 位），我不确定 Z3 或任何其他求解器能否有效处理。
3. 为每个内存字节创建单独的位向量变量，use nested ite expressions 将内存访问路由到相应的变量。但是，我担心这会使模型变得相当复杂，并且需要量词。
4. 使用未解释的函数代替数组，但这需要重新定义数组公理，其效率可能低于 Z3 自己的内置数组理论。

我还缺少什么更好的方法吗？

(*) 默认非增量求解器，Z3 分支unstable@aba79802cfb5

Answer 1

在 KLEE 风格的应用程序中使用数组有一点。 如果您使用方程式初始化数组，Z3 将无法正常工作：

  (assert (= A (store (store (store .. (store A0 i1 v1) ..) i4 v4) i5 v5)))

制定这样的约束更有效：

  (assert (= (select A i1) v1))
  (assert (= (select A i2) v2))

（当索引是不同的常数或已知不同时有效）

您还可以关闭数组的扩展性。默认情况下，数组被视为扩展。 对于 KLEE 风格的应用程序来说，这应该无关紧要。