I have the Coq project extracted to OCaml, which crashes with SIGSEGV when executing the binary. However, it works when I execute bytecode. Debug shows it crashing here:
Program received signal SIGSEGV, Segmentation fault.
camlBvector__entry () at coq/Bvector.ml:47
47 Vector.map negb
(gdb) bt
#0 camlBvector__entry () at coq/Bvector.ml:47
#1 0x00005555556a4759 in caml_program ()
#2 0x00005555557e788d in caml_start_program ()
The relevant code:
46: let coq_Bneg =
47: Vector.map negb
Extracted from standard library Bvector.v. Any suggestions on how to debug this?
The Coq Proof Assistant, version 8.16.1 compiled with OCaml 4.14.1
minimize the extracted ml by removing definitions to try to figure out what's going on
it looks like it fails on defining this function. When I add breakpoint at camlBvector__entry
I it shows initializing several functions from the same file and then crashing at Bneg
:
Breakpoint 1, 0x00005555556f6750 in camlBvector__entry () at coq/Bvector.ml:118
118 (fun p' -> coq_BshiftRa n (coq_BshiftRa_iter n bv p'))
(gdb) bt
#0 0x00005555556f6750 in camlBvector__entry () at coq/Bvector.ml:118
#1 0x00005555556a4759 in caml_program ()
#2 0x00005555557e788d in caml_start_program ()
#3 0x00005555557c270c in caml_startup_common (argv=0x7fffffffe3e8,
pooling=<optimized out>, pooling@entry=0) at startup_nat.c:160
#4 0x00005555557c275f in caml_startup_exn (argv=<optimized out>)
at startup_nat.c:172
#5 caml_startup (argv=<optimized out>) at startup_nat.c:172
#6 0x00005555556a4202 in main (argc=<optimized out>, argv=<optimized out>)
at main.c:37
(gdb) s
22 Vector.const true
(gdb) n
27 Vector.const false
(gdb)
32 Vector.hd
(gdb)
37 Vector.tl
(gdb)
42 Vector.last
(gdb)
47 Vector.map negb
(gdb)
Program received signal SIGSEGV, Segmentation fault.
The problem was with the extraction of Vector.v. Apparently, there is also vector module in ZArith library.
for what it's worth, whenever I've had SIGSEGV in extracted code, it's always been something related to Obj.magic
.
There is nothing wrong with the extracted code, as far as I can tell. Can you reproduce the segfault with some other version of OCaml?
So the initial problem was fixed by adding Vector
to Extraction Blacklist
. It was occurring with two different versions of OCaml. As I mentioned, there is another vector
module defined in ZArith, and this was causing problems. I did not look to deeply into how exactly this happened, just fixed it :). Now I am debugging another SIGSEGV, this time in extracted FMapAVL.ml
.
I still have another SIGSEGV in extracted code. I have a simple record with 2 boolean fields, and accessing one of them sometimes causes SIGSEGV. Any suggestions on how can I approach debugging this? Are there known cases when Coq to OCaml extraction produces incorrect code? The project is fairly big and extracting a small example could be problematic. Coq code uses monad typeclasses and extracted code has plenty of Obj.magic.
This is not very practical, but if you write a plugin that gives something like Extraction TestRun
a la Extraction TestCompile
, then you can run the bug minimizer on it to automatically minimize the example
Does the bug minimizer try to replace definitions with axioms? If so, the extracted code will instantly fail due to these unrealized axioms. So, there might not be much to miminize.
Still tracking this SISSEGV. I have a general, naive question. Since my Coq program type checks, such a crash in extracted OCaml likely indicates a bug in the Coq extraction or OCaml compiler? I am trying to narrow it down but even though it is 100% reproducible, it is hard to track down where exactly the memory is corrupted. (It is crashing on reading).
Or maybe it’s an unsound axiom/admitted lemma? (Or unsound extraction directive?) (not sure if there are even further options)
What kind of admitted lemma could lead to SISSEGV? I have some obligations like termination or expected lists sizes admitted but I do not see how they can lead to memory corruption. Looking at generated OCaml code I do not see anything suspicious.
No idea how likely that is, but if two types T1 = T2 differ but you assert they're equal, you risk trouble.
Silly examples: Axiom bad : bool = nat.
, but also Axiom oh_no : 1 = 2
used when casting Vector.t T 1
to Vector.t T 2
... Less silly: Axiom noes : some_length = 2
when some_length
is in fact 1.
Some of those might be hidden under Obj.magic
casts IIUC? OTOH exploiting bugs about _list_ sizes could be harder (not enough experience to guess).
Yes, type equality (or anything that makes it possible to derive one) makes it trivial to produce a segfault. And the equality does not even have to be inconsistent, it just has to be unprovable:
Axiom foo : unit = (unit -> unit).
Definition bar := @eq_rect Set _ (fun t => t) tt _ foo tt.
(* let bar = Obj.magic () () *)
... ooh! Isn't your foo example derivable from the univalence axiom?
I guess the deeper reason is that in the realizability model that describes/underlies extraction, univalence is false (and axiom K is true)?
Indeed for both remarks.
Another way to see it is that, from the point of view of extraction, the univalence axiom should live in Type
.
(That is, univalence is not non-informational.)
Univalence, or the identity type? I don't understand the first
I mean, I agree univalence needs equalities to contain information and not be erased (so those would have to move to Type); I'm just not sure if you mean more about the univalence axiom itself
I just meant univalence has a producer of instances of the identity types. So, you can restrict yourself to identity types living in Type
, if you wish.
Last updated: Oct 13 2024 at 01:02 UTC