|Anonymous | Login | Signup for a new account||2019-02-22 21:18 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007162||OCaml||~DO NOT USE (was: OCaml general)||public||2016-03-03 20:35||2016-03-24 16:47|
|Platform||OS||Linux||OS Version||Ubuntu 14.04|
|Target Version||4.03.0+dev / +beta1||Fixed in Version||4.03.0+dev / +beta1|
|Summary||0007162: Lablgtk-based GUI crashes with OCaml 4.03+beta1|
|Description||The Frama-C GUI, based on lablgtk, currently crashes when compiled with OCaml 4.03+beta1: a segmentation fault is produced in the Gtk code.|
Here's the end of the backtrace:
Program received signal SIGSEGV, Segmentation fault.
gtk_tree_view_row_inserted (model=0x160ae60, path=0x1561a40, iter=0x15ca020, data=0x12d1270) at /build/gtk+2.0-KsZSEA/gtk+2.0-2.24.23/gtk/gtktreeview.c:8464
8464 /build/gtk+2.0-KsZSEA/gtk+2.0-2.24.23/gtk/gtktreeview.c: No such file or directory.
#0 gtk_tree_view_row_inserted (model=0x160ae60, path=0x1561a40, iter=0x15ca020, data=0x12d1270) at /build/gtk+2.0-KsZSEA/gtk+2.0-2.24.23/gtk/gtktreeview.c:8464
#1 0x00007ffff72f33b8 in g_closure_invoke () from /usr/lib/x86_64-linux-gnu/libgobject-2.0.so.0
#2 0x00007ffff7304d3d in ?? () from /usr/lib/x86_64-linux-gnu/libgobject-2.0.so.0
0000003 0x00007ffff730ca29 in g_signal_emit_valist () from /usr/lib/x86_64-linux-gnu/libgobject-2.0.so.0
0000004 0x00007ffff730cce2 in g_signal_emit () from /usr/lib/x86_64-linux-gnu/libgobject-2.0.so.0
0000005 0x0000000000b15a8a in ml_custom_model_row_inserted (tree_model_val=<optimized out>, path=140737220365248, row=140737220365296) at ml_gtktree.c:1517
0000006 0x00000000009fd42f in camlGTree__fun_8134 ()
0000007 0x0000000000aad5b5 in camlList__iter_1258 () at list.ml:77
0000008 0x0000000000638687 in camlDesign__display_warnings_33195 () at src/plugins/gui/design.ml:1428
The last line is part of the Frama-C code.
I believe there might be several different factors contributing to this bug, but so far, after a manual bisection, I ended up at commit 8851e6b7 (Allow allocating custom blocks with finalizers in the minor heap.). The preceding commit (ceb5e0baa) does not crash.
I still don't know if the following is related, but when testing my program using ceb5e0baa or 8851e6b7, on longer runs, the following messages are produced in the console:
[ocaml] (use Sys.enable_runtime_warnings to control these warnings)
[ocaml] channel opened on file '/tmp/cppannot31a858.c' dies without being closed
[ocaml] channel opened on file '/tmp/cppannot11320f.c' dies without being closed
I had never seen these messages before, and they likely appear with several other commits. The named files are temporary files produced by Frama-C, which indicates that there might also be a bug in our code base. In the end, I think that there is an influence of several previously unnoticed bugs.
|Steps To Reproduce||- Compile the OCaml code corresponding to commit 8851e6b7;|
- Use it to compile Frama-C dependencies (especially lablgtk);
- Download, compile and install the latest public release of Frama-C (Magnesium);
- Create a "test.c" file containing a single line:
int i = 1.1;
- Run "frama-c-gui test.c". The program should crash almost instantly with the segmentation fault described above.
Note: it seems that it is not possible to install lablgtk directly from the stable versions of camlp4, so I preprocessed the lablgtk files and removed the camlp4 dependence. With the attached archive (which includes a "opam" file), it should be possible to locally do a `opam pin` on the lablgtk package and install the remaining Frama-C dependencies from opam.
I'll later try to add the (approximate) sequence of commands necessary to reproduce the entire installation.
|Tags||No tags attached.|
|Attached Files|| lablgtk-2.18.3-preprocessed.tar.gz [^] (900,070 bytes) 2016-03-03 20:35|
alloc_custom.diff [^] (3,816 bytes) 2016-03-05 13:54 [Show Content]
Seeing the name of the commit, this is not too surprising.
Indeed, lablgtk assumes that blocks created by alloc_custom do not move
(and disables compaction to ensure that).
I suppose we'll have to fix lablgtk.
Is there a simple way to ensure that a block allocated by alloc_custom is in the main heap?
I mean, other than using alloc_shr by hand?
|For reference the original bug solved by the commit is http://caml.inria.fr/mantis/view.php?id=3612, [^] the merge request introducing this commit is https://github.com/ocaml/ocaml/pull/92 [^]|
edited on: 2016-03-04 07:14
I think that this is simply a bug in LablGTK -- in fact, I think that assuming that any block in the OCaml heap does not move is a bug. LablGTK needs to be fixed to use a registered GC root to access all OCaml objects. If this is too expensive, a single root could hold a reference to an array of Obj.t that is resized when needed, and the references could be replaced by integers.
The other solution would be for OCaml to provide an API to allocate blocks in the C heap together with counterparts in the OCaml heap.
|Is it still useful to prepare a script to reproduce it? If so, I can do it, but it seems less needed now.|
|@garrigue you'll have to use alloc_shr.|
Can you try to apply the alloc_custom.diff patch to lablgtk and/or use the git version (either ocamlforge or github, they are the same)?
I basically reimplemented the original alloc_custom, which always calls alloc_shr.
If somebody had the courage to track down the places where it is required to remove them, this could be a better solution, but it is so easy to break something that works...
Originally this trick was only intended to be used for text iterators, but it may have creeped around.
I've updated my 4.03 branch to commit 95410ef232 and then applied your patch, and it works without problems.
I performed several tests and did not get any crashes or issues related to lablgtk.
I did not test 100% of our GUI, but I do believe every major component has been tested.
Thank you for the investigation and the patch!
|2016-03-03 20:35||maro||New Issue|
|2016-03-03 20:35||maro||File Added: lablgtk-2.18.3-preprocessed.tar.gz|
|2016-03-03 21:33||garrigue||Note Added: 0015428|
|2016-03-03 22:24||bobot||Note Added: 0015429|
|2016-03-04 07:07||dobenour||Note Added: 0015430|
|2016-03-04 07:14||dobenour||Note Edited: 0015430||View Revisions|
|2016-03-04 08:34||maro||Note Added: 0015431|
|2016-03-04 14:52||doligez||Note Added: 0015434|
|2016-03-05 13:54||garrigue||File Added: alloc_custom.diff|
|2016-03-05 13:59||garrigue||Note Added: 0015435|
|2016-03-05 13:59||garrigue||Assigned To||=> garrigue|
|2016-03-05 13:59||garrigue||Status||new => feedback|
|2016-03-07 10:14||maro||Note Added: 0015445|
|2016-03-07 10:14||maro||Status||feedback => assigned|
|2016-03-24 16:43||doligez||Relationship added||related to 0007161|
|2016-03-24 16:47||doligez||Status||assigned => closed|
|2016-03-24 16:47||doligez||Resolution||open => fixed|
|2016-03-24 16:47||doligez||Fixed in Version||=> 4.03.0+dev / +beta1|
|2016-03-24 16:47||doligez||Target Version||=> 4.03.0+dev / +beta1|
|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|