asm -> IR symbolic exec problem with dead code about miasm HOT 2 CLOSED

Hi

You are right and wrong:

• You are right because the shift code is actually dead.
• You are wrong because if you look at the IR you will see a new if/then bloc which doesn't appear in the original graph.

In x86, the shr instruction (like other shift instructions) has the following behavior:
If the counter is greater than 0, it will set the cf flag to the last bit getting of the source, and set eflag according to the result.
BUT, if the counter is null, it doesn't modify the eflag (cf, zf, sf, ...).

In Miasm, this behavior is simulated using a generated conditional branch.
To see the generated code, disassemble your code as following:

 python disasm/full.py -m x86_64   yourbinary  your_address -g

The  -g option is used to generate IR graph file. See it with xdot graph_irflow.txt
You can apply a light liveness analysis using option -s
But the liveness won't (for the moment 😄 ) delete if/then/else with empty sons.

So for now, the Z3 translator stops on the end of the first IR basic block.

from miasm.

Oh, you are right. I didn't think about working on IR basic blocks. Thanks for clarifying that! :)

from miasm.