GenC: replacing a VLA field should be forbidden

[mario-bucev]

We should perform such checks because the following snippet results in a C code exhibiting UB:

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

object GenCArrayFieldReplaceVLA {

  @cCode.noMangling
  case class Buffer(var array: Array[Int], extra: Int) // `array` is a VLA

  @cCode.noMangling
  def replace(b: Buffer): Unit = {
    b.array = Array.fill(20)(444)
  }


  @cCode.`export`
  def main(): Int = {
    implicit val state = stainless.io.newState
    val b = Buffer(Array.fill(10)(1), 42)
    replace(b)
    assert(b.array(14) == 444) // Valid VC
    StdOut.println(b.array(14))
    0
  }

}

This gets translated to:

typedef struct {
  int32_t* data;
  int32_t length;
} array_int32;

typedef struct {
  array_int32 array;
  int32_t extra;
} Buffer;

int32_t main(void) {
    int32_t stainless_buffer[10] = { 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 };
    array_int32 norm = (array_int32) { .data = stainless_buffer, .length = 10 };
    Buffer b = (Buffer) { .array = norm, .extra = 42 };
    replace(&b);
    printf("%d\n", b.array.data[14]);
    return 0;
}

static void replace(Buffer* b) {
    int32_t stainless_buffer[20] = { 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444, 444 };
    array_int32 norm = (array_int32) { .data = stainless_buffer, .length = 20 };
    b->array = norm; // refers to a local array that will go out of scope!
}

Running Valgrind on the compiled code yields an "invalid read".

Note: though this issue looks similar to https://github.com/epfl-lara/stainless/issues/1287, these issues are different. Here, we must forbid replacing a VLA array field because the lifetime of the local array ends when the function returns. In the other issue, we do not have this problem because Buffer has a fixed-size array field (and not a pointer). These issues may both be resolved by forbidding any array replacement, though for #1287 it may be a bit too restrictive.

[mario-bucev]

Somewhat related:

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

object VLAUpdate {
  @cCode.`export`
  def main(): Int = {
    implicit val state = stainless.io.newState

    val cond = true
    val arrr = Array.fill(3)(Array.fill(5)(123))

    if (cond) {
      arrr(0) = Array.fill(10)(1)
    }

    StdOut.println(arrr(0)(9))
    0
  }

}

The VLA declared in the if statement does not live long enough, as its lifetime is bound to the scope of the if:

typedef struct {
  int32_t* data;
  int32_t length;
} array_int32;

typedef struct {
  array_int32* data;
  int32_t length;
} array_array_int32;

int32_t main(void) {
    bool cond = true;
    
    int32_t stainless_buffer_0[5] = { 123, 123, 123, 123, 123 };
    array_int32 norm_0 = (array_int32) { .data = stainless_buffer_0, .length = 5 };
    int32_t stainless_buffer_1[5] = { 123, 123, 123, 123, 123 };
    array_int32 norm_1 = (array_int32) { .data = stainless_buffer_1, .length = 5 };
    int32_t stainless_buffer_2[5] = { 123, 123, 123, 123, 123 };
    array_int32 norm_2 = (array_int32) { .data = stainless_buffer_2, .length = 5 };
    
    array_int32 stainless_buffer_3[3] = { norm_0, norm_1, norm_2 };
    array_array_int32 arrr = (array_array_int32) { .data = stainless_buffer_3, .length = 3 };
    
    if (cond) {
        int32_t stainless_buffer_4[10] = { 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 };
        array_int32 norm = (array_int32) { .data = stainless_buffer_4, .length = 10 };
        arrr.data[0] = norm;
    } // arrr.data[0] invalidated
    
    printf("%d\n", arrr.data[0].data[9]);
    return 0;
}