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))
Mem は 8 ビットの配列であるのに対し、t3 は 8 ビットではなく 32 ビットであるため、これは間違っていることがわかります。
問題は、Select を使用して、上記の例で 1 バイトではなく 4 バイトを読み取るにはどうすればよいかということです。
Select4() など、4 バイトを読み取る新しい関数を作成できると思いますが、Z3 python で関数を作成する方法がわかりません。
どうもありがとう！