Simplify the conditions

[XVilka]

From the example in http://radare.today/posts/gsoc_2018_radeco_pseudo_c_code_generation/

fn sym.write_strlen () {
    int local_18h;
    unsigned int tmp;
    int local_8h;
    *((rsp - 8)) = rbp
    local_18h = rdi
    local_8h = local_18h
    while (1) {
        if (!((1 ^ (((((((*(local_8h) as 64) | (local_8h & 18446744069414584320)) & 4294967295) as 8) & ((((*(local_8h) as 64) | (local_8h & 18446744069414584320)) & 4294967295) as 8)) - 0) & 255)) as 1)) {
            tmp = sym.imp.printf(8196, unknown, rdx, rcx, r8, r9)
            return
        } else {
            local_8h = (local_8h + 1)
        }
    }
}

Obviously these conditions should be simplified.

[Mm7]

I'd love to work on this. Probably a new analysis is needed, something like analysis/arithmetic. It should take complex expressions, match them to some identities (like a^a=0, a+0=a, ...) and apply the substitution. I'm just wondering if analysis/inst_combine can be extended to do that.

[XVilka]

@Mm7 note it is partly related to https://github.com/radareorg/radeco-lib/pull/171

On the other hand, the simplification itself can be done without the graph access.

[XVilka]

I am thinking, what if we just reuse SMT solver for simplifying the expressions?

[radare]

Sounds like a good idea to me

On 14 Mar 2019, at 08:30, Anton Kochkov notifications@github.com wrote:

I am thinking, what if we just reuse SMT solver for simplifying the expressions?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.