| Anonymous | Login | Signup for a new account | 2013-05-25 06:20 CEST |  |
| Main | My View | View Issues | Change Log | Roadmap |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | |||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | |||
| 0005012 | OCaml | OCaml general | public | 2010-03-30 17:48 | 2012-03-24 15:01 | |||
| Reporter | Pascal Cuoq | |||||||
| Assigned To | ||||||||
| Priority | normal | Severity | crash | Reproducibility | always | |||
| Status | closed | Resolution | fixed | |||||
| Platform | OS | OS Version | ||||||
| Product Version | 3.11.2 | |||||||
| Target Version | Fixed in Version | 3.12.0+dev | ||||||
| Summary | 0005012: Bus error in 32-bit Snow Leopard OCaml-3.11.2-native-generated program (may be caused by Dynlink) | |||||||
| 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) | |||||||
| Tags | No tags attached. | |||||||
| Attached Files |  dynlink.tgz [^] (987 bytes) 2010-04-29 14:41 | |||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0005282) 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. |
|
(0005357) doligez (manager) 2010-04-21 15:18 |
Confirmed with 3.11.2, but can't reproduce with 3.12.0+dev18. |
|
(0005358) 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 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. |
|
(0005367) 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\";;" > test_dynlink.ml ocamlopt.opt -shared -o test_dynlink.cmxs test_dynlink.ml 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. |
|
(0005368) 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. |
|
(0005412) 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. |
|
(0005433) 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. |
|
(0005527) 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;; esac Do you think it is safe to add: i[3456]86-*-darwin10.*) if test $arch64 == true; then natdynlink=true fi;; ? |
|
(0005528) 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. |
|
(0005529) 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 ?). |
|
(0005537) 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. |
|
(0005538) frisch (developer) 2010-06-01 17:55 |
Can you give me the value of the $host variable for Mac OS X 10.5? |
|
(0005539) 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. |
|
Notes |
|
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 |
|
Issue History |
| Copyright © 2000 - 2011 MantisBT Group |
 |