zstd analysis failure: pointer-difference expression lowering and 64-bit constants
Trigger
Full CodeHawk-C analysis of zstd v1.5.7 with ZSTD_NO_ASM=1 and HAVE_THREAD=0.
Small repro: zstd-pointer-diff-and-u64-constant.c
Observed failures
The first full zstd run reported these blocking analyzer failures:
lib/common/xxhash, ZSTD_XXH64_reset: Failure Int64.of_string while creating an unsigned-to-unsigned-cast proof request for an expression containing 64-bit xxhash prime constants.lib/compress/zstd_lazy, ZSTD_safecopyLiterals: Unexpected types for integer promotion: (unsigned char*) and (unsigned char*) for not-null(op).- Similar pointer-pointer promotion failures in
zstdmt_compress, zstd_decompress_block, and legacy zstd_v05, zstd_v06, and zstd_v07.
Root Cause
Some invariant expressions that contain pointer subtraction or pointer comparisons are converted back to C expressions for global/API proof requests. Invalid arithmetic combinations fell through to get_integer_promotion, which is correct to reject two pointer operands, but the rejection was propagated as an analyzer crash.
The xxhash failure came from converting numerical constants outside signed 64-bit range through Int64.of_string, even when they are representable as unsigned 64-bit constants.
Sound Fix
Expression lowering now constructs explicit PlusPI, MinusPI, and MinusPP CIL operators when the operand types justify pointer arithmetic. For arithmetic combinations that are not valid C arithmetic, conversion records the unevaluated expression and returns None; the corresponding proof obligation remains open instead of being marked safe.
Numerical constant lowering now preserves fixed-width representation for values representable in 64 bits. Signed 64-bit values use IInt; unsigned 64-bit values use IULongLong with the two's-complement int64 bit pattern expected by the CIL constant representation. Values outside that range still fail explicitly.
zstd analysis failure: pointer-difference expression lowering and 64-bit constants
Trigger
Full CodeHawk-C analysis of zstd v1.5.7 with
ZSTD_NO_ASM=1andHAVE_THREAD=0.Small repro: zstd-pointer-diff-and-u64-constant.c
Observed failures
The first full zstd run reported these blocking analyzer failures:
lib/common/xxhash,ZSTD_XXH64_reset:Failure Int64.of_stringwhile creating an unsigned-to-unsigned-cast proof request for an expression containing 64-bit xxhash prime constants.lib/compress/zstd_lazy,ZSTD_safecopyLiterals:Unexpected types for integer promotion: (unsigned char*) and (unsigned char*)fornot-null(op).zstdmt_compress,zstd_decompress_block, and legacyzstd_v05,zstd_v06, andzstd_v07.Root Cause
Some invariant expressions that contain pointer subtraction or pointer comparisons are converted back to C expressions for global/API proof requests. Invalid arithmetic combinations fell through to
get_integer_promotion, which is correct to reject two pointer operands, but the rejection was propagated as an analyzer crash.The xxhash failure came from converting numerical constants outside signed 64-bit range through
Int64.of_string, even when they are representable as unsigned 64-bit constants.Sound Fix
Expression lowering now constructs explicit
PlusPI,MinusPI, andMinusPPCIL operators when the operand types justify pointer arithmetic. For arithmetic combinations that are not valid C arithmetic, conversion records the unevaluated expression and returnsNone; the corresponding proof obligation remains open instead of being marked safe.Numerical constant lowering now preserves fixed-width representation for values representable in 64 bits. Signed 64-bit values use
IInt; unsigned 64-bit values useIULongLongwith the two's-complementint64bit pattern expected by the CIL constant representation. Values outside that range still fail explicitly.