-
Notifications
You must be signed in to change notification settings - Fork 125
/
pass_CheckPatternMatching.ml
310 lines (285 loc) · 9.56 KB
/
pass_CheckPatternMatching.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
(*
Copyright © 2011 MLstate
This file is part of OPA.
OPA is free software: you can redistribute it and/or modify it under the
terms of the GNU Affero General Public License, version 3, as published by
the Free Software Foundation.
OPA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
more details.
You should have received a copy of the GNU Affero General Public License
along with OPA. If not, see <http://www.gnu.org/licenses/>.
*)
(* depends *)
module List = Base.List
let (|>) x f = f x
(* alias *)
module Q = QmlAst
(* refactoring in progress *)
(*
Utils
*)
let wclass = WarningClass.pattern
let dead =
let doc = "A branch of a match can never be matched" in
WarningClass.create ~parent:wclass ~name:"dead" ~doc ~err:true ~enable:true ()
let obfuscation =
let doc = "A variable matching an expr of a sum type is nammed like one of the sum case" in
WarningClass.create ~parent:wclass ~name:"obfuscation" ~doc ~err:true ~enable:true ()
let warning_set =
WarningClass.Set.create_from_list [
wclass;
]
let is_label_in_simple_case searched_label annotkey annotmap gamma =
match QmlAnnotMap.find_ty_opt annotkey annotmap with
| None -> false
| Some ty -> (
(* We are only interrested in sum types. But in case of names type, we
must first get its effective representation. *)
match QmlTypesUtils.Inspect.follow_alias_noopt gamma ty with
| QmlAst.TypeSum (QmlAst.TyCol (cases, _)) ->
List.exists
(fun case_fields ->
(* For each case of the sum, i.e. each list of fields of this
case, we check if the searched label belongs to list of
fields of this case. We stop searching as soon as we find a
positive hit. *)
List.exists
(fun (lbl, lbl_ty) ->
(* Found if the labels have the same name and the type of
this label is the empty record. Attention, we must
unwind named types before testing. *)
(lbl = searched_label) &&
(match QmlTypesUtils.Inspect.follow_alias_noopt gamma lbl_ty with
| QmlAst.TypeRecord (QmlAst.TyRow ([], None)) -> true
| _ -> false))
case_fields)
cases
| _ -> false
)
(*
Imperative simplification:
[gamma] and [annotmap] are available as global variables.
It is simplier to proced so, instead of passing [gamma] and [annotmap] around.
The [free_gamma_annotmap] function is for relaxing the GC.
*)
let gamma = ref ( QmlTypes.Env.empty : QmlTypes.gamma )
let annotmap = ref ( QmlAnnotMap.empty : QmlAst.annotmap )
let set_gamma g = gamma := g
let set_annotmap a = annotmap := a
let free_gamma_annotmap () =
gamma := QmlTypes.Env.empty ;
annotmap := QmlAnnotMap.empty
(*
This function tells if a pattern [p] hides a another pattern [p'].
For example, in :
{[
match e with
| _ -> "toto"
| 6 -> "tutu"
]}
The pattern [_] hids the pattern [6]
The question answered by this function is :
Does p kills (hides) p' ?
<!> beware with rowvar,
{[
| { a }
| { a ; ... }
]}
The second case in general is not killed by the first case. (depending on the type).
The check is syntactic.
*)
let rec is_killed_by p p' =
match p, p' with
| Q.PatCoerce (_, p, _), _ -> is_killed_by p p'
| _, Q.PatCoerce(_, p', _) -> is_killed_by p p'
| (Q.PatAny _ | Q.PatVar _), _ -> true
| Q.PatRecord _, Q.PatRecord _ -> all_fields_killed_by p p'
| Q.PatConst (_, c0), Q.PatConst (_, c1) -> c0 = c1
| _ -> false
(* This function is called whith complexe patterns, i.e with fields *)
and all_fields_killed_by p p' =
(*
gather all field of a pattern, and return an extra bool,
[true] if the pattern is strict (without { ; ...} )
*)
let fields_list p =
match p with
| Q.PatRecord (_, fields, rowvar) -> fields, rowvar = `closed
| _ ->
let context = QmlError.Context.annoted_pat !annotmap p in
QmlError.i_error None context (
"This pattern is not well formed.@\n%a"
)
QmlPrint.pp#pat p
in
let l1, strict1 = fields_list p in
let l2, strict2 = fields_list p' in
if strict1
then
if strict2
then
(*
All field of p' should be in p, and all should be killed.
The two list should have the same length.
*)
let cmp (a, _) (b, _) = String.compare a b in
let l1 = List.sort cmp l1 in
let l2 = List.sort cmp l2 in
Return.set_checkpoint (
fun label ->
let iter2 (a, p) (b, p') =
if a <> b || not (is_killed_by p p')
then Return.return label false
in
try
List.iter2 iter2 l1 l2 ;
true
with
| Invalid_argument _ -> false
)
else
(*
Syntactic check only.
No matter what fields are in p', if p is strict, and p' not,
the second pattern cover more cases than the first, so
is not hidden.
*)
false
else
(*
In this case, no matter the row variable of p', if all field p
are also present in p', and killed by p, the pattern is killed.
The fields present in p' but not in p would be matched inside
the row var of p.
*)
List.for_all (
fun (n, p)->
match List.assoc_opt n l2 with
| None -> false
| Some p' -> is_killed_by p p'
) l1
(*
Given a pattern [p] and a list of patterns [li] return the filtered list of [li],
containing only the pattern hidden by [p]
*)
let killed_patterns p li =
List.filter (fun (p', _) -> is_killed_by p p') li
(*
Given an ordered list of patterns, will return the assoc list of type : [(pat * pat list) list]
if [(p, li)] is in this list, that means that in the pattern matching, all pattern of [li]
are hidden by [p]
*)
let collect_killed_patterns li =
let rec aux acc = function
| [] -> List.rev acc
| (hd, _) :: tl ->
let killed_patterns = killed_patterns hd tl in
let acc =
if killed_patterns <> [] then (hd, killed_patterns)::acc else acc
in
aux acc tl
in
aux [] li
(*
Given an expression, check.
This is meant to be used with Traverse functions,
that's why the function is not recursive.
*)
let check_expr e =
match e with
| Q.Match (_, _, li) ->
(* First check: dead patterns *)
let iter (p, li) =
let iter (p', _) =
let c1 = QmlError.Context.annotmap !annotmap in
let c2 = QmlError.Context.pat p in
let c3 = QmlError.Context.pat p' in
let context = QmlError.Context.merge c1 [c2 ; c3] in
QmlError.warning ~wclass:dead context (
"@[<2>This kind of pattern matching is not allowed@\n"^^
"The first pattern hides the second one.@]"
)
in
List.iter iter li
in
List.iter iter (collect_killed_patterns li)
;
(* Second check: obfuscation *)
let iter (p, _) =
let iter p =
match p with
| Q.PatVar (_, ident) | Q.PatAs (_, _, ident) ->
let label = Ident.original_name ident in
if is_label_in_simple_case label (Q.QAnnot.pat p) !annotmap !gamma
then
let context = QmlError.Context.annoted_pat !annotmap p in
QmlError.warning ~wclass:obfuscation context (
"You should not name this pattern variable @{<bright>%s@} because@\n"^^
"the type of the matched expression contain a sum case @{<bright>{ %s }@}."
)
label label
| _ -> ()
in
QmlAstWalk.Pattern.iter_down iter p
in
let doit = match li with | _::_::_ -> true | _ -> false in
if doit then
List.iter iter li
| _ -> ()
(*
The function returns unit.
In case of illicit pattern, fail using QmlError with located error messages.
*)
let process_code gamma annotmap code =
if WarningClass.is_warn wclass then (
set_gamma gamma;
set_annotmap annotmap;
QmlAstWalk.CodeExpr.iter (QmlAstWalk.Expr.iter check_expr) code;
free_gamma_annotmap ()
)
(*
New pass of analysis. Testing
*)
let process_code gamma annotmap code =
process_code gamma annotmap code ;
if WarningClass.is_warn wclass then (
let foldmap annotmap = function
| Q.Match (label, matched_expr, patterns) as expr ->
let pattern_matching =
QmlPatternAnalysis.conversion ~gamma ~annotmap ~label ~matched_expr ~patterns
in
let normalized = QmlPatternAnalysis.normalize pattern_matching in
let () =
if QmlPatternAnalysis.has_public_exceptions () then (
let ctx = QmlError.Context.label label in
QmlError.warning ~wclass:wclass ctx "%a"
QmlPatternAnalysis.flush_exceptions_fmt ()
) in
let acc =
#<If:PATTERNS_NORMALIZE>
QmlPatternAnalysis.generation normalized
#<Else>
ignore normalized ;
annotmap, expr
#<End>
in
acc
| expr ->
annotmap, expr
in
let norm_annotmap, norm_code =
QmlAstWalk.CodeExpr.fold_map (QmlAstWalk.Expr.foldmap foldmap) annotmap code
in
let () = QmlPatternAnalysis.Env.reset () in
#<If:PATTERNS_NORMALIZE>
norm_annotmap, norm_code
#<Else> (
ignore norm_annotmap ;
ignore norm_code ;
annotmap, code
)
#<End>
) else
annotmap, code