GenC: Not enough checks for forbidding returning arrays

[mario-bucev]

One can "hide" arrays through class hierarchy/ADTs, as in the following snippet:

import stainless._
import stainless.lang._
import stainless.io._
import stainless.annotation._

object GenCReturnArray {

  @cCode.noMangling
  sealed trait OptionArray

  @cCode.noMangling
  case class SomeArray(arr: Array[Byte]) extends OptionArray

  @cCode.noMangling
  case class NoneArray() extends OptionArray

  @cCode.noMangling
  def test(): OptionArray =
    SomeArray(Array.fill(10)('A'))


  @cCode.`export`
  def main() = {
    implicit val state = newState
    val oa = test()
    oa match {
      case SomeArray(arr) =>
        val x = arr(0)
        StdOut.println(x)
      case NoneArray() => ()
    }
    0
  }

}

We must extend our check to the whole class hierchy, GenC emits incorrect code:

typedef struct {
  int8_t* data;
  int32_t length;
} array_int8;

typedef struct {
  array_int8 arr;
} SomeArray;

typedef struct {
  int8_t extra;
} NoneArray;

typedef union {
  SomeArray SomeArray_v;
  NoneArray NoneArray_v;
} union_OptionArray;

typedef struct {
  enum_OptionArray tag;
  union_OptionArray value;
} OptionArray;

int32_t main(void) {
    OptionArray oa = test();
    if (oa.tag == tag_SomeArray) {
        int8_t x = oa.value.SomeArray_v.arr.data[0];
        printf("%d\n", x);
    }
    return 0;
}
OptionArray test(void) {
    int8_t stainless_buffer_0[10] = { 65, 65, 65, 65, 65, 65, 65, 65, 65, 65 };
    array_int8 arr = (array_int8) { .data = stainless_buffer_0, .length = 10 };
    return (OptionArray) { .tag = tag_SomeArray, .value = (union_OptionArray) { .SomeArray_v = (SomeArray) { .arr = arr } } };
}

The test function returns a pointer to local array, which is UB (running through Valgrind confirms an invalid read).