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.
6 * MLton is released under a BSD-style license.
7 * See the file MLton-LICENSE for details.
10 functor TypeCheck2 (S: TYPE_CHECK2_STRUCTS): TYPE_CHECK2 =
15 datatype z = datatype Exp.t
16 datatype z = datatype Statement.t
17 datatype z = datatype Transfer.t
19 fun checkScopes (program as
20 Program.T {datatypes, globals, functions, main}): unit =
27 fun make' (layout, plist) =
30 Property.getSet (plist, Property.initConst Undefined)
33 Undefined => set (x, InScope v)
34 | _ => Error.bug (concat ["Ssa2.TypeCheck2.checkScopes: duplicate definition of ",
35 Layout.toString (layout x)])
39 | _ => Error.bug (concat ["Ssa2.TypeCheck2.checkScopes: reference to ",
40 Layout.toString (layout x),
43 fun unbind x = set (x, Defined)
44 in (bind, ignore o reference, reference, unbind)
46 fun make (layout, plist) =
47 let val (bind, reference, _, unbind) = make' (layout, plist)
48 in (fn x => bind (x, ()), reference, unbind)
51 val (bindTycon, getTycon, getTycon', _) = make' (Tycon.layout, Tycon.plist)
52 val (bindCon, getCon, _) = make (Con.layout, Con.plist)
53 val (bindVar, getVar, getVar', unbindVar) = make' (Var.layout, Var.plist)
54 fun getVars xs = Vector.foreach (xs, getVar)
55 val (bindFunc, getFunc, _) = make (Func.layout, Func.plist)
56 val (bindLabel, getLabel, unbindLabel) = make (Label.layout, Label.plist)
58 fun loopObjectCon oc =
60 datatype z = datatype ObjectCon.t
69 val {destroy = destroyLoopType, get = loopType, ...} =
75 datatype z = datatype Type.dest
79 | Datatype tycon => getTycon tycon
81 | Object {args, con, ...} =>
83 val _ = loopObjectCon con
84 val _ = Prod.foreach (args, loopType)
90 | Weak ty => loopType ty
95 fun loopTypes tys = Vector.foreach (tys, loopType)
96 (* Redefine bindVar to check well-formedness of types. *)
97 val bindVar = fn (x, ty) => (loopType ty; bindVar (x, ty))
103 | Inject {sum, variant, ...} => (getTycon sum; getVar variant)
104 | Object {args, con, ...} => (Option.app (con, getCon); getVars args)
105 | PrimApp {args, ...} => getVars args
106 | Select {base, ...} => Base.foreach (base, getVar)
111 fun loopStatement (s: Statement.t): unit =
115 Bind {exp, ty, var, ...} =>
119 val _ = Option.app (var, fn x => bindVar (x, ty))
124 | Update {base, value, ...} =>
125 (Base.foreach (base, getVar); getVar value)
129 handle exn => Error.reraiseSuffix (exn, concat [" in ", Layout.toString (Statement.layout s)])
131 fn Arith {args, ty, ...} => (getVars args; loopType ty)
133 | Call {func, args, ...} => (getFunc func; getVars args)
134 | Case {test, cases, default, ...} =>
136 fun doit (cases: ('a * 'b) vector,
137 equals: 'a * 'a -> bool,
139 numExhaustiveCases: IntInf.t) =
141 val table = HashSet.new {hash = hash}
148 (table, hash x, fn y => equals (x, y),
150 fn _ => Error.bug "Ssa2.TypeCheck2.loopTransfer: redundant branch in case")
154 val numCases = Int.toIntInf (Vector.length cases)
156 case (IntInf.equals (numCases, numExhaustiveCases), isSome default) of
158 Error.bug "Ssa2.TypeCheck2.loopTransfer: exhaustive case has default"
160 Error.bug "Ssa2.TypeCheck2.loopTransfer: non-exhaustive case has no default"
163 fun doitWord (ws, cases) =
164 doit (cases, WordX.equals, WordX.hash, WordSize.cardinality ws)
167 val numExhaustiveCases =
168 case Type.dest (getVar' test) of
169 Type.Datatype t => Int.toIntInf (getTycon' t)
170 | _ => Error.bug "Ssa2.TypeCheck2.loopTransfer: case test is not a datatype"
172 doit (cases, Con.equals, Con.hash, numExhaustiveCases)
177 Cases.Con cs => doitCon cs
178 | Cases.Word (ws, cs) => doitWord (ws, cs)
182 | Goto {args, ...} => getVars args
183 | Raise xs => getVars xs
184 | Return xs => getVars xs
185 | Runtime {args, ...} => getVars args
189 handle exn => Error.reraiseSuffix (exn, concat [" in ", Layout.toString (Transfer.layout t)])
190 fun loopFunc (f: Function.t) =
192 val {args, blocks, raises, returns, start, ...} = Function.dest f
193 (* Descend the dominator tree, verifying that variable definitions
194 * dominate variable uses.
196 fun loop (Tree.T (block, children)): unit =
198 val Block.T {label, args, statements, transfer, ...} = block
199 val _ = (Vector.foreach (args, bindVar)
200 ; Vector.foreach (statements, loopStatement)
201 ; loopTransfer transfer)
202 handle exn => Error.reraiseSuffix (exn, concat [" in ", Label.toString label])
203 val _ = Vector.foreach (children, loop)
204 val _ = Vector.foreach
206 Statement.foreachDef (s, unbindVar o #1))
207 val _ = Vector.foreach (args, unbindVar o #1)
211 val _ = Vector.foreach (args, bindVar)
212 val _ = Vector.foreach (blocks, bindLabel o Block.label)
213 (* Check that 'start' and all transfer labels are in scope.
214 * In the case that something is not in scope,
215 * "getLabel" gives a more informative error message
216 * than the CFG/dominatorTree construction failure.
218 val _ = getLabel start
219 val _ = Vector.foreach
220 (blocks, fn Block.T {transfer, ...} =>
221 Transfer.foreachLabel (transfer, getLabel))
222 val _ = loop (Function.dominatorTree f)
223 val _ = Vector.foreach (blocks, unbindLabel o Block.label)
224 val _ = Vector.foreach (args, unbindVar o #1)
225 val _ = Option.app (returns, loopTypes)
226 val _ = Option.app (raises, loopTypes)
227 val _ = Function.clear f
231 handle exn => Error.reraiseSuffix (exn, concat [" in ", Func.toString (Function.name f)])
232 val _ = Vector.foreach
233 (datatypes, fn Datatype.T {tycon, cons} =>
234 (bindTycon (tycon, Vector.length cons)
235 ; Vector.foreach (cons, fn {con, ...} =>
237 handle exn => Error.reraiseSuffix (exn, concat [" in Datatypes"])
238 val _ = Vector.foreach
239 (datatypes, fn Datatype.T {cons, ...} =>
240 Vector.foreach (cons, fn {args, ...} =>
241 Prod.foreach (args, loopType)))
242 handle exn => Error.reraiseSuffix (exn, concat [" in Datatypes"])
243 val _ = Vector.foreach (globals, loopStatement)
244 handle exn => Error.reraiseSuffix (exn, concat [" in Globals"])
245 val _ = List.foreach (functions, bindFunc o Function.name)
246 val _ = List.foreach (functions, loopFunc)
248 val _ = Program.clearTop program
249 val _ = destroyLoopType ()
254 val checkScopes = Control.trace (Control.Detail, "checkScopes") checkScopes
260 fun checkProf (f: t): unit =
263 val {blocks, start, ...} = dest f
264 val {get = labelInfo, rem, set = setLabelInfo, ...} =
267 Property.initRaise ("info", Label.layout))
268 val _ = Vector.foreach (blocks, fn b as Block.T {label, ...} =>
271 sources = ref NONE}))
272 fun goto (l: Label.t, sources: SourceInfo.t list) =
274 fun bug (msg: string): 'a =
278 (blocks, fn Block.T {label, ...} =>
280 val {sources, ...} = labelInfo label
284 (seq [Label.layout label,
287 (List.layout SourceInfo.layout)
293 (concat ["Ssa2.TypeCheck2.checkProf: bug found in ", Label.toString l,
303 outputl (seq [str "goto (",
306 List.layout SourceInfo.layout sources,
310 val {block, sources = r} = labelInfo l
315 val _ = r := SOME sources
316 val Block.T {statements, transfer, ...} = block
317 datatype z = datatype Statement.t
318 datatype z = datatype ProfileExp.t
321 (statements, sources, fn (s, sources) =>
325 Enter s => s :: sources
328 [] => bug "unmatched Leave"
330 if SourceInfo.equals (s, s')
332 else bug "mismatched Leave"))
341 outputl (List.layout SourceInfo.layout sources,
346 Call {return, ...} =>
348 datatype z = datatype Return.t
358 then (case sources of
360 | _ => bug "nonempty sources when leaving function")
363 Transfer.foreachLabel
364 (transfer, fn l => goto (l, sources))
367 if List.equals (sources, sources', SourceInfo.equals)
369 else bug "mismatched block"
371 val _ = goto (start, [])
372 val _ = Vector.foreach (blocks, fn Block.T {label, ...} => rem label)
378 fun checkProf (Program.T {functions, ...}): unit =
379 List.foreach (functions, fn f => Function.checkProf f)
381 val checkProf = Control.trace (Control.Detail, "checkProf") checkProf
383 fun typeCheck (program as Program.T {datatypes, ...}): unit =
385 val _ = checkScopes program
387 if !Control.profile <> Control.ProfileNone
388 then checkProf program
390 val {get = conInfo: Con.t -> {result: Type.t,
393 set = setConInfo, ...} =
395 (Con.plist, Property.initRaise ("Ssa2.TypeCheck2.conInfo", Con.layout))
396 val conTycon = #tycon o conInfo
399 (datatypes, fn Datatype.T {tycon, cons} =>
401 val result = Type.datatypee tycon
403 Vector.foreach (cons, fn {con, args} =>
404 setConInfo (con, {result = result,
405 ty = Type.conApp (con, args),
408 fun inject {sum: Tycon.t, variant: Type.t}: Type.t =
410 val error = fn msg =>
411 Error.bug (concat ["Ssa2.TypeCheck2.inject (",
413 (Layout.toString o Layout.record)
414 [("sum", Tycon.layout sum),
415 ("variant", Type.layout variant)],
418 case Type.dest variant of
419 Type.Object {con, ...} =>
422 if Tycon.equals (conTycon c, sum)
423 then Type.datatypee sum
424 else error "wrong sum"
425 | _ => error "no object-con")
426 | _ => error "no object"
428 fun coerce {from: Type.t, to: Type.t}: unit =
429 if Type.equals (from, to)
431 else Error.bug (concat ["SSa2.TypeCheck2.coerce (",
432 (Layout.toString o Layout.record)
433 [("from", Type.layout from),
434 ("to", Type.layout to)],
437 Trace.trace ("Ssa2.TypeCheck2.coerce",
438 fn {from, to} => let open Layout
439 in record [("from", Type.layout from),
440 ("to", Type.layout to)]
443 fun object {args, con, resultType} =
445 fun err () = Error.bug "Ssa2.TypeCheck2.object (bad object)"
447 case Type.dest resultType of
448 Type.Object {args = args', con = con'} =>
449 (if (case (con, con') of
450 (NONE, ObjectCon.Tuple) => true
451 | (SOME c, ObjectCon.Con c') => Con.equals (c, c')
453 andalso (Vector.foreach2
454 (Prod.dest args, Prod.dest args',
455 fn ({elt = t, isMutable = _}, {elt = t', ...}) =>
456 coerce {from = t, to = t'})
465 | Base.VectorSub {index, vector} =>
466 if Type.isVector vector
469 if Type.equals (index, Type.word (WordSize.seqIndex ()))
471 else Error.bug "Ssa2.TypeCheck2.base (vector-sub of non seqIndex)"
475 else Error.bug "Ssa2.TypeCheck2.base (vector-sub of non vector)"
476 fun select {base: Type.t, offset: int, resultType = _}: Type.t =
477 case Type.dest base of
478 Type.Object {args, ...} => Prod.elt (args, offset)
479 | _ => Error.bug "Ssa2.TypeCheck2.select (non object)"
480 fun update {base, offset, value} =
481 case Type.dest base of
482 Type.Object {args, ...} =>
484 val {elt, isMutable} = Prod.sub (args, offset)
485 val () = coerce {from = value, to = elt}
489 else Error.bug "Ssa2.TypeCheck2.update (non-mutable field)"
493 | _ => Error.bug "Ssa2.TypeCheck2.update (non object)"
494 fun filter {con, test, variant} =
496 val {result, ty, ...} = conInfo con
497 val () = coerce {from = test, to = result}
498 val () = Option.app (variant, fn to => coerce {from = ty, to = to})
502 fun filterWord (from, s) = coerce {from = from, to = Type.word s}
503 fun primApp {args, prim, resultType, resultVar = _} =
505 datatype z = datatype Prim.Name.t
507 if Type.checkPrimApp {args = args,
511 else Error.bug (concat ["Ssa2.TypeCheck2.primApp (",
518 Vector.layout Type.layout args]
525 analyze {base = base,
527 const = Type.ofConst,
529 filterWord = filterWord,
530 fromType = fn x => x,
532 layout = Type.layout,
538 useFromTypeOnBinds = true}
539 val _ = Program.clear program
544 val typeCheck = fn p =>
546 handle exn => Error.reraisePrefix (exn, "TypeError (SSA2): ")
548 val typeCheck = Control.trace (Control.Pass, "typeCheck") typeCheck