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

Question

在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中创建一个函数。

非常感谢！

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）：

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)