(* 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.foldi0 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.foldi0 PreIdentifiers.LabelTag (fun label stmt graph ->
let live = liveafter label in
match Glue.option_of_matitaoption (Liveness.eliminable globals live stmt) with
| Some _ ->
(* 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
| None ->
(* 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