symqemu icon indicating copy to clipboard operation
symqemu copied to clipboard

Setcond handling

Open ercoppa opened this issue 1 year ago • 3 comments

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.

ercoppa avatar Apr 06 '23 13:04 ercoppa

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

enlighten5 avatar Apr 20 '23 22:04 enlighten5

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.

ercoppa avatar Apr 21 '23 08:04 ercoppa

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

enlighten5 avatar Apr 21 '23 17:04 enlighten5