CodeHawk-C Issue: XMinus Pointer/Pointer Reconstructed As Arithmetic MinusA

[mgordon]

CodeHawk-C Issue: XMinus Pointer/Pointer Reconstructed As Arithmetic MinusA

Summary

CodeHawk-C can crash while checking a signed-to-unsigned cast proof obligation
when an abstract XMinus expression represents pointer subtraction. The
API-expression reconstruction path treats the expression as ordinary arithmetic
and calls get_integer_promotion on two pointer types.

SPEC Trigger

SPEC CPU2017 perlbench, ext/re/re_exec.c, function my_regexec:

MgBYTEPOS(mg, sv, strbeg, strend - strbeg)

Observed failure:

CCHFailure in function: my_regexec:
Failure Unexpected types for integer promotion: (char*) and (char*)
for ppo 104: signed-to-unsigned-cast-ub((long)(strend -p strbeg): unsigned long)

Small Reproducer

See repros/my_regexec_pointer_diff_cast.c.

Likely Cause

The original C dictionary preserves the expression as pointer subtraction
(MinusPP), but later abstract-expression reconstruction in
cCHPOQuery.ml:x2api sees only XMinus and rebuilds it as arithmetic MinusA.

Minimal Fix

When XMinus has two pointer-typed operands, reconstruct it as MinusPP
instead of MinusA.

my_regexec_pointer_diff_cast.c