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)