Muluh symbolic value is concretized

[ercoppa]

Symqemu defines a symbolic helper for muluh_i64:

void *HELPER(sym_muluh_i64)(uint64_t arg1, void *arg1_expr,
                            uint64_t arg2, void *arg2_expr)
{
    BINARY_HELPER_ENSURE_EXPRESSIONS;

    assert(_sym_bits_helper(arg1_expr) == 64 &&
           _sym_bits_helper(arg2_expr) == 64);
    void *full_result = _sym_build_mul(_sym_build_zext(arg1_expr, 64),
                                       _sym_build_zext(arg2_expr, 64));
    return _sym_extract_helper(full_result, 127, 64);
}

Which seems ok. When, e.g., mulu2_i64 is met, this is the instrumentation:

       TCGv_i64 t0 = tcg_temp_new_i64();
        tcg_gen_mul_i64(t0, arg1, arg2);
        gen_helper_sym_muluh_i64(tcgv_i64_expr(rh),
                                 arg1, tcgv_i64_expr(arg1),
                                 arg2, tcgv_i64_expr(arg2));
        gen_helper_muluh_i64(rh, arg1, arg2);
        tcg_gen_mov_i64(rl, t0);
        tcg_temp_free_i64(t0);

Which should be ok. However, gen_helper_muluh_i64 indirectly executes tcg_gen_callN which performs:

    if (ret != NULL && ret->symbolic_expression == 0) {
        /* This is an unhandled helper; we concretize, i.e., the expression for
         * the result is NULL */
        tcg_gen_op2i_i64(INDEX_op_movi_i64, temp_tcgv_i64(temp_expr(ret)), 0);
    }

that will concretize the symbolic value generated by the symbolic helper. Am I wrong?

If I am not wrong, we could just add a check for this special case, e.g.:

   if (ret != NULL 
        && ret->symbolic_expression == 0
        // helper_sym_muluh_i64 will take care of the return
        // symbolic value of helper_muluh_i64
        && func != helper_muluh_i64) {

Let me know what do you think. I can make a PR.

[ercoppa]

This may maybe help fix #12 (I did not test it).