Original bug ID: 7118
Reporter: bartjacobs
Assigned to: @gasche
Status: resolved (set by @gasche on 2016-03-08T13:36:16Z)
Resolution: fixed
Priority: normal
Severity: major
Version: 4.02.1
Target version: 4.03.1+dev
Fixed in version: 4.03.0+dev / +beta1
Category: back end (clambda to assembly)
Related to: #7120
Monitored by: @gasche

Bug description

It seems that Objective-C code sometimes performs a stack walk as part of its happy-path normal operation; such stack walks seem to sometimes crash on ocamlopt-generated stack frames.

Evidence for this is that my tool, VeriFast, has been crashing recently. See the attached crash report. VeriFast uses GTK through lablgtk for its GUI. On my OS X machine, I can make VeriFast 15.12 crash reliably (see below). Apparently, the sequence of events is as follows:

• VeriFast calls into lablgtk
• lablgtk calls into GTK
• GTK calls into Cocoa (AppKit)
• AppKit calls into the Objective-C runtime to add an exception handler.
• The runtime wants to find the innermost enclosing stack frame that handles Objective-C exceptions. It uses Apple's libunwind implementation to walk the stack to find such a frame.
• libunwind crashes while advancing the stack walking cursor.

I haven't been able to verify yet that the stack frame that libunwind crashes on is an ocamlopt-generated stack frame (I don't have debug symbols for libunwind and interpreting the machine state manually is a bit daunting), but that seems likely, given that ocamlopt-generated code generates unusually-shaped stack frames.

Note: initially, I though the problem manifested only when calling ocamlopt without the -g option, but recently, I'm seeing the crashing even with VeriFast 15.12, which is built with the -g option.

Unfortunately, it does not seem to be the case that libunwind always crashes on ocamlopt-generated stack frames. Apparently, it only does sometimes. For example, if I run VeriFast IDE inside a debugger (lldb), I don't get crashes. (I can only investigate the problem by generating a core dump.)

Assuming that it is indeed the case that libunwind crashes on ocamlopt-generated stack frames, there seem to be a number of possible solutions:

• Modify ocamlopt so that it generates stack frames that libunwind doesn't crash on
• Modify ocamlopt so that on OS X it generates stack walking backstops when calling into external functions.
• Modify libunwind so that it doesn't crash.
• Modify lablgtk so that it generates stack walking backstops.
• Modify GTK so that it generates stack walking backstops when calling into Cocoa.
• Modify the Objective-C runtime so that it doesn't walk the stack when adding an exception handler.
• Modify the Objective-C compiler so that it generates a stack walking backstop when C code calls Objective-C code.

Steps to reproduce

(This works on my machine reliably, but it seems rather brittle so it might not work on your machine.)

1. Download VeriFast 15.12 for OS X from http://www.cs.kuleuven.be/~bartj/
2. Unzip the tarball.
3. Run 'bin/vfide examples/termination/ackermann.c'
4. Issue the Verify command, either by clicking the Play toolbar button, pressing F5, or choosing the Verify menu item.
   VeriFast crashes after verification finishes, when it tries to scroll to the error location.

Additional information

I have also filed the following bugs:

• lablgtk bug 1518 (https://forge.ocamlcore.org/tracker/index.php?func=detail&aid=1518&group_id=220&atid=1032)
• GTK bug 759278 (https://bugzilla.gnome.org/show_bug.cgi?id=759278)
• Apple bug 24076902 (https://bugreport.apple.com/problem/viewproblem)

File attachments

• vfide-core_2016-01-05-192723_Bart-Jacobss-MacBook-Pro.crash