Incorrect transformation of inner functions mutating a local variable

[mario-bucev]

The following snippet:

object InnerFunctionVarMutation {

  def outer = {
    var i: BigInt = 0

    def inner1: BigInt = {
      val x = inner2
      x
    }

    def inner2: BigInt = {
      i += 1
      i
    }

    val x = inner1
    assert(i == 1)
  }
}

generates a "choose satisfiability" VC that is always invalid (choose of false). If we look at the trees after ImperativeCodeElimination, we have more insights:

def outer$25: Unit = {
  val i$32 = 0

  def inner1: BigInt = { // should take an `i` and return it alongside the result
    val x$30: BigInt = inner2 // `x$30` is a tuple, not a `BigInt`
    x$30
  }

  def inner2(i$33: BigInt): (BigInt, BigInt) = {
    val i$35 = i$33
    val i$36 = i$35 + 1
    (i$36, i$36)
  }
  val x$29 = inner1
  assert(i$32 == 1)
}

inner1 is lacking a transformation: we need to "thread" i (by taking it in parameter and returning it) and adapt the call to inner2 in consequence.

Note that swapping the order of inner1 and inner2 results in correct transformation, I think this is due to ImperativeCodeElimination not properly supporting LetRec (as written in this comment)