JavaScript compiler and labels issue

[MikaelMayer]

The following code crashes a compiled JavaScript code.

bug_js.dfy:

method GetNext(i: int) returns (j: int, possible: bool) {
  if i == 1 {
    possible := false;
    j := 0;
  } else {
    possible := true;
    j := if i % 2 == 0 then  i / 2 else i * 3 + 1;
  }
}

method Main()
{
  var i := 100;
  var k := 27;
  while i > 0
    invariant i >= 0
  {
    label before:
    var newK, possible := GetNext(k);
    if(!possible) {
      break;
    }
    k := newK;
    print k;
    i := i - 1;
  }
}

> dafny /spillTargetCode:2 /compileTarget:js /compile:3 bug_js.dfy

Running...

[stdin]:1004
        throw e
        ^

ReferenceError: _3_possible is not defined
    at Main ([stdin]:1098:13)
    at Object.$module.HandleHaltExceptions ([stdin]:999:7)

The generated code is ill-formed, but it's not possible to see it until it's executed:

    static Main() {
      let _0_i;
      _0_i = new BigNumber(100);
      let _1_k;
      _1_k = new BigNumber(27);
      L0: {
        while ((_dafny.ZERO).isLessThan((_0_i))) {
          C0: {
            L1: {
              let _2_newK;
              let _3_possible;
              let _out0;
              let _out1;
              let _outcollector0 = _module.__default.GetNext(_1_k);
              _out0 = _outcollector0[0];
              _out1 = _outcollector0[1];
              _2_newK = _out0;
              _3_possible = _out1;
            }
            if (!(_3_possible)) { // Here _3_possible is out of scope.
              break L0;
            }
            _1_k = _2_newK;
            process.stdout.write(_dafny.toString(_1_k));
            _0_i = (_0_i).minus((_dafny.ONE));
          }
        }
      }
      return;
    }

[cpitclaudel]

Duplicate of #2576 for Javascript, but good catch re. soundness

[cpitclaudel]

I'm closing this issue to track the problem in a separate issue dedicated to soundness problems coming from unbound variables: #2691.

[MikaelMayer]

I'm reopening this issue because #2691 was tracking two issues that were independently resolved, and a third one which is this one.