\myheading{Tests}

\leveldown{}

Despite simplicity of the decompiler, it's still error-prone.
We need to be sure that original expression and reduced one are equivalent to each other.

\myheading{Evaluating expressions}

First of all, we would just evaluate (or \emph{run}, or \emph{execute})
expression with random values as arguments, and then compare results.

Evaluator do arithmetical operations when possible, recursively.
When any symbol is encountered, its value (randomly generated before) is taken from a table.

\begin{lstlisting}
un_ops={"NEG":operator.neg,
        "~":operator.invert}

bin_ops={">>":operator.rshift,
        "<<":(lambda x, c: x<<(c&0x3f)), # operator.lshift should be here, but it doesn't handle too big counts
        "&":operator.and_,
        "|":operator.or_,
        "^":operator.xor,
        "+":operator.add,
        "-":operator.sub,
        "*":operator.mul,
        "/":operator.div,
        "%":operator.mod}

def eval_expr(e, symbols):
    t=get_expr_type (e)
    if t=="EXPR_SYMBOL":
        return symbols[get_symbol(e)]
    elif t=="EXPR_VALUE":
        return get_val (e)
    elif t=="EXPR_OP":
        if is_unary_op (get_op (e)):
            return un_ops[get_op(e)](eval_expr(get_op1(e), symbols))
        else:
            return bin_ops[get_op(e)](eval_expr(get_op1(e), symbols), eval_expr(get_op2(e), symbols))
    else:
        raise AssertionError

def do_selftest(old, new):
    for n in range(100):
        symbols={"arg1":random.getrandbits(64), 
                "arg2":random.getrandbits(64), 
                "arg3":random.getrandbits(64), 
                "arg4":random.getrandbits(64)}
        old_result=eval_expr (old, symbols)&0xffffffffffffffff # signed->unsigned
        new_result=eval_expr (new, symbols)&0xffffffffffffffff # signed->unsigned
        if old_result!=new_result:
            print "self-test failed"
            print "initial expression: "+expr_to_string(old)
            print "reduced expression: "+expr_to_string(new)
            print "initial expression result: ", old_result
            print "reduced expression result: ", new_result
            exit(0)
\end{lstlisting}

In fact, this is very close to what LISP \emph{EVAL} function does, or even LISP interpreter.
However, not all symbols are set.
If the expression is using initial values from RAX or RBX
(to which symbols ``initial\_RAX'' and ``initial\_RBX'' are assigned,
decompiler will stop with exception, because no random values assigned to these registers,
and these symbols are absent in \emph{symbols} dictionary.

Using this test, I've suddenly found a bug here (despite simplicity of all these reduction rules).
Well, no-one protected from eye strain.
Nevertheless, the test has a serious problem: some bugs can be revealed only if one of arguments is $0$, or $1$, or $-1$.
Maybe there are even more special cases exists.

Mentioned above \emph{aha!} superoptimizer tries at least these values as arguments while testing:
1, 0, -1, 0x80000000, 0x7FFFFFFF, 0x80000001, 0x7FFFFFFE, 0x01234567, 0x89ABCDEF, -2, 2, -3, 3,
-64, 64, -5, -31415.

Still, you cannot be sure.

\myheading{Using Z3 SMT-solver for testing}
\label{ToyDecompilerTestingZ3}

So here we will try Z3 SMT-solver.
SMT-solver can \emph{prove} that two expressions are equivalent to each other.

For example, with the help of \emph{aha!}, I've found another weird piece of code, which does nothing:

\begin{lstlisting}
; do nothing (obfuscation)

;Found a 5-operation program:
;   neg   r1,rx
;   neg   r2,r1
;   sub   r3,r1,3
;   sub   r4,r3,r1
;   sub   r5,r4,r3
;   Expr: (((-(x) - 3) - -(x)) - (-(x) - 3))

        mov rax, rdi
        neg rax
        mov rbx, rax
        ; rbx=-x
        mov rcx, rbx
        sub rcx, 3
        ; rcx=-x-3
        mov rax, rcx
        sub rax, rbx
        ; rax=(-(x) - 3) - -(x)
        sub rax, rcx
\end{lstlisting}

Using toy decompiler, I've found that this piece is reduced to \emph{arg1} expression:

\begin{lstlisting}
working out tests/t5_obf.s
going to reduce ((((-arg1) - 3) - (-arg1)) - ((-arg1) - 3))
reduction in reduce_SUB2() ((-arg1) - 3) -> (-(arg1 + 3))
reduction in reduce_SUB5() ((-(arg1 + 3)) - (-arg1)) -> ((-(arg1 + 3)) + arg1)
reduction in reduce_SUB2() ((-arg1) - 3) -> (-(arg1 + 3))
reduction in reduce_ADD_SUB() (((-(arg1 + 3)) + arg1) - (-(arg1 + 3))) -> arg1
going to reduce arg1
result=arg1
\end{lstlisting}

But is it correct?
I've added a function which can output expression(s) to SMT-LIB-format, it's as simple as a function which converts
expression to string.

And this is SMT-LIB-file for Z3:

\begin{lstlisting}
(assert
    (forall ((arg1 (_ BitVec 64)) (arg2 (_ BitVec 64)) (arg3 (_ BitVec 64)) (arg4 (_ BitVec 64)))
        (=
            (bvsub (bvsub (bvsub (bvneg arg1) #x0000000000000003) (bvneg arg1)) (bvsub (bvneg arg1) #x0000000000000003))
            arg1
        )
    )
)
(check-sat)
\end{lstlisting}

In plain English terms, what we asking it to be sure, that \emph{forall} four 64-bit arguments, two expressions
are equivalent (second is just \emph{arg1}).

The syntax maybe hard to understand, but in fact, this is very close to LISP, and arithmetical operations
are named ``bvsub'', ``bvadd'', etc, because ``bv'' stands for \emph{bit vector}.

While running, Z3 shows ``sat'', meaning ``satisfiable''.
In other words, Z3 couldn't find counterexample for this expression.

In fact, I can rewrite this expression in the following form: \emph{expr1 != expr2}, and we would ask
Z3 to find at least one set of input arguments, for which expressions are not equal to each other:

\begin{lstlisting}
(declare-const arg1 (_ BitVec 64))
(declare-const arg2 (_ BitVec 64))
(declare-const arg3 (_ BitVec 64))
(declare-const arg4 (_ BitVec 64))

(assert
    (not
        (=
            (bvsub (bvsub (bvsub (bvneg arg1) #x0000000000000003) (bvneg arg1)) (bvsub (bvneg arg1) #x0000000000000003))
            arg1
        )
    )
)
(check-sat)
\end{lstlisting}

Z3 says ``unsat'', meaning, it couldn't find any such counterexample.
In other words, for all possible input arguments, results of these two expressions are always equal to each other.

Nevertheless, Z3 is not omnipotent.
It fails to prove equivalence of the code which performs division by multiplication.
First of all, I extended it so both results will have size of 128 bit instead of 64:

\begin{lstlisting}
(declare-const x (_ BitVec 64))
    (assert
        (forall ((x (_ BitVec 64)))
            (=
                ((_ zero_extend 64) (bvudiv x (_ bv17 64)))
                (bvlshr (bvmul ((_ zero_extend 64) x) #x0000000000000000f0f0f0f0f0f0f0f1) (_ bv68 128))
            )
        )
    )
(check-sat)
(get-model)
\end{lstlisting}

(\emph{bv17} is just 64-bit number 17, etc. ``bv'' stands for ``bit vector'', as opposed to integer value.)

Z3 works too long without any answer, and I had to interrupt it.

As Z3 developers mentioned, such expressions are hard for Z3 so far:
\url{https://github.com/Z3Prover/z3/issues/514}.

Still, division by multiplication can be tested using previously described brute-force check.

\levelup{}