在Z3中表示内存缓冲区的最有效方法 [英] Most efficient way to represent memory buffers in Z3

问题描述

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

I would like to model fixed-size memory buffers and their access operations in Z3. The size of the buffers can be anywhere from a couple of bytes to hundreds of bytes. The standard way employed by several existing tools (e.g., KLEE) is to create array variables over the domain and range of bitvectors. Each memory buffer gets such an array and memory reads/writes are encoded using select/store operations.

可惜，在我的基准测试中，当使用这种方法时，Z3(*)似乎始终比STP慢.在更详细地分析查询以了解正在发生的事情之前，我想确保我使用的是正确"的方法来编码Z3中的内存操作(因为诚然，STP专门设计用于数组和位向量).

Alas, in my benchmarks, when using this approach, Z3(*) appears to be consistently slower than STP. Before analyzing the queries in more detail to figure out what's going on, I wanted to make sure I'm using the "right" approach to encoding memory operations in Z3 (since, admittedly, STP was specifically designed to be used with arrays and bitvectors).

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

So what is the most efficient way of representing memory buffers in Z3? I'm considering a couple of alternatives thus far:

1. 使用断言来指定初始值而不是使用嵌套的store -s.但是，在我的初步测试中，这似乎会使Z3的速度更加放慢.
2. 使用位向量对缓冲区进行编码.但是，生成的位向量可能会很大(〜1000比特)，我不确定Z3或任何其他求解器能否有效地处理该问题.
3. 为每个内存字节创建单独的位向量变量，并使用嵌套ite表达式将内存访问路由到相应的变量.但是，恐怕这会使模型变得非常复杂，并引入对量词的需求.
4. 使用未解释的函数代替数组，但这需要以比Z3内置数组理论低的效率重新定义数组公理.

1. Use assertions to specify the initial values of the memory buffer, instead of using nested store-s. However, in my preliminary tests, this appears to slow down Z3 even more.
2. Use bitvectors to encode the buffers. However, the resulting bitvectors can get quite large (~1000s of bits), and I'm not sure Z3 or any other solver could handle that efficiently.
3. Create individual bitvector variables for each memory byte and use nested ite expressions to route memory accesses to corresponding variables. However, I'm afraid this would complicate the model quite a lot and introduce the need for quantifiers.
4. Use uninterpreted functions instead of arrays, but this requires redefining the array axioms in a way that may be less efficient than Z3's own built-in array theory.

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

Are there any better approaches that I'm missing?

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

(*) Default non-incremental solver, Z3 branch unstable@aba79802cfb5

推荐答案

关于在KLEE风格的应用程序中使用数组有一点. 如果使用方程式初始化数组，则Z3不能很好地工作:

There is one point about using arrays for KLEE style applications. Z3 does not work well if you initialize an array using an equation:

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

制定如下约束更为有效:

It is much more efficient to formulate such constraints as:

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

(当索引为不同的常数或已知为不同的索引时有效)

(which works when the indices are different constants or known to be different)

您还可以关闭数组的扩展性.默认情况下，数组被视为扩展数组. 对于KLEE样式的应用程序来说应该没关系.

You can also turn off extensionality for arrays. Arrays are treated as extensional by default. It should not matter for KLEE style applications.

这篇关于在Z3中表示内存缓冲区的最有效方法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！