将Z3的AST转换为ASM代码的最佳方法是什么？ [英] What is the best way to translate Z3's AST into ASM code?

问题描述

有一个例子：

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

经过Z3简化后，我得到了（内存0x7FC70000表示为符号）：

After Z3 simplification I have got (memory 0x7FC70000 is symbolized):

bvadd (_ bv3423553726 32) MEM_0x7FC70000

现在我需要将Z3转换为ASM才能得到如下结果：

Now I need to convert Z3 into ASM to get result like this:

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

或类似的方式：

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

推荐答案

据我所知，没有可公开使用的工具。尚不清楚如何设计一种，因为它必须非常特定于特定机器的汇编语言。 （我想，X86的假设可能会使您走得更远。）将其编译为直线C，然后使用无处不在的gnu-c工具链走到最后一步可能会更好。但是当然，这完全取决于您的特定用例和需求。

There is no such tool publically available, to the best of my knowledge. And it's not quite clear how one would design one, as it would have to be very specific for a given machine's assembly language. (X86 assumption can take you far I suppose.) It might be better to compile it to straight-line C, and then use the ubiquitously available gnu-c toolchain to go the last mile. But of course, it all depends on your specific use case and needs.

请看此页面： http://smtlib.cs.uiowa.edu/utilities.shtml

也许如果您沿途开发工具，那么此处列出的工具可以为您提供一个起点。而且，如果您确实开发了这样的工具，请也在那里做广告。

Perhaps the tools listed there can give you a starting point if you go down the path of developing one. And if you do develop such a tool, please do advertise it there as well.

这篇关于将Z3的AST转换为ASM代码的最佳方法是什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！