CODEWITHSUNDEEP
pythonz3bitvector
peperunas
peperunas

Reputation: 438

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?

Upvotes: 0

Views: 1826

Answers (2)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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

Upvotes: 2

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

The constraints in a solver are implicitly a conjunction, i.e., you'll have to build a disjunction first and then s.add(...) that disjunction.

Upvotes: 2

Related Questions