z3 sort mismatch for different bytes of the same variable

Question

I'm simulating the behaviour of an algorithm using z3 python package, however I'm encountering problems using a bitwise XOR.

At first I define

    class State:
        def __init__(self):
            self.state = [0] * 0x270
            self.index = 0

    def mag(i):
        return z3.If(i == 0, 0x0, 0x9908b0df)

seed = z3.BitVec('seed', 32)
s= State()

And the script goes on, however when I run the Solver I get a z3.z3types.Z3Exception: sort mismatch caused by trying to execute the __xor__ in the line

s.state[i] = s.state[i + 0x18d] ^ ((s.state[i + 1] & 0x7fffffff | s.state[i] & 0x80000000) >> 1) ^ mag((s.state[1] & 1) *8)

Here every entry in s.state depends on the symbolic value of the seed.

I'm a beginner with these kind of solver and I'm not sure what exactly causes the issue.

Answer 1

There's nothing wrong in that line by itself. You can verify it by running the following:

from z3 import *

class State:
   def __init__(self):
     self.state = [BitVec('x', 32)] * 0x270
     self.index = 0

seed = z3.BitVec('seed', 32)
s= State()

i = 87
s.state[i] = s.state[i + 0x18d] ^ ((s.state[i + 1] & 0x7fffffff | s.state[i] & 0x80000000) >> 1)
print(s.state[I])

This prints:

x ^ (x & 2147483647 | x & 2147483648) >> 1

So, the problem must be originating from elsewhere in your program. You need to reduce it down to a minimal example (see here for guidelines: https://stackoverflow.com/help/minimal-reproducible-example) and hopefully in the process of simplification you'll find the issue yourself. If not, feel free to post again with a full-example that others can replicate.

Regarding the mag function:

Note that your mag function simply uses integers, so z3 cannot deduce that it's about bit-vectors. This is the reason why you're getting a sort-mismatch. To avoid the issue, define mag as follows:

def mag(i):
    return z3.If(i == 0, z3.BitVecVal(0x0, 64), z3.BitVecVal(0x9908b0df, 64))

Note the use of BitVecVal. This should fix the issue.