CODEWITHSUNDEEP
z3z3py
lllllllllllll
lllllllllllll

Reputation: 9110

Z3: Translate a BoolRef into a BitVecVal

I am trying to simulate the x86 assembly code using z3 formulas. Currently, I am trapped in simulating the semantics of setnz opcode.

the semantics of setnz is defined as 

checking the value of CPU flag `ZF`, and if it is equal to 1, then set a register byte as 1, otherwise set it as 0.

For example, the above procedure can be simulated in this way:

python
>>> from z3 import *
>>> a = BitVecVal(1, 1)
>>> c = (a == 1)
>>> set_register("al", c)

However, note that the type of c is a BoolRef, and I would like to set the value of al as a 8-bit long BitVecVal.

So here is my question:

  1. I am following the best practice to simulate such set opcodes?
  2. If so, how can I translate a BoolRef into a 8-bit long BitVecVal in order to set the register?

Upvotes: 0

Views: 202

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

You can use If:

If(c, BitVecVal(1,1), BitVecVal(0,1))

Upvotes: 1

Related Questions