Infer effective length for single-blob arrays

[karoliineh]

This PR fixes array out-of-bounds handling for dynamically allocated arrays whose abstract array length is initially represented as a single blob. This was found using the dashboard comparison between Goblint and Mopsa and was exposed by the SV-COMP task memsafety-cve/libredwg.i.

Goblint output spurious error messages for the program:

[Error][Behavior > Undefined > ArrayOutOfBounds > PastEnd] Must access array past end (/home/holterka/sv-benchmarks/c/memsafety-cve/libredwg.i:425:5-425:48)
[Error][Behavior > Undefined > ArrayOutOfBounds > PastEnd] Must access array past end (/home/holterka/sv-benchmarks/c/memsafety-cve/libredwg.i:425:5-425:48)
[Error][Behavior > Undefined > ArrayOutOfBounds > PastEnd] Must access array past end (/home/holterka/sv-benchmarks/c/memsafety-cve/libredwg.i:425:5-425:48)
[Error][Behavior > Undefined > ArrayOutOfBounds > PastEnd] Must access array past end (/home/holterka/sv-benchmarks/c/memsafety-cve/libredwg.i:425:5-425:48)

With the offending code being:

unsigned char *getRandomByteStream(int size) {
  unsigned char *randomString = (unsigned char *)calloc(size, sizeof(unsigned char));
  if (randomString == ((void *)0)) {
    printf("Out of memory\n");
    exit(1);
  }
  for (int i = 0; i < size; i++) {
    randomString[i] = __VERIFIER_nondet_uchar();
  }
  return randomString;

where size was a constant of 50 during the function call, but Goblint's array_oob_check considered the array size as 1.

The change computes an effective array length from the blob size divided by the element size, then uses that length before indexed reads and writes. This prevents valid accesses into calloc-allocated arrays from being treated imprecisely.

• Added a regression test for a valid access into a calloc-allocated unsigned char array.
• Added effective_array_length to derive array length from blob size when possible.
• Apply the effective length before array indexed reads.
• Apply the effective length before array indexed writes.

[sim642]

This seems a bit roundabout to try to recover the length after the fact if it's 1. Currently it's being set as 1 at calloc:

analyzer/src/analyses/base.ml

Line 2785 in 729eb71

let blob_set = Option.map_default (fun heap_var -> [heap_var, TVoid [], VD.Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, ZeroInit.calloc)))]) [] heap_var in

I don't really know why it's 1 there though, instead of the actual length given by the argument to calloc. I think this has come up before and for some reason we never changed it.

[michael-schwarz]

I think this should be fixed together with #1766, if we are already touching this part.

[michael-schwarz]

Related: #702 #135 #145

[karoliineh]

After spending time investigating the related issues and trying a few alternative approaches, I agree that this PR proposal is only a hacky remedy for one part of a broader problem rather than the right direction. A proper fix would require rethinking how calloc allocations, blob/array representations, and allocation-size reasoning interact throughout the base analysis, which makes solving this issue quite complex and is more work than I can prioritize right now. Closing this for the time being.