Z3: Как выбрать 4 байта из массива из 8 бит?

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)) 

Пока все в порядке. Однако теперь я хочу прочитать 4 байта из массива Mem, как показано ниже.

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. Эти две операции могут быть использованы для кодирования операций литья, доступные в языках программирования, таких как С.

Вот полный пример (также доступны в Интернете 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)