XPlus Pointer/Integer Reconstructed As Arithmetic PlusA

[mgordon]

CodeHawk-C Issue: XPlus Pointer/Integer Reconstructed As Arithmetic PlusA

Summary

CodeHawk-C can crash while checking an upper-bound proof obligation when an
abstract XPlus expression represents pointer arithmetic. The API-expression
reconstruction path treats the expression as ordinary arithmetic and calls
get_integer_promotion on (char *) and int.

SPEC Trigger

SPEC CPU2017 perlbench, cpan/Digest-MD5/MD5.c, function base64_16, around
the output-buffer increment:

*d++ = base64[c1 >> 2];

Observed failure:

CCHFailure in function: base64_16:
Failure Unexpected types for integer promotion: (char*) and int
for ppo 201: upper-bound(char, d)

Small Reproducer

See repros/pointer_plus_int_upper_bound.c.

Likely Cause

cCHPOQuery.ml:x2api reconstructs XPlus as:

BinOp (PlusA, a1, a2, get_integer_promotion ty1 ty2)

This is valid for integer arithmetic but not for pointer-plus-integer
expressions introduced by pointer increments or pointer indexing.

Minimal Fix

When XPlus has one pointer-typed operand and one integer-typed operand,
reconstruct it as PlusPI with the pointer expression first. This avoids the
integer-promotion failure and preserves the C pointer-arithmetic operator.

pointer_plus_int_upper_bound.c