(* Pasted from Pottier's PP compiler *)

open ERTL
open Untrusted_interference

let build globals int_fun uses liveafter =

  (* Create an interference graph whose vertices are the procedure's
     pseudo-registers. This graph initially has no edges. *)

  let f_locals =
   Identifiers.foldi PreIdentifiers.RegisterTag
    (fun id _ map -> Pset.add id map
    ) uses Pset.empty in

  let graph = create f_locals in

  (* Every pseudo register interferes with special forbidden registers. *)

  let graph = mkiph graph f_locals
   (Untrusted_interference.hwregisterset_of_list I8051.registersForbidden) in

  (* Iterate over all statements in the control flow graph and populate the
     interference graph with interference and preference edges. *)

  let graph =
    Identifiers.foldi PreIdentifiers.LabelTag (fun label stmt graph ->
      let live = liveafter label in
      if Liveness.eliminable globals live stmt = Bool.True then

	  (* This statement is eliminable and should be ignored. Eliminable
	     statements have not been eliminated yet, because we are still
	     in between ERTL and LTL. They *will* be eliminated soon, though,
	     so there is no reason to take them into account while building
	     the interference graph. *)

	  graph

      else

	  (* Create interference edges. The general rule is, every
	     pseudo-register or hardware register that is defined (written) by
	     a statement interferes with every pseudo-register or hardware
	     register (other than itself) that is live immediately after the
	     statement executes.

	     An exception to the general rule can be made for move
	     statements. In a move statement, we do not need the source
	     and destination pseudo-registers to be assigned distinct hardware
	     registers, since they contain the same value -- in fact, we would
	     like them to be assigned the same hardware register. So, for a
	     move statement, we let the register that is defined (written)
	     interfere with every pseudo-register, other than itself *and
	     other than the source pseudo-register*, that is live immediately
	     after the statement executes. This optimization is explained in
	     Chapter 10 of Appel's book (p. 221).

	     This special case is only a hack that works in many cases. There
	     are cases where it doesn't suffice. For instance, if two
	     successive move statements have the same source [r0], then
	     their destinations [r1] and [r2] *will* be considered as
	     interfering, even though it would in fact be correct and
	     desirable to map both of them to the same hardware register. A
	     more general solution would be to perform a static analysis that
	     determines, for every program point, which pseudo-registers
	     definitely hold the same value, and to exploit this information
	     to build fewer interference edges. *)

	  let defined = Liveness.defined globals stmt in
	  let exceptions =
	    match stmt with
	    | Joint.Sequential (Joint.Step_seq (Joint.MOVE arg),_) ->
               (match Obj.magic arg with
                  {Types.snd = Joint.Reg (ERTL.PSD sourcer)} ->
		   Liveness.rl_psingleton sourcer
	        | {Types.snd = Joint.Reg (ERTL.HDW sourcehwr)} ->
		   Liveness.rl_hsingleton sourcehwr
                | _ -> Liveness.rl_bottom)
	    | _ ->
		Liveness.rl_bottom
	  in
	  let graph =
	    mki graph (Obj.magic (Liveness.rl_diff live exceptions))
             (Obj.magic defined)
	  in

(*
	  (* Two registers written at the same time are interfering (they
	     obviously should not be associated the same address).
	     Only happens with St_addr. *)

	  let graph =
	    match stmt with
	      | St_addr (r1, r2, _, _) ->
		mki graph (Liveness.L.psingleton r1) (Liveness.L.psingleton r2)
	      | _ ->
		graph
	  in
*)

	  (* Create preference edges between pseudo-registers. Two registers
	     should preferably be assigned the same color when they are
	     related by a move statement, so that the move statement can
	     be eliminated. *)

	  let graph =
	    match stmt with
	    | Joint.Sequential (Joint.Step_seq (Joint.MOVE arg),_) ->
               (match Obj.magic arg with
                  {Types.fst = ERTL.PSD r1 ; snd = Joint.Reg (ERTL.PSD r2)} ->
		    mkppp graph r1 r2
                | {Types.fst = ERTL.PSD r1 ; snd = Joint.Reg (ERTL.HDW r2)}
                | {Types.fst = ERTL.HDW r2 ; snd = Joint.Reg (ERTL.PSD r1)} ->
		    mkpph graph r1 r2
                | _ -> graph)
	    | _ ->
		graph
	  in
  (*

	  (* Add interference edges between the hardware register [$zero]
	     and every pseudo-register that the statement renders
	     nonzeroable. See [Zero] for an explanation. *)

	  let graph =
	    mkiph graph (Zero.nonzeroable i) (MIPS.RegisterSet.singleton MIPS.zero)
	  in
  *)
	  graph

    ) (Obj.magic int_fun.Joint.joint_if_code) graph
  in

  (* Done. *)

  graph