Strict aliasing problem in lazy evaluation (Postiats 0.3.11 or 0.3.12)

[chemoelectric]

The following program segfaults if you change -fno-strict-aliasing to -fstrict-aliasing in the command patscc -DATS_MEMALLOC_LIBC -O2 -finline-functions -fno-strict-aliasing strict-aliasing-problem.dats && ./a.out

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

staload UN = "prelude/SATS/unsafe.sats"

fun
count_down {n : nat} (n : int n) : stream int =
  if n = 0 then
    stream_make_nil ()
  else
    $delay (stream_cons (n, (print! ("{", n, "}");
                             count_down (pred n))))

implement
main0 () =
  {
    val lst = count_down 5
    val () = print! ("(", $UN.cast {int} lst[0], ")")
    val () = print! ("(", $UN.cast {int} lst[1], ")")
    val () = print! ("(", $UN.cast {int} lst[2], ")")
    val () = print! ("(", $UN.cast {int} lst[3], ")")
    val () = print! ("(", $UN.cast {int} lst[4], ")")
    val () = print! "|"
    val lst = count_down 5
    val () = print! ("(", $UN.cast {int} lst[4], ")")
    val () = print! ("(", $UN.cast {int} lst[3], ")")
    val () = print! ("(", $UN.cast {int} lst[2], ")")
    val () = print! ("(", $UN.cast {int} lst[1], ")")
    val () = print! ("(", $UN.cast {int} lst[0], ")")
  }

[chemoelectric]

By the way, this means it will segfault with -O3.

[chemoelectric]

GCC version 7.3.0 by the way.

[githwxi]

Using gcc version 5.4.0 20160609, I did not get to see crash:

patscc -DATS_MEMALLOC_LIBC -O2 -finline-functions -fstrict-aliasing abcde.dats && ./a.out
({5}5)({4}4)({3}3)({2}2)({1}1)|({5}{4}{3}{2}{1}1)({5}{4}{3}{2}2)({5}{4}{3}3)({5}{4}4)({5}5)

Is it easy for you to tell the part of the generated C code that violates the strict aliasing rule in this example?

Thanks!