Exclude symbolic results from exceptions

[kettenbruch]

added test cases for #1159

Now the results are only evaluated when they are not symbolic.

[JonathanSalwan]

Thanks for this MR!

Yesterday I've reverted some idiv checks (b0d93a5d3d42ada59b04e56ba29c769418fba3d1) because they were wrong. Divide errors are raised for different reasons. I think this is why unit tests failed.

Now the results are only evaluated when they are not symbolic.

I'm not sure about this =/. For example what if your node is symbolic but the result of temp does not fit in the dst register (>0xffffffffffffffff), do you continue the execution while it should stop? I think it leads to an incorrect path predicate. What do you think?

[kettenbruch]

Before there were any exceptions in div_s Triton would just (_ extract 63 0) the lower 64 bits and continue execution while a real machine would throw a #DE.

Still, we should be able to use div on purely symbolic registers (see test_3) The problem is that we evaluate the symbolic register to 0, divide by it and get 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF which is too big to fit a 64bit register. The concrete value of temp is too big, but this doesn't matter in test_3 as everything is symbolic. If we throw an exception, Triton gets stuck at evaluating the div instruction and we never get a complete AST.

I think it leads to an incorrect path predicate

Yes, like it did before exceptions were included: I got a CTF which runs and produces correct results when adding a path constraint in Triton v0.9 but gets stuck on the div instruction in dev-v1.0 here.

I think symbolic and concrete cases need to be treated separately: checks for overflow for the concrete case and a path constraint for divisor!=0 and temp <= 0xffffffffffffffff in the symbolic case, but I don't know if that should be done by div_s function.

[JonathanSalwan]

If we throw an exception, Triton gets stuck at evaluating the div instruction

Yes indeed this one is another error. We have to reset the state as NO_FAULT for every new instructions executed. 1960dcb3a3af3fa7feb68ddd692b57a4f3247622 should fixes this.

[JonathanSalwan]

Regarding concret vs symbolic, i'm still convinced that we have to define the state as DE even if it's symbolic or not. Now that the state is not stuck in DE mode with the previous patch (1960dcb3a3af3fa7feb68ddd692b57a4f3247622), you have the choice to continue or not the execution. For example with your CTF challenge your code might look like this:

def emulate(ctx, pc):
    while pc:
        opcode = ctx.getConcreteMemoryAreaValue(pc, 16)
        instruction = Instruction(pc, opcode)
        exc = ctx.processing(instruction)

        if instruction.isSymbolized():
            print("\033[92m" + str(instruction) + "\033[0m")
        else:
            print(instruction)

        # still need to constrain RDX to avoid #DE on a real machine (RDX:RAX too big)
        # otherwise we get incorrect results (in v0.9 and dev-v1.0)
        if pc == 0x1090:  # div instruction address
            ctx.pushPathConstraint(ctx.getRegisterAst(ctx.registers.rdx) < 0x1000)

        if exc != EXCEPTION.NO_FAULT:
            print(f'Error processing {str(instruction)}: {exc:d}\n')
            pc = instruction.getNextAddress() # <- skip the DE exception
        else:
            pc = ctx.getRegisterAst(ctx.registers.rip).evaluate()
    return

[kettenbruch]

I see. I'll handle the exception in user code as you suggested. Thanks for the code and huge thanks for Triton in general, it's a really cool project !