Unexpected behavior when executing a single function

[Escapingbug]

---

Hi. While trying to evaluating a single function within a binary image, an interesting situation has been discovered.

The code is listed below:

import angr
import logging
import cle
import claripy

logging.getLogger().setLevel(logging.DEBUG)

def main():
    image = cle.loader.Loader('image', main_opts={'backend': 'blob', 'arch': 'x86_64', 'base_addr': 0, 'entry_point': 0x21b0d})
    p = angr.project.Project(image)

    inputs = [claripy.BVS(f'input_{i}', 8) for i in range(8)]
    input_str = claripy.Concat(*inputs)
    input_ptr = angr.PointerWrapper(input_str)

    state = p.factory.call_state(0x21b0d, input_ptr)

    for input_ch in inputs:
        state.solver.add(input_ch >= 0x5f)
        state.solver.add(input_ch <= 0x61) # this line, if change from 0x61 => 0x65, gets unsat


    simgr = p.factory.simulation_manager(state)
    simgr.explore(find=0x21c6d)

    assert len(simgr.found) == 1

    s = simgr.found[0]
    s.solver.add(s.regs.edx == 0xb9fa5d1e) # this is the correct answer for all input_ch == 0x61 (verified using state.solver.add(input_str == 0x6161616161616161) then s.solver.eval(s.regs.edx))
    print(hex(s.solver.eval(s.regs.edx)))
    print(hex(s.solver.eval(input_str)))

if __name__ == '__main__':
    main()

And the image is here:

image.zip

The interesting behavior is that, when loosing the input_str constraint, the final output is somehow unsat. And there's no other found paths.

The evaluating decompiled function is listed below:

void FUN_00021b0d(uint *param_1)

{
  uint uVar1;
  uint uVar2;
  uint uVar3;
  uint uVar4;
  uint uVar5;
  uint uVar6;
  int iVar7;
  
  FUN_00021de1();
  uVar1 = *param_1 >> 0x10;
  uVar2 = uVar1 * 7;
  if (uVar2 == 0) {
    uVar2 = -uVar1 - 6;
  }
  else {
    uVar2 = (uVar2 & 0xffff) - (uVar2 >> 0x10);
    uVar2 = uVar2 - (uVar2 >> 0x10);
  }
  uVar3 = *param_1 + 6;
  uVar4 = (param_1[1] >> 0x10) + 5;
  uVar5 = param_1[1] & 0xffff;
  uVar1 = uVar5 * 4;
  if (uVar5 == 0) {
    uVar1 = 0xfffffffd;
  }
  else {
    uVar1 = (uVar1 & 0xffff) - (uVar1 >> 0x10);
    uVar1 = uVar1 - (uVar1 >> 0x10);
  }
  uVar6 = (uVar4 ^ uVar2) & 0xffff;
  uVar5 = uVar6 * 3;
  if (uVar5 == 0) {
    iVar7 = -2 - uVar6;
  }
  else {
    uVar5 = (uVar5 & 0xffff) - (uVar5 >> 0x10);
    iVar7 = uVar5 - (uVar5 >> 0x10);
  }
  uVar6 = (uVar3 ^ uVar1) + iVar7 & 0xffff;
  uVar5 = uVar6 * 2;
  if (uVar6 == 0) {
    uVar5 = 0xffffffff;
  }
  else {
    uVar5 = (uVar5 & 0xffff) - (uVar5 >> 0x10);
    uVar5 = uVar5 - (uVar5 >> 0x10);
  }
  *param_1 = (uVar2 ^ uVar5) << 0x10 | (uVar5 ^ uVar4) & 0xffff;
  param_1[1] = (uVar1 ^ iVar7 + uVar5) & 0xffff | (uVar3 ^ iVar7 + uVar5) << 0x10; // <-- 0x21b0d here, edx is the rhs value
  return;
}

Got really confused on this..

[github-actions]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions]

This issue has been closed due to inactivity.