CakeML/cakeml

Make chars_to_nums tail-recursive?

オープン

#1,392 opened on 2026/05/18

 (1 件のコメント) (0 件のリアクション) (0 人の担当者)Standard ML (98 件のフォーク)auto 404
dev experiencegood first issuehelp wanted

Repository metrics

Stars
 (1,169 個のスター)
PR merge metrics
 (PR metrics pending)

説明

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.

コントリビューターガイド