Merge pull request #13138 from gasche/matching-bug-propagate-mut-2

+71 -32

2 changed files

expand all

Changes

lambda

matching.ml

+3 -2

Changes

··· 57 57 unsupported native backends (POWER, riscv64 and s390x) 58 58 (Miod Vallat, review by Nicolás Ojeda Bär) 59 59 60 - - #7241, #12555: fix a soundness bug in the pattern-matching compiler 61 - when side-effects mutate the scrutinee during matching. 60 + - #7241, #12555, #13076, #13138: fix a soundness bug in the 61 + pattern-matching compiler when side-effects mutate the scrutinee 62 + during matching. 62 63 Note that #7241 is not fully fixed yet, see the issue for the 63 64 current status. 64 65 (Gabriel Scherer, review by Nick Roberts)

+68 -30

lambda/matching.ml

··· 1047 1047 type 'a arg = { 1048 1048 arg : 'a; 1049 1049 binding_kind : let_kind; 1050 + mut : mutable_flag; 1051 + (** We track with a [mutable_flag] whether a mutable read was 1052 + performed to access the corresponding sub-value of the 1053 + scrutinee: an argument is [Mutable] if the path from the root of 1054 + the value to the argument contains a mutable field. More 1055 + precisely, a position is considered [Mutable] when accesses to 1056 + the same position in different branches of the pattern 1057 + matching -- outside the scope of the strict binding generated 1058 + for the mutable read -- may observe a different value. *) 1050 1059 } 1051 1060 1052 1061 type args = lambda arg list ··· 1087 1096 handlers : handler list; 1088 1097 or_matrix : 'matrix 1089 1098 } 1099 + 1100 + 1101 + (* The composed mutability of two argument positions: 1102 + is x.f.g a mutable position of x, depending whether f and g are mutable? 1103 + 1104 + Note that the following equations hold: 1105 + - compose_mut mut Immutable = mut 1106 + - compose_mut mut Mutable = Mutable 1107 + but we do *not* use them in the code of get_expr_args_* below. We prefer 1108 + to call [compose_mut] explicitly to make the logic more regular, make 1109 + it obvious that we thought about how this value should evolve (or not). 1110 + *) 1111 + let compose_mut m1 m2 = 1112 + match m1, m2 with 1113 + | Immutable, Immutable -> Immutable 1114 + | Mutable, _ | _, Mutable -> Mutable 1090 1115 1091 1116 (* Pattern matching after application of both the or-pat rule and the 1092 1117 mixture rule *) ··· 1601 1626 1602 1627 If the rest doesn't generate any split, abort and do_not_precompile. *) 1603 1628 match args.rest with 1604 - | { arg = Lvar v; binding_kind } :: rargs -> ( 1629 + | { arg = Lvar v; _ } as first :: rargs -> ( 1605 1630 (* We will use the name of the head column of the submatrix 1606 1631 we compile, and this is the *second* column of our argument. *) 1607 1632 match cls with ··· 1610 1635 do_not_precompile args cls def k 1611 1636 | _ -> ( 1612 1637 (* Precompile *) 1613 - let var_args = { 1614 - first = { arg = Var v; binding_kind }; 1615 - rest = rargs; 1616 - } in 1638 + let var_args = { first = { first with arg = Var v }; rest = rargs } in 1617 1639 let var_cls = 1618 1640 List.map 1619 1641 (fun ((p, ps), act) -> 1620 1642 assert (simple_omega_like p); 1621 - 1622 1643 (* we learned by pattern-matching on [args] 1623 1644 that [p::ps] has at least two arguments, 1624 1645 so [ps] must be non-empty *) ··· 1844 1865 (** a submatrix after specializing by discriminant pattern; 1845 1866 [ctx] is the context shared by all rows. *) 1846 1867 1847 - let make_matching get_expr_args head def ctx { first = { arg; _ }; rest } = 1848 - let def = Default_environment.specialize head def 1849 - and args = get_expr_args head (arg_of_pure arg) rest 1850 - and ctx = Context.specialize head ctx in 1868 + let make_matching get_expr_args head def ctx { first; rest } = 1869 + let def = Default_environment.specialize head def in 1870 + let first = { first with arg = arg_of_pure first.arg } in 1871 + let args = get_expr_args head first rest in 1872 + let ctx = Context.specialize head ctx in 1851 1873 { pm = { cases = []; args; default = def }; ctx; discr = head } 1852 1874 1853 - let make_line_matching get_expr_args head def { first = { arg; _ }; rest } = 1875 + let make_line_matching get_expr_args head def { first; rest } = 1876 + let first = { first with arg = arg_of_pure first.arg } in 1854 1877 { cases = []; 1855 - args = get_expr_args head (arg_of_pure arg) rest; 1878 + args = get_expr_args head first rest; 1856 1879 default = Default_environment.specialize head def 1857 1880 } 1858 1881 ··· 1947 1970 | { pat_desc = Tpat_construct (_, _, args, _) } -> args @ rem 1948 1971 | _ -> assert false 1949 1972 1950 - let get_expr_args_constr ~scopes head arg rem = 1973 + let get_expr_args_constr ~scopes head { arg; mut; _ } rem = 1951 1974 let cstr = 1952 1975 match head.pat_desc with 1953 1976 | Patterns.Head.Construct cstr -> cstr ··· 1961 1984 else 1962 1985 { 1963 1986 arg = Lprim (Pfield (pos, Pointer, Immutable), [ arg ], loc); 1987 + mut = compose_mut mut Immutable; 1964 1988 binding_kind; 1965 1989 } :: make_args (pos + 1) 1966 1990 in 1967 1991 make_args first_pos 1968 1992 in 1969 1993 if cstr.cstr_inlined <> None then 1970 - { arg; binding_kind = Alias } :: rem 1994 + { arg; binding_kind = Alias; mut } :: rem 1971 1995 else 1972 1996 match cstr.cstr_tag with 1973 1997 | Cstr_constant _ 1974 1998 | Cstr_block _ -> 1975 1999 make_field_accesses Alias 0 (cstr.cstr_arity - 1) rem 1976 - | Cstr_unboxed -> { arg; binding_kind = Alias } :: rem 2000 + | Cstr_unboxed -> { arg; binding_kind = Alias; mut } :: rem 1977 2001 | Cstr_extension _ -> make_field_accesses Alias 1 cstr.cstr_arity rem 1978 2002 1979 2003 let divide_constructor ~scopes ctx pm = ··· 1988 2012 1989 2013 let get_expr_args_variant_constant = drop_expr_arg 1990 2014 1991 - let get_expr_args_variant_nonconst ~scopes head arg rem = 2015 + let get_expr_args_variant_nonconst ~scopes head { arg; mut; _ } rem = 1992 2016 let loc = head_loc ~scopes head in 1993 2017 { 1994 2018 arg = Lprim (Pfield (1, Pointer, Immutable), [ arg ], loc); 1995 2019 binding_kind = Alias; 2020 + mut = compose_mut mut Immutable; 1996 2021 } :: rem 1997 2022 1998 2023 let divide_variant ~scopes row ctx { cases = cl; args; default = def } = ··· 2185 2210 tables (~ 250 elts); conditionals are better *) 2186 2211 inline_lazy_force_cond arg loc 2187 2212 2188 - let get_expr_args_lazy ~scopes head arg rem = 2213 + let get_expr_args_lazy ~scopes head { arg; mut; _ } rem = 2189 2214 let loc = head_loc ~scopes head in 2190 2215 { 2191 2216 arg = inline_lazy_force arg loc; 2192 2217 binding_kind = Strict; 2218 + mut = compose_mut mut Immutable; 2219 + (* A lazy pattern is considered immutable, forcing its argument 2220 + always returns the same value. *) 2193 2221 } :: rem 2194 2222 2195 2223 let divide_lazy ~scopes head ctx pm = ··· 2206 2234 | { pat_desc = Tpat_tuple args } -> args @ rem 2207 2235 | _ -> assert false 2208 2236 2209 - let get_expr_args_tuple ~scopes head arg rem = 2237 + let get_expr_args_tuple ~scopes head { arg; mut; _ } rem = 2210 2238 let loc = head_loc ~scopes head in 2211 2239 let arity = Patterns.Head.arity head in 2212 2240 let rec make_args pos = ··· 2216 2244 { 2217 2245 arg = Lprim (Pfield (pos, Pointer, Immutable), [ arg ], loc); 2218 2246 binding_kind = Alias; 2247 + mut = compose_mut mut Immutable; 2219 2248 } :: make_args (pos + 1) 2220 2249 in 2221 2250 make_args 0 ··· 2241 2270 record_matching_line num_fields lbl_pat_list @ rem 2242 2271 | _ -> assert false 2243 2272 2244 - let get_expr_args_record ~scopes head arg rem = 2273 + let get_expr_args_record ~scopes head { arg; mut; _ } rem = 2245 2274 let loc = head_loc ~scopes head in 2246 2275 let all_labels = 2247 2276 let open Patterns.Head in ··· 2272 2301 | Immutable -> Alias 2273 2302 | Mutable -> StrictOpt 2274 2303 in 2275 - { arg = access; binding_kind } :: make_args (pos + 1) 2304 + { 2305 + arg = access; 2306 + binding_kind; 2307 + mut = compose_mut mut lbl.lbl_mut; 2308 + } :: make_args (pos + 1) 2276 2309 in 2277 2310 make_args 0 2278 2311 ··· 2299 2332 | { pat_desc = Tpat_array patl } -> patl @ rem 2300 2333 | _ -> assert false 2301 2334 2302 - let get_expr_args_array ~scopes kind head arg rem = 2335 + let get_expr_args_array ~scopes kind head { arg; mut; _ } rem = 2303 2336 let len = 2304 2337 let open Patterns.Head in 2305 2338 match head.pat_desc with ··· 2319 2352 { 2320 2353 arg; 2321 2354 binding_kind = StrictOpt; 2355 + mut = compose_mut mut Mutable; 2322 2356 } :: make_args (pos + 1) 2323 2357 in 2324 2358 make_args 0 ··· 3568 3602 (m : (args, Typedtree.pattern Non_empty_row.t clause) pattern_matching) = 3569 3603 match m with 3570 3604 | { cases = []; args = [] } -> comp_exit ctx m.default 3571 - | { args = { arg; binding_kind } :: rest } -> 3605 + | { args = { arg; binding_kind; _ } as first :: rest } -> 3572 3606 let v = arg_to_var arg m.cases in 3573 3607 bind_match_arg binding_kind v arg ( 3574 - let args = { first = { arg = Var v; binding_kind = Alias }; rest } in 3608 + let args = { first = { first with arg = Var v }; rest } in 3575 3609 let cases = List.map (half_simplify_nonempty ~arg:(Lvar v)) m.cases in 3576 3610 let m = { m with args; cases } in 3577 3611 let first_match, rem = ··· 3877 3911 Lstaticcatch (lam, (final_exit, []), 3878 3912 failure_handler ~scopes loc ~failer ()) 3879 3913 end 3914 + 3915 + let root_arg arg binding_kind = 3916 + (* The mutability information denotes the mutability of a *position* 3917 + inside the value, which indicates whether looking inside the 3918 + value of the scrutinee is a pure operation. At the root we are 3919 + immutable. *) 3920 + { arg; binding_kind; mut = Immutable } 3880 3921 3881 3922 let compile_matching ~scopes loc ~failer repr arg pat_act_list partial = 3882 3923 let partial = check_partial pat_act_list partial in 3883 - let args = [ { arg; binding_kind = Strict } ] in 3924 + let args = [ root_arg arg Strict ] in 3884 3925 let rows = map_on_rows (fun pat -> (pat, [])) pat_act_list in 3885 3926 let handler = 3886 3927 toplevel_handler ~scopes loc ~failer partial args rows ··· 4084 4125 (* Easy case since variables are available *) 4085 4126 let for_tupled_function ~scopes loc paraml pats_act_list partial = 4086 4127 let partial = check_partial_list pats_act_list partial in 4087 - let args = 4088 - List.map (fun id -> { arg = Lvar id; binding_kind = Strict }) paraml in 4128 + let args = List.map (fun id -> root_arg (Lvar id) Strict) paraml in 4089 4129 let handler = 4090 4130 toplevel_handler ~scopes loc ~failer:Raise_match_failure 4091 4131 partial args pats_act_list in ··· 4170 4210 let sloc = Scoped_location.of_location ~scopes loc in 4171 4211 let args = List.map (fun id -> Lvar id) idl in 4172 4212 Lprim (Pmakeblock (0, Immutable, None), args, sloc) in 4173 - let input_args = 4174 - { first = { arg = Tuple arg; binding_kind = Strict }; rest = [] } in 4213 + let input_args = { first = root_arg (Tuple arg) Strict; rest = [] } in 4175 4214 let handler = 4176 4215 let partial = check_partial pat_act_list partial in 4177 4216 let rows = map_on_rows (fun p -> (p, [])) pat_act_list in ··· 4184 4223 in 4185 4224 let next, nexts = split_and_precompile_half_simplified pm1_half in 4186 4225 let size = List.length idl in 4187 - let args = 4188 - List.map (fun id -> { arg = Lvar id; binding_kind = Alias }) idl in 4226 + let args = List.map (fun id -> root_arg (Lvar id) Alias) idl in 4189 4227 let flat_next = flatten_precompiled size args next 4190 4228 and flat_nexts = 4191 4229 List.map (fun (e, pm) -> (e, flatten_precompiled size args pm)) nexts

Configure Feed

Configure Feed