Z3 Bitvec Extraction Using Symbolic High And Low

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 lan

Solution 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 functionsymbolswithdeclarationoftheform

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

where
- i, j, m, narenumerals
- 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 70) (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.)

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