Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005012OCaml~DO NOT USE (was: OCaml general)public2010-03-30 17:482015-06-11 17:56
ReporterPascal Cuoq 
Assigned To 
PlatformOSOS Version
Product Version3.11.2 
Target VersionFixed in Version3.12.0+dev 
Summary0005012: Bus error in 32-bit Snow Leopard OCaml-3.11.2-native-generated program (may be caused by Dynlink)

Compile OCaml-3.11.2 as 32-bit on Snow Leopard:
./configure -cc "gcc -m32" -as "as -arch i386" -aspp "gcc -m32 -c" -prefix /usr/local/ocaml-3.11.2-32


Modify .profile so that usr/local/ocaml-3.11.2-32/bin/ocamlopt is always used (the next steps spawn shells, so just "export PATH=..." in the current shell is not enough)

Download and extract [^]
cd frama-c-Beryllium-20090902
make bin/toplevel.byte
export FRAMAC_PLUGIN=./lib/plugins/ # This env variable is used to locate plug-ins
# nothing happens. This is the expected behavior.

make bin/toplevel.opt
Bus error
# The above is the bug.

# Nothing happens (expected behavior) when no plug-in to dynamically load is found
Additional InformationDynlink works as expected on this platform with 64-bit OCaml 3.11.2.
Dynlink worked with 32-bit OCaml 3.11.1 on Leopard. Furthermore, if the compiled files were copied to Show Leopard, they continued to work.

Reproducing the same behavior under gdb gives:

export FRAMAC_PLUGIN=./lib/plugins/
gdb bin/toplevel.opt

(gdb) run
Starting program: /Users/pascal/frama-c-Beryllium-20090902/bin/toplevel.opt
Reading symbols for shared libraries +. done
Reading symbols for shared libraries . done

Program received signal EXC_BAD_ACCESS, Could not access memory.
Reason: KERN_PROTECTION_FAILURE at address: 0x00000014
0x017330c8 in camlLtl_to_acsl__Spec_tools__entry ()
(gdb) disass
Dump of assembler code for function camlLtl_to_acsl__Spec_tools__entry:
0x01732f60 <camlLtl_to_acsl__Spec_tools__entry+0>: sub $0xc,%esp
0x01732f63 <camlLtl_to_acsl__Spec_tools__entry+3>: call 0x175a05c <dyld_stub_caml_alloc3>
0x01732f68 <camlLtl_to_acsl__Spec_tools__entry+8>: lea 0x4(%eax),%eax
0x01732f6b <camlLtl_to_acsl__Spec_tools__entry+11>: movl $0x400,-0x4(%eax)
0x01732f72 <camlLtl_to_acsl__Spec_tools__entry+18>: movl $0x1,(%eax)
0x01732f78 <camlLtl_to_acsl__Spec_tools__entry+24>: mov %eax,0x175c8d8
0x01732f7d <camlLtl_to_acsl__Spec_tools__entry+29>: add $0x8,%eax
0x01732f80 <camlLtl_to_acsl__Spec_tools__entry+32>: movl $0x400,-0x4(%eax)
0x01732f87 <camlLtl_to_acsl__Spec_tools__entry+39>: movl $0x1,(%eax)
0x01732f8d <camlLtl_to_acsl__Spec_tools__entry+45>: mov %eax,0x175c8dc
0x01732f92 <camlLtl_to_acsl__Spec_tools__entry+50>: mov $0x175cba8,%eax
0x01732f97 <camlLtl_to_acsl__Spec_tools__entry+55>: mov %eax,0x175c8e0
0x01732f9c <camlLtl_to_acsl__Spec_tools__entry+60>: mov $0x175cb9c,%eax
0x01732fa1 <camlLtl_to_acsl__Spec_tools__entry+65>: mov %eax,0x175c8e4
0x01732fa6 <camlLtl_to_acsl__Spec_tools__entry+70>: mov $0x175cb90,%eax
0x01732fab <camlLtl_to_acsl__Spec_tools__entry+75>: mov %eax,0x175c8e8
0x01732fb0 <camlLtl_to_acsl__Spec_tools__entry+80>: mov $0x175cb84,%eax
0x01732fb5 <camlLtl_to_acsl__Spec_tools__entry+85>: mov %eax,0x175c8ec
0x01732fba <camlLtl_to_acsl__Spec_tools__entry+90>: mov $0x175cb78,%eax
0x01732fbf <camlLtl_to_acsl__Spec_tools__entry+95>: mov %eax,0x175c8f0
0x01732fc4 <camlLtl_to_acsl__Spec_tools__entry+100>: mov $0x175cb6c,%eax
0x01732fc9 <camlLtl_to_acsl__Spec_tools__entry+105>: mov %eax,0x175c8f4
0x01732fce <camlLtl_to_acsl__Spec_tools__entry+110>: mov $0x175cb5c,%eax
0x01732fd3 <camlLtl_to_acsl__Spec_tools__entry+115>: mov %eax,0x175c8f8
0x01732fd8 <camlLtl_to_acsl__Spec_tools__entry+120>: mov $0x175cb4c,%eax
0x01732fdd <camlLtl_to_acsl__Spec_tools__entry+125>: mov %eax,0x175c8fc
0x01732fe2 <camlLtl_to_acsl__Spec_tools__entry+130>: mov $0x175cb3c,%eax
0x01732fe7 <camlLtl_to_acsl__Spec_tools__entry+135>: mov %eax,0x175c900
0x01732fec <camlLtl_to_acsl__Spec_tools__entry+140>: mov $0x175cb2c,%eax
0x01732ff1 <camlLtl_to_acsl__Spec_tools__entry+145>: mov %eax,0x175c904
0x01732ff6 <camlLtl_to_acsl__Spec_tools__entry+150>: mov $0x175cb1c,%eax
0x01732ffb <camlLtl_to_acsl__Spec_tools__entry+155>: mov %eax,0x175c908
0x01733000 <camlLtl_to_acsl__Spec_tools__entry+160>: mov $0x175cb0c,%eax
0x01733005 <camlLtl_to_acsl__Spec_tools__entry+165>: mov %eax,0x175c90c
0x0173300a <camlLtl_to_acsl__Spec_tools__entry+170>: mov $0x175cafc,%eax
0x0173300f <camlLtl_to_acsl__Spec_tools__entry+175>: mov %eax,0x175c910
0x01733014 <camlLtl_to_acsl__Spec_tools__entry+180>: mov $0x175caec,%eax
0x01733019 <camlLtl_to_acsl__Spec_tools__entry+185>: mov %eax,0x175c914
0x0173301e <camlLtl_to_acsl__Spec_tools__entry+190>: mov $0x175cadc,%eax
0x01733023 <camlLtl_to_acsl__Spec_tools__entry+195>: mov %eax,0x175c918
0x01733028 <camlLtl_to_acsl__Spec_tools__entry+200>: mov $0x175cad0,%eax
0x0173302d <camlLtl_to_acsl__Spec_tools__entry+205>: mov %eax,0x175c91c
0x01733032 <camlLtl_to_acsl__Spec_tools__entry+210>: mov $0x175cac4,%eax
0x01733037 <camlLtl_to_acsl__Spec_tools__entry+215>: mov %eax,0x175c920
0x0173303c <camlLtl_to_acsl__Spec_tools__entry+220>: mov $0x175cab8,%eax
0x01733041 <camlLtl_to_acsl__Spec_tools__entry+225>: mov %eax,0x175c924
0x01733046 <camlLtl_to_acsl__Spec_tools__entry+230>: mov $0x175caac,%eax
0x0173304b <camlLtl_to_acsl__Spec_tools__entry+235>: mov %eax,0x175c928
0x01733050 <camlLtl_to_acsl__Spec_tools__entry+240>: mov $0x175ca9c,%eax
0x01733055 <camlLtl_to_acsl__Spec_tools__entry+245>: mov %eax,0x175c92c
0x0173305a <camlLtl_to_acsl__Spec_tools__entry+250>: mov $0x175ca90,%eax
0x0173305f <camlLtl_to_acsl__Spec_tools__entry+255>: mov %eax,0x175c930
0x01733064 <camlLtl_to_acsl__Spec_tools__entry+260>: mov $0x175ca80,%eax
0x01733069 <camlLtl_to_acsl__Spec_tools__entry+265>: mov %eax,0x175c934
0x0173306e <camlLtl_to_acsl__Spec_tools__entry+270>: mov $0x175ca70,%eax
0x01733073 <camlLtl_to_acsl__Spec_tools__entry+275>: mov %eax,0x175c938
0x01733078 <camlLtl_to_acsl__Spec_tools__entry+280>: mov $0x175ca60,%eax
0x0173307d <camlLtl_to_acsl__Spec_tools__entry+285>: mov %eax,0x175c93c
0x01733082 <camlLtl_to_acsl__Spec_tools__entry+290>: mov $0x175ca50,%eax
0x01733087 <camlLtl_to_acsl__Spec_tools__entry+295>: mov %eax,0x175c940
0x0173308c <camlLtl_to_acsl__Spec_tools__entry+300>: mov $0x175ca40,%eax
0x01733091 <camlLtl_to_acsl__Spec_tools__entry+305>: mov %eax,0x175c944
0x01733096 <camlLtl_to_acsl__Spec_tools__entry+310>: mov $0x175ca30,%eax
0x0173309b <camlLtl_to_acsl__Spec_tools__entry+315>: mov %eax,0x175c948
0x017330a0 <camlLtl_to_acsl__Spec_tools__entry+320>: mov $0x175ca20,%eax
0x017330a5 <camlLtl_to_acsl__Spec_tools__entry+325>: mov %eax,0x175c94c
0x017330aa <camlLtl_to_acsl__Spec_tools__entry+330>: mov $0x175ca10,%eax
0x017330af <camlLtl_to_acsl__Spec_tools__entry+335>: mov %eax,0x175c950
0x017330b4 <camlLtl_to_acsl__Spec_tools__entry+340>: mov $0x175ca00,%eax
0x017330b9 <camlLtl_to_acsl__Spec_tools__entry+345>: mov %eax,0x175c954
0x017330be <camlLtl_to_acsl__Spec_tools__entry+350>: mov $0x175cbcc,%eax
0x017330c3 <camlLtl_to_acsl__Spec_tools__entry+355>: mov %eax,0x175c958
0x017330c8 <camlLtl_to_acsl__Spec_tools__entry+360>: mov 0x14,%ebx
0x017330ce <camlLtl_to_acsl__Spec_tools__entry+366>: mov $0x175cbc4,%eax
0x017330d3 <camlLtl_to_acsl__Spec_tools__entry+371>: mov (%ebx),%ecx
0x017330d5 <camlLtl_to_acsl__Spec_tools__entry+373>: call *%ecx
0x017330d7 <camlLtl_to_acsl__Spec_tools__entry+375>: mov %eax,0x175c95c
0x017330dc <camlLtl_to_acsl__Spec_tools__entry+380>: mov $0x175c9f0,%eax
0x017330e1 <camlLtl_to_acsl__Spec_tools__entry+385>: mov %eax,0x175c960
0x017330e6 <camlLtl_to_acsl__Spec_tools__entry+390>: mov $0x175c9e0,%eax
0x017330eb <camlLtl_to_acsl__Spec_tools__entry+395>: mov %eax,0x175c964
0x017330f0 <camlLtl_to_acsl__Spec_tools__entry+400>: mov $0x175c9d0,%eax
0x017330f5 <camlLtl_to_acsl__Spec_tools__entry+405>: mov %eax,0x175c968
0x017330fa <camlLtl_to_acsl__Spec_tools__entry+410>: mov $0x175c9c4,%eax
0x017330ff <camlLtl_to_acsl__Spec_tools__entry+415>: mov %eax,0x175c96c
0x01733104 <camlLtl_to_acsl__Spec_tools__entry+420>: mov $0x175c9b4,%eax
0x01733109 <camlLtl_to_acsl__Spec_tools__entry+425>: mov %eax,0x175c970
0x0173310e <camlLtl_to_acsl__Spec_tools__entry+430>: mov $0x175c9a4,%eax
0x01733113 <camlLtl_to_acsl__Spec_tools__entry+435>: mov %eax,0x175c974
0x01733118 <camlLtl_to_acsl__Spec_tools__entry+440>: mov $0x175c994,%eax
0x0173311d <camlLtl_to_acsl__Spec_tools__entry+445>: mov %eax,0x175c978
0x01733122 <camlLtl_to_acsl__Spec_tools__entry+450>: mov $0x175c984,%eax
0x01733127 <camlLtl_to_acsl__Spec_tools__entry+455>: mov %eax,0x175c97c
0x0173312c <camlLtl_to_acsl__Spec_tools__entry+460>: mov $0x1,%eax
0x01733131 <camlLtl_to_acsl__Spec_tools__entry+465>: add $0xc,%esp
0x01733134 <camlLtl_to_acsl__Spec_tools__entry+468>: ret
0x01733135 <camlLtl_to_acsl__Spec_tools__entry+469>: nop
End of assembler dump.
TagsNo tags attached.
Attached Filestgz file icon dynlink.tgz [^] (987 bytes) 2010-04-29 14:41

- Relationships
related to 0006900assignedshindere Native code compiler for 32-bit OS X 

-  Notes
Pascal Cuoq (reporter)
2010-03-30 18:03

I forgot to add that the function camlLtl_to_acsl__Spec_tools__entry () was part of the dynamically loaded code (source in src/ltl_to_acsl and binary plug-in copied to lib/plugins/Ltl_to_acsl.cmxs.
doligez (administrator)
2010-04-21 15:18

Confirmed with 3.11.2, but can't reproduce with 3.12.0+dev18.
pascal_cuoq (reporter)
2010-04-21 23:26

I may have to package the Mac OS X binary distribution for Frama-C Boron with 3.12.0+dev18 then. I am sure this was not the intention behind the public OCaml CVS/SVN, but 64-bit Gtk+ on Mac OS X is simply not ready for prime-time, and not having dynlink is going to become a real show-stopper, what with the tens of plug-ins people are going to develop all over the world.

I cannot imagine a Frama-C user filing a bug report in for the version we distribute, but if you object for whatever reason, I will postpone the Mac OS X binary release until 3.12.0 is official.
pascal_cuoq (reporter)
2010-04-23 14:58

Damien said: "but can't reproduce with 3.12.0+dev18."

That's because Frama-C's configure detects that dynlink is disfunctional with this compiler, and here is how it detects it:

echo "Dynlink.loadfile \"foo\";;" >
ocamlopt.opt -shared -o test_dynlink.cmxs
ld: absolute addressing (perhaps -mdynamic-no-pic) used in _camlTest_dynlink__entry from test_dynlink.o not allowed in slidable image. Use '-read_only_relocs suppress' to enable text relocs

The change in OCaml's configure that consisted to suppress option '-read_only_relocs suppress' for Mac OS X Snow Leopard is not fine enough: this option seems still to be necessary for 32-bit dynlink on Snow Leopard.
pascal_cuoq (reporter)
2010-04-23 15:12

The same "Bus error" with the instructions above still happens in SVN 10302 if reverting the change to "configure" before compiling OCaml.
xleroy (administrator)
2010-04-29 14:41

The problem can be reproduced with very simple C code, attached as "dynlink.tgz". Scenario "b" corresponds to the way Caml builds its .cmxs shared objects.

One sees clearly that the MacOS 10.6 linker, invoked with "-read_only_relocs suppress", silently produces a bundle that is missing relocation information: any reference to an external symbol other than a function call is not relocated.

This is a regression compared with MacOS 10.5's linker, which produces correct relocation info. I really wish Apple would stop tinkering with their linker.

The old linker, ld_classic, produces correct relocations both under 10.5 and 10.6. (Scenario "d" in the test code.) It might be possible to use ld_classic to produce .cmxs files, however we cannot use it to produce other shared libs in Caml (the stub libs for the mixed C-bytecode libraries) because ld_classic is incompatible with some system libraries.
Pascal Cuoq (reporter)
2010-04-30 18:22

It may not matter to us as much as I initially feared:

- the reason for trying to get 32-bit Dynlink to work was the incomplete state of 64-bit Mac OS X native gtk+ libraries. The problem is only for Mac OS X-native gtk+ specific bindings. 64-bit versions of generic gtk+ libraries were debugged a long time ago. Yes, they will have to move some things from Carbon to Cocoa, but what already works is promising.

- gtk+-on-X11 has meanwhile improved on Mac OS X. I tried it again and it works acceptably for Frama-C (and it only uses the gtk+ libraries that were debugged by users of 64-bit linuxes long ago, so it works as well in its 64-bit version).

- Distributing Leopard-compiled binaries is a good workaround for the short term (statically linking the native version of Frama-C was another).

The only remaining question for us is whether the X11 solution will remain acceptable at least until 64-bit native gtk+ is ready. MacPorts people have apparently already given up on the system X server and are systematically shipping their own. This means I may have to get used to the idea of shipping an X server in the Mac OS X Frama-C binary release (we do not require users to install MacPorts).

I'm surprised by this choice on Apple's part (what are developers on Snow Leopard who want to produce binaries that work on Leopard supposed to do?) but we can manage. Thanks for the time spent on this very uninteresting issue. I owe you respectively a beer and a glass of non-alcoholic beverage of your choice.
frisch (developer)
2010-05-28 12:24

We have switched to a system where the platforms which support natdynlink are explicitly listed in the configure script. For other platforms, dynlink.cmxa is no longer installer.

The current list of platforms where natdynlink is declared to be supported is:

  case "$host" in
    *-*-cygwin*) natdynlink=true;;
    i[3456]86-*-linux*) natdynlink=true;;
    x86_64-*-linux*) natdynlink=true;;

Do you think it is safe to add:

      if test $arch64 == true; then

pascal_cuoq (reporter)
2010-05-28 13:12

> Do you think it is safe to add [...]

Yes. Dynlink is working flawlessly for us with Mac OS X 10.6 (Snow Leopard) in 64-bit both in 3.11.2 and the last version I tried from the 3.12 branch.
frisch (developer)
2010-05-28 13:42

I've added this case (i[3456]86-*-darwin10.* in 64-bit).

Let me know if you think I should add other cases (for Mac OS X < 10.6, 32/64 bit; and what about PowerPC Macs ?).
pascal_cuoq (reporter)
2010-05-31 15:07

For Mac OS X 10.5, dynlink worked fine in 32-bit on Intel Macs. I remember issues with 64-bit dynlink at some time, but I do not remember the resolution of these issues. Dynlink never worked on Power PC Macs.
frisch (developer)
2010-06-01 17:55

Can you give me the value of the $host variable for Mac OS X 10.5?
xleroy (administrator)
2010-06-01 18:46

Hi Alain,

I'm testing the OCaml trunk on a Mac OS X 10.5 Intel machine, in 32 and 64 bit mode. Tomorrow, I'll update configure accordingly; don't worry about it.

- Issue History
Date Modified Username Field Change
2010-03-30 17:48 Pascal Cuoq New Issue
2010-03-30 18:03 Pascal Cuoq Note Added: 0005282
2010-04-21 15:18 doligez Note Added: 0005357
2010-04-21 15:18 doligez Status new => acknowledged
2010-04-21 23:26 pascal_cuoq Note Added: 0005358
2010-04-23 14:58 pascal_cuoq Note Added: 0005367
2010-04-23 15:12 pascal_cuoq Note Added: 0005368
2010-04-29 14:41 xleroy Note Added: 0005412
2010-04-29 14:41 xleroy File Added: dynlink.tgz
2010-04-30 16:50 doligez Note Added: 0005432
2010-04-30 16:50 doligez Note Deleted: 0005432
2010-04-30 18:22 Pascal Cuoq Note Added: 0005433
2010-05-28 12:24 frisch Note Added: 0005527
2010-05-28 12:25 frisch Status acknowledged => feedback
2010-05-28 13:12 pascal_cuoq Note Added: 0005528
2010-05-28 13:42 frisch Note Added: 0005529
2010-05-31 15:07 pascal_cuoq Note Added: 0005537
2010-06-01 17:55 frisch Note Added: 0005538
2010-06-01 18:46 xleroy Note Added: 0005539
2010-06-07 19:19 xleroy Status feedback => resolved
2010-06-07 19:19 xleroy Resolution open => fixed
2010-06-07 19:19 xleroy Fixed in Version => 3.12.0+dev
2012-03-24 15:01 xleroy Status resolved => closed
2015-06-11 17:56 doligez Relationship added related to 0006900
2017-02-23 16:36 doligez Category OCaml general => -OCaml general
2017-03-03 17:55 doligez Category -OCaml general => -(deprecated) general
2017-03-03 18:01 doligez Category -(deprecated) general => ~deprecated (was: OCaml general)
2017-03-06 17:04 doligez Category ~deprecated (was: OCaml general) => ~DO NOT USE (was: OCaml general)

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker