Z3Py：我应该如何表示一些 32 位； 16位和8位寄存器？答案

【问题标题】：Z3Py: How should I represent some 32-bit; 16-bit and 8-bit registers?Z3Py：我应该如何表示一些 32 位； 16位和8位寄存器？
【发布时间】：2015-09-13 18:29:55
【问题描述】：

我是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 中这样做吗？或者有没有更好的方法..？

我说清楚了吗？非常感谢！

【问题讨论】：

标签： z3 z3py

【解决方案1】：

您可以提取位向量的一部分，从而生成一个新的、更小的位向量值，您可以使用任何您喜欢的方式（例如添加）。

您可以通过首先提取所有部分然后将较小的位向量连接成一个大的位向量来替换位向量的部分。

例如增加 eax 的上半部分如下：

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

（伪代码）

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

【讨论】：