Array and bitvector theory to model flat memory queries

[andreaslindner]

This issue/question is about the default approach that z3 takes to solve queries involving array and bitvector theory. The application we have is using these two theories to model binary code computations that also involve flat memory of the machine.

We first encountered problems when using our queries that worked for z3 4.8.4, but get completely stuck with newer versions like 4.8.17 or 4.13.0. As an example, let's consider this one, which starts by definining macros followed by the query:

; memory 64->8
; ----------------------
(define-fun loadfun_64_8_32 ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)))
                            (_ BitVec 32)
  (concat (select a (bvadd ad (_ bv3 64)))
          (select a (bvadd ad (_ bv2 64)))
          (select a (bvadd ad (_ bv1 64)))
          (select a (bvadd ad (_ bv0 64)))
  )
)

(define-fun storefun_64_8_32 ((a (Array (_ BitVec 64) (_ BitVec 8))) (ad (_ BitVec 64)) (v (_ BitVec 32)))
                                 (Array (_ BitVec 64) (_ BitVec 8))
  (store
    (store
      (store
        (store a (bvadd ad (_ bv3 64)) ((_ extract 31 24) v))
                 (bvadd ad (_ bv2 64)) ((_ extract 23 16) v))
                 (bvadd ad (_ bv1 64)) ((_ extract 15  8) v))
                 (bvadd ad (_ bv0 64)) ((_ extract  7  0) v))
)

; --------------------------------------------------------------------------------------------


(declare-const ad1_deref (_ BitVec 32))
(declare-const ad0_deref (_ BitVec 32))
(declare-const ad1 (_ BitVec 64))
(declare-const ad0 (_ BitVec 64))
(declare-const M (Array (_ BitVec 64) (_ BitVec 8)))

(assert (= (bvand ad0 (_ bv3 64)) (_ bv0 64)))
(assert (= (bvand ad1 (_ bv3 64)) (_ bv0 64)))
(assert (= (loadfun_64_8_32 M ad0) ad0_deref))
(assert (= (loadfun_64_8_32 M ad1) ad1_deref))


(assert (not (and
  (= (loadfun_64_8_32 (storefun_64_8_32 (storefun_64_8_32 M ad0 ad1_deref) ad1 ad0_deref) ad0) ad1_deref)
  (= (loadfun_64_8_32 (storefun_64_8_32 (storefun_64_8_32 M ad0 ad1_deref) ad1 ad0_deref) ad1) ad0_deref))))

(check-sat)

I have defined several of these macros with different parameters to capture different cases of memory accesses and sizes. The example only contains the ones relevant for the query to keep things as compact as possible here. Interestingly, this approach seemed to work well until we used newer versions of z3 as described above. After further experiments with different versions of this example query (different sizes of the bitvectors that get stored and loaded into the memory array), I have found that this approach works for 8, 32 and 64 bit, but for some reason the old version of z3 also gets stuck on 16 bits. The newer versions get stuck on this query when it is phrased like in the example.

In fact, my experiments with rephrasing the query have been successful, but with this issue I am trying to understand what would be an intended usage here. I can also conceive other approaches with tactics/parameters as well as some form of axiomatic definitions of the functions for loading and storing. I also noticed difference in behavior when using z3 stacking operations between the macro definitions and subsequent queries.

Is there an intuitive explanation for this change of behavior between the old and newer versions of z3? Is there a known set of tactics/parameters to restore the old behavior with the latest version of z3 for queries like this? Alternatively, are the queries phrased in a non-standard way such that the default tactics/parameters are not driving z3 well "towards" a solution? If yes, what would be a standard phrasing that z3 is expected to be able to handle well (possibly throughout the different versions)?