Fix #7333: vm_compute segfaults / Anomaly with cofix

We eta-expand cofixpoints when needed, so that their call-by-need
evaluation is correctly implemented by VM and native_compute.

7 files changed, 36 insertions, 3 deletions

diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
index 4a3c03d85..f42c46175 100644
--- a/kernel/cinstr.mli
+++ b/kernel/cinstr.mli
@@ -31,7 +31,7 @@ and lambda =
   | Lprim         of pconstant * int (* arity *) * instruction * lambda array
   | Lcase         of case_info * reloc_table * lambda * lambda * lam_branches
   | Lfix          of (int array * int) * fix_decl
-  | Lcofix        of int * fix_decl
+  | Lcofix        of int * fix_decl (* must be in eta-expanded form *)
   | Lmakeblock    of int * lambda array
   | Lval          of structured_constant
   | Lsort         of Sorts.t
@@ -39,6 +39,10 @@ and lambda =
   | Lproj         of int * Constant.t * lambda
   | Luint         of uint
 
+(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation
+to be correct. Otherwise, memoization of previous evaluations will be applied
+again to extra arguments (see #7333). *)
+
 and lam_branches =
   { constant_branches : lambda array;
     nonconstant_branches : (Name.t array * lambda) array }
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 619dd608f..8389dd326 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -700,6 +700,7 @@ let rec lambda_of_constr env c =
     Lfix(rec_init, (names, ltypes, lbodies))
 
   | CoFix(init,(names,type_bodies,rec_bodies)) ->
+    let rec_bodies = Array.map2 (Reduction.eta_expand env.global_env) rec_bodies type_bodies in
     let ltypes = lambda_of_args env 0 type_bodies in
     Renv.push_rels env names;
     let lbodies = lambda_of_args env 0 rec_bodies in
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index 9c17cc2b5..c319be32d 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -37,7 +37,7 @@ and lambda =
                   (* annotations, term being matched, accu, branches *)
   | Lif           of lambda * lambda * lambda
   | Lfix          of (int array * int) * fix_decl 
-  | Lcofix        of int * fix_decl 
+  | Lcofix        of int * fix_decl (* must be in eta-expanded form *)
   | Lmakeblock    of prefix * pconstructor * int * lambda array
                   (* prefix, constructor name, constructor tag, arguments *)
 	(* A fully applied constructor *)
@@ -50,6 +50,10 @@ and lambda =
   | Llazy
   | Lforce
 
+(* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation
+to be correct. Otherwise, memoization of previous evaluations will be applied
+again to extra arguments (see #7333). *)
+
 and lam_branches = (constructor * Name.t array * lambda) array 
 
 and fix_decl =  Name.t array * lambda array * lambda array
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index a49bf62b3..8b61ed0c5 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -570,6 +570,7 @@ let rec lambda_of_constr env sigma c =
       Lfix(rec_init, (names, ltypes, lbodies))
 	
   | CoFix(init,(names,type_bodies,rec_bodies)) ->
+      let rec_bodies = Array.map2 (Reduction.eta_expand !global_env) rec_bodies type_bodies in
       let ltypes = lambda_of_args env sigma 0 type_bodies in 
       Renv.push_rels env names;
       let lbodies = lambda_of_args env sigma 0 rec_bodies in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6cd3917c7..8ca596d48 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -862,6 +862,17 @@ let dest_prod env =
   in
   decrec env Context.Rel.empty
 
+let dest_lam env =
+  let rec decrec env m c =
+    let t = whd_all env c in
+    match kind t with
+      | Lambda (n,a,c0) ->
+          let d = LocalAssum (n,a) in
+          decrec (push_rel d env) (Context.Rel.add d m) c0
+      | _ -> m,t
+  in
+  decrec env Context.Rel.empty
+
 (* The same but preserving lets in the context, not internal ones. *)
 let dest_prod_assum env =
   let rec prodec_rec env l ty =
@@ -907,3 +918,12 @@ let is_arity env c =
     let _ = dest_arity env c in
     true
   with NotArity -> false
+
+let eta_expand env t ty =
+  let ctxt, codom = dest_prod env ty in
+  let ctxt',t = dest_lam env t in
+  let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in
+  let eta_args = List.rev_map mkRel (List.interval 1 d) in
+  let t = Term.applistc (Vars.lift d t) eta_args in
+  let t = Term.it_mkLambda_or_LetIn t (List.firstn d ctxt) in
+  Term.it_mkLambda_or_LetIn t ctxt'
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 2e10f98c5..e53ab6aef 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -118,9 +118,12 @@ val betazeta_appvect : int -> constr -> constr array -> constr
 
 val dest_prod       : env -> types -> Context.Rel.t * types
 val dest_prod_assum : env -> types -> Context.Rel.t * types
+val dest_lam        : env -> types -> Context.Rel.t * constr
 val dest_lam_assum  : env -> types -> Context.Rel.t * types
 
 exception NotArity
 
 val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *)
 val is_arity   : env -> types -> bool
+
+val eta_expand : env -> constr -> types -> constr
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e07833204..12c82e20d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -955,7 +955,7 @@ let set_strategy e k l = { e with env =
 
 open Retroknowledge
 
-(* the Environ.register function syncrhonizes the proactive and reactive
+(* the Environ.register function synchronizes the proactive and reactive
    retroknowledge. *)
 let dispatch =