Is there a way to specify the PDEP/PEXT instructions efficiently in SMTlib bitvector syntax?
My best attempt for PEXT ends up with something to the tune of: "Iff bit N in mask
is set, then bit count_bits(mask[0..N])
in the result is equal to bit N in the input value.". But this requires a way to count bits, which isn't available in QF_BV
.
Similarly for PDEP I end up with something like: "Iff bit N in mask
is set, then bit N in the result is equal to bit count_bits(mask[0..N])
in the input value." Which again, requires counting bits.
I could write a naive bit counting function, but that would probably require evaluating all bits in the bitvector one-by-one. The entire specification would end up being O(N^2)
, which shouldn't be necessary.
Intel gives this implementation for PDEP:
TEMP := SRC1;
MASK := SRC2;
DEST := 0 ;
m := 0, k := 0;
DO WHILE m < OperandSize
IF MASK[ m] = 1 THEN
DEST[ m] := TEMP[ k];
k := k+ 1;
FI
m := m+ 1;
OD
...but I am having trouble translating the while loop to SMTlib syntax.
When programming symbolically, you can't really avoid this sort of complexity. Note that your implementation must work correctly for all symbolic values of the input and the mask: Without having a concrete value for these, it's pointless to optimize: The solver will have to consider all possible paths, and hence optimization tricks don't really work. (You can think of symbolic simulation as "running for all possible inputs," so no shortcuts apply.)
So, instead of focussing on the complexity of the loop, simply write the necessary constraints on the final value. Unfortunately SMTLib isn't terribly a good choice for this sort of programming, as it doesn't allow for many usual programming idioms. But that's precisely why we have programmable API's built on top of solvers. Z3 can be scripted from many languages, including C/C++/Python/Haskell/Java.. etc.; so I'd recommend using a language you're most familiar with and learning the bindings there.
Based on this, I'll show how to code PEXT using both the popular Python API, and also the Haskell version. At the end, I'll also show how to do this in SMTLib by generating the code, which might come in handy. Note that I haven't extensively tested these, so while I trust the basic implementation is correct, you should double check before using it for anything serious.
Python
When I run this, I get:
Of course, this is just one example; so please convince yourself by studying the implementation in detail.
Haskell
For Haskell, I'll use the SBV library (https://hackage.haskell.org/package/sbv). Compared to Python, it's much more expressive and a lot easier to use; if you're familiar with Haskell:
Which can be tested by:
which prints:
And here's
pdep
for completeness:Hopefully you can adopt these ideas, and implement them in your language of choice in a similar fashion. Again, please test further before using it for anything serious though, I only tested these for just the one value I shown above.
SMTLib
As I mentioned, SMTLib isn't really suitable for this sort of programming, since it lacks usual programming language idioms. But if you have to have this coded in SMTLib, then you can use the sbv library in Haskell to generate the function for you. Note that SMTLib is a "monomorphic" language, that is, you can't have a definition of PEXT that works for arbitrary bit-sizes. You'll have to generate one for each size you need. The generated code will not be pretty to look at, as it will be a full unfolding, but I trust it should perform well. Here's the output for the 2-bit case. (As you can imagine, longer bit sizes will yield bigger functions).
You can drop the above (or at whatever size you generate it at) in your SMTLib program and use as is, if you really must stick to SMTLib.