Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (* Copyright (C) 2009,2011,2017 Matthew Fluet. |
2 | * Copyright (C) 1999-2008 Henry Cejtin, Matthew Fluet, Suresh | |
3 | * Jagannathan, and Stephen Weeks. | |
4 | * Copyright (C) 1997-2000 NEC Research Institute. | |
5 | * | |
6 | * MLton is released under a BSD-style license. | |
7 | * See the file MLton-LICENSE for details. | |
8 | *) | |
9 | ||
10 | functor TypeCheck (S: TYPE_CHECK_STRUCTS): TYPE_CHECK = | |
11 | struct | |
12 | ||
13 | open S | |
14 | ||
15 | datatype z = datatype Exp.t | |
16 | datatype z = datatype Transfer.t | |
17 | ||
18 | fun checkScopes (program as | |
19 | Program.T {datatypes, globals, functions, main}): unit = | |
20 | let | |
21 | datatype 'a status = | |
22 | Undefined | |
23 | | InScope of 'a | |
24 | | Defined | |
25 | ||
26 | fun make' (layout, plist) = | |
27 | let | |
28 | val {get, set, ...} = | |
29 | Property.getSet (plist, Property.initConst Undefined) | |
30 | fun bind (x, v) = | |
31 | case get x of | |
32 | Undefined => set (x, InScope v) | |
33 | | _ => Error.bug ("Ssa.TypeCheck.checkScopes: duplicate definition of " | |
34 | ^ (Layout.toString (layout x))) | |
35 | fun reference x = | |
36 | case get x of | |
37 | InScope v => v | |
38 | | _ => Error.bug (concat | |
39 | ["Ssa.TypeCheck.checkScopes: reference to ", | |
40 | Layout.toString (layout x), | |
41 | " not in scope"]) | |
42 | fun unbind x = set (x, Defined) | |
43 | in (bind, ignore o reference, reference, unbind) | |
44 | end | |
45 | fun make (layout, plist) = | |
46 | let val (bind, reference, _, unbind) = make' (layout, plist) | |
47 | in (fn x => bind (x, ()), reference, unbind) | |
48 | end | |
49 | ||
50 | val (bindTycon, getTycon, getTycon', _) = make' (Tycon.layout, Tycon.plist) | |
51 | val (bindCon, getCon, _) = make (Con.layout, Con.plist) | |
52 | val (bindVar, getVar, getVar', unbindVar) = make' (Var.layout, Var.plist) | |
53 | fun getVars xs = Vector.foreach (xs, getVar) | |
54 | val (bindLabel, getLabel, unbindLabel) = make (Label.layout, Label.plist) | |
55 | val (bindFunc, getFunc, _) = make (Func.layout, Func.plist) | |
56 | ||
57 | val {destroy = destroyLoopType, get = loopType, ...} = | |
58 | Property.destGet | |
59 | (Type.plist, | |
60 | Property.initRec | |
61 | (fn (ty, loopType) => | |
62 | let | |
63 | datatype z = datatype Type.dest | |
64 | val _ = | |
65 | case Type.dest ty of | |
66 | Array ty => loopType ty | |
67 | | CPointer => () | |
68 | | Datatype tycon => getTycon tycon | |
69 | | IntInf => () | |
70 | | Real _ => () | |
71 | | Ref ty => loopType ty | |
72 | | Thread => () | |
73 | | Tuple tys => Vector.foreach (tys, loopType) | |
74 | | Vector ty => loopType ty | |
75 | | Weak ty => loopType ty | |
76 | | Word _ => () | |
77 | in | |
78 | () | |
79 | end)) | |
80 | fun loopTypes tys = Vector.foreach (tys, loopType) | |
81 | (* Redefine bindVar to check well-formedness of types. *) | |
82 | val bindVar = fn (x, ty) => (loopType ty; bindVar (x, ty)) | |
83 | fun loopExp exp = | |
84 | let | |
85 | val _ = | |
86 | case exp of | |
87 | ConApp {con, args, ...} => (getCon con ; getVars args) | |
88 | | Const _ => () | |
89 | | PrimApp {args, targs, ...} => (loopTypes targs; getVars args) | |
90 | | Profile _ => () | |
91 | | Select {tuple, ...} => getVar tuple | |
92 | | Tuple xs => getVars xs | |
93 | | Var x => getVar x | |
94 | in | |
95 | () | |
96 | end | |
97 | fun loopStatement (s as Statement.T {var, ty, exp, ...}) = | |
98 | let | |
99 | val _ = loopExp exp | |
100 | val _ = loopType ty | |
101 | val _ = Option.app (var, fn x => bindVar (x, ty)) | |
102 | in | |
103 | () | |
104 | end | |
105 | handle exn => Error.reraiseSuffix (exn, concat [" in ", Layout.toString (Statement.layout s)]) | |
106 | val loopTransfer = | |
107 | fn Arith {args, ty, ...} => (getVars args; loopType ty) | |
108 | | Bug => () | |
109 | | Call {func, args, ...} => (getFunc func; getVars args) | |
110 | | Case {test, cases, default, ...} => | |
111 | let | |
112 | fun doit (cases: ('a * 'b) vector, | |
113 | equals: 'a * 'a -> bool, | |
114 | hash: 'a -> word, | |
115 | numExhaustiveCases: IntInf.t) = | |
116 | let | |
117 | val table = HashSet.new {hash = hash} | |
118 | val _ = | |
119 | Vector.foreach | |
120 | (cases, fn (x, _) => | |
121 | let | |
122 | val _ = | |
123 | HashSet.insertIfNew | |
124 | (table, hash x, fn y => equals (x, y), | |
125 | fn () => x, | |
126 | fn _ => Error.bug "Ssa.TypeCheck.loopTransfer: redundant branch in case") | |
127 | in | |
128 | () | |
129 | end) | |
130 | val numCases = Int.toIntInf (Vector.length cases) | |
131 | in | |
132 | case (IntInf.equals (numCases, numExhaustiveCases), isSome default) of | |
133 | (true, true) => | |
134 | Error.bug "Ssa.TypeCheck.loopTransfer: exhaustive case has default" | |
135 | | (false, false) => | |
136 | Error.bug "Ssa.TypeCheck.loopTransfer: non-exhaustive case has no default" | |
137 | | _ => () | |
138 | end | |
139 | fun doitWord (ws, cases) = | |
140 | doit (cases, WordX.equals, WordX.hash, WordSize.cardinality ws) | |
141 | fun doitCon cases = | |
142 | let | |
143 | val numExhaustiveCases = | |
144 | case Type.dest (getVar' test) of | |
145 | Type.Datatype t => Int.toIntInf (getTycon' t) | |
146 | | _ => Error.bug "Ssa.TypeCheck.loopTransfer: case test is not a datatype" | |
147 | in | |
148 | doit (cases, Con.equals, Con.hash, numExhaustiveCases) | |
149 | end | |
150 | val _ = getVar test | |
151 | val _ = | |
152 | case cases of | |
153 | Cases.Con cs => doitCon cs | |
154 | | Cases.Word (ws, cs) => doitWord (ws, cs) | |
155 | in | |
156 | () | |
157 | end | |
158 | | Goto {args, ...} => getVars args | |
159 | | Raise xs => getVars xs | |
160 | | Return xs => getVars xs | |
161 | | Runtime {args, ...} => getVars args | |
162 | val loopTransfer = | |
163 | fn t => | |
164 | (loopTransfer t) | |
165 | handle exn => Error.reraiseSuffix (exn, concat [" in ", Layout.toString (Transfer.layout t)]) | |
166 | fun loopFunc (f: Function.t) = | |
167 | let | |
168 | val {args, blocks, raises, returns, start, ...} = Function.dest f | |
169 | (* Descend the dominator tree, verifying that variable definitions | |
170 | * dominate variable uses. | |
171 | *) | |
172 | fun loop (Tree.T (block, children)): unit = | |
173 | let | |
174 | val Block.T {label, args, statements, transfer, ...} = block | |
175 | val _ = (Vector.foreach (args, bindVar) | |
176 | ; Vector.foreach (statements, loopStatement) | |
177 | ; loopTransfer transfer) | |
178 | handle exn => Error.reraiseSuffix (exn, concat [" in ", Label.toString label]) | |
179 | val _ = Vector.foreach (children, loop) | |
180 | val _ = Vector.foreach | |
181 | (statements, fn s => | |
182 | Option.app (Statement.var s, unbindVar)) | |
183 | val _ = Vector.foreach (args, unbindVar o #1) | |
184 | in | |
185 | () | |
186 | end | |
187 | val _ = Vector.foreach (args, bindVar) | |
188 | val _ = Vector.foreach (blocks, bindLabel o Block.label) | |
189 | (* Check that 'start' and all transfer labels are in scope. | |
190 | * In the case that something is not in scope, | |
191 | * "getLabel" gives a more informative error message | |
192 | * than the CFG/dominatorTree construction failure. | |
193 | *) | |
194 | val _ = getLabel start | |
195 | val _ = Vector.foreach | |
196 | (blocks, fn Block.T {transfer, ...} => | |
197 | Transfer.foreachLabel (transfer, getLabel)) | |
198 | val _ = loop (Function.dominatorTree f) | |
199 | val _ = Vector.foreach (blocks, unbindLabel o Block.label) | |
200 | val _ = Vector.foreach (args, unbindVar o #1) | |
201 | val _ = Option.app (returns, loopTypes) | |
202 | val _ = Option.app (raises, loopTypes) | |
203 | val _ = Function.clear f | |
204 | in | |
205 | () | |
206 | end | |
207 | handle exn => Error.reraiseSuffix (exn, concat [" in ", Func.toString (Function.name f)]) | |
208 | val _ = Vector.foreach | |
209 | (datatypes, fn Datatype.T {tycon, cons} => | |
210 | (bindTycon (tycon, Vector.length cons) | |
211 | ; Vector.foreach (cons, fn {con, ...} => | |
212 | bindCon con))) | |
213 | handle exn => Error.reraiseSuffix (exn, concat [" in Datatypes"]) | |
214 | val _ = Vector.foreach | |
215 | (datatypes, fn Datatype.T {cons, ...} => | |
216 | Vector.foreach (cons, fn {args, ...} => | |
217 | Vector.foreach (args, loopType))) | |
218 | handle exn => Error.reraiseSuffix (exn, concat [" in Datatypes"]) | |
219 | val _ = Vector.foreach (globals, loopStatement) | |
220 | handle exn => Error.reraiseSuffix (exn, concat [" in Globals"]) | |
221 | val _ = List.foreach (functions, bindFunc o Function.name) | |
222 | val _ = getFunc main | |
223 | val _ = List.foreach (functions, loopFunc) | |
224 | val _ = Program.clearTop program | |
225 | val _ = destroyLoopType () | |
226 | in | |
227 | () | |
228 | end | |
229 | ||
230 | val checkScopes = Control.trace (Control.Detail, "checkScopes") checkScopes | |
231 | ||
232 | structure Function = | |
233 | struct | |
234 | open Function | |
235 | ||
236 | fun checkProf (f: t): unit = | |
237 | let | |
238 | val debug = false | |
239 | val {blocks, start, ...} = dest f | |
240 | val {get = labelInfo, rem, set = setLabelInfo, ...} = | |
241 | Property.getSetOnce | |
242 | (Label.plist, | |
243 | Property.initRaise ("info", Label.layout)) | |
244 | val _ = Vector.foreach (blocks, fn b as Block.T {label, ...} => | |
245 | setLabelInfo (label, | |
246 | {block = b, | |
247 | sources = ref NONE})) | |
248 | fun goto (l: Label.t, sources: SourceInfo.t list) = | |
249 | let | |
250 | fun bug (msg: string): 'a = | |
251 | let | |
252 | val _ = | |
253 | Vector.foreach | |
254 | (blocks, fn Block.T {label, ...} => | |
255 | let | |
256 | val {sources, ...} = labelInfo label | |
257 | open Layout | |
258 | in | |
259 | outputl | |
260 | (seq [Label.layout label, | |
261 | str " ", | |
262 | Option.layout | |
263 | (List.layout SourceInfo.layout) | |
264 | (!sources)], | |
265 | Out.error) | |
266 | end) | |
267 | in | |
268 | Error.bug | |
269 | (concat ["Ssa.TypeCheck.checkProf: bug found in ", Label.toString l, | |
270 | ": ", msg]) | |
271 | end | |
272 | val _ = | |
273 | if not debug | |
274 | then () | |
275 | else | |
276 | let | |
277 | open Layout | |
278 | in | |
279 | outputl (seq [str "goto (", | |
280 | Label.layout l, | |
281 | str ", ", | |
282 | List.layout SourceInfo.layout sources, | |
283 | str ")"], | |
284 | Out.error) | |
285 | end | |
286 | val {block, sources = r} = labelInfo l | |
287 | in | |
288 | case !r of | |
289 | NONE => | |
290 | let | |
291 | val _ = r := SOME sources | |
292 | val Block.T {statements, transfer, ...} = block | |
293 | datatype z = datatype Statement.t | |
294 | datatype z = datatype ProfileExp.t | |
295 | val sources = | |
296 | Vector.fold | |
297 | (statements, sources, | |
298 | fn (Statement.T {exp, ...}, sources) => | |
299 | case exp of | |
300 | Profile pe => | |
301 | (case pe of | |
302 | Enter s => s :: sources | |
303 | | Leave s => | |
304 | (case sources of | |
305 | [] => bug "unmatched Leave" | |
306 | | s' :: sources => | |
307 | if SourceInfo.equals (s, s') | |
308 | then sources | |
309 | else bug "mismatched Leave")) | |
310 | | _ => sources) | |
311 | val _ = | |
312 | if not debug | |
313 | then () | |
314 | else | |
315 | let | |
316 | open Layout | |
317 | in | |
318 | outputl (List.layout SourceInfo.layout sources, | |
319 | Out.error) | |
320 | end | |
321 | val _ = | |
322 | if (case transfer of | |
323 | Call {return, ...} => | |
324 | let | |
325 | datatype z = datatype Return.t | |
326 | in | |
327 | case return of | |
328 | Dead => false | |
329 | | NonTail _ => false | |
330 | | Tail => true | |
331 | end | |
332 | | Raise _ => true | |
333 | | Return _ => true | |
334 | | _ => false) | |
335 | then (case sources of | |
336 | [] => () | |
337 | | _ => bug "nonempty sources when leaving function") | |
338 | else () | |
339 | in | |
340 | Transfer.foreachLabel | |
341 | (transfer, fn l => goto (l, sources)) | |
342 | end | |
343 | | SOME sources' => | |
344 | if List.equals (sources, sources', SourceInfo.equals) | |
345 | then () | |
346 | else bug "mismatched block" | |
347 | end | |
348 | val _ = goto (start, []) | |
349 | val _ = Vector.foreach (blocks, fn Block.T {label, ...} => rem label) | |
350 | in | |
351 | () | |
352 | end | |
353 | end | |
354 | ||
355 | fun checkProf (Program.T {functions, ...}): unit = | |
356 | List.foreach (functions, fn f => Function.checkProf f) | |
357 | ||
358 | val checkProf = Control.trace (Control.Detail, "checkProf") checkProf | |
359 | ||
360 | fun typeCheck (program as Program.T {datatypes, ...}): unit = | |
361 | let | |
362 | val _ = checkScopes program | |
363 | val _ = | |
364 | if !Control.profile <> Control.ProfileNone | |
365 | then checkProf program | |
366 | else () | |
367 | fun coerce {from: Type.t, to: Type.t}: unit = | |
368 | if Type.equals (from, to) | |
369 | then () | |
370 | else Error.bug (concat ["Ssa.TypeCheck.coerce (", | |
371 | (Layout.toString o Layout.record) | |
372 | [("from", Type.layout from), | |
373 | ("to", Type.layout to)], | |
374 | ")"]) | |
375 | fun coerces (from, to) = | |
376 | Vector.foreach2 (from, to, fn (from, to) => | |
377 | coerce {from = from, to = to}) | |
378 | val coerce = | |
379 | Trace.trace ("Ssa.TypeCheck.coerce", | |
380 | fn {from, to} => let open Layout | |
381 | in record [("from", Type.layout from), | |
382 | ("to", Type.layout to)] | |
383 | end, | |
384 | Unit.layout) coerce | |
385 | fun select {tuple: Type.t, offset: int, resultType = _}: Type.t = | |
386 | case Type.deTupleOpt tuple of | |
387 | NONE => Error.bug ("Ssa.TypeCheck.select (non tuple)") | |
388 | | SOME ts => Vector.sub (ts, offset) | |
389 | val {get = conInfo: Con.t -> {args: Type.t vector, | |
390 | result: Type.t}, | |
391 | set = setConInfo, ...} = | |
392 | Property.getSetOnce | |
393 | (Con.plist, Property.initRaise ("Ssa.TypeCheck.conInfo", Con.layout)) | |
394 | val _ = | |
395 | Vector.foreach | |
396 | (datatypes, fn Datatype.T {tycon, cons} => | |
397 | let val result = Type.datatypee tycon | |
398 | in Vector.foreach | |
399 | (cons, fn {con, args} => | |
400 | setConInfo (con, {args = args, | |
401 | result = result})) | |
402 | end) | |
403 | fun conApp {con, args} = | |
404 | let | |
405 | val {args = args', result, ...} = conInfo con | |
406 | val _ = coerces (args', args) | |
407 | in | |
408 | result | |
409 | end | |
410 | fun filter (test, con, args) = | |
411 | let | |
412 | val {result, args = args'} = conInfo con | |
413 | val _ = coerce {from = test, to = result} | |
414 | val _ = coerces (args', args) | |
415 | in () | |
416 | end | |
417 | fun primApp {args, prim, resultType, resultVar = _, targs} = | |
418 | let | |
419 | datatype z = datatype Prim.Name.t | |
420 | val () = | |
421 | if Type.checkPrimApp {args = args, | |
422 | prim = prim, | |
423 | result = resultType, | |
424 | targs = targs} | |
425 | then () | |
426 | else Error.bug (concat ["Ssa.TypeCheck.primApp (", | |
427 | let | |
428 | open Layout | |
429 | in | |
430 | (toString o seq) | |
431 | [Prim.layout prim, | |
432 | if Vector.isEmpty targs | |
433 | then empty | |
434 | else Vector.layout Type.layout targs, | |
435 | str " ", | |
436 | Vector.layout Type.layout args] | |
437 | end, | |
438 | ")"]) | |
439 | in | |
440 | resultType | |
441 | end | |
442 | val _ = | |
443 | analyze { | |
444 | coerce = coerce, | |
445 | conApp = conApp, | |
446 | const = Type.ofConst, | |
447 | filter = filter, | |
448 | filterWord = fn (from, s) => coerce {from = from, | |
449 | to = Type.word s}, | |
450 | fromType = fn x => x, | |
451 | layout = Type.layout, | |
452 | primApp = primApp, | |
453 | program = program, | |
454 | select = select, | |
455 | tuple = Type.tuple, | |
456 | useFromTypeOnBinds = true | |
457 | } | |
458 | val _ = Program.clear program | |
459 | in | |
460 | () | |
461 | end | |
462 | ||
463 | val typeCheck = fn p => | |
464 | (typeCheck p) | |
465 | handle exn => Error.reraisePrefix (exn, "TypeError (SSA): ") | |
466 | ||
467 | val typeCheck = Control.trace (Control.Pass, "typeCheck") typeCheck | |
468 | ||
469 | end |