Issue with inference and open, causes segmentation fault

[TimWhiting]

I keep getting segmentation faults when I start using a bunch of handlers, or once my program gets big enough. Usually I try to understand what is happening, and work around it, but this one is a particularly problematic one. The stack only has 98 frames, so it's not hitting a stack limit I think. (I've tried with ulimit -s unlimited as well). I've tried with both mimalloc and the standard allocator, and end up with the same issue.

 0x000055555556cad0 in mi_heap_malloc_small_zero (heap=0x200000a0150, size=24, zero=<optimized out>) at /home/tim/koka/kklib/src/../mimalloc/src/alloc.c:116
#2  0x000055555556cbaf in mi_heap_malloc_small (heap=<optimized out>, size=size@entry=24) at /home/tim/koka/kklib/src/../mimalloc/src/alloc.c:134
#3  0x000055555557f745 in kk_malloc_small (ctx=0x20000040390, sz=24) at /home/tim/koka/kklib/include/kklib.h:495
#4  kk_block_alloc (ctx=0x20000040390, tag=KK_TAG_FUNCTION, scan_fsize=2, size=24) at /home/tim/koka/kklib/include/kklib.h:617
#5  new_std_fs_core_fs_hnd_lambda_kk__std__core__hnd____ev (fnPtr=fnPtr@entry=0x555555582de0 <kk_std_core_hnd_clause_tail0_fun11376>, field_1=..., field_1@entry=..., _ctx=_ctx@entry=0x20000061620)
    at .koka/v2.4.2/gcc-debug/std_core_hnd.h:1359
#6  0x0000555555582ff0 in kk_std_core_hnd_new_clause_tail0_fun11376 (_ctx=0x20000061620, ev=...) at .koka/v2.4.2/gcc-debug/std_core_hnd.c:2487
#7  kk_std_core_hnd_clause_tail0_fun11373 (_fself=..., ___wildcard__562__14=..., ev=..., _ctx=0x20000061620) at .koka/v2.4.2/gcc-debug/std_core_hnd.c:2549
#8  0x0000555555598992 in kk_std_core_error_pattern (location=..., location@entry=..., definition=definition@entry=..., _ctx=_ctx@entry=0x20000010140) at .koka/v2.4.2/gcc-debug/std_core.c:5674
#9  0x00005555555e2654 in kk_analysis_adi_cache_evcache_fun10620 (_fself=..., e=..., _ctx=0x20000010140) at .koka/v2.4.2/gcc-debug/analysis_adi_cache.c:2496

Crucially, you'll notice that _ctx changes between kk_std_core_error_pattern and kk_std_core_hnd_claus_tail0 which I assumed would never happen.

Additionally the exception handler should have a clause with 1 parameter, not 0, which is probably why the ctx address is wrong as well.

So, my conclusion is that there is something wrong with the evidence vector or the lookup into the evidence vector here.

[TimWhiting]

I found the place where I was doing an incomplete pattern match and fixed it which resolved the issue.

This doesn't exhibit the same error, but is like the code that caused this error, and also behaves strangely:

effect change<v>
  ctl change(v:v): maybe<v>

type greet
  Hi
  Bye

fun show(g: greet): string
  match g
    Hi -> "Hi"
    Bye -> "Bye"

fun test()
  match change(1)
    Just(v) | v % 2 == 1 -> Hi
    Nothing -> Bye

fun main()
  with handler
    ctl change(v)
      resume(Just(v))
      resume(Just(v + 1))
  test().show.println

Which outputs

Hi
Bye
Hi

It should only output

Hi
** Some sort of match exception

[TimWhiting]

Stepping through the C code using gdb, it never hits the kk_yield_final code, or the default exception handler code at all, instead it returns from test through unboxing the dummy box that get's returned from the exception call. This does print something in this case due to the fact that the match in the greet show just checks g against the Hi constructor, and if it is not, then assumes that it is the Bye constructor. I believe it is calling the wrong handler, which suggests the evidence vector is not being adjusted propertly.

[TimWhiting]

Adding an explicit match and exception throwing, causes exn to be inferred, which then allows for opening the evidence vector to the right spot, which is not happening for the incomplete pattern match code.

// monadic lift
 fun .mlift397-test : (.y.386 : maybe<int>) -> (change<int>) greet
  = fn<(change<int>)>(.y.386: maybe<int>){
    match (.y.386) {
      ((std/core/types/Just((v0: int)) : maybe<int> ) as .pat: (maybe<int>))
         | std/core/(==.1)((std/core/(%)(v0, 2)), 1) -> scratch/testbroken/Hi;
      ((std/core/types/Nothing() : maybe<int> ) as .pat0: (maybe<int>))
         -> scratch/testbroken/Bye;
      (.pat1: (maybe<int>))
         -> std/core/error-pattern("../koka_code/scratch/testbroken.kk(14, 3)", "test");
    };
  };

// monadic lift
 fun .mlift416-test : (.y.400 : maybe<int>) -> <change<int>,exn> greet
  = fn<<change<int>,exn>>(.y.400: maybe<int>){
    match (.y.400) {
      ((std/core/types/Just((v0: int)) : maybe<int> ) as .pat: (maybe<int>))
         | std/core/(==.1)((std/core/(%)(v0, 2)), 1) -> scratch/testbroken/Hi;
      ((std/core/types/Just((.pat1: int)) : maybe<int> ) as .pat0: (maybe<int>))
         -> std/core/hnd/.open-at2((std/core/ssize_t(1)), std/core/throw, "Error", std/core/types/None);
      ((.skip std/core/types/Nothing() : maybe<int> ) as .pat2: (maybe<int>))
         -> scratch/testbroken/Bye;
    };
  };

Additionally it seems like the type issue is only present in the code that has been monadically lifted, and separating the match expression to match on a variable that stores the value of the effect call has the correct type, but they are all missing open-at to correctly adjust the effect vector..

[TimWhiting]

Related #271