2

使用 Python Z3，我有一个字节数组，可以使用 Select 读取 1 个字节，如下所示。

MI = BitVecSort(32)
MV = BitVecSort(8)
Mem = Array('Mem', MI, MV)

pmt = BitVec('pmt', 32)
pmt2 = BitVec('pmt2', 8)

g = True
g = And(g, pmt2 == Select(Mem, pmt))

到目前为止，这还可以。但是，现在我想从 Mem 数组中读取 4 个字节，如下所示。

t3 = BitVec('t3', 32)
g = And(g, t3 == Select(Mem, pmt))

事实证明这是错误的，因为 t3 是 32 位的，而不是 8 位的，而 Mem 是 8 位的数组。

问题是：如何使用 Select 读取 4 个字节，而不是上面示例中的 1 个字节？

我想我可以创建一个新函数来读取 4 个字节，比如说 Select4()，但我不确定如何在 Z3 python 中创建一个函数。

太感谢了！

4

1 回答 1

4

我们可以定义Select4为

def Select4(M, I):
  return Concat(Select(M, I + 3), Select(M, I + 2), Select(M, I+1), Select(M, I))

该操作Concat本质上是附加四个位向量。Z3也支持操作Extract。这两个操作可用于对编程语言（如 C）中可用的转换操作进行编码。

这是完整的示例（也可在此处在线获得）：

MI = BitVecSort(32)
MV = BitVecSort(8)
Mem = Array('Mem', MI, MV)

pmt = BitVec('pmt', 32)
pmt2 = BitVec('pmt2', 8)

def Select4(M, I):
  return Concat(Select(M, I + 3), Select(M, I + 2), Select(M, I+1), Select(M, I))

g = True
g = And(g, pmt2 == Select(Mem, pmt))
t3 = BitVec('t3', 32)
g = And(g, t3 == Select4(Mem, pmt))

solve(g, pmt2 > 10)
于 2013-04-10T15:07:00.143 回答