What is the best way to translate Z3's AST into ASM code?

Question

There is an example:

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

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

bvadd (_ bv3423553726 32) MEM_0x7FC70000

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

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

Or like that:

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

Answer 1

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.

Take a look at this page: 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.