Krishath Krishath - 1 month ago 15
Python Question

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?

Answer
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
Comments