From 442bd1fe4007d2f3b46cb565abbcd64011db1af4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 16 May 2018 00:36:08 +0200
Subject: 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.
---
 kernel/cinstr.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel/cinstr.mli')

diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
index 4a3c03d85e..f42c46175c 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 }
-- 
cgit v1.2.3