Skip to content

Commit 3ad57db

Browse files
cristianocclaude
andcommitted
Give saved graphs independent mutability classes
Saving previously duplicated a field's mutability class only when the row terminator was generic, sharing the resolved source cell otherwise. That left one lifetime exception to the copy invariant: a structure-generalized source (non-generic terminator, share policy) and its saved copy (generic terminator after for_saving relevels, duplicate policy) could own one class with incompatible row-copy classifications - copying both in a single session would then pick a policy depending on which owner was reached first. copy_type_desc gains a fresh_mutability flag and Subst.typexp_rec passes it for for_saving, so a saved graph now owns fresh value cells unconditionally: it shares no mutability class with its source, contains no link chains, and duplication through the session memo still preserves equivalence-class sharing within the saved graph. Ordinary copying alone decides sharing from row-terminator genericity. In passing, the Tlink arm of copy_type_desc now forwards keep_names (and the new flag) instead of silently dropping them on recursion. New pins: for_saving_copy_order_is_irrelevant builds the previously hazardous fixture (source and saved copy with different terminator classifications) and copies both in one session in both orders; for_saving_fresh_copy_preserves_internal_aliasing checks freshness keeps intra-graph sharing; the closed-row saving test now also asserts the saved cell is not the source's. The q1_ test-name prefixes are dropped along with the retracted universal terminator-sharing claim they referred to. Signed-Off-By: Cristiano Calcagno <ccrisccris@gmail.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PCtQiaDijUqA2fujQXvKUw
1 parent a3bafc8 commit 3ad57db

4 files changed

Lines changed: 98 additions & 40 deletions

File tree

compiler/ml/btype.ml

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -454,10 +454,10 @@ let dup_mutability r =
454454
r := Mutability_link r';
455455
r'
456456

457-
(* Copy policy for an object row, memoized per node so copying a row is
458-
linear in its length: duplicate the mutability cells iff the row ends in
459-
a generic variable (a scheme instantiation); share them otherwise (a
460-
structure-generalized copy, whose occurrences must see promotions). *)
457+
(* Copy policy for an object row, memoized per node so its terminator is
458+
classified once per session: duplicate the mutability cells iff the row
459+
ends in a generic variable (a scheme instantiation); share them otherwise
460+
(a structure-generalized copy, whose occurrences must see promotions). *)
461461
let row_terminator_generic rest =
462462
let session = current_type_copy_session () in
463463
let copy_policy_memo =
@@ -489,7 +489,8 @@ let row_terminator_generic rest =
489489
in
490490
go rest
491491

492-
let rec copy_type_desc ?(keep_names = false) f = function
492+
let rec copy_type_desc ?(keep_names = false) ?(fresh_mutability = false) f =
493+
function
493494
| Tvar _ as ty -> if keep_names then ty else Tvar None
494495
| Tarrow (params, ret) ->
495496
Tarrow (List.map (fun arg -> {arg with typ = f arg.typ}) params, f ret)
@@ -498,19 +499,20 @@ let rec copy_type_desc ?(keep_names = false) f = function
498499
| Tobject ty -> Tobject (f ty)
499500
| Tvariant _ -> assert false (* too ambiguous *)
500501
| Tfield f_ ->
501-
(* The mutability cell follows the row variable's sharing law:
502-
instantiating a generalized row (generic terminator) duplicates each
503-
cell once per session via [dup_mutability], so aliases within the
504-
instance stay correlated while the scheme and sibling instances are
505-
untouched; other copies hold the shared representative, so
506-
promotions reach every occurrence. *)
502+
(* Unless the caller requests an independent graph, the mutability cell
503+
follows the row variable's sharing law: instantiating a generalized row
504+
(generic terminator) duplicates each cell once per session via
505+
[dup_mutability], so aliases within the instance stay correlated while
506+
the scheme and sibling instances are untouched; other copies hold the
507+
shared representative, so promotions reach every occurrence. *)
507508
let mutability =
508-
if row_terminator_generic f_.rest then dup_mutability f_.mutability
509+
if fresh_mutability || row_terminator_generic f_.rest then
510+
dup_mutability f_.mutability
509511
else mutability_ref_repr f_.mutability
510512
in
511513
Tfield {f_ with mutability; typ = f f_.typ; rest = f f_.rest}
512514
| Tnil -> Tnil
513-
| Tlink ty -> copy_type_desc f ty.desc
515+
| Tlink ty -> copy_type_desc ~keep_names ~fresh_mutability f ty.desc
514516
| Tsubst _ -> assert false
515517
| Tunivar _ as ty -> ty (* always keep the name *)
516518
| Tpoly (ty, tyl) ->

compiler/ml/btype.mli

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,11 @@ val unmark_iterators : type_iterators
118118
(* Unmark any structure containing types. See [unmark_type] below. *)
119119

120120
val copy_type_desc :
121-
?keep_names:bool -> (type_expr -> type_expr) -> type_desc -> type_desc
121+
?keep_names:bool ->
122+
?fresh_mutability:bool ->
123+
(type_expr -> type_expr) ->
124+
type_desc ->
125+
type_desc
122126
(* Copy on types *)
123127

124128
val copy_row :

compiler/ml/subst.ml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -219,7 +219,8 @@ let rec typexp_rec s ty =
219219
else Some (type_path s p, tl));
220220
}
221221
| None -> Tvariant row))
222-
| _ -> copy_type_desc (typexp_rec s) desc);
222+
| _ ->
223+
copy_type_desc ~fresh_mutability:s.for_saving (typexp_rec s) desc);
223224
ty'
224225

225226
(*

tests/ounit_tests/ounit_object_mutability_tests.ml

Lines changed: 76 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
(* Representation-level tests for object-field mutability state: the
2-
linkable [field_mutability] cells in [Tfield] (doc §7). These properties
2+
linkable [field_mutability] cells in [Tfield] (doc §6.7). These properties
33
are not observable from generated JavaScript, so they are tested here
44
directly against [Ctype]/[Btype].
55
@@ -149,9 +149,7 @@ let test_structure_generalized_occurrences_share _ =
149149
assert_bool "promotion is visible through the annotation itself"
150150
(flag_of annotated = Asttypes.Mutable)
151151

152-
(* ---- §7.4 Q1: every path that shares a mutability class between two
153-
owners also shares the row terminator node, so terminator genericity is
154-
a property of the sharing class and the copy policy is well defined. *)
152+
(* Copy-policy coverage for ordinary typing and substitution paths. *)
155153

156154
let terminator_of ty =
157155
let _, rest = Ctype.flatten_fields (Ctype.object_fields ty) in
@@ -173,22 +171,22 @@ let abstract_type_decl type_manifest : Types.type_declaration =
173171
type_inlined_types = [];
174172
}
175173

176-
let test_q1_unified_owners_share_terminator _ =
174+
let test_unified_owners_share_terminator _ =
177175
let a = obj_with_cell (immutable_cell ()) in
178176
let b = obj_with_cell ~closed:true (immutable_cell ()) in
179177
Ctype.unify Env.empty a b;
180178
assert_bool "unification makes both rows end at the same terminator node"
181179
(terminator_of a == terminator_of b)
182180

183-
let test_q1_shared_copy_shares_terminator _ =
181+
let test_shared_copy_shares_terminator _ =
184182
let annotated = obj_with_cell (immutable_cell ()) in
185183
Ctype.generalize_structure annotated;
186184
let occurrence = Ctype.instance Env.empty annotated in
187185
assert_bool "class shared" (cell_of occurrence == cell_of annotated);
188186
assert_bool "terminator shared"
189187
(terminator_of occurrence == terminator_of annotated)
190188

191-
let test_q1_generalized_instance_fresh_cell_fresh_terminator _ =
189+
let test_generalized_instance_fresh_cell_fresh_terminator _ =
192190
Ctype.begin_def ();
193191
let scheme = obj_with_cell (immutable_cell ()) in
194192
Ctype.end_def ();
@@ -197,7 +195,7 @@ let test_q1_generalized_instance_fresh_cell_fresh_terminator _ =
197195
assert_bool "class fresh" (cell_of inst != cell_of scheme);
198196
assert_bool "terminator fresh" (terminator_of inst != terminator_of scheme)
199197

200-
let test_q1_subst_generic_copy_gets_fresh_cell _ =
198+
let test_subst_generic_copy_gets_fresh_cell _ =
201199
Ctype.begin_def ();
202200
let scheme = obj_with_cell (immutable_cell ()) in
203201
Ctype.end_def ();
@@ -283,12 +281,10 @@ let test_nondep_failure_ends_copy_session _ =
283281
| Types.Mutability_value Asttypes.Immutable -> true
284282
| Types.Mutability_value Asttypes.Mutable | Types.Mutability_link _ -> false)
285283

286-
let test_saving_closed_row_resolves_links _ =
287-
(* Closed rows have no generic terminator, so saving shares the source's
288-
cell rather than duplicating it (safe: marshalling deep-copies). The
289-
shared cell must be the resolved representative — saved graphs never
290-
contain [Mutability_link], even when the source field's own ref is a
291-
link left by an earlier class merge. *)
284+
let test_saving_closed_row_gets_fresh_resolved_cell _ =
285+
(* A saved graph owns fresh cells even for closed rows. The copied cell must
286+
contain the resolved value: saved graphs never contain [Mutability_link],
287+
even when the source field's own ref is a merged-class link. *)
292288
let rep = immutable_cell () in
293289
let a = obj_with_cell ~closed:true (ref (Types.Mutability_link rep)) in
294290
assert_bool "the source field holds a link (a merged class member)"
@@ -301,7 +297,9 @@ let test_saving_closed_row_resolves_links _ =
301297
| Types.Mutability_value _ -> true
302298
| Types.Mutability_link _ -> false);
303299
assert_bool "the saved flag is the class value"
304-
(flag_of saved = Asttypes.Immutable)
300+
(flag_of saved = Asttypes.Immutable);
301+
assert_bool "the saved graph does not retain the source cell"
302+
(cell_of saved != cell_of a)
305303

306304
let test_saving_marshal_round_trip _ =
307305
(* The real persistence claim: after [for_saving] the graph marshals, and
@@ -350,6 +348,56 @@ let test_saving_preserves_class_sharing _ =
350348
| Types.Mutability_value _ -> true
351349
| Types.Mutability_link _ -> false)
352350

351+
let test_for_saving_copy_order_is_irrelevant _ =
352+
(* [generalize_structure] makes the field spine generic while leaving its
353+
open-row terminator non-generic. [for_saving] makes the copied terminator
354+
generic. If the two graphs still share one mutability cell, copying them
355+
in one session can then choose different policies for that cell. *)
356+
Ctype.begin_def ();
357+
let source = obj_with_cell (immutable_cell ()) in
358+
Ctype.end_def ();
359+
Ctype.generalize_structure source;
360+
let saved = Subst.type_expr (Subst.for_saving Subst.identity) source in
361+
assert_bool "the fixture has different row-copy classifications"
362+
((terminator_of source).level <> Btype.generic_level
363+
&& (terminator_of saved).level = Btype.generic_level);
364+
assert_bool "for_saving gives the copied graph an independent class"
365+
(cell_of source != cell_of saved);
366+
let copy_pair first second =
367+
match Ctype.instance_list Env.empty [first; second] with
368+
| [first'; second'] -> (first', second')
369+
| _ -> OUnit.assert_failure "expected two copied object types"
370+
in
371+
let source_first, saved_second = copy_pair source saved in
372+
let saved_first, source_second = copy_pair saved source in
373+
let source_first_shares = cell_of source_first == cell_of saved_second in
374+
let saved_first_shares = cell_of saved_first == cell_of source_second in
375+
assert_bool "source-first copies are separate" (not source_first_shares);
376+
assert_bool "saved-first copies are separate" (not saved_first_shares);
377+
assert_bool
378+
"copying owners of one class must not depend on their order in the session"
379+
(source_first_shares = saved_first_shares)
380+
381+
let test_for_saving_fresh_copy_preserves_internal_aliasing _ =
382+
Ctype.begin_def ();
383+
let cell = immutable_cell () in
384+
let source =
385+
Ctype.newty (Types.Ttuple [obj_with_cell cell; obj_with_cell cell])
386+
in
387+
Ctype.end_def ();
388+
Ctype.generalize_structure source;
389+
let saved = Subst.type_expr (Subst.for_saving Subst.identity) source in
390+
let source_a, source_b, saved_a, saved_b =
391+
match ((Btype.repr source).desc, (Btype.repr saved).desc) with
392+
| Types.Ttuple [source_a; source_b], Types.Ttuple [saved_a; saved_b] ->
393+
(source_a, source_b, saved_a, saved_b)
394+
| _ -> OUnit.assert_failure "expected source and saved object pairs"
395+
in
396+
assert_bool "the source aliases share one class"
397+
(cell_of source_a == cell_of source_b);
398+
assert_bool "the saved aliases share one fresh class"
399+
(cell_of saved_a == cell_of saved_b && cell_of saved_a != cell_of source_a)
400+
353401
let suites =
354402
__FILE__
355403
>::: [
@@ -365,23 +413,26 @@ let suites =
365413
>:: test_generalized_instance_preserves_internal_aliasing;
366414
"structure_generalized_occurrences_share"
367415
>:: test_structure_generalized_occurrences_share;
368-
"q1_unified_owners_share_terminator"
369-
>:: test_q1_unified_owners_share_terminator;
370-
"q1_shared_copy_shares_terminator"
371-
>:: test_q1_shared_copy_shares_terminator;
372-
"q1_generalized_instance_fresh_cell_fresh_terminator"
373-
>:: test_q1_generalized_instance_fresh_cell_fresh_terminator;
374-
"q1_subst_generic_copy_gets_fresh_cell"
375-
>:: test_q1_subst_generic_copy_gets_fresh_cell;
416+
"unified_owners_share_terminator"
417+
>:: test_unified_owners_share_terminator;
418+
"shared_copy_shares_terminator" >:: test_shared_copy_shares_terminator;
419+
"generalized_instance_fresh_cell_fresh_terminator"
420+
>:: test_generalized_instance_fresh_cell_fresh_terminator;
421+
"subst_generic_copy_gets_fresh_cell"
422+
>:: test_subst_generic_copy_gets_fresh_cell;
376423
"nondep_type_ends_its_copy_session"
377424
>:: test_nondep_type_ends_its_copy_session;
378425
"nondep_nested_copy_preserves_class_sharing"
379426
>:: test_nondep_nested_copy_preserves_class_sharing;
380427
"nondep_failure_ends_copy_session"
381428
>:: test_nondep_failure_ends_copy_session;
382-
"saving_closed_row_resolves_links"
383-
>:: test_saving_closed_row_resolves_links;
429+
"saving_closed_row_gets_fresh_resolved_cell"
430+
>:: test_saving_closed_row_gets_fresh_resolved_cell;
384431
"saving_marshal_round_trip" >:: test_saving_marshal_round_trip;
385432
"saving_preserves_class_sharing"
386433
>:: test_saving_preserves_class_sharing;
434+
"for_saving_copy_order_is_irrelevant"
435+
>:: test_for_saving_copy_order_is_irrelevant;
436+
"for_saving_fresh_copy_preserves_internal_aliasing"
437+
>:: test_for_saving_fresh_copy_preserves_internal_aliasing;
387438
]

0 commit comments

Comments
 (0)