同一变量的不同字节的z3排序不匹配

Question

我正在使用z3-python包模拟算法的行为，但我在使用逐位XOR时遇到了问题。

起初我定义

class State:
def __init__(self):
self.state = [0] * 0x270
self.index = 0
def mag(i):
return z3.If(i == 0, 0x0, 0x9908b0df)
seed = z3.BitVec('seed', 32)
s= State()

脚本继续，但是当我运行解算器时，由于尝试执行行中的__xor__，我得到了一个z3.z3types.Z3Exception: sort mismatch

s.state[i] = s.state[i + 0x18d] ^ ((s.state[i + 1] & 0x7fffffff | s.state[i] & 0x80000000) >> 1) ^ mag((s.state[1] & 1) *8)

这里，s.state中的每个条目都取决于种子的符号值。

我是这种解决方案的初学者，我不确定问题的确切原因。

Answer 1

这一行本身没有错。您可以通过运行以下程序进行验证：

from z3 import *
class State:
def __init__(self):
self.state = [BitVec('x', 32)] * 0x270
self.index = 0
seed = z3.BitVec('seed', 32)
s= State()
i = 87
s.state[i] = s.state[i + 0x18d] ^ ((s.state[i + 1] & 0x7fffffff | s.state[i] & 0x80000000) >> 1)
print(s.state[I])

此打印：

x ^ (x & 2147483647 | x & 2147483648) >> 1

因此，问题一定是源于程序中的其他地方。您需要将其简化为一个最小的示例(有关指导原则，请参阅此处：https://stackoverflow.com/help/minimal-reproducible-example)希望在简化的过程中你能自己找到问题所在。如果没有，请随意再次发布其他人可以复制的完整示例。

关于mag函数：

注意，mag函数只是使用整数，所以z3不能推断它是关于位向量的。这就是你得到排序不匹配的原因。为了避免这个问题，定义mag如下：

def mag(i):
return z3.If(i == 0, z3.BitVecVal(0x0, 64), z3.BitVecVal(0x9908b0df, 64))

注意BitVecVal的使用。这应该可以解决问题。