Z3：如何从8位数组中选择4个字节？

Question

对于pythonz3，我有一个字节数组，可以使用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个字节，如下所示。在

^{pr2}$

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

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

我假设我可以创建一个新函数来读取4个字节，比如Select4（），但我不确定如何在z3python中创建函数。在

非常感谢你！在

Answer 1

我们可以将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等编程语言中可用的铸造操作进行编码

以下是完整的示例（也可在线查看here）：

^{pr2}$