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

Question

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

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

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

1. 使用断言来指定内存缓冲区的初始值，而不是使用嵌套的store-s。但是，在我的初步测试中，这似乎会进一步减慢 Z3 的速度。
2. 使用位向量对缓冲区进行编码。但是，生成的位向量可能会变得非常大（约 1000 位），我不确定 Z3 或任何其他求解器能否有效地处理这个问题。
3. 为每个内存字节创建单独的位向量变量，并使用嵌套ite表达式将内存访问路由到相应的变量。但是，我担心这会使模型变得相当复杂，并引入对量词的需求。
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 风格的应用程序来说，这无关紧要。