Multi-return-value assignment is translated wrong when mutable local variables are involved

[RalfJung]

This code

func DecodeMapU64ToU64(enc_in []byte) (map[uint64]uint64, []byte) {
	var enc = enc_in
	kvs := make(map[uint64]uint64, 0)
	numEntries, enc := marshal.ReadInt(enc)

gets translated to

  WP let: "enc" := ref_to (slice.T byteT) enc_sl in
     let: "kvs" := NewMap (slice.T byteT) #() in
     let: "__p" := marshal.ReadInt ![slice.T byteT] (Var "enc") in
     let: "numEntries" := Fst (Var "__p") in
     let: "enc" := Snd (Var "__p") in

Note how it creates a new binding for enc when it really should store to the existing enc instead.

[tchajed]

I didn't intend to support this, so it should probably be rejected for now. It's a bit unfortunate since this is idiomatic Go and the alternative won't be as easy to read.

[sanjit-bhat]

Ran into this as well. Came up with the following slightly reduced examples:

func oneRet(b []byte) []byte {
    return b
}

func twoRet(b []byte) (uint64, []byte) {
    return 0, b
}

func badGoose() []byte {
    var b = make([]byte, 0)
    // Goose isn't doing a ptr store for the second arg.
    a, b := twoRet(b)
    var a2 = a
    a2 += 1
    return b
}

func goodGoose1() []byte {
    var b = make([]byte, 0)
    // It stores when one of the lvals is anonymous.
    _, b = twoRet(b)
    return b
}

func goodGoose2() []byte {
    var b = make([]byte, 0)
    // It stores when the func only rets one var.
    b = oneRet(b)
    return b
}

get translated into

Definition oneRet: val :=
  rec: "oneRet" "b" :=
    "b".

Definition twoRet: val :=
  rec: "twoRet" "b" :=
    (#0, "b").

Definition badGoose: val :=
  rec: "badGoose" <> :=
    let: "b" := ref_to (slice.T byteT) (NewSlice byteT #0) in
    let: ("a", "b") := twoRet (![slice.T byteT] "b") in
    let: "a2" := ref_to uint64T "a" in
    "a2" <-[uint64T] ((![uint64T] "a2") + #1);;
    ![slice.T byteT] "b".

Definition goodGoose1: val :=
  rec: "goodGoose1" <> :=
    let: "b" := ref_to (slice.T byteT) (NewSlice byteT #0) in
    let: ("0_ret", "1_ret") := twoRet (![slice.T byteT] "b") in
    "0_ret";;
    "b" <-[slice.T byteT] "1_ret";;
    ![slice.T byteT] "b".

Definition goodGoose2: val :=
  rec: "goodGoose2" <> :=
    let: "b" := ref_to (slice.T byteT) (NewSlice byteT #0) in
    "b" <-[slice.T byteT] (oneRet (![slice.T byteT] "b"));;
    ![slice.T byteT] "b".