Semantics of SSA do not model the binary logic

[user1342234]

Hello! The ircfg_to_ssa transformation isn't numbering my variables correctly. In, loc_fffff8022ed3962a, I have a statement (1) RAX.0=RAX+0xFFFFFFFFF4E120DA which is eventually used to resolve the next jump. This makes no sense to me. Even if I was able to solve the opaque predicates in my graph (provided below), i would end with the statements: RAX.1=RAX.0, RAX.0=RAX+0xFFFFFFFFF4E120DA. Through expression propagation, we get statement (2): RAX.1=RAX + 0xFFFFFFFFF4E120DA which is used to find the next block. But, I am unable to solve this statement since RAX is unknown. In the real binary, the RAX in statement (2) is replaced by 0xFFFFF80239D83800, but, this value is assigned RAX.1=0xFFFFF80239D83800 in loc_fffff8022e0e7ce9. So I am unable to propagate it and solve the jump.

I'm trying to understand why this is happening and how I can fix it to find the correct destination.

[serpilliere]

Hi @user1342234 !

I didn't understand exactly the whole logic you are explaining here, but if you think that there is a propagation error (or a missed propagation here) here is how we usually debug it in miasm:

• we build a "patological" example extracted from your example
• we try to make it minimalist
• and then analyse the steps during simplification.

Do you think that generating a minimalist example would be possible?

[user1342234]

Hi! Yes, I can try and generate a minimalist example to reproduce the behaviour

[user1342234]

Hi @serpilliere ! Unfortunately, I'm unable to reproduce the behaviour but I think I have an idea of what I'm doing incorrectly.

In my current analysis, I have a function which parses each IRBlock's IRDst and then adds it to the ssa.graph where I proceed to call ircfg_to_ssa to translate it. In ircfg_to_ssa, I see that we transform variables to SSA and number them using a stack ( _stack_lhs in this case). Do you think that my analysis interfering with this numbering somehow?

Some evidence for this interference is in the image below. According to the SSA algorithm, the Phi node assigned to RAX.0 should actually be RAX.1 since the predecessor block has the mapping {ExprId("RAX",64) : 0}