Support multidimensional VLAs

[michael-schwarz]

One-dimensional VLAs are (kind of) supported via turning them into alloca calls.
But this fails for multidimensional arrays:

int main() {
  int x = 1;
  int y = 1;
  int m[x][y];

  m[0][0] = 0;
} 

leads to Error: Cannot resolve variable m.

Changing it to int m[x][1]; makes it work again.

[vogler]

Source of raised error:
https://github.com/goblint/cil/blob/develop/src/frontc/cabs2cil.ml#L2904

[vogler]

The question is whether the above is considered a variable length array since its length is constant.

https://en.wikipedia.org/wiki/Variable-length_array#C99

vla.c

int main(int argc, char** argv) {
  int l = argc;
  int a[l];
  return a[1];
}

Tried to get the compiler to complain about it, but it doesn't:

$ gcc-9 -std=c89 -Wall vla.c && ./a.out; echo $?
254

[michael-schwarz]

The length in your example vla.c is not really constant (as in known at compile-time) though?

I think the reason GCC does not complain is that it allows some extensions and apparently VLA is among them, maybe try with -pedantic
-> https://stackoverflow.com/questions/4159746/variable-length-arrays-in-c89

[vogler]

Thanks, with -pedantic it gives the desired output :

$ gcc-9 -std=c90 -pedantic vla.c
vla.c: In function 'main':
vla.c:4:3: warning: ISO C90 forbids variable length array 'a' [-Wvla]
    4 |   int a[l];
      |   ^~~

The length in your example vla.c is not really constant (as in known at compile-time) though?

That was the point - check if the warning disappears after making it const int l = 3;, which it does not (only after after changing to c99 or gnu99).

[vogler]

./goblint vla.c --enable justcil:

...
  int l ;
  int *a ;
  unsigned long __lengthofa ;
  void *tmp ;

  {
  {
#line 3
  l = argc;
#line 4
  __lengthofa = (unsigned long )l;
#line 4
  tmp = __builtin_alloca(sizeof(*a) * __lengthofa);
#line 4
  a = (int *)tmp;
  }
#line 5
  return (*(a + 1));
...

Changing vla.c to:

int main(int argc, char** argv) {
  int l = argc;
  int a[3][l];
  return a[1][1];
}

  int l ;

  {
  {
#line 3
  l = argc;
  }
  booo_statement: /* CIL Label */
  {
#line 5
  __asm__  ("booo_exp(vla.c:5)":);
  }
#line 5
  return (0);

booo 😄

[vogler]

Ok, we should patch it to also support nested arrays by calling alloca with the product of their sizes.

Size:
https://github.com/goblint/cil/blob/develop/src/frontc/cabs2cil.ml#L5557
Call:
https://github.com/goblint/cil/blob/develop/src/frontc/cabs2cil.ml#L5569-L5583
TBD how allowVarSizeArrays is set and why it's false here:
https://github.com/goblint/cil/blob/develop/src/frontc/cabs2cil.ml#L2888

[michael-schwarz]

As soon as one of the dimensions of an array is not a constant, we should consider the entire thing a VLA and turn it into an alloca.

So all of these should be considered VLAs:

int a[2][2][n];
int b[2][n][2];
int c[n][2][2];

The logic for this should go into isVariableSizedArray:3020 in cabs2cil.ml.
This probably entails changing the places where a VLA is accessed as well as the trick with
a[e] == *(a+e) no longer works if we flatten multi-dimensional VLAs.

[michael-schwarz]

After some discussion with Helmut we have come to the decision that is probably nicer to

• stop turning VLAs into calls to alloca
• allow arrays to have a non-constant size in the CIL representation and
• see if this requires any changes in Goblint

I hope it should not be too much work, I'll get started on this

[michael-schwarz]

Works for good-natured cases in 11e6aa0.

Things that are still TODO:

• Handling of multidimensional VLA in which more than one of the sizes comes from an expression with side-effects:
  This works so far int x[call()][m];, this int x[call()][call()]; and this int x[m][call()]; does not
• Look into what happens with array-typed arguments of functions
• Necessary changes in Goblint to adapt to this
• Cleanup

[michael-schwarz]

The changes to Goblint are in https://github.com/goblint/analyzer/tree/allow_vla_in_cil_result

So far it works for VLAs that are used as local variables, but still crashes for functions that take VLA as an argument.