Stream: Coq users

Topic: SIGSEGV on extracted code


view this post on Zulip Vadim Zaliva (Dec 26 2022 at 23:27):

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?

view this post on Zulip Vadim Zaliva (Dec 26 2022 at 23:29):

The Coq Proof Assistant, version 8.16.1 compiled with OCaml 4.14.1

view this post on Zulip Gaëtan Gilbert (Dec 26 2022 at 23:56):

minimize the extracted ml by removing definitions to try to figure out what's going on

view this post on Zulip Vadim Zaliva (Dec 26 2022 at 23:58):

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.

view this post on Zulip Vadim Zaliva (Dec 27 2022 at 01:01):

The problem was with the extraction of Vector.v. Apparently, there is also vector module in ZArith library.

view this post on Zulip Karl Palmskog (Dec 27 2022 at 08:38):

for what it's worth, whenever I've had SIGSEGV in extracted code, it's always been something related to Obj.magic.

view this post on Zulip Guillaume Melquiond (Dec 27 2022 at 09:58):

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?

view this post on Zulip Vadim Zaliva (Dec 27 2022 at 19:15):

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.

view this post on Zulip Vadim Zaliva (Dec 29 2022 at 19:17):

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.

view this post on Zulip Jason Gross (Dec 31 2022 at 05:13):

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

view this post on Zulip Guillaume Melquiond (Dec 31 2022 at 08:25):

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.

view this post on Zulip Vadim Zaliva (Jan 04 2023 at 17:17):

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).

view this post on Zulip Paolo Giarrusso (Jan 04 2023 at 22:32):

Or maybe it’s an unsound axiom/admitted lemma? (Or unsound extraction directive?) (not sure if there are even further options)

view this post on Zulip Vadim Zaliva (Jan 05 2023 at 01:01):

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.

view this post on Zulip Paolo Giarrusso (Jan 05 2023 at 03:13):

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).

view this post on Zulip Guillaume Melquiond (Jan 05 2023 at 07:36):

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 () () *)

view this post on Zulip Paolo Giarrusso (Jan 05 2023 at 07:46):

... ooh! Isn't your foo example derivable from the univalence axiom?

view this post on Zulip Paolo Giarrusso (Jan 05 2023 at 07:46):

I guess the deeper reason is that in the realizability model that describes/underlies extraction, univalence is false (and axiom K is true)?

view this post on Zulip Pierre-Marie Pédrot (Jan 05 2023 at 07:47):

Indeed for both remarks.

view this post on Zulip Guillaume Melquiond (Jan 05 2023 at 07:52):

Another way to see it is that, from the point of view of extraction, the univalence axiom should live in Type.

view this post on Zulip Guillaume Melquiond (Jan 05 2023 at 07:55):

(That is, univalence is not non-informational.)

view this post on Zulip Paolo Giarrusso (Jan 05 2023 at 07:55):

Univalence, or the identity type? I don't understand the first

view this post on Zulip Paolo Giarrusso (Jan 05 2023 at 07:58):

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

view this post on Zulip Guillaume Melquiond (Jan 05 2023 at 07:59):

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