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寄存器？

无论如何，我可以从32位BitVec中提取8-bit部分，为其分配一些值，然后将其还原？我可以在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