On Thu, Mar 26, 2020 at 01:20:58PM +0900, Stephen J. Turnbull wrote:
Where is the segfault? Is it in coqc or is it in the generated code
or is it in the OCaml compiler or is it somewhere else?
I managed to reproduce this on my mostly Rawhide x86-64 development
machine by running fedpkg build in a loop overnight. This also
captured a core dump.
Unfortunately the stack trace, even with full debuginfo installed, was
not very helpful. I'm now trying to run the unstable bin/coqc command
over and over again under gdb, but the bug has not reproduced there so
far.
One thing I did learn from the stack trace is that it appears to fail
in C code (in the garbage collector). However that might be because
the OCaml heap is corrupted by an earlier event. Another thing I
learned is that it happens when doing something or other with weak
references, which can be non-deterministic.
If you can't rule out OCaml: does it produce native code
directly, or
does it produce C or similar and then use GCC or similar to produce
the native code?
OCaml produces native code directly. GCC is only used to link the
final object files together.
Rich.
Core was generated by `bin/coqc -coqlib . -q -native-compiler yes
theories/FSets/FMapFullAVL.v'.
Program terminated with signal SIGSEGV, Segmentation fault.
#0 0x0000556989736c94 in ?? ()
(gdb) t a a bt
Thread 1 (Thread 0x7f7453e1ec00 (LWP 2710541)):
#0 0x0000556989736c94 in ?? ()
#1 0x0000000000000001 in ?? ()
#2 0x0000000000000001 in ?? ()
#3 0x00007f7453440ec8 in ?? ()
#4 0xfffffffffffffec0 in ?? ()
#5 0x00005569c42daba8 in ?? ()
#6 0x0000000000000004 in ?? ()
#7 0x0000000000000002 in ?? ()
#8 0x000000042d7f6c00 in ?? ()
#9 0x0000000000000001 in ?? ()
^------ probable bad stack frame
#10 0x00005569c35adc63 in caml_alloc_shr ()
^------ garbage collector
https://github.com/ocaml/ocaml/blob/0756052841d0d3e6266c8c1ca4a608dc16c11...
#11 0x00005569c35c00bc in caml_ephe_set_key ()
^------ weak ephemerons
https://github.com/ocaml/ocaml/blob/0756052841d0d3e6266c8c1ca4a608dc16c11...
#12 0x00005569c35419e8 in camlStdlib__obj__set_key_306 ()
#13 0x00005569c358da66 in camlStdlib__ephemeron__create_1033 ()
^------ OCaml functions Stdlib.Obj.set_key & Stdlib.Ephemeron.create
#14 0x00007ffd45de5508 in ?? ()
#15 0x00007ffd45de5500 in ?? ()
#16 0x00007f744b7cf7b0 in ?? ()
#17 0x0000000030124a25 in ?? ()
#18 0x00007f7453745e88 in ?? ()
#19 0x0000000000000225 in ?? ()
#20 0x4917d3992e9b8500 in ?? ()
#21 0x00005569c3a3c858 in camlCsymtable__9 ()
#22 0x0000000000000000 in ?? ()
--
Richard Jones, Virtualization Group, Red Hat
http://people.redhat.com/~rjones
Read my programming and virtualization blog:
http://rwmj.wordpress.com
libguestfs lets you edit virtual machines. Supports shell scripting,
bindings from many languages.
http://libguestfs.org