(* check-il-fn.sml
 *
 * COPYRIGHT (c) 2010 The Diderot Project (http://diderot.cs.uchicago.edu)
 * All rights reserved.
 *
 * Correctness checker for SSA-based ILs.
 *
 * 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 argument types
   * are given.  Returns NONE if the argument types are
   * invalid for the IL.
   *)
    val typeOfCons : ty list -> ty option

  end

functor CheckILFn (

    structure IL : SSA
    structure OpTy : OPERATOR_TY
	where type rator = IL.Op.rator
	where type ty = IL.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 * IL.program -> bool

  end = struct

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

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

	structure IL = IL
	type t = VSet.set

	val bottom = VSet.empty

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

	fun transfer (input, IL.ND{kind, ...}) = (case kind
	       of IL.NULL => raise Fail "unexpected NULL"
		| IL.JOIN{phis, ...} => let
		  (* add the lhs of the phi node, while removing the rhs variables *)
		    fun doPhi ((y, xs), vs) =
			  VSet.add(
			    VSet.difference(vs, VSet.fromList xs),
			    y)
		    in
		      List.foldl doPhi input (!phis)
		    end
		| IL.BLOCK{body, ...} => let
		    fun doAssign ((y, _), vs) = VSet.add(vs, y)
		    in
		      List.foldl doAssign input (!body)
		    end
		| _ => input
	       (* end case *))

	val same = VSet.equal

	fun toString vs = let
	      fun f (v, []) = [IL.Var.toString v, "}"]
		| f (v, l) = IL.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 | V of IL.var | VTYS of IL.var list | TY of Ty.ty | TYS of Ty.ty list

    fun error errBuf toks = let
	  fun tok2str NL = "\n  ** "
	    | tok2str (S s) = 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), ")"
		]
	  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(IL.assignToString(y, rhs))
		  ]
	  fun tyError (ty1, ty2) = errFn [
		  S "type mismatch in \"", S(IL.assignToString (y, rhs)), S "\"",
		  NL, S "lhs: ", TY ty1, NL, S "rhs: ", TY 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(IL.assignToString (y, rhs))
		  ]
		else ();
	      case rhs
	       of IL.VAR x => (
		    checkVar x;
		    if Ty.same(V.ty y, V.ty x)
		      then ()
		      else tyError (V.ty y, V.ty x))
		| IL.LIT lit => let
		    val ty = (case lit
			   of Literal.Int _ => Ty.intTy
			    | Literal.Float _ => Ty.realTy
			    | Literal.String _ => Ty.StringTy
			    | Literal.Bool _ => Ty.BoolTy
			  (* end case *))
		    in
		      if Ty.same(V.ty y, ty)
			then ()
			else tyError (V.ty y, ty)
		    end
		| IL.OP(rator, xs) => let
		    val (resTy, argTys) = OpTy.sigOf rator
		    in
		      List.app checkVar xs;
		      if Ty.same(V.ty y, resTy)
			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(IL.assignToString (y, rhs)), S "\"",
			    NL, S "expected: ", TYS argTys,
			    NL, S "found:    ", VTYS xs
			  ]
		    end
		| IL.CONS xs => (
		    List.app checkVar xs;
		    case OpTy.typeOfCons (List.map V.ty xs)
		     of NONE => errFn [S "invalid ", S(IL.assignToString(y, rhs))]
		      | SOME ty => if Ty.same(V.ty y, ty)
			  then ()
			  else tyError (V.ty y, ty)
		    (* end case *))
	      (* end case *);
	      VSet.add(bvs, y)
	    end

    fun checkPhi errFn bvs (y, xs) = let
	  val ty = V.ty y
	  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(IL.phiToString (y, xs))
		]
	      else ();
	  (* check that rhs vars have the correct type *)
	    if List.all (fn x => Ty.same(V.ty x, ty)) xs
	      then ()
	      else errFn [
		  S "type mismatch in \"", S(IL.phiToString (y, xs)), S "\"",
		  NL, S "lhs: ", TY ty, NL, S "rhs: ", VTYS xs
		]
	  end

    fun check (phase, IL.Program{globals, globalInit, actors}) = let
	  val errBuf = ref []
	  val errFn = error errBuf
	  fun final () = (case !errBuf
		 of [] => false
		  | errs => (
		      Log.msg(concat["********** IL 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
	  fun checkStmt (vs, stm) = let
		val bvs = VSet.fromList vs
	      (* compute the variables available on entry to each block *)
		val nodes = Avail.analyse (bvs, stm)
		fun checkNd (nd as IL.ND{kind, ...}) = (case kind
		       of IL.NULL => raise Fail "unexpected NULL"
			| IL.JOIN{phis, ...} =>
			    List.app (checkPhi (VSet.union(Avail.inValue nd, bvs))) (!phis)
			| IL.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"]
			| IL.BLOCK{body, ...} =>
			    ignore (List.foldl checkAssign (VSet.union(Avail.inValue nd, bvs)) (!body))
			| IL.NEW{actor, 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 actor)
				    ]
			    in
			      List.app checkVar args
			    end
			| _ => ()
		      (* end case *))
		in
		  List.app checkNd nodes;
		(* cleanup *)
		  Avail.scrub nodes
		end
	(* check an actor definition *)
	  fun checkActor (IL.Actor{params, state, stateInit, methods, ...}) = let
		fun checkMethod (IL.Method{stateIn, body, ...}) =
		      checkStmt (globals@stateIn, body)
		in
		  checkStmt (globals@params, stateInit);
		  List.app checkMethod methods
		end
	  in
	  (* check the global part *)
	    checkStmt ([], globalInit);
	  (* check the actors *)
	    List.app checkActor actors;
	  (* check for errors *)
	    final()
	  end

  end