Z3 BitVec extraction using symbolic high and low

Question

I've been playing around with proving certain SIMD vectorizations using Z3 and I'm running into a problem trying to model SIMD operations that conditionally move around bits or lanes (such as Intel _mm_shuffle_epi8 for example)

The problem occurs when I try to use symbolic high and low with Extract which does not seem supported:

assert a.sort() == BitVecSort(128)
assert b.sort() == BitVecSort(128)
Extract( Extract(i+3,i,b)*8+7, Extract(i+3,i,b)*8, a)

results in

z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.

The problem appears to be two-fold:

Z3 does not appear to support symbolically sized BitVecs

>>> a = Int('a')
>>> b = BitVec('b', a)
ctypes.ArgumentError: argument 2: <class 'TypeError'>: wrong type

Would be neat, but alas. As a result, Extract needs to be able to know the precise BitVec sort of its return value, and demands that both high and low are concrete, even though it appears the only real requirement should be that simplify(high - low) results in a concrete value.

What's the correct way of doing this?

Answer 1

SMTLib bit-vector logic is only defined for concrete bit-sizes. This is not just an oversight: It is a fundamental limitation of the logic: There's no decision procedure that can decide correctness of bit-vector formulae that can involve symbolic sizes, since truth of bit-vector formulae can change depending on the size. The classic example is:

x <= 7

if x is a bitvector of size <= 3, then the above is true, otherwise it isn't. If that looks contrived, consider the following:

x*x <= x+x+x

Again, this is true if x is 2-bits wide, but not true if it is 3-bits wide. Thus, SMTLib requires all bit-vector sizes to be concrete at specification time. Note that you can write higher-level programs that work for arbitrary bit-sizes, but once they are rendered and sent to the solver, all bit-vector sizes must be known concrete constants.

Regarding your question about Extract. You're right, strictly speaking, concreteness of the final length is sufficient. But z3py is a thin-layer on top of SMTLib, and it doesn't do such simplifications. The "concreteness" requirement follows from the similar limitation on the corresponding SMTLib function:

All function symbols with declaration of the form

  ((_ extract i j) (_ BitVec m) (_ BitVec n))

where
- i, j, m, n are numerals
- m > i ≥ j ≥ 0,
- n = i - j + 1  "

see here: http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml Note that even the logic itself is called "FixedSizeBitVectors" for this very reason, not just "BitVectors".

However, it isn't really hard to extract a fixed sized chunk, simply right shift by lo, and mask/extract the required amount of bits:

 ((_ extract 7 0) (bvlshr x lo))

If your chunk size is not constant, then again you land in the world of symbolic bit-vector sizes and SMTLib avoids this for the reasons I mentioned above. (And this is also the reason why extract takes concrete integers as arguments and written in that funny SMTLib notation to indicate the arguments are concrete values.)

If you do have to work with "symbolic" word sizes, your best bet is to write your program and prove for each "symbolic" size of interest separately, by making sure the sizes are concrete in each case. (Essentially a case split for all the sizes you are interested in.)

Answer 2

Yep, high/low need to be constant so that the resulting type is known statically. You can use shifts and/or masks to do what you want, though you'll need to fix a maximum size for the output.