From ab84e2f45e2cdf99e5c69b90b628ef6618fe880a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 10 Jun 2018 18:25:09 +0200 Subject: Fix #7723: vm_compute segfaults with universe polymorphism Was revealing a critical bug in VM universe handling introduced in 8.5. --- kernel/cbytecodes.ml | 1 + kernel/cbytecodes.mli | 1 + kernel/cbytegen.ml | 33 ++++++++++++++++++++++++--------- 3 files changed, 26 insertions(+), 9 deletions(-) (limited to 'kernel') diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 521f540d2..6931fec03 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -217,6 +217,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (* number of universes on the stack, *) (* universes are always at the bottom. *) nb_stack : int; (* number of variables on the stack *) diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 238edc0af..de21401b3 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -159,6 +159,7 @@ type vm_env = { type comp_env = { + arity : int; (* arity of the current function, 0 if none *) nb_uni_stack : int ; (** number of universes on the stack *) nb_stack : int; (** number of variables on the stack *) in_stack : int list; (** position in the stack *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 7a27a3d20..1b909a8d0 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -112,8 +112,9 @@ let push_fv d e = { let fv r = !(r.in_env) -let empty_comp_env ?(univs=0) ()= - { nb_uni_stack = univs; +let empty_comp_env ()= + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -148,7 +149,8 @@ let rec add_param n sz l = if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) let comp_env_fun ?(univs=0) arity = - { nb_uni_stack = univs ; + { arity; + nb_uni_stack = univs ; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = 0; @@ -159,7 +161,8 @@ let comp_env_fun ?(univs=0) arity = let comp_env_fix_type rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -173,7 +176,8 @@ let comp_env_fix ndef curr_pos arity rfv = for i = ndef downto 1 do prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -183,7 +187,8 @@ let comp_env_fix ndef curr_pos arity rfv = } let comp_env_cofix_type ndef rfv = - { nb_uni_stack = 0; + { arity = 0; + nb_uni_stack = 0; nb_stack = 0; in_stack = []; nb_rec = 0; @@ -197,7 +202,8 @@ let comp_env_cofix ndef arity rfv = for i = 1 to ndef do prec := Kenvacc i :: !prec done; - { nb_uni_stack = 0; + { arity; + nb_uni_stack = 0; nb_stack = arity; in_stack = add_param arity 0 []; nb_rec = ndef; @@ -249,8 +255,17 @@ let pos_rel i r sz = Kenvacc(r.offset + pos) let pos_universe_var i r sz = - if i < r.nb_uni_stack then - Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) + (* Compilation of a universe variable can happen either at toplevel (the + current closure correspond to a constant and has local universes) or in a + local closure (which has no local universes). *) + if r.nb_uni_stack != 0 then begin + (* Universe variables are represented by De Bruijn levels (not indices), + starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] + with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access + the last universe. *) + Printf.eprintf "pos_univ i=%i sz=%i arity=%i nb_univ=%i\n" i sz r.arity r.nb_uni_stack; + Kacc (sz - r.arity - (r.nb_uni_stack - i)) + end else let env = !(r.in_env) in let db = FVuniv_var i in -- cgit v1.2.3 From 18880888d56b3f5f1e69ddadb7aadf02b0c56401 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 12 Jun 2018 11:35:08 +0200 Subject: Test file for #7723 --- kernel/cbytegen.ml | 4 +-- test-suite/bugs/closed/7723.v | 58 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 59 insertions(+), 3 deletions(-) create mode 100644 test-suite/bugs/closed/7723.v (limited to 'kernel') diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 1b909a8d0..f17313230 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -258,14 +258,12 @@ let pos_universe_var i r sz = (* Compilation of a universe variable can happen either at toplevel (the current closure correspond to a constant and has local universes) or in a local closure (which has no local universes). *) - if r.nb_uni_stack != 0 then begin + if r.nb_uni_stack != 0 then (* Universe variables are represented by De Bruijn levels (not indices), starting at 0. The shape of the stack will be [v1|..|vn|u1..up|arg1..argq] with size = n + p + q, and q = r.arity. So Kacc (sz - r.arity - 1) will access the last universe. *) - Printf.eprintf "pos_univ i=%i sz=%i arity=%i nb_univ=%i\n" i sz r.arity r.nb_uni_stack; Kacc (sz - r.arity - (r.nb_uni_stack - i)) - end else let env = !(r.in_env) in let db = FVuniv_var i in diff --git a/test-suite/bugs/closed/7723.v b/test-suite/bugs/closed/7723.v new file mode 100644 index 000000000..216290123 --- /dev/null +++ b/test-suite/bugs/closed/7723.v @@ -0,0 +1,58 @@ +Set Universe Polymorphism. + +Module Segfault. + +Inductive decision_tree : Type := . + +Fixpoint first_satisfying_helper {A B} (f : A -> option B) (ls : list A) : option B + := match ls with + | nil => None + | cons x xs + => match f x with + | Some v => Some v + | None => first_satisfying_helper f xs + end + end. + +Axiom admit : forall {T}, T. +Definition dtree4 : option decision_tree := + match first_satisfying_helper (fun pat : nat => Some pat) (cons 0 nil) + with + | Some _ => admit + | None => admit + end +. +Definition dtree'' := Eval vm_compute in dtree4. (* segfault *) + +End Segfault. + +Module OtherExample. + +Definition bar@{i} := Type@{i}. +Definition foo@{i j} (x y z : nat) := + @id Type@{j} bar@{i}. +Eval vm_compute in foo. + +End OtherExample. + +Module LocalClosure. + +Definition bar@{i} := Type@{i}. + +Definition foo@{i j} (x y z : nat) := + @id (nat -> Type@{j}) (fun _ => Type@{i}). +Eval vm_compute in foo. + +End LocalClosure. + +Require Import Hurkens. +Polymorphic Inductive unit := tt. + +Polymorphic Definition foo := + let x := id tt in (x, x, Type). + +Lemma bad : False. + refine (TypeNeqSmallType.paradox (snd foo) _). + vm_compute. + Fail reflexivity. +Abort. -- cgit v1.2.3