initialized-range over casted startof can abort on missing memory reference

[mgordon]

initialized-range over casted startof can abort on missing memory reference

Summary

During perlbench iteration 1, CH-C aborts while checking an initialized-range
proof obligation if the base expression is a casted start-of-stack-array
expression and the corresponding memory-reference id cannot be resolved.

Reproducer

See repros/initialized_range_cast_startof.c.

The relevant shape is:

char tmpbuf[8];
tmpbuf[0] = 'x';
tmpbuf[1] = '\0';
strlen((char *)tmpbuf);

This produces an initialized-range obligation over an expression shaped like:

initialized-range(caste(startof(tmpbuf)), ntp[caste(startof(tmpbuf))])

Observed Failure

In SPEC CPU 2017 perlbench, the second analysis round failed in
mg:Perl_magic_setenv with:

CCHFailure in function: Perl_magic_setenv:
Failure No memory reference found with index: 14 for ppo 391:
initialized-range(caste (startof (tmpbuf):(char*)),
                  ntp[caste (startof (tmpbuf):(char*))])

The exception is raised from memory_reference_manager_t#get_memory_reference
and propagates out of check_initialized_range, causing the whole file
analysis subprocess to fail.

Minimal Workaround

For the SPEC perlbench run, the checker now catches CCHFailure inside
check_initialized_range, records the message as a diagnostic argument, and
returns false. This leaves the specific proof obligation open instead of
crashing the project analysis.

Suggested Proper Fix

The better fix is to preserve/reconstruct the memory reference for casted
startof(array) expressions so that initialized-range can reason about the
underlying stack array. The current workaround intentionally sacrifices
precision only for this failing obligation.

initialized_range_cast_startof.c

[sipma]

Unable to reproduce. The initialized-range proof obligation is reported open, without causing a crash on the reproducer program.