[CN] stack overflow in lexer on array of size -1u

[peterohanley]

There is obvious similarity to #777 but this looks like a totally different cause.

int b[-1u];

cn verify pre.c
cn: internal error, uncaught exception:
    Stack overflow
    Raised at Stdlib__Hashtbl.find in file "hashtbl.ml", line 539, characters 13-28
    Called from C_lexer.__ocaml_lex_initial_rec in file "parsers/c/c_lexer.mll", line 601, characters 8-31

% cn --version
git-6791a6c6b-dirty [2024-12-19 17:41:16 -0500]

[dc-mak]

I'm not getting that exact message (I'm using OCaml version 5.2.0) but I am getting a stack overflow:

Backtrace

19:27 ➜  cerberus git:(6791a6c6b) lldb-15 -- cn verify tmp.c
Traceback (most recent call last):
  File "<string>", line 1, in <module>
ModuleNotFoundError: No module named 'lldb.embedded_interpreter'
(lldb) target create "cn"
Current executable set to '/home/dhruv/.opam/5.2.0/bin/cn' (x86_64).
(lldb) settings set -- target.run-args  "verify" "tmp.c"
(lldb) breakpoint set -n camlLem_list.replicate_716
Breakpoint 1: where = cn`camlLem_list.replicate_716, address = 0x0000000001618540
(lldb) run
Process 2963 launched: '/home/dhruv/.opam/5.2.0/bin/cn' (x86_64)
Process 2963 stopped and restarted: thread 1 received signal: SIGCHLD
Process 2963 stopped
* thread #1, name = 'cn', stop reason = breakpoint 1.1
    frame #0: 0x0000555556b6c540 cn`camlLem_list.replicate_716
cn`camlLem_list.replicate_716:
->  0x555556b6c540 <+0>:  leaq   -0x148(%rsp), %r10
    0x555556b6c548 <+8>:  cmpq   0x28(%r14), %r10
    0x555556b6c54c <+12>: jb     0x555556b6c5ab            ; <+107>
    0x555556b6c54e <+14>: subq   $0x8, %rsp
(lldb) bt
* thread #1, name = 'cn', stop reason = breakpoint 1.1
  * frame #0: 0x0000555556b6c540 cn`camlLem_list.replicate_716
    frame #1: 0x00005555564601ca cn`camlCerb_frontend__Cabs_to_ail_aux.mk_zeroInit_aux_1862 at cabs_to_ail_aux.ml:127:34
    frame #2: 0x000055555646046e cn`camlCerb_frontend__Cabs_to_ail_aux.mk_zeroInit_1906 at cabs_to_ail_aux.ml:161:17
    frame #3: 0x0000555556472806 cn`camlCerb_frontend__Cabs_to_ail_effect.fun_7430 at cabs_to_ail_effect.ml:2709:51
    frame #4: 0x0000555555f81808 cn`caml_apply2 + 56
    frame #5: 0x00005555563b691f cn`camlCerb_frontend__State_exception.fun_1115 at state_exception.ml:19:24
    frame #6: 0x00005555563b691f cn`camlCerb_frontend__State_exception.fun_1115 at state_exception.ml:19:24
    frame #7: 0x00005555563b691f cn`camlCerb_frontend__State_exception.fun_1115 at state_exception.ml:19:24
    frame #8: 0x00005555563b691f cn`camlCerb_frontend__State_exception.fun_1115 at state_exception.ml:19:24
    frame #9: 0x00005555563b737c cn`camlCerb_frontend__State_exception.fun_1286 at state_exception.ml:94:94
    frame #10: 0x000055555616a0e9 cn`camlCerb_backend__Pipeline.desugar_1715 at pipeline.ml:191:4
    frame #11: 0x000055555616aca3 cn`camlCerb_backend__Pipeline.fun_5560 at pipeline.ml:233:2
    frame #12: 0x000055555616ae72 cn`camlCerb_backend__Pipeline.c_frontend_and_elaboration_inner_5575 at pipeline.ml:238:2
    frame #13: 0x0000555555f81e8e cn`camlDune__exe__Main.fun_6077 at main.ml:77:4
    frame #14: 0x0000555555f824da cn`camlDune__exe__Main.with_well_formedness_check_2678 at main.ml:144:6
    frame #15: 0x000055555615e9c8 cn`camlCmdliner_term.fun_658 at cmdliner_term.ml:24:19
    frame #16: 0x0000555556162f39 cn`camlCmdliner_eval.run_parser_589 at cmdliner_eval.ml:35:37
    frame #17: 0x000055555616412d cn`camlCmdliner_eval.eval_value_inner_1715 at cmdliner_eval.ml:203:14
    frame #18: 0x0000555556164910 cn`camlCmdliner_eval.eval_1466 at cmdliner_eval.ml:258:2
    frame #19: 0x0000555555f88c84 cn`camlDune__exe__Main.entry at main.ml:1181:22
    frame #20: 0x0000555555f7a0a7 cn`caml_program + 11639
    frame #21: 0x0000555556c53d54 cn`caml_start_program + 112
    frame #22: 0x0000555556c536f6 cn`caml_startup_common at startup_nat.c:132:9
    frame #23: 0x0000555556c53610 cn`caml_startup_common(argv=0x00007fffffffe4f8, pooling=<unavailable>) at startup_nat.c:88:7
    frame #24: 0x0000555556c5376f cn`caml_main [inlined] caml_startup_exn(argv=<unavailable>) at startup_nat.c:139:10
    frame #25: 0x0000555556c53768 cn`caml_main at startup_nat.c:144:15
    frame #26: 0x0000555556c53768 cn`caml_main(argv=<unavailable>) at startup_nat.c:151:3
    frame #27: 0x0000555555f77232 cn`main(argc=<unavailable>, argv=<unavailable>) at main.c:37:3
    frame #28: 0x00007ffff7c42d90 libc.so.6`__libc_start_call_main(main=(cn`main at main.c:31:1), argc=3, argv=0x00007fffffffe4f8) at libc_start_call_main.h:58:16
    frame #29: 0x00007ffff7c42e40 libc.so.6`__libc_start_main_impl(main=(cn`main at main.c:31:1), argc=3, argv=0x00007fffffffe4f8, init=<unavailable>, fini=<unavailable>, rtld_fini=<unavailable>, stack_end=0x00007fffffffe4e8) at libc-start.c:392:3
    frame #30: 0x0000555555f77265 cn`_start + 37
(lldb)

The issue is here

cerberus/frontend/model/cabs_to_ail_aux.lem

Line 124 in 0766055

List.replicate (natFromInteger n) (mk_zeroInit_aux tagDefs elem_ty)

Basically, the array is too large (negative unsigned integer wraps around) and the way Cerberus works is by allocating an element for each index (because initialisers can be complicated and nested in general) and them some other code in OCaml stack overflows when trying to construct a list the large.

@kmemarian thoughts on how to limit this?