Crash on proof obligation for floating-point divisor expression [codex]

[mgordon]

CH-C crash on proof obligation for floating-point divisor expression

Summary

While analyzing SPEC CPU2017 538.imagick_r, CH-C crashed during proof-obligation generation for magick/composite.c, function ColorDodge.

The generated PO was a nonzero divisor obligation over a floating-point expression:

((Sa - Sca):MagickRealType != 0)

The analyzer failed with:

CCHFailure in function: ColorDodge:
Failure Unexpected types for integer promotion: float and float

Small reproducer

See imagick-float-arithmetic-po.c.

It mirrors the relevant ColorDodge expression from ImageMagick:

typedef double MagickRealType;

static MagickRealType ColorDodge(const MagickRealType Sca,
  const MagickRealType Sa,const MagickRealType Dca,const MagickRealType Da)
{
  if ((Sca*Da+Dca*Sa) >= Sa*Da)
    return Sa*Da+Sca*(1.0-Da)+Dca*(1.0-Sa);
  return Dca*Sa*Sa/(Sa-Sca)+Sca*(1.0-Da)+Dca*(1.0-Sa);
}

Likely cause

cCHPOQuery.ml uses get_integer_promotion while translating arithmetic expressions in API predicates, including expressions used in generated proof obligations. For integer arithmetic this is appropriate, but the same path is reached for floating-point arithmetic in a divisor nonzero PO.

get_integer_promotion in cCHTypesUtil.ml only accepted integer types and raised on TFloat operands, so the analyzer crashed before producing results for the file.

Minimal progress fix

Extend get_integer_promotion to return the usual arithmetic result type for floating-point operands:

• float/float -> promoted floating kind;
• float/int and int/float -> the floating kind;
• existing int/int behavior unchanged.

This is deliberately minimal. A cleaner long-term fix would likely rename or split the helper so the callers use an explicitly named "usual arithmetic conversion" operation instead of an integer-only helper.

imagick-float-arithmetic-po.c