Finish SSAVerifier

[ZhangZhuoSJTU]

SSAVerifier / Verified add to ensure IR invariants are maintained and never violated. This will help future developer to make sure their changes on IR is correct and viable.

Some invariants are as follows. (Please remind me if i forget some invariants)

• [x] All the basic block should have one unconditional outgoing edge or two conditional outgoing edges.
• [x] For basic blocks, which have two conditional outgoing edges, a selector is necessary.
• [x] For basic blocks, which only have one unconditional outgoing edge, they could not have any selector.
• [ ] Unreachable block should be deleted, which means all the basic block should be reached from start_node.
• [ ] Every operation node should have the same operands as its arity.
• [ ] Every operation node's operands should correspond width rule.
• [x] Every operation node, except phi node, should not have back use-def edge or self loop.
• [x] Every use-def SCC should be reachable
• [x] There is only one copy for every constant
• [x] Every constant must be registered into constants HashMap

[XVilka]

You can gain some inspiration from BIL verifier https://github.com/BinaryAnalysisPlatform/bap-veri

[sushant94]

After #95, the selector test for unconditional branches has been disabled. This needs to be re-enabled and checked when the target of an unconditional is not:

1. A single target - Analysis of an indirect CF transfer may resolve it to a set of possible targets.
2. Unresolved - No analysis has been run to determine the possible targets.

[XVilka]

@ZhangZhuoSJTU any update on this one?

[XVilka]

So, what with this one?

[ZhangZhuoSJTU]

Let me check the code later today, I am not sure whether these have been finished by other people by chance.

[XVilka]

@ZhangZhuoSJTU are there any updates on this one?

[XVilka]

@ZhangZhuoSJTU ping? We want to make the first version next month.

[XVilka]

@ZhangZhuoSJTU can you please finish this one? Seems not that much work is left.

[ZhangZhuoSJTU]

Sorry, I forgot this one. Right now I have a finished SSAVerifier, but it will fail (all the time) because our SSA does have many bugs. If we want to let the test pass, we should close the verifier.

Anyway, I will finish this one this week when I am free. It's quick.

[XVilka]

This is good that it shows the bugs, it is the purpose after all.

On Thu, Sep 27, 2018, 1:59 AM izhuer [email protected] wrote:

Sorry, I forgot this one. Right now I have a finished SSAVerifier, but it will fail (all the time) because our SSA does have many bugs. If we want to let the test pass, we should close the verifier.

Anyway, I will finish this one this week when I am free. It's quick.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/radareorg/radeco-lib/issues/85#issuecomment-424812078, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMZ_YsP7gd1XbUqNXoo3R8fk-9lrMBkks5ue8BigaJpZM4PPnyY .

[XVilka]

@ZhangZhuoSJTU can you please write what is the state of it? @Mm7 this one is important for making sure we get a valid results.

[ZhangZhuoSJTU]

@XVilka

I am sorry I might not be able to upload my local SSAVerifier. It seems RadecoIL has changed a lot so that my old code failed. I am so sorry that I do not have enough time to work on this right now.

But I think it might be easy to rewrite the verifier by someone who is familiar with the new IR. It would also be a good chance to get familiar with our IR.

Someone who will work on this can get hints from the original SSAVerifier. If he needs any help, I can answer in this issue.