diff options
| -rw-r--r-- | doc/changelog/01-kernel/14007-fix-14006.rst | 7 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 5 | ||||
| -rw-r--r-- | kernel/vmlambda.ml | 4 | ||||
| -rw-r--r-- | kernel/vmvalues.ml | 2 | ||||
| -rw-r--r-- | kernel/vmvalues.mli | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_14006.v | 3 |
6 files changed, 11 insertions, 11 deletions
diff --git a/doc/changelog/01-kernel/14007-fix-14006.rst b/doc/changelog/01-kernel/14007-fix-14006.rst new file mode 100644 index 0000000000..6765768295 --- /dev/null +++ b/doc/changelog/01-kernel/14007-fix-14006.rst @@ -0,0 +1,7 @@ +- **Fixed:** + Never store persistent arrays as VM / native structured values. + This could be used to make vo marshalling crash, and probably + breaking some other invariants of the kernel + (`#14007 <https://github.com/coq/coq/pull/14007>`_, + fixes `#14006 <https://github.com/coq/coq/issues/14006>`_, + by Pierre-Marie Pédrot). diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index f3b483467d..aa30a01134 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -381,10 +381,7 @@ let makeblock env ind tag nparams arity args = Lmakeblock(prefix, ind, tag, args) let makearray args def = - try - let p = Array.map get_value args in - Lval (Nativevalues.parray_of_array p (get_value def)) - with Not_found -> Lparray (args, def) + Lparray (args, def) (* Translation of constants *) 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" diff --git a/test-suite/bugs/closed/bug_14006.v b/test-suite/bugs/closed/bug_14006.v new file mode 100644 index 0000000000..b857959ae9 --- /dev/null +++ b/test-suite/bugs/closed/bug_14006.v @@ -0,0 +1,3 @@ +From Coq Require Import Int63 PArray. +Definition t : array nat := [| 1; 3; 2 | 4 |]. +Definition vm_accu_set v := Eval vm_compute in t.[1 <- v]. |