Non-terminating _excavate_ite

[B03901108]

Description

A SimState.step() was stuck in claripy's _excavate_ite when I symbolically executed an ARM Cortex-M firmware. During the non-terminating _excavate_ite (running for at least an hour), the size of the "ast_queue" remained below 90, and the depth of each "ast" remained below 40. The caller of the _excavate_ite is op_concretize in angr. The "op" therein has depth 95.

Steps to reproduce the bug

There are four files in the zip file:

1. mini_hang.py: the Python script for reproducing the hang
2. Robot.elf: the firmware's binary image
3. Robot.objdump.disasm: the firmware's disassembly (for manual inspection)
4. mmio_access_state_bbid_0001cae9_pc_080025a8_addr_40005410: the initial SimState

One may reproduce the hang with the following command: python3 mini_hang.py Robot.elf mmio_access_state_bbid_0001cae9_pc_080025a8_addr_40005410 The script may take 10~20 minutes to reach the basic block (0x08000268 in <__adddf3>) causing the hang.

script for reproducing the hang: claripy_hang.zip

Environment

angr 9.2.61 claripy 9.2.61 z3-solver 4.10.2.0.

Additional context

I discussed the related questions on angr's Slack channel with @rhelmot 2~3 days ago. At that time, I was working on another ARM Cortex-M firmware whose symbolic execution was also stuck in claripy's _excavate_ite. The symbolic execution code for that firmware (Thermostat.elf) is a bit too complicated for me to write a simple script that reproduces the hang. So, here I report the hang with the Robot.elf firmware.

In the case of Thermostat.elf, the "op" in op_concretize before calling _excavate_ite has a depth 1, each "ast" in the loop of _excavate_ite has a depth below 30, and most of the ast depths are below 5. The following is the basic block (0xa51e in <__cmpdf2>) causing the hang: 0000a4e8 <__cmpdf2>: ...... a51e: cmn.w r0, #0 a522: teq r1, r3 a526: it pl a528: cmppl r1, r3 a52a: it eq a52c: cmpeq r0, r2 a52e: ite cs a530: asrcs r0, r3, #31 a532: mvncc.w r0, r3, asr #31 a536: orr.w r0, r0, #1 a53a: bx lr ......

firmware binary: uEmu_thermostat.zip