Как лучше всего перевести AST Z3 в код 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

Возможно, перечисленные там инструменты могут стать отправной точкой, если вы пойдете по пути ее разработки. И если вы действительно разрабатываете такой инструмент, пожалуйста, рекламируйте его и там.