Manipulating info.branch.taken

[arullier-cs]

Hello,

I wonder if manipulating the attribute info.branch.taken allows internally to trigger solver in order to pursue exploration of both branches.

To clarify:

test    esi, esi
mov     eax, 336F9B7Fh
mov     ecx, 0CA6A7046h
cmovz   eax, ecx
mov     ecx, 0E9213AF1h

There is an extract of the script:

def cb_path(m:MaatEngine): 

    if take_snapshot: 
        m.take_snapshot()
        return ACTION.HALT
    return ACTION.CONTINUE 


def exec(start:int):
     global m

     stop_r =  m.run_from(start)
     take_snapshot = False

      m.restore_snapshot(remove=False)
      m.info.branch.taken = True
      m.run()

      print(f"first solution: {m.cpu.eax}")

      m.restore_snapshot(remove=False)
      m.info.branch.taken = False
      m.run()

      print(f"first solution: {m.cpu.eax}")

The output

python exec_bb.py -b bin  -s 8405
[Info] Run 0x8405: TEST ESI,ESI
[Info] Run 0x8407: MOV EAX,0x336f9b7f
[Info] Run 0x840c: MOV ECX,0xca6a7046
[Info] Run 0x8411: CMOVZ EAX,ECX
[Error] Purely symbolic branch condition
[Error] Unexpected error when processing IR instruction, aborting...
[Info] Run 0x8411: CMOVZ EAX,ECX
[Error] Purely symbolic branch condition
[Error] Unexpected error when processing IR instruction, aborting...
first solution: 0x336f9b7f
[Info] Run 0x8411: CMOVZ EAX,ECX
[Error] Purely symbolic branch condition
[Error] Unexpected error when processing IR instruction, aborting...
second solution: 0x336f9b7f

What is weird is that in the first exec, it manages to inject model to get the first value of eax. But during the second execution it seems to use equivalent model and fails to found the second possible value (0xca6a7046).

I wonder if it is a bug, or I'm miss something on how to manipulate such info attribute.

reproduce.zip

Cheers,

Anthony