CakeML/cakeml

Make chars_to_nums tail-recursive?

開放

#1,392 建立於 2026年5月18日

 (1 則留言) (0 個反應) (0 位負責人)Standard ML (98 個分叉)auto 404
dev experiencegood first issuehelp wanted

倉庫指標

星標
 (1,169 顆星)
PR 合併指標
 (PR 指標待抓取)

描述

When I tried to perf Candle using a custom version of the compiler that "simulates" the calls in CakeML by adjusting the C stack (pushing/popping two addresses), I ran into segfaults:

warning: failed to parse execution context from corefile: Cannot access memory at address 0x7ffede486ff0
Failed to read a valid object file image from memory.
Core was generated by `./cake --candle'.
Program terminated with signal SIGSEGV, Segmentation fault.
#0  0x00005618030e23f8 in cml_decodeProg_chars_to_nums_9849 ()
#0  0x00005618030e23f8 in cml_decodeProg_chars_to_nums_9849 ()
Backtrace stopped: Cannot access memory at address 0x7ffeda487000
rsp            0x7ffeda487000      0x7ffeda487000
rbp            0x7ffeda487000      0x7ffeda487000
rip            0x5618030e23f8      0x5618030e23f8 <cml_decodeProg_chars_to_nums_9849+38>

Note that this happens on startup and also happens with --repl.

Claude suggests that this is because chars_to_nums is not tail-recursive (which it isn't):

Definition chars_to_nums_def:
  chars_to_nums ns =
    if NULL ns then [] else
      let (k,ks) = dec_next 0 1 ns in
        k :: chars_to_nums ks

The "fix" was to bump up my ulimit -s to something larger. Claude suggests that it needs to be ~80MB with the current definition.

貢獻者指南