将 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

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