Search code examples
pythonz3bitvector

Z3 - How to set a byte constraint on a BitVec

I'm trying to set a list of possible allowed bytes in a BitVec but I'm not sure I'm actually setting the constraints in the right way.

E.g:

Let us have a 32 bit BV called bv and a Solver() called s:

s = Solver()
bv = BitVec(8 * 4)

I want that each byte can be either 0x2 or 0x34 or 0xFF so I used Extract():

i = 0
while (i < 8 * 4):
    s.add(Extract(i + 7, i, bv) == 0x2)
    s.add(Extract(i + 7, i, bv) == 0x34)
    s.add(Extract(i + 7, i, bv) == 0xFF) 
    i += 8

Sadly, s.check() returns unsat.

I think this is not the correct way to express that those bytes may be 0x2 OR 0x34 OR 0xFF. Did I write the constraints in the right way or my thought process is just plain wrong?

Solution 
  • i = 0
while (i < 8 * 4):
   s.add(Or(Extract(i + 7, i, bv) == 0x2), 
            Extract(i + 7, i, bv) == 0x34),
            Extract(i + 7, i, bv) == 0xFF)) 
i += 8