mlton/ssa/type-check.fun

   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