Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006329OCamlruntime systempublic2014-02-18 10:392017-02-21 17:19
Assigned Toshinwell 
PlatformOSOS Version
Product Version4.01.0 
Target Version4.05.0+devFixed in Version 
Summary0006329: File "", line 63, characters 6-12: Assertion failed.
DescriptionThere is an assertion failed in the OCaml runtime when dynamically loading a recursive module. Unfortunately, the bug is highly sensitive to conditions: changing the size of the code segment, changing the size of the data segment, changing the size of the read-only data segment, changing the number of relocations, etc, all cause the bug to vanish. As a consequence, we were unable to produce a small testcase, sorry. This bug report is mostly for the record. That said, it is perfectly reproducible and we were able to trigger it on three systems with OCaml 4.01.0 and Coq 8.4pl3.
Steps To Reproducegit clone git:// [^]
cd why3
git checkout a8c13660788c726a134fab9109e384592881e8d7
cat > src/util/ << EOF
let version = "1234567812345678123456781234567812345678123456781234567812345678123456781234567"
let builddate = ""
let libdir = ""
let datadir = ""
let localdir = Some ""
let compile_time_support = [ "", ""; "", "" ]
make src/coq-tactic/.why3-vo-opt
Attached Files

- Relationships

-  Notes
frisch (developer)
2014-02-20 11:36

Could it be the case that two units of the same name where dynlinked in the same process? Do you use -pack?
frisch (developer)
2014-02-20 11:59

$ make src/coq-tactic/.why3-vo-opt
Ocamldep src/util/
Ocamldep src/util/
Ocamldep src/util/
Ocamldep src/util/
Ocamldep src/util/
Ocamldep src/util/
make: *** No rule to make target `src/coq-tactic/.why3-vo-opt'. Stop.

Do we need to install anything else in addition to OCaml itself?
gmelquiond (reporter)
2014-02-20 12:20

I don't think there are two units with the same name. (Any way to make sure?) We are using -pack, so that all our modules are submodules of Why3.

Also, you need Coq, since the dynamically-loaded module is actually a Coq plugin and it depends on various Coq modules. Due to the high sensitivity on the size of the segments and the number of relocations, I was unfortunately not able to remove Coq from the equation.
shinwell (developer)
2014-05-30 13:02

I tried to reproduce this, building a clean 4.01 OCaml installation, and then compiling coq-8.4pl3 from the distribution tarball. With both of the installation directories on my PATH, the configure script for why3 said:

Verbose make : no
OCaml compiler : yes
    Version : 4.01.1+dev2-2013-12-18+CLOSED
    Library path : /home/mark/dev/pr/6329/ocaml/lib/ocaml
    Native compilation : yes
    Profiling : no
IDE : no (lablgtk2 not found)
Bench tool : no (sqlite3 not found)
Documentation : no (rubber not found)
Coq support : yes
    Version : 8.4pl3
    Library path : /home/mark/dev/pr/6329/coq-install/lib/coq
    "why3" tactic : no (camlp5o not found)
    Realization support : yes
        FP arithmetic : no (Flocq >= 2.2 not found)
PVS support : no (pvs not found)
Isabelle support : no (isabelle not found)
Frama-C support : no
Hypothesis selection : no (ocamlgraph not found)
Installable : yes
    Binary path : ${exec_prefix}/bin
    Lib path : ${exec_prefix}/lib/why3
    Data path : ${prefix}/share/why3
    Ocaml Library : /home/mark/dev/pr/6329/ocaml/lib/ocaml/why3
    Relocatable : no

However, I still get the same error "make: *** No rule to make target `src/coq-tactic/.why3-vo-opt'. Stop.". I think it might be because some dependency of lib/coq-tactic/why3tac.cmxs can't or won't build.

Could you please adjust the repro instructions, and then we can try again? Thanks.
shinwell (developer)
2014-05-30 13:17

Ah, the error was caused by missing camlp5...
shinwell (developer)
2014-05-30 13:55
edited on: 2014-05-30 13:58

OK, so I managed to get that make command to complete successfully.

Maybe you could prepare a tarball that includes all of the sources and objects from a tree where this bug has been observed.

Also, it would be useful if you could get this to fail having altered your OCaml source tree such that instead of just bombing out with an assertion failure, it prints the values of:
- n
- Obj.tag n
- Obj.size n
- Array.length comps

gmelquiond (reporter)
2015-03-10 18:15

This bug started popping up again, this time on our regression server. So I took the chance to create a minimal environment for reliably reproducing it. Since the chroot is 1GB-large, I will not post its tarball here. ("Minimal" meant the smallest Debian system able to compile the Why3 plugin nowadays, so it is quite large.)

Due to the high sensitivity to the compilation conditions (see original report: even adding a string causes the bug to vanish), I have not tried modifying the standard library of Ocaml to add some debug printfs. However, I am willing to keep the chroot around and try any non-intrusive method you can think of. In particular, if you can think of a way of recovering n, Obj.tag n, etc from e.g. gdb, please do to tell.
shinwell (developer)
2015-05-07 14:57

Can you please put the tarball somewhere on the web such that I can download it, and try to reproduce this problem?
xleroy (administrator)
2015-11-15 17:40

Any news about this mysterious failure?
doligez (administrator)
2016-02-11 14:18

I'm in contact with gmelquiond who will give me the repro file.
doligez (administrator)
2016-04-04 17:16

I got the repro file (364 MB).
shinwell (developer)
2016-12-08 09:24

@doligez Are you able to reproduce this bug using the repro file (which only you have)?
xleroy (administrator)
2017-02-16 11:18

So, is this issue reproducible or not?
doligez (administrator)
2017-02-21 17:19

I'm sorry I dropped the ball on this one. I still have the repro file and I'll try it shortly.

- Issue History
Date Modified Username Field Change
2014-02-18 10:39 gmelquiond New Issue
2014-02-19 20:46 doligez Tag Attached: recmod
2014-02-20 11:36 frisch Note Added: 0010963
2014-02-20 11:59 frisch Note Added: 0010964
2014-02-20 12:20 gmelquiond Note Added: 0010965
2014-05-30 13:02 shinwell Note Added: 0011590
2014-05-30 13:17 shinwell Note Added: 0011591
2014-05-30 13:55 shinwell Note Added: 0011592
2014-05-30 13:55 shinwell Assigned To => shinwell
2014-05-30 13:55 shinwell Status new => feedback
2014-05-30 13:58 shinwell Note Edited: 0011592 View Revisions
2014-07-08 11:30 doligez Target Version => 4.03.0+dev / +beta1
2015-03-10 18:15 gmelquiond Note Added: 0013426
2015-03-10 18:15 gmelquiond Status feedback => assigned
2015-05-07 14:57 shinwell Note Added: 0013862
2015-05-07 14:57 shinwell Status assigned => feedback
2015-11-15 17:40 xleroy Note Added: 0014685
2016-02-11 14:18 doligez Note Added: 0015343
2016-04-04 17:16 doligez Note Added: 0015674
2016-04-14 16:31 doligez Target Version 4.03.0+dev / +beta1 => 4.03.1+dev
2016-12-08 09:24 shinwell Note Added: 0016819
2016-12-08 09:46 shinwell Status feedback => assigned
2017-02-16 11:18 xleroy Note Added: 0017281
2017-02-16 11:18 xleroy Target Version 4.03.1+dev => 4.05.0+dev
2017-02-21 17:19 doligez Note Added: 0017392
2017-02-23 16:43 doligez Category OCaml runtime system => runtime system

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker