The unpac monorepo manager self-hosting as a monorepo using unpac
Merge pull request #14084 from bclement-ocp/dynarray-opaque
Use an opaque abstract type for Dynarray.Dummy.with_dummy
authored by
Gabriel Scherer
and committed by
GitHub
5fe966a8
2c82a9c9
+88
-36
+3
Changes
+3
Changes
···
187
187
(Émile Trotignon, review by Nicolás Ojeda Bär, Jan Midtgaard and
188
188
Damien Doligez)
189
189
190
+
- #14084: Future-proof Dynarray implementation against a smarter compiler
191
+
(Basile Clément, review by Gabriel Scherer)
192
+
190
193
### Type system:
191
194
192
195
- #13781: Set scope of internal type nodes during abbreviation expansion
+85
-36
stdlib/dynarray.ml
+85
-36
stdlib/dynarray.ml
···
183
183
('a, 'stamp2) with_dummy array -> 'stamp2 dummy -> int ->
184
184
len:int ->
185
185
unit
186
+
(** Raises [Dummy_found i] if there is a dummy at any index [i] in
187
+
the source region. *)
186
188
187
189
val prefix :
188
190
('a, 'stamp) with_dummy array ->
···
226
228
r := Some dummy;
227
229
Fresh dummy
228
230
229
-
type ('a, 'stamp) with_dummy = 'a
231
+
(* Use an abstract type to prevent the compiler from assuming anything about
232
+
the representation of [with_dummy] values.
233
+
234
+
Representation: We explicitly use "%opaque" primitives when converting
235
+
to/from [with_dummy] types and/or arrays of [with_dummy] types, because
236
+
using "transparent" identity (e.g. `Obj.magic`) might break assumptions
237
+
that the compiler makes about value representations (for instance, a value
238
+
of type [(int, 'stamp) with_dummy array] could contain blocks, while a
239
+
value of type [int array] certainly does not).
240
+
241
+
While it would be possible to use transparent identity in {b some} places,
242
+
it would require careful reasoning to make sure it is safe to do so
243
+
(especially in a forward-compatible way) and it is not clear the benefit
244
+
is worth the effort. *)
245
+
type ('a, 'stamp) with_dummy
230
246
231
-
let of_val v = v
247
+
external of_val : 'a -> ('a, 'stamp) with_dummy = "%opaque"
232
248
233
-
let of_dummy (type a stamp) (dummy : stamp dummy) =
234
-
(Obj.magic dummy : (a, stamp) with_dummy)
249
+
external of_dummy : 'stamp dummy -> ('a, 'stamp) with_dummy = "%opaque"
235
250
236
251
let is_dummy v dummy =
237
252
v == of_dummy dummy
238
253
239
-
let unsafe_get v =
240
-
v
254
+
(* Safety: the argument must not be the ['stamp dummy]. *)
255
+
external unsafe_get : ('a, 'stamp) with_dummy -> 'a = "%opaque"
241
256
242
257
module Array = struct
243
258
let make n x ~dummy =
···
249
264
arr
250
265
end
251
266
267
+
(* Safety: must not be called on float arrays. *)
268
+
external unsafe_nocopy_from_non_float_array :
269
+
'a array -> ('a, 'stamp) with_dummy array
270
+
= "%opaque"
271
+
252
272
let copy_from_array a ~dummy =
253
273
if Obj.(tag (repr a) <> double_array_tag) then
254
-
Array.copy a
274
+
unsafe_nocopy_from_non_float_array (Array.copy a)
255
275
else begin
256
276
let n = Array.length a in
257
277
let arr = Array.make n (of_dummy dummy) in
···
264
284
265
285
let unsafe_nocopy_from_array a ~dummy =
266
286
if Obj.(tag (repr a) <> double_array_tag) then
267
-
a
287
+
unsafe_nocopy_from_non_float_array a
268
288
else copy_from_array a ~dummy
269
289
270
290
exception Dummy_found of int
271
291
292
+
(* Safety: the argument must not contain any dummies, and must not contain
293
+
floats. *)
294
+
external unsafe_nocopy_to_non_float_array :
295
+
('a, 'stamp) with_dummy array -> 'a array
296
+
= "%opaque"
297
+
272
298
let unsafe_nocopy_to_array a ~dummy =
273
-
let arr =
274
-
if Array.length a = 0 || Obj.(tag (repr a.(0)) <> double_tag) then
275
-
a
276
-
else begin
277
-
let n = Array.length a in
278
-
let a' = Array.make n a.(0) in
279
-
for i = 1 to n - 1 do
280
-
Array.unsafe_set a' i (unsafe_get (Array.unsafe_get a i))
281
-
done;
282
-
a'
283
-
end
284
-
in
285
-
Array.iteri
286
-
(fun i v -> if is_dummy v dummy then raise (Dummy_found i))
287
-
arr;
288
-
arr
299
+
let n = Array.length a in
300
+
if n = 0 || Obj.(tag (repr a.(0)) <> double_tag) then begin
301
+
for i = 0 to n - 1 do
302
+
if is_dummy (Array.unsafe_get a i) dummy then raise (Dummy_found i)
303
+
done;
304
+
unsafe_nocopy_to_non_float_array a
305
+
end else begin
306
+
let a' = Array.make n (unsafe_get a.(0)) in
307
+
for i = 1 to n - 1 do
308
+
let v = Array.unsafe_get a i in
309
+
if is_dummy v dummy then raise (Dummy_found i);
310
+
Array.unsafe_set a' i (unsafe_get v)
311
+
done;
312
+
a'
313
+
end
289
314
290
315
let init n f ~dummy =
291
316
let arr = Array.make n (of_dummy dummy) in
···
296
321
297
322
let blit_array src src_pos dst dst_pos ~len =
298
323
if Obj.(tag (repr src) <> double_array_tag) then
299
-
Array.blit src src_pos dst dst_pos len
324
+
Array.blit
325
+
(unsafe_nocopy_from_non_float_array src)
326
+
src_pos dst
327
+
dst_pos len
300
328
else begin
301
329
for i = 0 to len - 1 do
302
330
dst.(dst_pos + i) <- of_val src.(src_pos + i)
303
331
done;
304
332
end
305
333
334
+
(* Safety: both arrays must have the same dummy, i.e. the ['stamp1 dummy]
335
+
and the ['stamp2 dummy] must be physically equal. *)
336
+
external unsafe_cast_stamp_array :
337
+
('a, 'stamp1) with_dummy array -> ('a, 'stamp2) with_dummy array
338
+
= "%opaque"
339
+
306
340
let blit src src_dummy src_pos dst dst_dummy dst_pos ~len =
307
341
if src_dummy == dst_dummy then
308
-
Array.blit src src_pos dst dst_pos len
342
+
Array.blit (unsafe_cast_stamp_array src) src_pos dst dst_pos len
309
343
else begin
310
344
if len < 0
311
345
|| src_pos < 0
···
323
357
end;
324
358
(* We failed the check [src_dummy == dst_dummy] above, so we
325
359
know that in fact [src != dst] -- two dynarrays with
326
-
distinct dummies cannot share the same backing arrays. *)
327
-
assert (src != dst);
360
+
distinct dummies cannot share the same backing arrays.
361
+
362
+
We use [Obj.repr] for the comparison since [src] and [dst] have
363
+
different dummies. *)
364
+
assert (Obj.repr src != Obj.repr dst);
328
365
(* In particular, the source and destination arrays cannot
329
366
overlap, so we can always copy in ascending order without
330
-
risking overwriting an element needed later. *)
367
+
risking overwriting an element needed later.
368
+
369
+
We also must check for dummies (invalid state) in the source
370
+
array: having two different dummies in the same array would be
371
+
memory unsafe. *)
331
372
for i = 0 to len - 1 do
373
+
let v = Array.unsafe_get src (src_pos + i) in
374
+
(* The combination of [of_val] and [unsafe_get] below allows to change
375
+
the stamp mark, which is only safe on a non-dummy value. *)
376
+
if is_dummy v src_dummy then
377
+
raise (Dummy_found (src_pos + i));
332
378
Array.unsafe_set dst (dst_pos + i)
333
-
(Array.unsafe_get src (src_pos + i));
379
+
(of_val (unsafe_get v));
334
380
done
335
381
end
336
382
···
738
784
if dst_pos + blit_length > dst_length then begin
739
785
dst.length <- dst_pos + blit_length;
740
786
end;
741
-
(* note: [src] and [dst] may be equal when self-blitting, so
742
-
[src.length] may have been mutated here. *)
743
-
Dummy.Array.blit
744
-
src_arr src.dummy src_pos
745
-
dst_arr dst.dummy dst_pos
746
-
~len:blit_length
787
+
try
788
+
(* note: [src] and [dst] may be equal when self-blitting, so
789
+
[src.length] may have been mutated here. *)
790
+
Dummy.Array.blit
791
+
src_arr src.dummy src_pos
792
+
dst_arr dst.dummy dst_pos
793
+
~len:blit_length
794
+
with Dummy.Array.Dummy_found i ->
795
+
Error.missing_element ~i ~length:src_length
747
796
748
797
let blit ~src ~src_pos ~dst ~dst_pos ~len =
749
798
let src_length = length src in