Skip to content

Transformed VLA allocation into heap allocation and bounded the allocation size

🤖 SoSy-Bot 🤖 requested to merge github/fork/ccadar/vla into master

Created by: ccadar

There are several benchmarks which use variable-length arrays (VLAs), which look like this:

...
SIZE = __VERIFIER_nondet_int();
if (SIZE > 1) {
   int a[SIZE];
...

There are several issues with this pattern:

  1. VLAs are an optional feature in C11
  2. The Test-Comp rules say nothing about VLA allocation (they only talk about malloc and alloca)
  3. Huge values of SIZE can lead to unpredictible results.

For instance, consider this program:

int main() {
  int a[1073745936], i;

  for (i=0; i < 1000; i++)
    a[i] = 1;

  return 0;
}

At least on my machine, if you compile it with gcc and then run the resulting binary with Valgrind, you'll see that Valgrind complains about invalid writes, because the large VLA allocation has failed.

My proposal is to replace all such allocations with malloc, and set a bound on the allocation size. The latter is also needed to make sure that the allocation succeeds during validation in Test-Comp.

I changed two benchmarks as an example of what I mean. If you are happy with these changes, I can try to update the other benchmarks using this pattern too (although there's quite a large number of them).

Merge request reports