Problem with short circuiting

[athas]

Consider this program:

def main k =
  let src = iota k
  let dst = iota 5
  in dst with [1:4] = src

Short-circuiting will put the array src in the same memory as dst, but before constructing dst. This means that the construction of dst will overwrite src.

Worse, if k is too large, we will write out-of-bounds, as short-circuiting does not ensure that the bounds check is done before src is constructed.

This is a pretty bad bug that can result in anything from invalid results to memory corruption.

[athas]

Regarding the overwriting, it appears we do not correctly check safety condition 3 for short-circuiting statements of form let y[i] = b^{lu}:

--      3. there is no use of the left-hand side memory block @m_y@
--           during the liveness of @b@, i.e., in between its last use
--           and its creation.

In this case the memory block m_dst is certainly used (to construct dst) during the lifetime of src.

(Incidentally, it's somewhat confusing that the comments use the let y[i] = ...-shorthand, as that's not what the IR actually does.)