Z3：将 BoolRef 转换为 BitVecVal
Z3: Translate a BoolRef into a BitVecVal
我正在尝试使用 z3 公式模拟 x86 汇编代码。目前，我陷入了模拟 setnz 操作码的语义。
setnz 的语义定义为
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.
比如上面的程序可以这样模拟：
python
>>> from z3 import *
>>> a = BitVecVal(1, 1)
>>> c = (a == 1)
>>> set_register("al", c)
但是，注意c的类型是BoolRef，我想将al的值设置为8位长BitVecVal.
所以这是我的问题：
- 我正在按照最佳实践来模拟这样的
set 操作码？
- 如果是这样，我如何将
BoolRef 翻译成 8 位长的 BitVecVal 以便设置寄存器？
您可以使用 If:
If(c, BitVecVal(1,1), BitVecVal(0,1))
我正在尝试使用 z3 公式模拟 x86 汇编代码。目前，我陷入了模拟 setnz 操作码的语义。
setnz 的语义定义为
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.
比如上面的程序可以这样模拟：
python
>>> from z3 import *
>>> a = BitVecVal(1, 1)
>>> c = (a == 1)
>>> set_register("al", c)
但是，注意c的类型是BoolRef，我想将al的值设置为8位长BitVecVal.
所以这是我的问题：
- 我正在按照最佳实践来模拟这样的
set操作码？ - 如果是这样，我如何将
BoolRef翻译成 8 位长的BitVecVal以便设置寄存器？
您可以使用 If:
If(c, BitVecVal(1,1), BitVecVal(0,1))