Fix for stack overflow problems due large output from Z3.#870
Conversation
|
No way to fix this better until proper stack overflow detection for win64 lands in OCaml -- see ocaml/ocaml#938 (comment) Thanks for the detective work! |
|
No worries, happy I figured out what was going on :-) I saw all of this on Ubuntu though (proper VM, not WSL). Is the stack overflow detection broken on all platforms? I did get proper exception messages when I ran it synchronously, without the child thread though. |
|
My recollections are that stack overflow exceptions are guaranteed to be caught when they occur in OCaml code (modulo the win64 issue), but not when they occur while C code is running on the stack... |
|
@msprotz I see, exceptions in C/C++ are definitely tricky to handle! I submitted a short bug repro to the OCaml bug-tracker yesterday, to get their opinion. They acknowledged it as a real bug and are working on a fix (see Mantis and GitHub). For us, this issue is fixed as |
These changes turn
read_outinask_processinto a tail-recursion, so that OCaml doesn't run into stack overflows.I encountered this problem while dumping proofs from Z3, which sometimes are large (many lines of output). It surprised me that OCaml would run out of stack space relatively quickly, but more importantly it didn't provide any useful error messages (just "segfault (core dumped)" in non-descript thread with empty stack trace (empty even in debug mode)).
I tried catching
Failure _,Stack_overflow, and_inread_out, but none of this worked; I suppose when the stack is full, OCaml can't find room for a proper error message. I tried setting a pre-allocated Boolean to true upon "with _ -> ...", but even that segfaults before it gets there. If OCaml experts out there know how to make it provide us with a useful error message, please let me know!