Polymorphic function segfaults with optimization less than -O2

[jrfondren]

Of a file named myvect.dats:

#include "share/atspre_staload.hats"

datatype MyVect(a:t@ype, int) =
    | Empty(a, 0)
    | {n:nat} Cons(a, n) of (a, MyVect(a, n-1))

extern prfun lemma_myvect_rest{a:t@ype}{n:int}(rest: MyVect(a, n)): [n >= 0] void

fun lengthMyVect{a:t@ype}{n:nat}(list: MyVect(a, n)): int(n) =
    case+ list of
    | Empty() => 0
    | Cons(_, rest) => 1 + lengthMyVect(rest) where {
            prval () = lemma_myvect_rest(rest)
    }

val+ 3 = lengthMyVect(Cons{..}{3}(1, Cons(2, Cons(3, Empty()))))

implement main0() = ()

I get these results:

$ patscc
ATS/Postiats version 0.3.12 with Copyright (c) 2011-2018 Hongwei Xi
$ patscc -DATS_MEMALLOC_LIBC -o myvect myvect.dats
$ ./myvect
Segmentation fault
$ patscc -O1 -DATS_MEMALLOC_LIBC -o myvect myvect.dats
$ ./myvect
Segmentation fault
$ patscc -O2 -DATS_MEMALLOC_LIBC -o myvect myvect.dats
$ ./myvect
$

This is also the case with -DATS_MEMALLOC_GCBDW and -lgc.

[githwxi]

This is due to the size of 'a' being unknown (t@ype). There is not an easy way for me to fix it at this point. Please turn the length function into a function template: fun{a:t@ype} lengthMyVect{n:nat}(list: MyVect(a, n)): int(n) =

…

On Wed, Sep 26, 2018 at 12:57 AM jrfondren ***@***.***> wrote: Of a file named myvect.dats: #include "share/atspre_staload.hats" datatype ***@***.***, int) = | Empty(a, 0) | {n:nat} Cons(a, n) of (a, MyVect(a, n-1)) extern prfun ***@***.***}{n:int}(rest: MyVect(a, n)): [n >= 0] void fun ***@***.***}{n:nat}(list: MyVect(a, n)): int(n) = case+ list of | Empty() => 0 | Cons(_, rest) => 1 + lengthMyVect(rest) where { prval () = lemma_myvect_rest(rest) } val+ 3 = lengthMyVect(Cons{..}{3}(1, Cons(2, Cons(3, Empty())))) implement main0() = () I get these results: $ patscc ATS/Postiats version 0.3.12 with Copyright (c) 2011-2018 Hongwei Xi $ patscc -DATS_MEMALLOC_LIBC -o myvect myvect.dats $ ./myvect Segmentation fault $ patscc -O1 -DATS_MEMALLOC_LIBC -o myvect myvect.dats $ ./myvect Segmentation fault $ patscc -O2 -DATS_MEMALLOC_LIBC -o myvect myvect.dats $ ./myvect $ This is also the case with -DATS_MEMALLOC_GCBDW and -lgc. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#216>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAl811o-4PAxk2hnsH1TE2BpfEdTVJ9Qks5uewkqgaJpZM4W55sX> .