From 35c1d9e7add9a415d1406e6bb1eae7bd67ba5357 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 25 Mar 2021 17:23:03 +0100
Subject: Never store persistent arrays as VM structured values.

Bytecode execution of persistent arrays can modify structured values meant
to be marshalled in vo files. Some VM values are not marshallable, leading
to this anomaly.

There are further issues with the use of a hash table to store structured
values, since they rely on structural equality and hashing functions.
Persistent arrays are not safe in this context.

Fixes #14006: Coqc cannot save .vo files containing primitive arrays.
---
 kernel/vmlambda.ml  | 4 ----
 kernel/vmvalues.ml  | 2 --
 kernel/vmvalues.mli | 1 -
 3 files changed, 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index e353348ac7..ee32384ec9 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -494,10 +494,6 @@ let makeblock tag nparams arity args =
   else Lmakeblock(tag, args)
 
 let makearray args def =
-  try
-    let p = Array.map get_value args in
-    Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def))
-  with Not_found ->
     let ar = Lmakeblock(0, args) in (* build the ocaml array *)
     let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *)
     Lmakeblock(0,[|kind|]) (* the reference *)
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 9944458d6b..938d1f28f7 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -459,8 +459,6 @@ let val_of_int i = (Obj.magic i : values)
 
 let val_of_uint i = (Obj.magic i : structured_values)
 
-let val_of_parray p = (Obj.magic p : structured_values)
-
 let atom_of_proj kn v =
   let r = Obj.new_block proj_tag 2 in
   Obj.set_field r 0 (Obj.repr kn);
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index d15595766a..534a85d773 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -148,7 +148,6 @@ val val_of_atom : atom -> values
 val val_of_int : int -> structured_values
 val val_of_block : tag -> structured_values array -> structured_values
 val val_of_uint : Uint63.t -> structured_values
-val val_of_parray : structured_values Parray.t -> structured_values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 external val_of_proj_name : Projection.Repr.t -> values = "%identity"
-- 
cgit v1.2.3