mlton/ssa/type-check2.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 TypeCheck2 (S: TYPE_CHECK2_STRUCTS): TYPE_CHECK2 =
  11 struct
  12
  13 open S
  14
  15 datatype z = datatype Exp.t
  16 datatype z = datatype Statement.t
  17 datatype z = datatype Transfer.t
  18
  19 fun checkScopes (program as
  20                  Program.T {datatypes, globals, functions, main}): unit =
  21    let
  22       datatype 'a status =
  23          Undefined
  24        | InScope of 'a
  25        | Defined
  26
  27       fun make' (layout, plist) =
  28          let
  29             val {get, set, ...} =
  30                Property.getSet (plist, Property.initConst Undefined)
  31             fun bind (x, v) =
  32                case get x of
  33                   Undefined => set (x, InScope v)
  34                 | _ => Error.bug (concat ["Ssa2.TypeCheck2.checkScopes: duplicate definition of ",
  35                                           Layout.toString (layout x)])
  36             fun reference x =
  37                case get x of
  38                   InScope v => v
  39                 | _ => Error.bug (concat ["Ssa2.TypeCheck2.checkScopes: reference to ",
  40                                           Layout.toString (layout x),
  41                                           " not in scope"])
  42
  43             fun unbind x = set (x, Defined)
  44          in (bind, ignore o reference, reference, unbind)
  45          end
  46       fun make (layout, plist) =
  47          let val (bind, reference, _, unbind) = make' (layout, plist)
  48          in (fn x => bind (x, ()), reference, unbind)
  49          end
  50
  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)
  57
  58       fun loopObjectCon oc =
  59          let
  60             datatype z = datatype ObjectCon.t
  61             val _ =
  62                case oc of
  63                   Con con => getCon con
  64                 | Tuple => ()
  65                 | Vector => ()
  66          in
  67             ()
  68          end
  69       val {destroy = destroyLoopType, get = loopType, ...} =
  70          Property.destGet
  71          (Type.plist,
  72           Property.initRec
  73           (fn (ty, loopType) =>
  74            let
  75               datatype z = datatype Type.dest
  76               val _ =
  77                  case Type.dest ty of
  78                     CPointer => ()
  79                   | Datatype tycon => getTycon tycon
  80                   | IntInf => ()
  81                   | Object {args, con, ...} =>
  82                        let
  83                           val _ = loopObjectCon con
  84                           val _ = Prod.foreach (args, loopType)
  85                        in
  86                           ()
  87                        end
  88                   | Real _ => ()
  89                   | Thread => ()
  90                   | Weak ty => loopType ty
  91                   | Word _ => ()
  92            in
  93               ()
  94            end))
  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))
  98       fun loopExp exp =
  99          let
 100             val _ =
 101                case exp of
 102                   Const _ => ()
 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)
 107                 | Var x => getVar x
 108          in
 109             ()
 110          end
 111       fun loopStatement (s: Statement.t): unit =
 112          let
 113             val _ =
 114                case s of
 115                   Bind {exp, ty, var, ...} =>
 116                      let
 117                         val _ = loopExp exp
 118                         val _ = loopType ty
 119                         val _ = Option.app (var, fn x => bindVar (x, ty))
 120                      in
 121                         ()
 122                      end
 123                 | Profile _ => ()
 124                 | Update {base, value, ...} =>
 125                      (Base.foreach (base, getVar); getVar value)
 126          in
 127             ()
 128          end
 129          handle exn => Error.reraiseSuffix (exn, concat [" in ", Layout.toString (Statement.layout s)])
 130       val loopTransfer =
 131          fn Arith {args, ty, ...} => (getVars args; loopType ty)
 132           | Bug => ()
 133           | Call {func, args, ...} => (getFunc func; getVars args)
 134           | Case {test, cases, default, ...} =>
 135                let
 136                   fun doit (cases: ('a * 'b) vector,
 137                             equals: 'a * 'a -> bool,
 138                             hash: 'a -> word,
 139                             numExhaustiveCases: IntInf.t) =
 140                      let
 141                         val table = HashSet.new {hash = hash}
 142                         val _ =
 143                            Vector.foreach
 144                            (cases, fn (x, _) =>
 145                             let
 146                                val _ =
 147                                   HashSet.insertIfNew
 148                                   (table, hash x, fn y => equals (x, y),
 149                                    fn () => x,
 150                                    fn _ => Error.bug "Ssa2.TypeCheck2.loopTransfer: redundant branch in case")
 151                             in
 152                                ()
 153                             end)
 154                         val numCases = Int.toIntInf (Vector.length cases)
 155                      in
 156                         case (IntInf.equals (numCases, numExhaustiveCases), isSome default) of
 157                            (true, true) =>
 158                               Error.bug "Ssa2.TypeCheck2.loopTransfer: exhaustive case has default"
 159                          | (false, false) =>
 160                               Error.bug "Ssa2.TypeCheck2.loopTransfer: non-exhaustive case has no default"
 161                          | _ => ()
 162                      end
 163                   fun doitWord (ws, cases) =
 164                      doit (cases, WordX.equals, WordX.hash, WordSize.cardinality ws)
 165                   fun doitCon cases =
 166                      let
 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"
 171                      in
 172                         doit (cases, Con.equals, Con.hash, numExhaustiveCases)
 173                      end
 174                   val _ = getVar test
 175                   val _ =
 176                      case cases of
 177                         Cases.Con cs => doitCon cs
 178                       | Cases.Word (ws, cs) => doitWord (ws, cs)
 179                in
 180                   ()
 181                end
 182           | Goto {args, ...} => getVars args
 183           | Raise xs => getVars xs
 184           | Return xs => getVars xs
 185           | Runtime {args, ...} => getVars args
 186       val loopTransfer =
 187          fn t =>
 188          (loopTransfer t)
 189          handle exn => Error.reraiseSuffix (exn, concat [" in ", Layout.toString (Transfer.layout t)])
 190       fun loopFunc (f: Function.t) =
 191          let
 192             val {args, blocks, raises, returns, start, ...} = Function.dest f
 193             (* Descend the dominator tree, verifying that variable definitions
 194              * dominate variable uses.
 195              *)
 196             fun loop (Tree.T (block, children)): unit =
 197                let
 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
 205                           (statements, fn s =>
 206                            Statement.foreachDef (s, unbindVar o #1))
 207                   val _ = Vector.foreach (args, unbindVar o #1)
 208                in
 209                   ()
 210                end
 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.
 217              *)
 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
 228          in
 229              ()
 230          end
 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, ...} =>
 236                                   bindCon 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)
 247       val _ = getFunc main
 248       val _ = Program.clearTop program
 249       val _ = destroyLoopType ()
 250    in
 251       ()
 252    end
 253
 254 val checkScopes = Control.trace (Control.Detail, "checkScopes") checkScopes
 255
 256 structure Function =
 257    struct
 258       open Function
 259
 260       fun checkProf (f: t): unit =
 261          let
 262             val debug = false
 263             val {blocks, start, ...} = dest f
 264             val {get = labelInfo, rem, set = setLabelInfo, ...} =
 265                Property.getSetOnce
 266                (Label.plist,
 267                 Property.initRaise ("info", Label.layout))
 268             val _ = Vector.foreach (blocks, fn b as Block.T {label, ...} =>
 269                                     setLabelInfo (label,
 270                                                   {block = b,
 271                                                    sources = ref NONE}))
 272             fun goto (l: Label.t, sources: SourceInfo.t list) =
 273                let
 274                   fun bug (msg: string): 'a =
 275                      let
 276                         val _ =
 277                            Vector.foreach
 278                            (blocks, fn Block.T {label, ...} =>
 279                             let
 280                                val {sources, ...} = labelInfo label
 281                                open Layout
 282                             in
 283                                outputl
 284                                (seq [Label.layout label,
 285                                      str " ",
 286                                      Option.layout
 287                                      (List.layout SourceInfo.layout)
 288                                      (!sources)],
 289                                 Out.error)
 290                             end)
 291                      in
 292                         Error.bug
 293                         (concat ["Ssa2.TypeCheck2.checkProf: bug found in ", Label.toString l,
 294                                  ": ", msg])
 295                      end
 296                   val _ =
 297                      if not debug
 298                         then ()
 299                      else
 300                      let
 301                         open Layout
 302                      in
 303                         outputl (seq [str "goto (",
 304                                       Label.layout l,
 305                                       str ", ",
 306                                       List.layout SourceInfo.layout sources,
 307                                       str ")"],
 308                                  Out.error)
 309                      end
 310                   val {block, sources = r} = labelInfo l
 311                in
 312                   case !r of
 313                      NONE =>
 314                         let
 315                            val _ = r := SOME sources
 316                            val Block.T {statements, transfer, ...} = block
 317                            datatype z = datatype Statement.t
 318                            datatype z = datatype ProfileExp.t
 319                            val sources =
 320                               Vector.fold
 321                               (statements, sources, fn (s, sources) =>
 322                                case s of
 323                                   Profile pe =>
 324                                      (case pe of
 325                                          Enter s => s :: sources
 326                                        | Leave s =>
 327                                             (case sources of
 328                                                 [] => bug "unmatched Leave"
 329                                               | s' :: sources =>
 330                                                    if SourceInfo.equals (s, s')
 331                                                       then sources
 332                                                    else bug "mismatched Leave"))
 333                                 | _ => sources)
 334                            val _ =
 335                               if not debug
 336                                  then ()
 337                               else
 338                               let
 339                                  open Layout
 340                               in
 341                                  outputl (List.layout SourceInfo.layout sources,
 342                                           Out.error)
 343                               end
 344                            val _ =
 345                               if (case transfer of
 346                                      Call {return, ...} =>
 347                                         let
 348                                            datatype z = datatype Return.t
 349                                         in
 350                                            case return of
 351                                               Dead => false
 352                                             | NonTail _ => false
 353                                             | Tail => true
 354                                         end
 355                                    | Raise _ => true
 356                                    | Return _ => true
 357                                    | _ => false)
 358                                  then (case sources of
 359                                           [] => ()
 360                                         | _ => bug "nonempty sources when leaving function")
 361                               else ()
 362                         in
 363                            Transfer.foreachLabel
 364                            (transfer, fn l => goto (l, sources))
 365                         end
 366                    | SOME sources' =>
 367                         if List.equals (sources, sources', SourceInfo.equals)
 368                            then ()
 369                         else bug "mismatched block"
 370                end
 371             val _ = goto (start, [])
 372             val _ = Vector.foreach (blocks, fn Block.T {label, ...} => rem label)
 373          in
 374             ()
 375          end
 376    end
 377
 378 fun checkProf (Program.T {functions, ...}): unit =
 379    List.foreach (functions, fn f => Function.checkProf f)
 380
 381 val checkProf = Control.trace (Control.Detail, "checkProf") checkProf
 382
 383 fun typeCheck (program as Program.T {datatypes, ...}): unit =
 384    let
 385       val _ = checkScopes program
 386       val _ =
 387          if !Control.profile <> Control.ProfileNone
 388             then checkProf program
 389          else ()
 390       val {get = conInfo: Con.t -> {result: Type.t,
 391                                     ty: Type.t,
 392                                     tycon: Tycon.t},
 393            set = setConInfo, ...} =
 394          Property.getSetOnce
 395          (Con.plist, Property.initRaise ("Ssa2.TypeCheck2.conInfo", Con.layout))
 396       val conTycon = #tycon o conInfo
 397       val _ =
 398          Vector.foreach
 399          (datatypes, fn Datatype.T {tycon, cons} =>
 400           let
 401              val result = Type.datatypee tycon
 402           in
 403              Vector.foreach (cons, fn {con, args} =>
 404                              setConInfo (con, {result = result,
 405                                                ty = Type.conApp (con, args),
 406                                                tycon = tycon}))
 407           end)
 408       fun inject {sum: Tycon.t, variant: Type.t}: Type.t =
 409          let
 410             val error = fn msg =>
 411                Error.bug (concat ["Ssa2.TypeCheck2.inject (",
 412                                   msg, " ",
 413                                   (Layout.toString o Layout.record)
 414                                   [("sum", Tycon.layout sum),
 415                                    ("variant", Type.layout variant)],
 416                                   ")"])
 417          in
 418             case Type.dest variant of
 419                Type.Object {con, ...} =>
 420                   (case con of
 421                       ObjectCon.Con c =>
 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"
 427          end
 428       fun coerce {from: Type.t, to: Type.t}: unit =
 429          if Type.equals (from, to)
 430             then ()
 431          else Error.bug (concat ["SSa2.TypeCheck2.coerce (",
 432                                  (Layout.toString o Layout.record)
 433                                  [("from", Type.layout from),
 434                                   ("to", Type.layout to)],
 435                                  ")"])
 436       val coerce =
 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)]
 441                                        end,
 442                                     Unit.layout) coerce
 443       fun object {args, con, resultType} =
 444          let
 445             fun err () = Error.bug "Ssa2.TypeCheck2.object (bad object)"
 446          in
 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')
 452                         | _ => false)
 453                       andalso (Vector.foreach2
 454                                (Prod.dest args, Prod.dest args',
 455                                 fn ({elt = t, isMutable = _}, {elt = t', ...}) =>
 456                                 coerce {from = t, to = t'})
 457                                ; true)
 458                       then resultType
 459                    else err ())
 460              | _ => err ()
 461          end
 462       fun base b =
 463          case b of
 464             Base.Object ty => ty
 465           | Base.VectorSub {index, vector} =>
 466                if Type.isVector vector
 467                   then let
 468                           val _ =
 469                              if Type.equals (index, Type.word (WordSize.seqIndex ()))
 470                                 then ()
 471                              else Error.bug "Ssa2.TypeCheck2.base (vector-sub of non seqIndex)"
 472                        in
 473                           vector
 474                        end
 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, ...} =>
 483                let
 484                   val {elt, isMutable} = Prod.sub (args, offset)
 485                   val () = coerce {from = value, to = elt}
 486                   val () =
 487                      if isMutable
 488                         then ()
 489                      else Error.bug "Ssa2.TypeCheck2.update (non-mutable field)"
 490                in
 491                   ()
 492                end
 493           | _ => Error.bug "Ssa2.TypeCheck2.update (non object)"
 494       fun filter {con, test, variant} =
 495          let
 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})
 499          in
 500             ()
 501          end
 502       fun filterWord (from, s) = coerce {from = from, to = Type.word s}
 503       fun primApp {args, prim, resultType, resultVar = _} =
 504          let
 505             datatype z = datatype Prim.Name.t
 506             val () =
 507                if Type.checkPrimApp {args = args,
 508                                      prim = prim,
 509                                      result = resultType}
 510                   then ()
 511                else Error.bug (concat ["Ssa2.TypeCheck2.primApp (",
 512                                        let
 513                                           open Layout
 514                                        in
 515                                           (toString o seq)
 516                                           [Prim.layout prim,
 517                                            str " ",
 518                                            Vector.layout Type.layout args]
 519                                        end,
 520                                        ")"])
 521          in
 522             resultType
 523          end
 524       val _ =
 525          analyze {base = base,
 526                   coerce = coerce,
 527                   const = Type.ofConst,
 528                   filter = filter,
 529                   filterWord = filterWord,
 530                   fromType = fn x => x,
 531                   inject = inject,
 532                   layout = Type.layout,
 533                   object = object,
 534                   primApp = primApp,
 535                   program = program,
 536                   select = select,
 537                   update = update,
 538                   useFromTypeOnBinds = true}
 539       val _ = Program.clear program
 540    in
 541       ()
 542    end
 543
 544 val typeCheck = fn p =>
 545    (typeCheck p)
 546    handle exn => Error.reraisePrefix (exn, "TypeError (SSA2): ")
 547
 548 val typeCheck = Control.trace (Control.Pass, "typeCheck") typeCheck
 549
 550 end