Z3Py: как я должен представлять 32-битные; 16-битные и 8-битные регистры?

Question

Я новичок Z3. Извините, если это глупый вопрос ..

Я в основном пытаюсь реализовать простой символический механизм выполнения на x86-32bit инструкциях по сборке. Вот проблема, с которой я сейчас сталкиваюсь:

Предположим перед выполнением, я инициализировал некоторые регистры, используя BitVec.

self.eq['%eax'] = BitVec('reg%d' % 1, 32) 
self.eq['%ebx'] = BitVec('reg%d' % 2, 32) 
self.eq['%ecx'] = BitVec('reg%d' % 3, 32) 
self.eq['%edx'] = BitVec('reg%d' % 4, 32) 

Так вот мой вопрос, как справиться с некоторыми 16-bit или даже 8-bit регистров?

В любом случае я могу извлечь часть 8-bit из 32-разрядного BitVec, назначив его некоторым значением, а затем верну его обратно? Могу ли я это сделать в z3? Или есть лучший способ ...?

Я проясняю? большое спасибо!

Answer 1

Вы можете извлечь части битвектора, что приведет к новому меньшему значению битвектора, которое вы можете использовать любым способом (например, добавить).

Вы можете заменить части битвектора, сначала извлекая все части, а затем объединив меньшие битвекторы в один большой.

Например увеличивающимся верхнюю половину EAX будет выглядеть так:

eaxNew = concat(add(extract(eaxOld, upperHalf), 1), extract(eaxOld, lowerHalf)) 

(Псевдо-код)

http://research.microsoft.com/en-us/um/redmond/projects/z3/namespacez3py.html