z3py BitVector与整数操作混合

Question

具有(lst_v) BitVectors列表和布尔表达式值(lst_b)列表。如何使用z3py执行下列操作：

• 使用lst_b掩蔽lst_v中的元素。掩蔽需要使用And函数，因为布尔表达式需要在最后一步中求解。
• 计算所有剩余元素的xor
• 使用Solve类z3py测试结果中的所有位。

这个问题的一个变化是用加法交换xor。

Answer 1

目前还不完全清楚你在努力实现什么，但也许以下几点会让你走上正轨：

from z3 import *

# Assume we have a list of 3 32-bit values
x, y, z = BitVecs('x y z', 32)
lst_v = [x, y, z]

# Corresponding booleans:
mx, my, mz = Bools('mx my mz')
lst_b = [mx, my, mz]

# 32-bit zero
zero = BitVecVal(0, 32)

# Mask
masked = [If(b, v, zero) for (b, v) in zip(lst_b, lst_v)]

# Xor reduce
final = reduce(lambda x, y: x^y, masked, zero)

# 32-bit all 1's
allOnes = BitVecVal(-1, 32)

s = Solver()
s.add(final == allOnes)

# make it interesting, assert some known values and constraints
s.add(x == BitVecVal(123212, 32))
s.add(UGT(x + y,  z+12))
s.add(ULT(y, allOnes))

if s.check() == sat:
   print s.model()
else:
   print "No solution"

当我运行这个时，我得到：

[mz = True,
 mx = False,
 my = True,
 z = 2147479427,
 y = 2147487868,
 x = 123212]

这意味着，我应该将异或y和z作为32位值；它给出4294967295，它的所有位都设置为32位数量。