Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)

3 files changed, 24 insertions, 9 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 487385a78..3095ce148 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 881bfae19..6677db2fd 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,15 @@ 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
+    (* 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. *)
+    Kacc (sz - r.arity - (r.nb_uni_stack - i))
   else
     let env = !(r.in_env) in
     let db = FVuniv_var i in