source: Deliverables/D2.2/8051/src/RTLabs/redundancyElimination.ml @ 1580

(** This module implements partial redundancy elimination, which subsumes
    common subexpression elimination and loop-invariant code motion.
    This is a reformulation of material found in Muchnick, Advanced compiler
    design and implementation. *)


open RTLabs
open AST

module Trans = GraphUtilities.Trans(RTLabsGraph)(RTLabsGraph)
module Util = GraphUtilities.Util(RTLabsGraph)

(* Notes: To move loop-invariant computation, peeling is needed. It would *)
(* also profit from algebraic transformations that piece together *)
(* loop-constants: if x and y are loop-invariants, then x*y*i won't be *)
(* optimized unless it is transformed to (x*y)*i. Pretty important for *)
(* array addresses. *)

(* Why I'm removing critical edge elimination:
   It seems to me that the invariant about the presence of labels after
   every branching prevents critical edges from appearing: every time a node
   has more than one successor, all of its successors are cost emit statements.

   We cannot jump directly to such a cost emittance from elsewhere. *)

(* (\* ----- PHASE 0 : critical edge elimination ------ *\) *)

(* (\* a critical edge is one between a node with several successors and a node*\) *)
(* (\* with several predecessors. In order for the optimization to work best   *\) *)
(* (\* these must be avoided, inserting an empty node in-between. *\) *)
(* (\* Note: maybe in our case we can avoid this, as branchings will have *\) *)
(* (\* emit cost nodes afterwards. To be checked. Empirically I haven't found *\) *)
(* (\* an example where this transformation really applies. *\) *)

(* (\* a labels will not be in the domain of the map if it does not have any *)
(*    predecessor. It will be bound to false if it has just one of them, *)
(*    and it will bound to true is it has more than two *\) *)
(* let mark_multi_predecessor *)
(*     (g : graph) *)
(*     : bool Label.Map.t = *)
(*   let f lbl s m = *)
(*     let f' m succ = *)
(*       try *)
(*         if Label.Map.find succ m then *)
(*           m *)
(*         else *)
(*           Label.Map.add succ true m *)
(*       with *)
(*         | Not_found -> Label.Map.add succ false m in *)
(*     List.fold_left f' m (RTLabsGraph.successors s) in *)
(*   Label.Map.fold f g Label.Map.empty *)

(* (\* will give the set of nodes that *)
(*    1) have more than one successor *)
(*    2) at least one of those successors has more *)
(*       than one predecessor *\) *)
(* let remove_critical_edges fresh g = *)
(*   let multi_pred_marks = mark_multi_predecessor g in *)
(*   let is_multi_pred lbl = *)
(*     try Label.Map.find lbl multi_pred_marks with *)
(*       | Not_found -> false in *)
(*   let trans () l = function *)
(*     | St_cond (r, l1, l2) when is_multi_pred l1 || is_multi_pred l2 -> *)
(*         ((), [St_cond (r, l, l)], [[] ; []], [[l1] ; [l2]]) *)
(*     | St_jumptable (r, ls) *)
(*       when List.length ls > 1 && List.exists is_multi_pred ls -> *)
(*       let blocks = MiscPottier.make [] (List.length ls) in *)
(*       let succs = List.map (fun l -> [l]) ls in *)
(*       ((), [St_jumptable (r, [])], blocks, succs) *)
(*     | stmt -> ((), [], [[stmt]], [RTLabsGraph.successors stmt]) in *)
(*   snd (Trans.translate_general trans fresh () g) *)

(* let critical_edge_elimination *)
(*     (f_def : internal_function) *)
(*     : internal_function = *)
(*   let g = f_def.f_graph in *)
(*   let fresh () = Label.Gen.fresh f_def.f_luniverse in *)
(*   { f_def with f_graph = remove_critical_edges fresh g } *)

(* Expressions, expression sets, and operations thereof *)

(* Load and store ops are not taken into account, maybe later *)
type expr =
  (* | Cst of cst (\* do we need to consider constants? only big ones? *\) *)
  | UnOp of op1 * Register.t * AST.sig_type
  | BinOp of op2 * argument * argument * AST.sig_type

let expr_of_stmt type_of (s : statement) : expr option = match s with
  (* | St_cst (_, c, _) -> Some (Cst c) *)
  | St_op1 (op, r, s, _) when op <> Op_id ->
    Some (UnOp (op, s, type_of r))
  | St_op2 (op, r, s, t, _) -> Some (BinOp (op, s, t, type_of r))
  | _ -> None

let expr_of type_of (g : graph) (n : Label.t) : expr option =
  expr_of_stmt type_of (Label.Map.find n g)

(* the register modified by a node *)
let modified_at_stmt = RTLabsGraph.modified_at_stmt

let modified_at = RTLabsGraph.modified_at

(* registers on which the value computed at the statement depends, which are*)
(* needed if the modified register is needed. Below used_at lists those*)
(* registers that may be needed regardless (i.e. in non-side-effect-free *)
(* statements).*)
let vars_of_stmt = function
  | St_op2 (_, _, Reg s, Reg t, _) ->
    Register.Set.add s (Register.Set.singleton t)
  | St_load (_, Reg s, _, _)
  | St_op1 (_, _, s, _)
  | St_op2 (_, _, Reg s, _, _)
  | St_op2 (_, _, _, Reg s, _) -> Register.Set.singleton s
  | _ -> Register.Set.empty

let vars_of (g : graph) (n : Label.t) : Register.Set.t =
  vars_of_stmt (Label.Map.find n g)

(* used in possibly non side-effect-free statements *)
let used_at_stmt stmt =
  let add_arg s = function
    | Reg r -> Register.Set.add r s
    | Imm _ -> s in
  match stmt with
    | St_call_id (_, rs, _, _, _)
    | St_call_ptr (_, rs, _, _, _)
    | St_tailcall_id (_, rs, _)
    | St_tailcall_ptr (_, rs, _) ->
      List.fold_left add_arg Register.Set.empty rs
    | St_store (_, a, b, _) ->
      add_arg (add_arg Register.Set.empty a) b
    | St_return (Some (Reg r))
    | St_cond (r, _, _) -> Register.Set.singleton r
    | _ -> Register.Set.empty

let used_at g n = used_at_stmt (Label.Map.find n g)

module ExprOrdered = struct
  type t = expr
  let compare = compare
end

module ExprSet = Set.Make(ExprOrdered)
module ExprMap = Map.Make(ExprOrdered)

type expr_set = ExprSet.t

let ( ^^ ) = ExprSet.inter

let ( ++ ) = ExprSet.union

let ( ++* ) s = function
  | None -> s
  | Some e -> ExprSet.add e s

let ( --* ) s = function
  | None -> s
  | Some e -> ExprSet.remove e s

let ( -- ) = ExprSet.diff

let big_inter (f : Label.t -> ExprSet.t) (ls : Label.t list) : ExprSet.t =
        (* generalized intersection, but in case of empty list it is empty *)
  match ls with
    | [] -> ExprSet.empty
    (* these two cases are singled out for speed, as they will be common *)
    | [l] -> f l
    | [l1 ; l2] -> f l1 ^^ f l2
    | l :: ls ->
      let inter s l' = s ^^ f l' in
      List.fold_left inter (f l) ls

let big_union (f : Label.t -> Register.Set.t) (ls : Label.t list)
    : Register.Set.t =
  (* generalized union *)
  let union s l' = Register.Set.union s (f l') in
  List.fold_left union Register.Set.empty ls

let filter_unchanged (r : Register.t option) (s : expr_set) : expr_set =
  match r with
    | None -> s
    | Some r ->
      let filter = function
        | UnOp (_, s, _) when r = s -> false
        | BinOp (_, s, t, _) when s = Reg r || t = Reg r -> false
        | _ -> true in
      ExprSet.filter filter s

module Lpair = struct

        (* A property is a pair of sets of expressions. *)
  type property = expr_set * expr_set

  let bottom = (ExprSet.empty, ExprSet.empty)

  let equal (ant1, nea1) (ant2, nea2) =
    ExprSet.equal ant1 ant2 && ExprSet.equal nea1 nea2

  let is_maximal _ = false

end

module Lsing = struct

  (* A property is a set of expressions. *)
  type property = expr_set

  let bottom = ExprSet.empty

  let equal = ExprSet.equal

  let is_maximal _ = false

end

module Lexprid = struct

  (* A property is a set of expressions and a set of registers. *)
  type property = expr_set * Register.Set.t

  let bottom = (ExprSet.empty, Register.Set.empty)

  let equal (a, b) (c, d) = ExprSet.equal a c && Register.Set.equal b d

  let is_maximal _ = false

end

module Fpair = Fix.Make (Label.ImpMap) (Lpair)

module Fsing = Fix.Make (Label.ImpMap) (Lsing)

module Fexprid = Fix.Make (Label.ImpMap) (Lexprid)

(* printing tools to debug *)

let print_expr = function
    (*    | Cst c ->
          (RTLabsPrinter.print_cst c)*)
  | UnOp (op, r, t) ->
    (RTLabsPrinter.print_op1 op r ^ " : " ^ Primitive.print_type t)
  | BinOp (op, r, s, t) ->
    (RTLabsPrinter.print_op2 op r s  ^ " : " ^ Primitive.print_type t)

let print_prop_pair (p : Fpair.property) =
  let (ant, nea) = p in
  let f e = Printf.printf "%s, " (print_expr e) in
  Printf.printf "{ ";
  ExprSet.iter f ant;
  Printf.printf "}; { ";
  ExprSet.iter f nea;
  Printf.printf "}\n"

let print_valu_pair (valu : Fpair.valuation) (g : graph) (entry : Label.t) =
  let f lbl _ =
    Printf.printf "%s: " lbl;
    print_prop_pair (valu lbl) in
  Util.dfs_iter f g entry

let print_prop_sing (p : Fsing.property) =
  let f e = Printf.printf "%s, " (print_expr e) in
  Printf.printf "{ ";
  ExprSet.iter f p;
  Printf.printf "}\n"

let print_valu_sing (valu : Fsing.valuation) (g : graph) (entry : Label.t) =
  let f lbl _ =
    Printf.printf "%s: " lbl;
    print_prop_sing (valu lbl) in
  Util.dfs_iter f g entry


(* ----- PHASE 1 : Anticipatability and erliestness ------ *)
(* An expression e is anticipatable at point p if every path from p contains  *)
(* a computation of e and evaluating e at p holds the same result as all such *)
(* computations. *)
(* An expression e is earliest at point p if there is no computation of e *)
(* preceding p giving the same value. *)
(* We will compute anticipatable expressions and *non*-earliest ones for every*)
(* point with a single invocation to a fixpoint calculation. *)


let semantics_ant_nea
    (g : graph)
    (type_of : Register.t -> AST.sig_type)
    (pred_table : Label.t list Label.Map.t)
    (lbl : Label.t)
    (valu : Fpair.valuation)
    : Fpair.property =
  let succs = RTLabsGraph.successors (Label.Map.find lbl g) in
  let preds = Label.Map.find lbl pred_table in

        (* anticipatable expressions at entry *)
        (* take anticipatable expressions of successors... *)
  let ant l = fst (valu l) in
  let nea l = snd (valu l) in
  let ant_in = big_inter ant succs in
        (* ... filter out those that contain the register being changed ...*)
  let ant_in = filter_unchanged (modified_at g lbl) ant_in in
        (* ... and add the expression being calculated ... *)
  let ant_in = ant_in ++* expr_of type_of g lbl in

        (* non-earliest expressions at entry *)
        (* take non-earliest or anticipatable expressions of predecessors, *)
        (* filtered so that just unchanged expressions leak *)
  let ant_or_nea l =
    filter_unchanged (modified_at g l) (ant l ++ nea l) in
  let nea_in = big_inter ant_or_nea preds in

  (ant_in, nea_in)

let compute_anticipatable_and_non_earliest
    (f_def : internal_function)
    (type_of : Register.t -> AST.sig_type)
    (pred_table : Label.t list Label.Map.t)
    : Fpair.valuation =

  Fpair.lfp (semantics_ant_nea f_def.f_graph  type_of pred_table)

(* ------------ PHASE 2 : delayedness and lateness ----------- *)
(* An expression e is delayable at position p there is a point p' preceding it*)
(* in the control flow where e could be safely placed, and between p'and p *)
(* excluded e is never used. *)


let semantics_delay
    (g : graph)
    (type_of : Register.t -> AST.sig_type)
    (pred_table : Label.t list Label.Map.t)
    (ant_nea : Fpair.valuation)
    (lbl : Label.t)
    (valu : Fsing.valuation)
    : Fsing.property =
  let preds = Label.Map.find lbl pred_table in

  (* delayed expressions at entry *)
  (* take delayed expressions of predecessors which are not the expressions *)
  (* of such predecessors... *)
  let rem_pred lbl' = valu lbl' --* expr_of type_of g lbl' in
  let delay_in = big_inter rem_pred preds in
                (* ... and add in anticipatable and earliest expressions *)
  let (ant, nea) = ant_nea lbl in
  delay_in ++ (ant -- nea)

let compute_delayed
    (f_def : internal_function)
    (type_of : Register.t -> AST.sig_type)
    (pred_table : Label.t list Label.Map.t)
    (ant_nea : Fpair.valuation)
    : Fsing.valuation =

  Fsing.lfp (semantics_delay f_def.f_graph type_of pred_table ant_nea)

(* An expression is latest at p if it cannot be delayed further *)
let late
    (g : graph)
    (type_of : Register.t -> AST.sig_type)
    (delay : Fsing.valuation)
    : Fsing.valuation = fun lbl ->
      let stmt = Label.Map.find lbl g in
      let succs = RTLabsGraph.successors stmt in

      let eo = match expr_of type_of g lbl with
        | Some e when ExprSet.mem e (delay lbl) -> Some e
        | _ -> None in

      (delay lbl -- big_inter delay succs) ++* eo


(* --------------- PHASE 3 : isolatedness, optimality and redudancy --------*)

(* An expression e is isolated at point p if on every path from p a use of *)
(* e is preceded by an optimal computation point for it. These are expressions*)
(* which will not be touched *)
(* A variable is used at entry if every use of it later in the execution path *)
(* is to compute variables which are in turn used. *)
let semantics_isolated_used
    (g : graph)
    (type_of : Register.t -> AST.sig_type)
    (late : Fsing.valuation)
    (lbl : Label.t)
    (valu : Fexprid.valuation)
    : Fexprid.property =

  let stmt = Label.Map.find lbl g in
  let succs = RTLabsGraph.successors stmt in
  let f l = late l ++ (fst (valu l) --* expr_of type_of g l) in
  let isol = big_inter f succs in

  let f l =
    let used_out = snd (valu l) in
    let used_out = match modified_at g l with
      | Some r when Register.Set.mem r used_out ->
        Register.Set.union (Register.Set.remove r used_out) (vars_of g l)
      | _ -> used_out in
    Register.Set.union used_out (used_at g l) in
  let used = big_union f succs in

  (isol, used)

let compute_isolated_used
    (f_def : internal_function)
    (type_of : Register.t -> AST.sig_type)
    (delayed : Fsing.valuation)
    : Fexprid.valuation =

  let graph = f_def.f_graph in

  Fexprid.lfp
    (semantics_isolated_used graph type_of (late graph type_of delayed))

(* expressions that are optimally placed at point p, without being isolated *)
let optimal (late : Fsing.valuation) (isol : Fsing.valuation)
    : Fsing.valuation = fun lbl ->
      late lbl -- isol lbl

(* mark instructions that are redundant and can be replaced by a copy *)
let redundant g type_of late isol lbl =
  match expr_of type_of g lbl with
    | Some e when ExprSet.mem e (isol lbl) ->
      false
    | Some _ -> true
    | _ -> false

(* mark instructions that modify an unused register *)
let unused g used lbl =
  match modified_at g lbl with
    | Some r when Register.Set.mem r (used lbl) ->
      false
    | Some r -> true
    | _ -> false

(*------ PHASE 4 : place expressions, remove reduntant ones -------------*)

let stmt_of_expr
    (r : Register.t)
    (e : expr)
    (l : Label.t)
    : statement =
  match e with
    (* | Cst c -> St_cst (r, c, l) *)
    | UnOp (op, s, _) -> St_op1 (op, r, s, l)
    | BinOp (op, s, t, _) -> St_op2 (op, r, s, t, l)

let trans freshr type_of is_redundant is_unused optimal tmps lbl stmt =
  let get_r expr tmps =
    try
      (tmps, ExprMap.find expr tmps)
    with
      | Not_found ->
        let r = freshr () in
        (ExprMap.add expr r tmps, r) in
  let f expr (tmps, instrs) =
    let (tmps, r) = get_r expr tmps in
    (tmps, stmt_of_expr r expr lbl :: instrs) in
  let (tmps, optimals) = ExprSet.fold f (optimal lbl) (tmps, []) in
  match stmt, is_unused lbl, is_redundant lbl with
    | St_cost (cost_lbl, next) as s, _, _ ->
      (* in this case we place optimal calculations after the cost one *)
      (tmps, s :: optimals)
    | _, true, _ ->
      (* here we can remove the statement altogether *)
      (tmps, optimals)
    | _, _, false ->
      (tmps, optimals @ [stmt])
    | _, _, true ->
      match modified_at_stmt stmt, expr_of_stmt type_of stmt with
        | Some s, Some e ->
          let (tmps, r) = get_r e tmps in
          (tmps, optimals @ [St_op1 (Op_id, s, r, lbl)])
        | _ -> assert false (* if redundant must be an expression *)

let type_of_expr = function
  | UnOp (_, _, t) -> t
  | BinOp (_, _, _, t) -> t

let add_decls expr_regs decls =
  let f e r decls = (r, type_of_expr e) :: decls in
  ExprMap.fold f expr_regs decls

(* piecing it all together *)
let transform_internal f_def =
  let pred_table = Util.compute_predecessor_lists f_def.f_graph in
  let type_table = RTLabsGraph.compute_type_map f_def in
  let type_of r = Register.Map.find r type_table in
  (* analysis *)
  let ant_nea =
    compute_anticipatable_and_non_earliest f_def type_of pred_table in
  let delay = compute_delayed f_def type_of pred_table ant_nea in
  let late = late f_def.f_graph type_of delay in
  let isol_used = compute_isolated_used f_def type_of delay in
  let isol = fun lbl -> fst (isol_used lbl) in
  let used = fun lbl -> snd (isol_used lbl) in
  let opt = optimal late isol in
  let redn = redundant f_def.f_graph type_of late isol in
  let unusd = unused f_def.f_graph used in
  (* end of analysis *)
  let freshr () = Register.fresh f_def.f_runiverse in
  let freshl () = Label.Gen.fresh f_def.f_luniverse in
  let trans = trans freshr type_of redn unusd opt in
  let expr_regs = ExprMap.empty in
  let (expr_regs, g) = Trans.translate freshl trans expr_regs f_def.f_graph in
  let d = add_decls expr_regs f_def.f_locals in

  { f_def with f_locals = d ; f_graph = g }

let transform_funct = function
  | (f, F_int f_def) -> (f, F_int (transform_internal f_def))
  | f -> f

let trans = Languages.RTLabs, function
  | Languages.AstRTLabs p ->
    Languages.AstRTLabs { p with functs = List.map transform_funct p.functs }
  | _ -> assert false (* wrong language *)