arm: Account for Thumb instruction widths in IT lookback

[zardus]

THIS MESSAGE WAS GENERATED BY AN AUTOMATED PROCESS

Problem

Lifting Thumb memchr at 0x8002451 in libopencm3_adc-dac-printf.elf, block 0x80024e9, can retain ITSTATE after a mixed-width IT group has ended and emit a false conditional exit to 0x80024eb.

Root cause

The ARM decoder treated every guarded instruction as one halfword during its backward IT search. It could not prove that a mixed-width group had expired, and an expired 0xbf08 halfword inside LDREX could hide an older active IT candidate.

Fix

Walk forward from each candidate using the actual 16- or 32-bit Thumb instruction widths. Mark the current instruction conditional only when the candidate reaches it, and continue searching after an expired false candidate.

Testing

The dependent PyVEX regression covers the public memchr case, mixed-width expiry, conservative boundary cases, the false LDREX candidate, and the lookback-window edge. The native VEX build and the 68-test PyVEX suite passed. Validation: #92 (comment)

session: sharpen

[zardus]

THIS MESSAGE WAS GENERATED BY AN AUTOMATED PROCESS

Validation record for head 881703eda064a67a803cf51974c992286a8bdf4f against baseline 875f7c9a5f6be621b4f000c29c016e15ddf32207.

• Native build: make -f Makefile-gcc -j1 all — passed; guest_arm_toIR.c compiled without a new diagnostic
• Downstream regression: python -m pytest -q tests/test_arm_postprocess.py in the coordinated PyVEX checkout — 6 passed; the baseline emits a false exit to 0x80024eb, while head emits none
• Downstream full suite: python -m pytest -q in PyVEX — 68 passed
• Lint/type: all configured PyVEX pre-commit hooks passed; merge-base Pylint/Pyright comparison passed with 10.00 -> 10.00 and improved type badness
• Workspace gate: adopted PyVEX/VEX only — workspace checks 9/9, test-input policy passed, all 12 feature-instance scenarios passed, PyVEX 68 passed; unadopted ecosystem repositories were not tested
• Reproducer: DecBench 4b42a0dc6158913db0648a9123e76d6ddd9ab9cf, O2-noinline/libopencm3/adc-dac-printf.elf SHA-256 9145af6d42a26620009ffd84334a012d0a118b55302287913efb9f8a52615d19, Thumb memchr at 0x8002451, target block 0x80024e9
• Behavioral A/B on angr 5d32d30d6da9e017484b11363de5f778f21c697e: baseline has one ITSTATE read, one exit to 0x80024eb, and an undefined goto under SAILR and Phoenix; head has none, with identical 17-node/25-edge function CFG topology

Caveat: the executable regressions live in the dependent PyVEX pull request; this repository's local gate is its native build.

[zardus]

THIS MESSAGE WAS GENERATED BY AN AUTOMATED PROCESS

Full lift-state result for Thumb memchr block 0x80024e9 in libopencm3_adc-dac-printf.elf, before and after this VEX change.

Before — fixed-width lookback retains a stale ITSTATE guard:

VEX baseline 875f7c9

ITSTATE reads: 1
conditional exits: [0x80024eb]
function CFG edge to 0x80024eb: absent

After — width-aware lookback proves the instruction unconditional:

with this change at 881703e

ITSTATE reads: 0
conditional exits: []
function CFG topology: unchanged at 17 nodes / 25 edges