(* 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_opaccsA (_, _, _, _, l)
  | St_opaccsB (_, _, _, _, l)
  | St_op1 (_, _, _, l)
  | St_op2 (_, _, _, _, l)
  | St_clear_carry l
  | St_set_carry l
  | St_load (_, _, _, l)
  | St_store (_, _, _, l)
  | St_call_id (_, _, l)
  | St_call_ptr (_, _, _, l) ->
    Label.Set.singleton l
  | St_cond (_, 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_store _
  | St_cond _
  | St_return _ ->
    L.bottom
  | St_clear_carry _
  | St_set_carry _ ->
    Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
  | 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, _, _)
  | St_get_hdw (r, _, _)
  | St_framesize (r, _)
  | St_pop (r, _)
  | St_int (r, _, _)
  | St_addrH (r, _, _)
  | St_addrL (r, _, _)
  | St_move (r, _, _)
  | St_opaccsA (_, r, _, _, _)
  | St_opaccsB (_, 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 _ | St_call_ptr _  ->
      (* 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 set_of_list =
  let f set r = I8051.RegisterSet.add r set in
  List.fold_left f I8051.RegisterSet.empty

let ret_regs = set_of_list I8051.rets

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 _
  | St_set_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_call_ptr (r1, r2, nparams, _) ->
    (* Reads the hardware registers that are used to pass parameters. *)
    Register.Set.of_list [r1 ; r2],
    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_cond (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_opaccsA (_, _, r1, r2, _)
  | St_opaccsB (_, _, 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 ret_regs

(* 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_set_carry _
  | St_store _
  | St_call_id _
  | St_call_ptr _
  | St_cond _
  | 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_opaccsA (_, r, _, _, l)
  | St_opaccsB (_, 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