stainless icon indicating copy to clipboard operation
stainless copied to clipboard

GenC: incorrect use of copy instead of reference when binding values (with `if` expressions)

Open mario-bucev opened this issue 2 years ago • 0 comments

Similar to https://github.com/epfl-lara/stainless/issues/1284, the following snippet is incorrectly translated:

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

object GenCRefCopy2 {

  @cCode.noMangling
  case class Ref(var x: Int, var y: Int)

  @cCode.`export`
  def main(): Int = {
    implicit val state = stainless.io.newState
    val cond = false
    val r1 = Ref(1, 2)
    val r2 = if (cond) Ref(12, 34) else r1 // Note: if we don't use ifs, r2 gets correctly translated to a reference to r1
    r2.x = 10
    assert(r1.x == 10) // Valid VC
    StdOut.println(r1.x) // Transpiled code prints 1 instead of 10
    0
  }

}

Generated (cleaned) code:

typedef struct {
  int32_t x;
  int32_t y;
} Ref;

int32_t main(void) {
    bool cond = false;
    Ref r1 = (Ref) { .x = 1, .y = 2 };
    Ref norm;
    if (cond) {
        norm = (Ref) { .x = 12, .y = 34 }; // Ok
    } else {
        norm = r1; // Copy instead of a reference!
    }
    Ref* r2 = &norm;
    r2->x = 10;
    printf("%d\n", r1.x);
    return 0;
}

mario-bucev avatar Jun 07 '22 14:06 mario-bucev