(* Pasted from Pottier's PP compiler *)
open ERTL
(* In the following, a ``variable'' means a pseudo-register or an
allocatable hardware register. *)
(* These functions allow turning an [ERTL] control flow graph into an
explicit graph, that is, making successor edges explicit. This is
useful in itself and facilitates the computation of predecessor
edges. *)
let statement_successors (stmt : statement) =
match stmt with
| St_return _ ->
Label.Set.empty
| St_skip l
| St_comment (_, l)
| St_cost (_, l)
| St_set_hdw (_, _, l)
| St_get_hdw (_, _, l)
| St_hdw_to_hdw (_, _, l)
| St_newframe l
| St_delframe l
| St_framesize (_, l)
| St_push (_, l)
| St_pop (_, l)
| St_addrH (_, _, l)
| St_addrL (_, _, l)
| St_int (_, _, l)
| St_move (_, _, l)
| St_opaccs (_, _, _, _, l)
| St_op1 (_, _, _, l)
| St_op2 (_, _, _, _, l)
| St_clear_carry l
| St_load (_, _, _, l)
| St_store (_, _, _, l)
| St_call_id (_, _, l) ->
Label.Set.singleton l
| St_condacc (_, l1, l2) ->
Label.Set.add l1 (Label.Set.singleton l2)
(* The analysis uses the lattice of sets of variables. The lattice's
join operation is pointwise set union, which reflects the fact that
a variable is deemed live at a program point if and only if it is
live at any of the successors of that program point. *)
module L = struct
(* A set of variable is represented as a pair of a set of
pseudo-registers and a set of hardware registers. *)
type t =
Register.Set.t * I8051.RegisterSet.t
type property =
t
let bottom =
Register.Set.empty, I8051.RegisterSet.empty
let psingleton r =
Register.Set.singleton r, I8051.RegisterSet.empty
let hsingleton hwr =
Register.Set.empty, I8051.RegisterSet.singleton hwr
let join (rset1, hwrset1) (rset2, hwrset2) =
(Register.Set.union rset1 rset2, I8051.RegisterSet.union hwrset1 hwrset2)
let diff (rset1, hwrset1) (rset2, hwrset2) =
(Register.Set.diff rset1 rset2, I8051.RegisterSet.diff hwrset1 hwrset2)
let equal (rset1, hwrset1) (rset2, hwrset2) =
Register.Set.equal rset1 rset2 && I8051.RegisterSet.equal hwrset1 hwrset2
let is_maximal _ =
false
end
module Label_ImperativeMap = struct
type key =
Label.Map.key
type 'data t =
'data Label.Map.t ref
let create () =
ref Label.Map.empty
let clear t =
t := Label.Map.empty
let add k d t =
t := Label.Map.add k d !t
let find k t =
Label.Map.find k !t
let iter f t =
Label.Map.iter f !t
end
module F = Fix.Make (Label_ImperativeMap) (L)
(* These are the sets of variables defined at (written by) a statement. *)
let defined (stmt : statement) : L.t =
match stmt with
| St_skip _
| St_comment _
| St_cost _
| St_push _
| St_clear_carry _
| St_store _
| St_condacc _
| St_return _ ->
L.bottom
| St_op2 (I8051.Add, r, _, _, _)
| St_op2 (I8051.Addc, r, _, _, _)
| St_op2 (I8051.Sub, r, _, _, _) ->
L.join (L.hsingleton I8051.carry) (L.psingleton r)
| St_op1 (I8051.Inc, r, _, _) ->
L.join (L.hsingleton I8051.carry) (L.psingleton r)
| St_get_hdw (r, _, _)
| St_framesize (r, _)
| St_pop (r, _)
| St_int (r, _, _)
| St_addrH (r, _, _)
| St_addrL (r, _, _)
| St_move (r, _, _)
| St_opaccs (_, r, _, _, _)
| St_op1 (_, r, _, _)
| St_op2 (_, r, _, _, _)
| St_load (r, _, _, _) ->
L.psingleton r
| St_set_hdw (r, _, _)
| St_hdw_to_hdw (r, _, _) ->
L.hsingleton r
| St_call_id _ ->
(* Potentially destroys all caller-save hardware registers. *)
Register.Set.empty, I8051.caller_saved
| St_newframe _
| St_delframe _ ->
L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
let set_of_list rl =
List.fold_right I8051.RegisterSet.add rl I8051.RegisterSet.empty
(* This is the set of variables used at (read by) a statement. *)
let dptr =
I8051.RegisterSet.add I8051.dph (I8051.RegisterSet.singleton I8051.dpl)
let used (stmt : statement) : L.t =
match stmt with
| St_skip _
| St_comment _
| St_cost _
| St_framesize _
| St_pop _
| St_addrH _
| St_addrL _
| St_int _
| St_clear_carry _ ->
L.bottom
| St_call_id (_, nparams, _) ->
(* Reads the hardware registers that are used to pass parameters. *)
Register.Set.empty,
set_of_list (MiscPottier.prefix nparams I8051.parameters)
| St_get_hdw (_, r, _)
| St_hdw_to_hdw (_, r, _) ->
L.hsingleton r
| St_set_hdw (_, r, _)
| St_push (r, _)
| St_move (_, r, _)
| St_op1 (_, _, r, _)
| St_condacc (r, _, _) ->
L.psingleton r
| St_op2 (I8051.Addc, _, r1, r2, _) ->
L.join (L.join (L.psingleton r1) (L.psingleton r2))
(L.hsingleton I8051.carry)
| St_opaccs (_, _, r1, r2, _)
| St_op2 (_, _, r1, r2, _)
| St_load (_, r1, r2, _) ->
L.join (L.psingleton r1) (L.psingleton r2)
| St_store (r1, r2, r3, _) ->
L.join (L.join (L.psingleton r1) (L.psingleton r2)) (L.psingleton r3)
| St_newframe _
| St_delframe _ ->
L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
| St_return _ ->
Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved dptr
(* A statement is considered pure if it has no side effect, that is, if
its only effect is to write a value to its destination variable.
A pure statement whose destination is dead after the statement will
be eliminated during the translation of [ERTL] to [LTL]. This is done by
replacing the statement with an [St_skip] statement.
[eliminable liveafter stmt] returns [Some l], where [l] is [stmt]'s single
successor, if statement [stmt] is eliminable. Otherwise, it returns
[None]. The parameter [liveafter] is the set of variables that are live
after the statement. *)
let eliminable ((pliveafter, hliveafter) : L.t) (stmt : statement) =
match stmt with
| St_skip _
| St_comment _
| St_cost _
| St_newframe _
| St_delframe _
| St_pop _
| St_push _
| St_clear_carry _
| St_store _
| St_call_id _
| St_condacc _
| St_return _ ->
None
| St_get_hdw (r, _, l)
| St_framesize (r, l)
| St_int (r, _, l)
| St_addrH (r, _, l)
| St_addrL (r, _, l)
| St_move (r, _, l)
| St_opaccs (_, r, _, _, l)
| St_op1 (_, r, _, l)
| St_op2 (_, r, _, _, l)
| St_load (r, _, _, l) ->
if (Register.Set.mem r pliveafter) ||
(I8051.RegisterSet.mem I8051.carry hliveafter) then None else Some l
| St_set_hdw (r, _, l)
| St_hdw_to_hdw (r, _, l) ->
if I8051.RegisterSet.mem r hliveafter then None else Some l
(* This is the abstract semantics of instructions. It defines the
variables that are live before the instruction in terms of
those that are live after the instruction. *)
(* The standard definition is: a variable is considered live
before the instruction if either (1) it is used by the instruction,
or (2) it is live after the instruction and not defined by the
instruction.
As an exception to this rule, if the instruction is eliminable,
then a variable is considered live before the instruction
if and only if it is live after the instruction. This anticipates
on the instruction's elimination.
This exception means that the source variables of a pure
instruction need not be considered live if the instruction's result
is unused. This allows a sequence of pure instructions whose end
result is dead to be considered entirely dead.
It is a simple, but not entirely trivial, exercise to check that
this transfer function is monotone. *)
let statement_semantics (stmt : statement) (liveafter : L.t) : L.t =
match eliminable liveafter stmt with
| None ->
L.join (L.diff liveafter (defined stmt)) (used stmt)
| Some _ ->
liveafter
(* A valuation is a function that maps a program point (a control flow
graph label) to the set of variables that are live after that
point. *)
type valuation =
Label.t -> L.t
(* This is how we turn an [ERTL] procedure into a liveness analysis
problem and solve it. *)
let analyze (int_fun : internal_function) : valuation =
(* Formulate the problem. Construct a system (recursive) equations
that describe the live variables before and after each
instruction. *)
(* The following two functions, [livebefore] and [liveafter],
define these equations. Both use an oracle, a valuation --
also called [liveafter] -- which is supposed to tell us
which variables are live after each label. *)
(* The live variables before an instruction are computed, using the
instruction's semantics, in terms of the live variables after the
instruction -- which are given by the oracle. *)
let livebefore label (liveafter : valuation) : L.t =
let stmt : statement = Label.Map.find label int_fun.f_graph in
statement_semantics stmt (liveafter label)
in
(* The live variables after an instruction are the union of the live
variables before each of the instruction's successors. *)
let liveafter label (liveafter : valuation) : L.t =
let stmt : statement = Label.Map.find label int_fun.f_graph in
Label.Set.fold (fun successor accu ->
L.join (livebefore successor liveafter) accu
) (statement_successors stmt) L.bottom
in
(* Compute the least fixed point of these recursive equations. *)
F.lfp liveafter