invoke a debugger instead of going via addr2line and friends

MichaelRawson commented 1 month ago

In #412 I (perhaps foolishly, in hindsight) removed the CALL mechanism with some code that found stack frames, then asked the system to resolve them to function names. This had a lot of benefits, but it was a bit flaky and had to be improved in #504 so that we shell out to addr2line.

This worked, but in itself was also flaky in the presence of ASLR, which is becoming harder to avoid. On ARM Macs, for example, it seems you can't switch it off easily.

So: since we already shell out to a program, why not use something designed for this? Replace the whole mess with invocations of gdb or lldb in their batch modes to get a backtrace. This should (hopefully) be the last attempt in this sorry saga.

Things still to check:

Does this work for @quickbeam123 , the perennial tricky customer?
Does it work on StarExec? (possibly of reduced importance given StarExec's impending decommissioning)
Does it interact well with #577?

MichaelRawson commented 1 month ago

No dice on StarExec. Not sure if we care.

quickbeam123 commented 1 month ago

Will try to investigate a bit more, but currently, this kills my terminal with terminal.txt

MichaelRawson commented 1 month ago

...your actual terminal emulator dies, right? I have no idea what to do about that, sorry. If you redirect output to a file does it perhaps not crash the terminal?

vprover / vampire

invoke a debugger instead of going via addr2line and friends #579