Original bug ID: 4690
Reporter: herbelin
Assigned to: @xavierleroy
Status: closed (set by @xavierleroy on 2011-05-29T10:14:17Z)
Resolution: fixed
Priority: normal
Severity: crash
Version: 3.11.0+beta
Fixed in version: 3.11.1+dev
Category: ~DO NOT USE (was: OCaml general)

Bug description

On Mac OS 10.5, using the ocaml-based coq system, some calls to dynamically loaded functions result in a bus error in caml_oldify_local_roots (line 191 of roots.c, d is NULL in "if (d->retaddr == retaddr) break;").

This has been reproduced in exactly the same situation on two different installations of Mac OS 10.5 but the problem, even on a given installation, is sensible to the execution context. For instance, changing the name of the files or directories may change the way the problem appears. I was unable to find a simple example (I guess that the program has to run for a while to set the gc in the faulty configuration).

The simplest way to certainly reproduce the problem is to export coq svn trunk revision 11773 (svn checkout -r 11773 svn://scm.gforge.inria.fr/svn/coq/trunk) with ocaml 3.11 and camlp5 5.10 installed, then "configure -local; make". Depending on the installation context, a problem appears either while compiling coq file theories/Classes/RelationClasses.v or theories/Logic/ChoiceFacts.v or theories/ZArith/Zdiv.v, ... (see also http://logical.saclay.inria.fr/coq-bugs/show_bug.cgi?id=2024). My own installation is 10.5.6 and Xcode Tools 3.2.1 on Core 2 Duo. Statistically, the compilation of the coq system is large enough to trigger the problem at least once (I no nobody who has succeeded to compile the recent modularisation of coq using dynamic loading on Mac OS 10.5 in full yet). No problem at all has been encountered on Mac OS 10.4.

The trace before crashing is the following:

Program received signal EXC_BAD_ACCESS, Could not access memory.
Reason: KERN_PROTECTION_FAILURE at address: 0x00000000
caml_oldify_local_roots () at roots.c:191
191 if (d->retaddr == retaddr) break;
(gdb) bt full
#0 caml_oldify_local_roots () at roots.c:191
sp = 0xbfffe7f0 "\\005j"
retaddr = 18865600
regs = (value *) 0xbfffe7d0
d = (frame_descr *) 0x0
h = 261048
i = 283
j = <value temporarily unavailable, due to optimizations>
n = 0
ofs = <value temporarily unavailable, due to optimizations>
p = <value temporarily unavailable, due to optimizations>
glob = <value temporarily unavailable, due to optimizations>
root = <value temporarily unavailable, due to optimizations>
lr = <value temporarily unavailable, due to optimizations>
lnk = (link *) 0x0
#1 0x00306234 in caml_empty_minor_heap () at minor_gc.c:229
r = <value temporarily unavailable, due to optimizations>
#2 0x00306385 in caml_minor_collection () at minor_gc.c:272
prev_alloc_words = 0
#3 0x003041ad in caml_garbage_collection () at signals_asm.c:68
No locals.
#4 0x00313aeb in caml_call_gc ()
No symbol table info available.
Cannot access memory at address 0x5

File attachments

• ocaml-3.11.0-macosx-dynlink.patch