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.

贡献者指南