Reputation: 387
I need something like that for x86 arch:
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
The last step is converting Z3's AST into ASM code to get result like this:
mov edi, dword ptr [0x7fc70000]
add edi, 0xCC0F48BE
Is there any efficient way to perform last step? Should I parse SMT formula and convert it manually (bv -> mov...)?
Upvotes: 0
Views: 227