eurecom-s3 / symqemu

SymQEMU: Compilation-based symbolic execution for binaries
http://www.s3.eurecom.fr/tools/symbolic_execution/symqemu.html
Other
331 stars 44 forks source link

Setcond handling #26

Open ercoppa opened 1 year ago

ercoppa commented 1 year ago

For instance, let us consider the handling of setcond_i32:

        tcg_gen_op4i_i32(INDEX_op_setcond_i32, ret, arg1, arg2, cond);
        TCGv_i32 cond_temp = tcg_const_i32(cond);
        gen_helper_sym_setcond_i32(
            tcgv_i32_expr(ret), cpu_env,
            arg1, tcgv_i32_expr(arg1),
            arg2, tcgv_i32_expr(arg2),
            cond_temp, ret);
        tcg_temp_free_i32(cond_temp);

This code first executes the concrete computation and then performs the symbolic reasoning. However, when ret is the same TCG temp of arg1 or arg2 there is a problem: the concrete value of arg1 or arg2 taken by the symbolic helper has been already updated by the concrete computation.

To fix this problem, we can make a copy of arg1 or arg2 in case of aliasing with ret to preserve the original value. Let me know if this a reasonable PR or how to improve it.

enlighten5 commented 1 year ago

I think this can be avoided by calling the symbolic helper before generating INDEX_op_setcond_i32.

ercoppa commented 1 year ago

I think the code was written in this was because the symbolic helper takes as input the ret value computed by INDEX_op_setcond_i32.

enlighten5 commented 1 year ago

Yes, you are right. I thought the branch result is computed in the backend.