assembly - 将 Z3 的 AST 转换为 ASM 代码的最佳方法是什么？

Question

有一个例子：

mov edi, dword ptr [0x7fc70000]
add edi, 0x11
sub edi, 0x33F0B753

Z3简化后我得到了（内存0x7FC70000被符号化）：

bvadd (_ bv3423553726 32) MEM_0x7FC70000

现在我需要将 Z3 转换为 ASM 以获得如下结果：

mov edi, 0xCC0F48BE
add edi, dword ptr [0x7fc70000]

或者像这样：

mov edi, dword ptr [0x7fc70000]
add edi, 0xCC0F48BE

Answer 1

据我所知，没有公开可用的此类工具。而且还不太清楚如何设计一个，因为它必须非常特定于给定机器的汇编语言。（我想 X86 假设可以带你走很远。）最好将它编译成直线 C，然后使用无处不在的 gnu-c 工具链来完成最后一英里。但是，当然，这完全取决于您的具体用例和需求。

看看这个页面：http ://smtlib.cs.uiowa.edu/utilities.shtml

如果您走上开发工具的道路，也许那里列出的工具可以为您提供一个起点。如果你确实开发了这样的工具，也请在那里做广告。