5

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.

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).

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

  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?

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

1 Answer 1

5

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)

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

2
  • I didn't know extensionality can be turned off. I will try that -- thanks! Jun 17, 2014 at 14:05
  • Re. solver configuration, I used the defaults that Z3 provides (including a plain Z3_mk_solver(context)). Would it make any difference if I explicitly enabled the theories that I need (BV + non-extensional arrays) using perhaps the Z3_mk_solver_for_logic call? Jun 17, 2014 at 14:13

Your Answer

Reminder: Answers generated by Artificial Intelligence tools are not allowed on Stack Overflow. Learn more

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.