list_length does not work

[ImagineHaxing]

I am following the book "Introduction to Programming in ATS" and I am trying to compile the following code

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

datatype list(a:t@ype+, int) =
  | list_nil (a,0) of ()
  | {n:nat} list_cons (a, n+1) of (a, list(a, n))
 
fun {a:t@ype}
list_length {n:nat} .<n>. (xs: list(a,n)): int n =
  case+ xs of
    | list_nil () => 0
    | list_cons (_, xs1) => 1 + list_length(xs1)
  
val list_test = list_cons("hello", list_cons("world", list_nil()))
val () = print(list_length(list_test))
   
implement main0() = ()

with this command line

patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -O2 -o main main.dats -latslib && ./main

and it is printing out "1" instead of "2". What am I doing wrong here?

[Hongwei Xi]

Thanks for reporting it.

It is a very interesting bug! But is it a bug in ATS2 or a big in GCC?

If you change -O2 to -O0, you should get 2 (instead of 1). Looks like GCC doing something "fishy" here with -O2?

BTW, if you do

val () = print(list_length<string>(list_test))

you should get 2 as well. Template argument needs to be supplied in this case.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/ats-lang-users/1edd4fef-4d7f-4732-8b33-14ecd923debfn%40googlegroups.com.

[Hongwei Xi]

BTW, here is what I got:

patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -O0 -o main main.dats -latslib && ./main

mylist_length: xs = ...
mylist_length: xs = ...
mylist_length: xs = ...
2hwxi@zoe:/tmp$ patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -O2 -o main main.dats -latslib && ./main
mylist_length: xs = ...
mylist_length: xs = ...

Why '-O0' and '-O2' yield different results? I really don't have time to look at the assembly output right now.

[ImagineHaxing]

I've done some research and Claude said that -O2 enables strict aliasing which means that trying to access memory location with a pointer of a type other than that of the location results in UB. So I think the issue is that when the type is not specified to be string the template infers it to be something else that causes the UB.
Btw, with -O2 is shows as 1 no matter the length of the list (I tried with 3 and 4, I didn't test with it being empty)

[ImagineHaxing]

I've tried to compile the initial code but also add -fno-strict-aliasing next to -O2 ("patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -I${PATSHOME} -I${PATSHOME}/ccomp/runtime -O2 -fno-strict-aliasing -o main main.dats -latslib && ./main") and it printed "2".