将 Z3 的 AST 转换为 ASM 代码的最佳方法是什么？ [关闭]

【问题标题】：What is the best way to translate Z3's AST into ASM code? [closed]将 Z3 的 AST 转换为 ASM 代码的最佳方法是什么？ [关闭]
【发布时间】：2020-05-14 15:26:24
【问题描述】：

有一个例子：

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

【问题讨论】：

标签： assembly compiler-construction z3 smt triton

【解决方案1】：

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

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

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

【讨论】：