Home My Page Projects Code Snippets Project Openings diderot
Summary Activity Tracker Tasks SCM

SCM Repository

[diderot] View of /branches/vis15/src/compiler/cfg-ir/check-ir-fn.sml
ViewVC logotype

View of /branches/vis15/src/compiler/cfg-ir/check-ir-fn.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3485 - (download) (annotate)
Sun Dec 6 13:48:48 2015 UTC (3 years, 7 months ago) by jhr
File size: 16741 byte(s)
working on merge
(* check-ir-fn.sml
 *
 * This code is part of the Diderot Project (http://diderot-language.cs.uchicago.edu)
 *
 * COPYRIGHT (c) 2015 The University of Chicago
 * All rights reserved.
 *
 * Correctness checker for SSA-based IRs.
 *
 * TODO:
 *      check that the state variables and method stateOut variables are all defined.
 *)

signature OPERATOR_TY =
  sig
    type rator
    type ty

  (* returns the signature of an operator as (rng, dom). *)
    val sigOf : rator -> ty * ty list

  (* return the type of a CONS, where the first argument is the annotated type
   * and the second argument is the list of argument types.  Returns false if
   * there is a type error.
   *)
    val typeOfCons : ty * ty list -> bool

  end

functor CheckIRFn (

    structure IR : SSA
    structure OpTy : OPERATOR_TY
        where type rator = IR.Op.rator
        where type ty = IR.Ty.ty

  ) : sig

  (* check the program for type errors, etc.  The first argument will be used to
   * identify the phase that the check follows and the return result will be true
   * if any errors were detected.
   *)
    val check : string * IR.program -> bool

  end = struct

    structure IR = IR
    structure Ty = IR.Ty
    structure V = IR.Var
    structure VSet = V.Set

  (* forward analysis to determine the variables that are available in blocks *)
    structure Avail = ForwardDFAFn (
      struct

        structure IR = IR
        type t = VSet.set

        val bottom = VSet.empty

        fun join inputs = List.foldl VSet.union bottom inputs

        fun transfer (input, nd as IR.ND{kind, ...}) = (case kind
               of IR.JOIN{phis, ...} => let
                  (* add the lhs of the phi node.  We do not remove the rhs variables, since
                   * after value numbering, they may have further uses.
                   *)
                    fun doPhi ((y, _), vs) = VSet.add(vs, y)
                    val output = List.foldl doPhi input (!phis)
                    in
                      output
                    end
                | IR.ASSIGN{stm=(y, _), ...} => VSet.add(input, y)
                | IR.MASSIGN{stm=(ys, _, _), ...} => VSet.addList(input, ys)
                | _ => input
               (* end case *))

        val same = VSet.equal

        fun toString vs = let
              fun f (v, []) = [IR.Var.toString v, "}"]
                | f (v, l) = IR.Var.toString v :: "," :: l
              in
                if VSet.isEmpty vs then "{}" else String.concat("{" :: VSet.foldl f [] vs)
              end

      end)

    datatype token
      = NL | S of string | A of Atom.atom | V of IR.var | VTYS of IR.var list
      | TY of Ty.ty | TYS of Ty.ty list
      | ND of IR.node

    fun error errBuf toks = let
          fun tok2str NL = "\n  ** "
            | tok2str (S s) = s
            | tok2str (A s) = Atom.toString s
            | tok2str (V x) = V.toString x
            | tok2str (VTYS xs) = tok2str(TYS(List.map V.ty xs))
            | tok2str (TY ty) = Ty.toString ty
            | tok2str (TYS []) = "()"
            | tok2str (TYS[ty]) = Ty.toString ty
            | tok2str (TYS tys) = String.concat[
                  "(", String.concatWith " * " (List.map Ty.toString tys), ")"
                ]
            | tok2str (ND nd) = IR.Node.toString nd
          in
            errBuf := concat ("**** Error: " :: List.map tok2str toks)
              :: !errBuf
          end

    fun checkAssign errFn ((y, rhs), bvs) = let
        (* check a variable use *)
          fun checkVar x = if VSet.member(bvs, x)
                then ()
                else errFn [
                    S "variable ", V x, S " is not bound in", NL,
                    S(IR.assignToString(y, rhs))
                  ]
          fun tyError (ty1, ty2) = errFn [
                  S "type mismatch in \"", S(IR.assignToString (y, rhs)), S "\"",
                  NL, S "lhs: ", TY ty1, NL, S "rhs: ", TY ty2
                ]
          fun checkTys (ty1, ty2) = if Ty.same(ty1, ty2)
                then ()
                else tyError (ty1, ty2)
          in
            (* check that y is not bound twice *)
              if VSet.member(bvs, y)
                then errFn [
                    S "variable ", V y, S " is bound twice in", NL,
                    S(IR.assignToString (y, rhs))
                  ]
                else ();
              case rhs
               of IR.GLOBAL x => checkTys(V.ty y, IR.GlobalVar.ty x)
                | IR.STATE x => checkTys(V.ty y, IR.StateVar.ty x)
                | IR.VAR x => (
                    checkVar x;
                    checkTys (V.ty y, V.ty x))
                | IR.LIT lit => let
                    val ty = (case lit
                           of Literal.Int _ => Ty.intTy
                            | Literal.Real _ => Ty.realTy
                            | Literal.String _ => Ty.StringTy
                            | Literal.Bool _ => Ty.BoolTy
                          (* end case *))
                    in
                      checkTys (V.ty y, ty)
                    end
                | IR.OP(rator, xs) => let
                    val (resTy, argTys) = OpTy.sigOf rator
                    in
                      List.app checkVar xs;
                      checkTys (V.ty y, resTy);
                      if ListPair.allEq (fn (x, ty) => Ty.same(V.ty x, ty)) (xs, argTys)
                        then ()
                        else errFn [
                            S "argument type mismatch in \"", S(IR.assignToString (y, rhs)), S "\"",
                            NL, S "expected: ", TYS argTys,
                            NL, S "found:    ", VTYS xs
                          ]
                    end
                | IR.CONS(xs, ty) => (
                    List.app checkVar xs;
                    if OpTy.typeOfCons (ty, List.map V.ty xs)
                      then checkTys (V.ty y, ty)
                      else errFn [S "invalid ", S(IR.assignToString(y, rhs))])
                | IR.SEQ(xs, ty) => (
                    List.app checkVar xs;
(* FIXME: check types of sequence elements *)())
		| IR.EINAPP(ein, xs) => (
                    List.app checkVar xs;
(* FIXME: check ein *)())
              (* end case *);
              VSet.add(bvs, y)
            end

    fun checkMAssign errFn (stm as (ys, rator, xs), bvs) = let
        (* check that a lhs variable is not bound twice *)
          fun checkBind y = if VSet.member(bvs, y)
                then errFn [
                    S "variable ", V y, S " is bound twice in", NL,
                    S(IR.massignToString stm)
                  ]
                else ()
        (* check a variable use *)
          fun checkVar x = if VSet.member(bvs, x)
                then ()
                else errFn [
                    S "variable ", V x, S " is not bound in", NL,
                    S(IR.massignToString stm)
                  ]
          fun tyError (ty1, ty2) = errFn [
                  S "type mismatch in \"", S(IR.massignToString stm), S "\"",
                  NL, S "lhs: ", TY ty1, NL, S "rhs: ", TY ty2
                ]
          in
            (* check that the lhs variables are not bound twice *)
              List.app checkBind ys;
(* FIXME:
            (* check the types *)
              val (resTys, argTys) = OpTy.sigOf rator
              in
                List.app checkVar xs;
                if ListPair.allEq (fn (y, ty) => Ty.same(V.ty y, ty)) (ys, resTys)
                  then ()
                  else tyError (V.ty y, resTy);
                if ListPair.allEq (fn (x, ty) => Ty.same(V.ty x, ty)) (xs, argTys)
                  then ()
                  else errFn [
                      S "argument type mismatch in \"", S(IR.massignToString stm), S "\"",
                      NL, S "expected: ", TYS argTys,
                      NL, S "found:    ", VTYS xs
                    ]
              end
*)
              VSet.addList(bvs, ys)
            end

    fun checkPhi errFn (nd, bvs, mask) (y, xs) = let
          val ty = V.ty y
          fun chkTy x = if Ty.same(V.ty x, ty)
                  then ()
                  else errFn [
                      S "type mismatch in \"", S(IR.phiToString (y, xs)), S "\"", NL,
                      S "typeof(", V y, S "): ", TY ty, NL,
                      S "typeof(", V x, S "): ", TY(V.ty x)
                    ]
          fun chkRHS ([], []) = ()
            | chkRHS (true::ms, NONE::xs) = chkRHS (ms, xs)
            | chkRHS (false::ms, (SOME x)::xs) = (chkTy x; chkRHS (ms, xs))
            | chkRHS _ = errFn [S "phi/mask mismatch in ", ND nd]
          in
          (* check that y is not bound twice *)
            if VSet.member(bvs, y)
              then errFn [
                  S "variable ", V y, S " is bound twice in", NL,
                  S(IR.phiToString (y, xs))
                ]
              else ();
          (* check that rhs vars have the correct type *)
            chkRHS (mask, xs)
          end

    fun check (phase, prog) = let
	  val IR.Program{
		  props, consts, inputs, globals,
		  constInit, globalInit, strand, create, update
		} = prog
          val errBuf = ref []
          val errFn = error errBuf
          fun final () = (case !errBuf
                 of [] => false
                  | errs => (
                      Log.msg(concat["********** IR Errors detected after ", phase, " **********\n"]);
                      List.app (fn msg => Log.msg(msg ^ "\n")) (List.rev errs);
                      true)
                (* end case *))
          val checkPhi = checkPhi errFn
          val checkAssign = checkAssign errFn
          val checkMAssign = checkMAssign errFn
          fun checkCFG (vs, cfg) = let
                val bvs = VSet.fromList vs
              (* compute the variables available on entry to each block *)
                val nodes = Avail.analyse (bvs, cfg)
              (* check the edges of a node.  For each predecessor, the node should appear in the
               * successor list and for each successor, the node should appear in the predecessor
               * list.
               *)
                fun checkEdges nd = let
                      fun eqNd nd' = IR.Node.same(nd, nd')
                      fun chkPred src = if List.exists eqNd (IR.Node.succs src)
                            then ()
                            else errFn [
                                S "predecessor edge from ", ND nd, S " -> ", ND src,
                                S " not matched by successor edge"
                              ]
                      fun chkSucc dst = if List.exists eqNd (IR.Node.preds dst)
                            then ()
                            else errFn [
                                S "successor edge from ", ND nd, S " -> ", ND dst,
                                S " not matched by predecessor edge"
                              ]
                      in
                        List.app chkPred (IR.Node.preds nd);
                        List.app chkSucc (IR.Node.succs nd)
                      end
                fun checkNd (nd as IR.ND{kind, ...}) = (case kind
                       of IR.NULL => errFn [S "unexpected ", ND nd]
                        | IR.JOIN{mask, phis, ...} =>
                            List.app
                              (checkPhi (nd, VSet.union(Avail.inValue nd, bvs), !mask))
                                (!phis)
                        | IR.COND{cond, ...} =>
                            if VSet.member(Avail.inValue nd, cond)
                            orelse VSet.member(bvs, cond)
                              then ()
                              else errFn [S "unbound variable ", V cond, S " in conditional"]
			| IR.FOREACH{phis, mask, var, src, ...} => (
			    if VSet.member(Avail.inValue nd, src)
                            orelse VSet.member(bvs, src)
                              then ()
                              else errFn [S "unbound variable ", V src, S " in foreach"];
			    List.app
                              (checkPhi (nd, VSet.union(Avail.inValue nd, bvs), !mask))
                                (!phis))
                        | IR.ASSIGN{stm, ...} =>
                            ignore (checkAssign (stm, VSet.union(Avail.inValue nd, bvs)))
                        | IR.MASSIGN{stm, ...} =>
                            ignore (checkMAssign (stm, VSet.union(Avail.inValue nd, bvs)))
                        | IR.GASSIGN{lhs, rhs, ...} => let
                            val bvs = VSet.union(Avail.inValue nd, bvs)
                            in
                              if VSet.member(bvs, rhs)
                                then ()
                                else errFn [
                                    S "variable ", V rhs, S " is not bound in global assignment ",
                                    S(IR.GlobalVar.toString lhs)
                                  ];
                              if Ty.same(IR.GlobalVar.ty lhs, V.ty rhs)
                                then ()
                                else errFn [
                                    S "type mismatch in \"", S(IR.GlobalVar.toString lhs),
                                    S " = ", S(V.toString rhs), S "\"",
                                    NL, S "lhs: ", TY(IR.GlobalVar.ty lhs),
                                    NL, S "rhs: ", TY(V.ty rhs)
                                  ]
                            end
                        | IR.NEW{strand, args, ...} => let
                            val bvs = VSet.union(Avail.inValue nd, bvs)
                          (* check a variable use *)
                            fun checkVar x = if VSet.member(bvs, x)
                                  then ()
                                  else errFn [
                                      S "variable ", V x, S " is not bound in new ",
                                      S(Atom.toString strand)
                                    ]
                            in
                              List.app checkVar args
                            end
                        | IR.SAVE{lhs, rhs, ...} => let
                            val bvs = VSet.union(Avail.inValue nd, bvs)
                            in
                              if VSet.member(bvs, rhs)
                                then ()
                                else errFn [
                                    S "variable ", V rhs, S " is not bound in save ",
                                    S(IR.StateVar.toString lhs)
                                  ];
                              if Ty.same(IR.StateVar.ty lhs, V.ty rhs)
                                then ()
                                else errFn [
                                    S "type mismatch in \"", S(IR.StateVar.toString lhs),
                                    S " = ", S(V.toString rhs), S "\"",
                                    NL, S "lhs: ", TY(IR.StateVar.ty lhs),
                                    NL, S "rhs: ", TY(V.ty rhs)
                                  ]
                            end
                        | _ => ()
                      (* end case *))
                in
                  List.app checkEdges nodes;
                  List.app checkNd nodes;
                (* cleanup *)
                  Avail.scrub nodes
                end
        (* check a strand definition *)
          fun checkStrand (IR.Strand{name, params, state, stateInit, initM, updateM, stabilizeM}) =
		let
                val nStateVars = List.length state
                val extraVars = params
                fun checkMethod body = checkCFG (extraVars, body)
(*DEBUG*)handle ex => raise ex
                in
                  checkCFG (extraVars, stateInit)
(*DEBUG*)handle ex => raise ex;
		  Option.app checkMethod initM;
		  checkMethod updateM;
		  Option.app checkMethod stabilizeM
                end
        (* handle exceptions *)
          fun onExn exn =
		errFn (S "uncaught exception: " :: S(exnMessage exn) ::
		  List.foldr (fn (s, msg) => NL :: S "    raised at " :: S s :: msg)
		    [] (SMLofNJ.exnHistory exn))
	  fun checkCFG' cfg = (checkCFG ([], cfg) handle ex => onExn ex)
          in
          (* check the input part *)
            checkCFG' constInit;
          (* check the global part *)
            checkCFG' globalInit;
	  (* check initial strand creation *)
	    case create of IR.Create{dim, code} => checkCFG' code;
          (* check the strands *)
            (checkStrand strand) handle ex => onExn ex;
	  (* check the optional global update *)
	    Option.app checkCFG' update;
          (* check for errors *)
            final()
          end

  end

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0