CakeML/cakeml

Make chars_to_nums tail-recursive?

Offen

#1.392 geöffnet am 18.05.2026

 (1 Kommentar) (0 Reaktionen) (0 zugewiesene Personen)Standard ML (98 Forks)auto 404
dev experiencegood first issuehelp wanted

Repository-Metriken

Stars
 (1.169 Sterne)
PR-Merge-Metriken
 (PR-Metriken ausstehend)

Beschreibung

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.

Contributor Guide