Skip to content

Commit 008e42d

Browse files
anfelorgoldfirere
anfelor
and
goldfirere
authored
Consume patterns that do not have a working unique barrier yet (#3335)
* Consume patterns that do not have a working unique barrier yet * Add comment by @goldfirere Co-authored-by: Richard Eisenberg <rae@richarde.dev> * Add more comments to explain what a memory access is --------- Co-authored-by: Richard Eisenberg <rae@richarde.dev>
1 parent 5d8f1aa commit 008e42d

File tree

2 files changed

+195
-88
lines changed

2 files changed

+195
-88
lines changed

‎testsuite/tests/typing-unique/unique.ml

+74-2
Original file line numberDiff line numberDiff line change
@@ -597,10 +597,18 @@ let array_pats (arr : int option array) =
597597
| [| o |] -> let _ = unique_id arr in aliased_id o
598598
| _ -> None
599599
[%%expect{|
600-
val array_pats : int option array @ unique -> int option = <fun>
600+
Line 3, characters 33-36:
601+
3 | | [| o |] -> let _ = unique_id arr in aliased_id o
602+
^^^
603+
Error: This value is used here as unique,
604+
but it has already been used in an array pattern:
605+
Line 3, characters 4-11:
606+
3 | | [| o |] -> let _ = unique_id arr in aliased_id o
607+
^^^^^^^
608+
601609
|}]
602610
603-
let array_pats (arr : int option iarray) =
611+
let iarray_pats (arr : int option iarray) =
604612
match arr with
605613
| [: o :] -> let _ = unique_id arr in unique_id o
606614
| _ -> None
@@ -622,3 +630,67 @@ let shadow x =
622630
[%%expect{|
623631
val shadow : 'a -> 'a * (int * int) = <fun>
624632
|}]
633+
634+
let array_pat_barrier (arr : int option array) =
635+
match arr with
636+
| [| _ |] -> unique_id arr
637+
| _ -> [| None |]
638+
[%%expect{|
639+
Line 3, characters 25-28:
640+
3 | | [| _ |] -> unique_id arr
641+
^^^
642+
Error: This value is used here as unique,
643+
but it has already been used in an array pattern:
644+
Line 3, characters 4-11:
645+
3 | | [| _ |] -> unique_id arr
646+
^^^^^^^
647+
648+
|}]
649+
650+
let iarray_pat_barrier (arr : int option iarray) =
651+
match arr with
652+
| [: _ :] -> unique_id arr
653+
| _ -> [: None :]
654+
[%%expect{|
655+
Line 3, characters 25-28:
656+
3 | | [: _ :] -> unique_id arr
657+
^^^
658+
Error: This value is used here as unique,
659+
but it has already been used in an array pattern:
660+
Line 3, characters 4-11:
661+
3 | | [: _ :] -> unique_id arr
662+
^^^^^^^
663+
664+
|}]
665+
666+
let constant_pat_barrier (opt : int option) =
667+
match opt with
668+
| Some 1 -> unique_id opt
669+
| _ -> None
670+
[%%expect{|
671+
Line 3, characters 24-27:
672+
3 | | Some 1 -> unique_id opt
673+
^^^
674+
Error: This value is used here as unique,
675+
but part of it has already been used in a constant pattern:
676+
Line 3, characters 9-10:
677+
3 | | Some 1 -> unique_id opt
678+
^
679+
680+
|}]
681+
682+
let lazy_pat_barrier (l : int Lazy.t) =
683+
match l with
684+
| lazy 1 -> unique_id l
685+
| _ -> lazy 2
686+
[%%expect{|
687+
Line 3, characters 24-25:
688+
3 | | lazy 1 -> unique_id l
689+
^
690+
Error: This value is used here as unique,
691+
but it has already been used in a lazy pattern:
692+
Line 3, characters 4-10:
693+
3 | | lazy 1 -> unique_id l
694+
^^^^^^
695+
696+
|}]

‎typing/uniqueness_analysis.ml

+121-86
Original file line numberDiff line numberDiff line change
@@ -227,8 +227,10 @@ module Aliased : sig
227227
type t
228228

229229
type reason =
230-
| Forced (** aliased because forced *)
231-
| Lazy (** aliased because it is the argument of lazy forcing *)
230+
| Forced (** aliased because forced due to multiple usage *)
231+
| Lazy (** aliased because of a lazy pattern *)
232+
| Array (** aliased because of an array pattern *)
233+
| Constant (** aliased because of an constant pattern *)
232234
| Lifted of Maybe_aliased.access
233235
(** aliased because lifted from implicit borrowing, carries the original
234236
access *)
@@ -246,6 +248,8 @@ end = struct
246248
type reason =
247249
| Forced
248250
| Lazy
251+
| Array
252+
| Constant
249253
| Lifted of Maybe_aliased.access
250254

251255
type t = Occurrence.t * reason
@@ -261,6 +265,8 @@ end = struct
261265
let print_reason ppf = function
262266
| Forced -> fprintf ppf "Forced"
263267
| Lazy -> fprintf ppf "Lazy"
268+
| Array -> fprintf ppf "Array"
269+
| Constant -> fprintf ppf "Constant"
264270
| Lifted ma -> fprintf ppf "Lifted(%a)" Maybe_aliased.print_access ma
265271
in
266272
fprintf ppf "(%a,%a)" Occurrence.print occ print_reason reason
@@ -1819,82 +1825,121 @@ let rec pattern_match_tuple pat values =
18191825
let ext, uf' = pattern_match_single pat paths in
18201826
ext, UF.seq uf uf'
18211827

1822-
and pattern_match_single pat paths : Ienv.Extension.t * UF.t =
1828+
(** This function ensures the soundness of pattern-matching in the presence
1829+
of destructive updates on the memory that was matched on.
1830+
If the pattern-match reads from the underlying memory, we need to ensure
1831+
either that the memory access is not pushed down or that no destructive
1832+
updates can be performed on the memory.
1833+
Reads from the underlying memory occur when the pattern has to inspect the
1834+
tag or content of the memory to decide whether a branch should be taken
1835+
as well as when binding the contents of a subpattern to a name.
1836+
1837+
Each pattern falls into one of three cases:
1838+
- If we do not read from the underlying memory,
1839+
we do not have to take an action.
1840+
- We can allow destructive updates later on by borrowing the
1841+
memory address. Then we have to protect the read from getting
1842+
pushed down using a unique barrier.
1843+
- We can disallow any destructive updates following the read
1844+
by consuming the memory address as aliased.
1845+
1846+
[pattern_match_single] recurs down the structure of the pattern,
1847+
calling [pattern_match_barrier] at each step, so [pattern_match_barrier]
1848+
itself does not need to recur into subpatterns. *)
1849+
and pattern_match_barrier pat paths : UF.t =
18231850
let loc = pat.pat_loc in
18241851
let occ = Occurrence.mk loc in
1825-
(* To read from the allocation, we need to borrow its memory cell
1826-
and set the unique_barrier. However, we do not read in every case,
1827-
since the user might want use a wildcard for already-consumed data. *)
1828-
let no_borrow_memory_address () =
1829-
Unique_barrier.enable pat.pat_unique_barrier;
1830-
ignore (Unique_barrier.resolve pat.pat_unique_barrier)
1852+
Unique_barrier.enable pat.pat_unique_barrier;
1853+
let no_memory_access () =
1854+
ignore (Unique_barrier.resolve pat.pat_unique_barrier);
1855+
UF.unused
18311856
in
18321857
let borrow_memory_address () =
1833-
Unique_barrier.enable pat.pat_unique_barrier;
18341858
Paths.mark_implicit_borrow_memory_address occ (Read pat.pat_unique_barrier)
18351859
paths
18361860
in
1861+
let consume_memory_address reason =
1862+
ignore (Unique_barrier.resolve pat.pat_unique_barrier);
1863+
Paths.mark_aliased occ reason paths
1864+
in
18371865
match pat.pat_desc with
1838-
| Tpat_or (pat0, pat1, _) ->
1839-
no_borrow_memory_address ();
1840-
let ext0, uf0 = pattern_match_single pat0 paths in
1841-
let ext1, uf1 = pattern_match_single pat1 paths in
1842-
Ienv.Extension.disjunct ext0 ext1, UF.choose uf0 uf1
1843-
| Tpat_any ->
1844-
no_borrow_memory_address ();
1845-
Ienv.Extension.empty, UF.unused
1846-
| Tpat_var (id, _, _, _) ->
1847-
no_borrow_memory_address ();
1848-
Ienv.Extension.singleton id paths, UF.unused
1849-
| Tpat_alias (pat', id, _, _, _) ->
1850-
no_borrow_memory_address ();
1851-
let ext0 = Ienv.Extension.singleton id paths in
1852-
let ext1, uf = pattern_match_single pat' paths in
1853-
Ienv.Extension.conjunct ext0 ext1, uf
1866+
| Tpat_or _ -> no_memory_access ()
1867+
| Tpat_any -> no_memory_access ()
1868+
| Tpat_var _ -> no_memory_access ()
1869+
| Tpat_alias _ -> no_memory_access ()
18541870
| Tpat_constant _ ->
1855-
let uf_read = borrow_memory_address () in
1856-
Ienv.Extension.empty, uf_read
1857-
| Tpat_construct (lbl, cd, pats, _) ->
1858-
let uf_tag =
1859-
Paths.learn_tag { tag = cd.cstr_tag; name_for_error = lbl } paths
1860-
in
1861-
let uf_read = borrow_memory_address () in
1862-
let pats_args = List.combine pats cd.cstr_args in
1863-
let ext, uf_pats =
1864-
List.mapi
1865-
(fun i (pat, { Types.ca_modalities = gf; _ }) ->
1866-
let name = Longident.last lbl.txt in
1867-
let paths = Paths.construct_field gf name i paths in
1868-
pattern_match_single pat paths)
1869-
pats_args
1870-
|> conjuncts_pattern_match
1871-
in
1872-
ext, UF.pars [uf_tag; uf_read; uf_pats]
1873-
| Tpat_variant (lbl, arg, _) ->
1874-
let uf_read = borrow_memory_address () in
1875-
let ext, uf_arg =
1871+
(* This is necessary since we can not guarantee that
1872+
the reads of constants in the pattern-matching code
1873+
are never pushed down.
1874+
CR uniqueness: We can probably use [borrow_memory_address]
1875+
for certain constants (eg. integers) here. *)
1876+
consume_memory_address Constant
1877+
| Tpat_construct _ -> borrow_memory_address ()
1878+
| Tpat_variant _ -> borrow_memory_address ()
1879+
| Tpat_record _ -> borrow_memory_address ()
1880+
| Tpat_array _ ->
1881+
(* This is necessary since we do not yet guarantee that
1882+
the reads of arrays in the pattern-matching code
1883+
are never pushed down.
1884+
CR uniqueness: we should add a unique barrier to array reads
1885+
and change this to use [borrow_memory_address] as well. *)
1886+
consume_memory_address Array
1887+
| Tpat_lazy _ ->
1888+
(* Lazy patterns consume their memory anyway since
1889+
forcing a lazy expression is like calling a nullary-function *)
1890+
consume_memory_address Lazy
1891+
| Tpat_tuple _ -> borrow_memory_address ()
1892+
| Tpat_unboxed_tuple _ ->
1893+
(* unboxed tuples are not allocations *)
1894+
no_memory_access ()
1895+
| Tpat_record_unboxed_product _ ->
1896+
(* unboxed records are not allocations *)
1897+
no_memory_access ()
1898+
1899+
and pattern_match_single pat paths : Ienv.Extension.t * UF.t =
1900+
let uf_read = pattern_match_barrier pat paths in
1901+
let ext, uf_pats =
1902+
match pat.pat_desc with
1903+
| Tpat_or (pat0, pat1, _) ->
1904+
let ext0, uf0 = pattern_match_single pat0 paths in
1905+
let ext1, uf1 = pattern_match_single pat1 paths in
1906+
Ienv.Extension.disjunct ext0 ext1, UF.choose uf0 uf1
1907+
| Tpat_any -> Ienv.Extension.empty, UF.unused
1908+
| Tpat_var (id, _, _, _) -> Ienv.Extension.singleton id paths, UF.unused
1909+
| Tpat_alias (pat', id, _, _, _) ->
1910+
let ext0 = Ienv.Extension.singleton id paths in
1911+
let ext1, uf = pattern_match_single pat' paths in
1912+
Ienv.Extension.conjunct ext0 ext1, uf
1913+
| Tpat_constant _ -> Ienv.Extension.empty, UF.unused
1914+
| Tpat_construct (lbl, cd, pats, _) ->
1915+
let uf_tag =
1916+
Paths.learn_tag { tag = cd.cstr_tag; name_for_error = lbl } paths
1917+
in
1918+
let pats_args = List.combine pats cd.cstr_args in
1919+
let ext, uf_pats =
1920+
List.mapi
1921+
(fun i (pat, { Types.ca_modalities = gf; _ }) ->
1922+
let name = Longident.last lbl.txt in
1923+
let paths = Paths.construct_field gf name i paths in
1924+
pattern_match_single pat paths)
1925+
pats_args
1926+
|> conjuncts_pattern_match
1927+
in
1928+
ext, UF.par uf_tag uf_pats
1929+
| Tpat_variant (lbl, arg, _) -> (
18761930
match arg with
18771931
| Some arg ->
18781932
let paths = Paths.variant_field lbl paths in
18791933
pattern_match_single arg paths
1880-
| None -> Ienv.Extension.empty, UF.unused
1881-
in
1882-
ext, UF.pars [uf_read; uf_arg]
1883-
| Tpat_record (pats, _) ->
1884-
let uf_read = borrow_memory_address () in
1885-
let ext, uf_pats =
1934+
| None -> Ienv.Extension.empty, UF.unused)
1935+
| Tpat_record (pats, _) ->
18861936
List.map
18871937
(fun (_, l, pat) ->
18881938
let paths = Paths.record_field l.lbl_modalities l.lbl_name paths in
18891939
pattern_match_single pat paths)
18901940
pats
18911941
|> conjuncts_pattern_match
1892-
in
1893-
ext, UF.par uf_read uf_pats
1894-
| Tpat_record_unboxed_product (pats, _) ->
1895-
(* No borrow since unboxed data can not be consumed. *)
1896-
no_borrow_memory_address ();
1897-
let ext, uf_pats =
1942+
| Tpat_record_unboxed_product (pats, _) ->
18981943
List.map
18991944
(fun (_, l, pat) ->
19001945
let paths =
@@ -1903,50 +1948,37 @@ and pattern_match_single pat paths : Ienv.Extension.t * UF.t =
19031948
pattern_match_single pat paths)
19041949
pats
19051950
|> conjuncts_pattern_match
1906-
in
1907-
ext, uf_pats
1908-
| Tpat_array (mut, _, pats) ->
1909-
let uf_read = borrow_memory_address () in
1910-
let ext, uf_pats =
1951+
| Tpat_array (mut, _, pats) ->
19111952
List.mapi
19121953
(fun idx pat ->
19131954
let paths = Paths.array_index mut idx paths in
19141955
pattern_match_single pat paths)
19151956
pats
19161957
|> conjuncts_pattern_match
1917-
in
1918-
ext, UF.par uf_read uf_pats
1919-
| Tpat_lazy arg ->
1920-
no_borrow_memory_address ();
1921-
(* forced below: *)
1922-
(* forcing a lazy expression is like calling a nullary-function *)
1923-
let uf_force = Paths.mark_aliased occ Lazy paths in
1924-
let paths = Paths.fresh () in
1925-
let ext, uf_arg = pattern_match_single arg paths in
1926-
ext, UF.par uf_force uf_arg
1927-
| Tpat_tuple args ->
1928-
let uf_read = borrow_memory_address () in
1929-
let ext, uf_args =
1958+
| Tpat_lazy arg ->
1959+
(* forcing a lazy expression is like calling a nullary-function *)
1960+
let loc = pat.pat_loc in
1961+
let occ = Occurrence.mk loc in
1962+
let uf_force = Paths.mark_aliased occ Lazy paths in
1963+
let ext, uf_arg = pattern_match_single arg (Paths.fresh ()) in
1964+
ext, UF.par uf_force uf_arg
1965+
| Tpat_tuple args ->
19301966
List.mapi
19311967
(fun i (_, arg) ->
19321968
let paths = Paths.tuple_field i paths in
19331969
pattern_match_single arg paths)
19341970
args
19351971
|> conjuncts_pattern_match
1936-
in
1937-
ext, UF.par uf_read uf_args
1938-
| Tpat_unboxed_tuple args ->
1939-
(* No borrow since unboxed data can not be consumed. *)
1940-
no_borrow_memory_address ();
1941-
let ext, uf_args =
1972+
| Tpat_unboxed_tuple args ->
1973+
(* No borrow since unboxed data can not be consumed. *)
19421974
List.mapi
19431975
(fun i (_, arg, _) ->
19441976
let paths = Paths.tuple_field i paths in
19451977
pattern_match_single arg paths)
19461978
args
19471979
|> conjuncts_pattern_match
1948-
in
1949-
ext, uf_args
1980+
in
1981+
ext, UF.par uf_read uf_pats
19501982

19511983
let pattern_match pat = function
19521984
| Match_tuple values -> pattern_match_tuple pat values
@@ -2535,7 +2567,10 @@ let report_multi_use inner first_is_of_second =
25352567
Maybe_aliased.string_of_access (Maybe_aliased.extract_access t)
25362568
| Usage.Aliased t -> (
25372569
match Aliased.reason t with
2538-
| Forced | Lazy -> "used"
2570+
| Forced -> "used"
2571+
| Lazy -> "used in a lazy pattern"
2572+
| Array -> "used in an array pattern"
2573+
| Constant -> "used in a constant pattern"
25392574
| Lifted access ->
25402575
Maybe_aliased.string_of_access access
25412576
^ " in a closure that might be called later")

0 commit comments

Comments
 (0)