如何将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工具链来完成最后的工作。但当然，这一切都取决于你的具体用例和需求。

如果你想开发一个工具，也许那里列出的工具可以给你一个起点。如果你确实开发了这样的工具，也请在那里做广告。