Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007162OCaml~DO NOT USE (was: OCaml general)public2016-03-03 20:352016-03-24 16:47
Reportermaro 
Assigned Togarrigue 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSLinuxOS VersionUbuntu 14.04
Product Version 
Target Version4.03.0+dev / +beta1Fixed in Version4.03.0+dev / +beta1 
Summary0007162: Lablgtk-based GUI crashes with OCaml 4.03+beta1
DescriptionThe 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.
(gdb) bt
#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.
TagsNo tags attached.
Attached Filesgz file icon lablgtk-2.18.3-preprocessed.tar.gz [^] (900,070 bytes) 2016-03-03 20:35
diff file icon alloc_custom.diff [^] (3,816 bytes) 2016-03-05 13:54 [Show Content]

- Relationships
related to 0007161closed Ephemerons lead to crash related to weak hash tables 

-  Notes
(0015428)
garrigue (manager)
2016-03-03 21:33

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?
(0015429)
bobot (reporter)
2016-03-03 22:24

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 [^]
(0015430)
dobenour (reporter)
2016-03-04 07:07
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.

(0015431)
maro (reporter)
2016-03-04 08:34

Is it still useful to prepare a script to reproduce it? If so, I can do it, but it seems less needed now.
(0015434)
doligez (administrator)
2016-03-04 14:52

@garrigue you'll have to use alloc_shr.
(0015435)
garrigue (manager)
2016-03-05 13:59

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.
(0015445)
maro (reporter)
2016-03-07 10:14

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!

- Issue History
Date Modified Username Field Change
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
Powered by Mantis Bugtracker