New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Bus error in 32-bit Snow Leopard OCaml-3.11.2-native-generated program (may be caused by Dynlink) #5012
Comments
Comment author: Pascal Cuoq 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. |
Comment author: @damiendoligez Confirmed with 3.11.2, but can't reproduce with 3.12.0+dev18. |
Comment author: pascal_cuoq 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 caml.inria.fr/mantis 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. |
Comment author: pascal_cuoq 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";;" > test_dynlink.ml 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. |
Comment author: pascal_cuoq The same "Bus error" with the instructions above still happens in SVN 10302 if reverting the change to "configure" before compiling OCaml. |
Comment author: @xavierleroy 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. |
Comment author: Pascal Cuoq It may not matter to us as much as I initially feared:
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. |
Comment author: @alainfrisch 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 Do you think it is safe to add:
? |
Comment author: pascal_cuoq
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. |
Comment author: @alainfrisch 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 ?). |
Comment author: pascal_cuoq 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. |
Comment author: @alainfrisch Can you give me the value of the $host variable for Mac OS X 10.5? |
Comment author: @xavierleroy 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. |
Original bug ID: 5012
Reporter: Pascal Cuoq
Status: closed (set by @xavierleroy on 2012-03-24T14:01:47Z)
Resolution: fixed
Priority: normal
Severity: crash
Version: 3.11.2
Fixed in version: 3.12.0+dev
Category: ~DO NOT USE (was: OCaml general)
Related to: #6900
Monitored by: "Julien Signoles"
Bug description
STEPS TO REPRODUCE:
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
Install
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 http://frama-c.com/download/frama-c-Beryllium-20090902.tar.gz
cd frama-c-Beryllium-20090902
./configure
make bin/toplevel.byte
export FRAMAC_PLUGIN=./lib/plugins/ # This env variable is used to locate plug-ins
bin/toplevel.byte
nothing happens. This is the expected behavior.
make bin/toplevel.opt
bin/toplevel.opt
Bus error
The above is the bug.
export FRAMAC_PLUGIN=/
bin/toplevel.opt
Nothing happens (expected behavior) when no plug-in to dynamically load is found
Additional information
Dynlink 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.
(gdb)
File attachments
The text was updated successfully, but these errors were encountered: