Crash translating pointer-plus-index expression in pointer upper-bound PO [codex]

[mgordon]

CH-C crash translating pointer-plus-index expression in pointer upper-bound PO

Summary

While analyzing SPEC CPU2017 538.imagick_r, CH-C crashed in magick/quantum-import.c, function ImportIndexAlphaQuantum, during iteration 0.

The failing PO was:

ptr-upperbound(((indexes + i x):unsigned short)

The analyzer failed with:

CCHFailure in function: ImportIndexAlphaQuantum:
Failure Unexpected types for integer promotion: int and (unsigned short*) for ppo 2038

Small reproducer

See imagick-pointer-plus-index-global-po.c.

It mirrors the relevant ImageMagick pattern:

set_index(indexes + x + bit / 2, 1);

where indexes is an IndexPacket *restrict and x/bit are signed loop counters.

Likely cause

cCHPOQuery.ml has an x2api translation path that distinguishes pointer-plus-integer from arithmetic addition and emits PlusPI.

The x2global translation path did not make that distinction. It translated every binary XPlus into PlusA and later called get_integer_promotion for operands that could be (integer, pointer).

This is valid C pointer arithmetic, but get_integer_promotion is not the right helper for it, so the analyzer crashed while translating the proof-obligation expression.

Minimal progress fix

Mirror the existing pointer/integer checks from x2api in x2global:

• pointer + integer -> PlusPI;
• integer + pointer -> PlusPI with operands reordered;
• pointer - pointer -> MinusPP;
• pointer - integer -> MinusPI;
• otherwise preserve the existing arithmetic path.

This is intentionally narrow and should not change the generated expression for ordinary integer or floating arithmetic.

imagick-pointer-plus-index-global-po.c