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:
mini_hang.py: the Python script for reproducing the hang
Robot.elf: the firmware's binary image
Robot.objdump.disasm: the firmware's disassembly (for manual inspection)
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.
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, #0a522: teq r1, r3a526: it pla528: cmppl r1, r3a52a: it eqa52c: cmpeq r0, r2a52e: ite csa530: asrcs r0, r3, #31a532: mvncc.w r0, r3, asr #31a536: orr.w r0, r0, #1a53a: bx lr......
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:
One may reproduce the hang with the following command:
python3 mini_hang.py Robot.elf mmio_access_state_bbid_0001cae9_pc_080025a8_addr_40005410The 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, #0a522: teq r1, r3a526: it pla528: cmppl r1, r3a52a: it eqa52c: cmpeq r0, r2a52e: ite csa530: asrcs r0, r3, #31a532: mvncc.w r0, r3, asr #31a536: orr.w r0, r0, #1a53a: bx lr......firmware binary: uEmu_thermostat.zip