Fix for stack overflow problems due large output from Z3.

[wintersteiger]

These changes turn read_out in ask_process into 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 _ in read_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!

[msprotz]

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!

[msprotz]

I should also mention that several of us have had inexplicable segfaults (@nswamy, @ad-l) and this may be just the culprit. Thanks for a great fix!

[wintersteiger]

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.

[msprotz]

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...

[wintersteiger]

@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 read_out doesn't use any stack space that it could run out of anymore.