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/0756052841d0d3e6266c8c1ca4a608dc16c11441/runtime/memory.c#L560
#11 0x00005569c35c00bc in caml_ephe_set_key ()
^------ weak ephemerons
https://github.com/ocaml/ocaml/blob/0756052841d0d3e6266c8c1ca4a608dc16c11441/runtime/weak.c#L211
#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
_______________________________________________
devel mailing list -- devel@xxxxxxxxxxxxxxxxxxxxxxx
To unsubscribe send an email to devel-leave@xxxxxxxxxxxxxxxxxxxxxxx
Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/
List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines
List Archives: https://lists.fedoraproject.org/archives/list/devel@xxxxxxxxxxxxxxxxxxxxxxx
