source: Deliverables/D2.2/8051/src/RTL/RTLConstPropagation.ml @ 1589

open RTL

let error_prefix = "RTLabs to RTL"
let error = Error.global_error error_prefix

let error_int () = error "int16 and int32 not supported."
let error_float () = error "float not supported."
let error_shift () = error "Shift operations not supported."


(* The analysis uses the lattice of maps from registers to values with a top *)
(* element which indicates the register is known not to be constant. *)
(* The lattice's join operation is pointwise join, where pointwise bottom is *)
(* represented by the absence of a binding in the map. *)

module Mem = Driver.RTLMemory
module Val = Mem.Value

let to_opt_2 f x y = try Some (f x y) with Not_found -> None

module L : sig

  type t =
    | T
    | V of Val.t

  type property

  val bottom : property
  val join : property -> property -> property

  val bind : Register.t -> t option -> property -> property
  val bind_carry : t option -> property -> property
  val set_carry : property -> property
  val clear_carry : property -> property
  val bind_reg_n_carry
    : Register.t -> t option * t option -> property -> property
  val bind_2
    : Register.t -> Register.t -> t option * t option -> property -> property
  val find_in : Register.t -> property -> t option
  val find_out : Register.t -> property -> t option
  val find_carry_in : property -> t option
  val equal : property -> property -> bool
  val is_maximal : property -> bool
  val is_cst_in : Register.t -> property -> bool
  val find_cst_in : Register.t -> property -> int
  val find_cst_opt_in : Register.t -> property -> int option
  val is_cst_out : Register.t -> property -> bool
  val find_cst_out : Register.t -> property -> int
  val find_cst_opt_out : Register.t -> property -> int option
  val find_cst_carry_in : property -> int option

end = struct

  (* bottom will be when the map is undefined, so we do not need it explicitly*)
  type t =
    | T
    | V of Val.t


  type property = {
    in_regs : t Register.FlexMap.t ;
    out_regs : t Register.FlexMap.t ;
    in_c : t option ;
    out_c : t option
  }

  let bottom : property =
    { in_regs = Register.FlexMap.empty;
      out_regs = Register.FlexMap.empty;
      in_c = None; out_c = None }

  let join_t x y = match x, y with
    | Some (V v1), Some (V v2) when Mem.Value.equal v1 v2 -> Some (V v1)
    | Some _, Some _ -> Some T
    | None, x | x, None -> x

  let join (p : property) (q : property) : property =
    let choose _ = join_t in
    let carry = join_t p.out_c q.out_c in
    let regs = Register.FlexMap.merge choose p.out_regs q.out_regs in
    {
      in_regs = regs;
      out_regs = regs;
      in_c = carry;
      out_c = carry
    }

  let bind r t p =
    let regs = match t with
      | Some v -> Register.FlexMap.add r v p.out_regs
      | None -> Register.FlexMap.remove r p.out_regs in
    { p with out_regs = regs }

  let bind_carry t p = { p with out_c = t }
  let set_carry  = bind_carry (Some (V (Val.of_bool true)))
  let clear_carry = bind_carry (Some (V (Val.of_bool false)))

  let bind_reg_n_carry  r (v, c) p =
    bind_carry c (bind r v p)

  let bind_2 r s (v, u) p =
    (* beware, order is first r, then s (possibly overwriting r) *)
    bind s u (bind r v p)

  let find_in r p = to_opt_2 Register.FlexMap.find r p.in_regs
  let find_out r p = to_opt_2 Register.FlexMap.find r p.out_regs
  let find_carry_in p = p.in_c

  let equal_t x y = match x, y with
    | T, T -> true
    | V v1, V v2 -> Val.equal v1 v2
    | _ -> false

  let equal_t_opt_as_bool x y = match x, y with
    | Some T, Some T -> true
    | Some (V v1), Some (V v2) when Val.is_true v1 -> Val.is_true v2
    | Some (V _), Some (V v2) -> Val.is_false v2
    | None, None -> true
    | _ -> false

  let equal p q : bool =
    equal_t_opt_as_bool p.in_c q.in_c &&
      equal_t_opt_as_bool p.out_c q.out_c &&
      Register.FlexMap.equal equal_t p.in_regs q.in_regs &&
      Register.FlexMap.equal equal_t p.out_regs q.out_regs


  let is_maximal _ = false

  let is_cst_in r p =
    try
      match Register.FlexMap.find r p.in_regs with
        | V _ -> true
        | T -> false
    with
      | Not_found -> false

  let is_cst_out r p =
    try
      match Register.FlexMap.find r p.out_regs with
        | V _ -> true
        | T -> false
    with
      | Not_found -> false

  let find_cst_in r p =
    match find_in r p with
      | Some (V v) -> Val.to_int v
      | _ -> raise Not_found

  let find_cst_out r p =
    match find_out r p with
      | Some (V v) -> Val.to_int v
      | _ -> raise Not_found

  let find_cst_opt_in r p =
    try Some (find_cst_in r p) with
      | Not_found -> None

  let find_cst_opt_out r p =
    try Some (find_cst_in r p) with
      | Not_found -> None

  let find_cst_carry_in p =
    match find_carry_in p with
      | Some (V v) when Val.to_int v > 0 -> Some 1
      | Some (V _) -> Some 0
      | _ -> None
  (* let print = function *)
  (*   | T -> "T" *)
  (*   | V v -> Val.to_string v *)

end

module F = Fix.Make (Label.ImpMap) (L)

module Eval = I8051.Eval (Val)

let cst i =  L.V (Val.of_int i)

let find_arg_in a prop = match a with
  | Reg r -> L.find_in r prop
  | Imm k -> Some (cst k)

let do_the_op1
    (op : I8051.op1)
    (prop : F.property)
    (j : Register.t)
    : L.t option =
  let x = L.find_in j prop in
  match x with
    | Some (L.V v) -> Some (L.V (Eval.op1 op v))
    | _ -> x


(* as the carry bit could be known to be set or unset or unchanged even
   if arguments are bottom, the case for op2 is more complicated *)
let do_the_op2
    (op : I8051.op2)
    (prop : F.property)
    (a : argument)
    (b : argument)
    : L.t option * L.t option =
  let x = find_arg_in a prop in
  let y = find_arg_in b prop in
  let c = L.find_carry_in prop in
  match x, y, c, op with
  | Some (L.V v1), Some(L.V v2), Some(L.V vc), _ ->
    let (v', c') = Eval.op2 vc op v1 v2 in
    (Some (L.V v'), Some (L.V c'))
  | Some (L.V v1), Some (L.V v2), _, (I8051.And | I8051.Xor | I8051.Or) ->
    (* carry bit does not matter and is unchanged *)
    let (v', _) = Eval.op2 (Val.of_bool false) op v1 v2 in
    (Some (L.V v'), c)
  | Some _, _, _, (I8051.And | I8051.Xor | I8051.Or)
  | _, Some _, _, (I8051.And | I8051.Xor | I8051.Or) ->
    (* carry bit unchanged, result variable *)
    (Some L.T, c)
  | None, None, _, (I8051.And | I8051.Xor | I8051.Or) ->
    (* carry bit unchanged, result unknown *)
    (None, c)
  | Some (L.V v1), Some (L.V v2), _, I8051.Add ->
    (* carry bit does not matter and is changed *)
    let (v', c') = Eval.op2 (Val.of_bool false) op v1 v2 in
    (Some (L.V v'), Some (L.V c'))
  | Some (L.V v1), Some (L.V v2), _, (I8051.Addc | I8051.Sub) ->
    (* we can predict at least the carry bit in some cases *)
    (* c must be either Some L.T or None, can be reused for results *)
    (* if it becomes clear when set, it will always be clear *)
    let (_, c') = Eval.op2 (Val.of_bool true) op v1 v2 in
    if Val.is_false c' then (c, Some (L.V c')) else
    (* if it becomes set when clear, it will always be set *)
    let (_, c') = Eval.op2 (Val.of_bool false) op v1 v2 in
    if Val.is_true c' then (c, Some (L.V c'))
    else (c, c)
  | _, Some (L.V v1), Some (L.V v2), (I8051.Addc | I8051.Sub)
    when Val.is_false v1 && Val.is_false v2 ->
    (* result unknown or variable, but carry bit surely unset
       [x] must be either None or Some L.T, can be reused for result *)
    (x, Some (L.V (Val.of_bool false)))
  | Some (L.V v1), _, Some (L.V v2), I8051.Addc
    when Val.is_false v1 && Val.is_false v2 ->
    (* result unknown or variable, but carry bit surely unset
       [y] must be either None or Some L.T, can be reused for result *)
    (y, Some (L.V (Val.of_bool false)))
  | Some (L.V v1), _, Some (L.V v2), I8051.Sub
    when Val.is_false v1 && Val.is_true v2 ->
    (* result unknown or variable, but carry bit surely set
       [y] must be either None or Some L.T, can be reused for result *)
    (y, Some (L.V (Val.of_bool true)))
  | (Some (L.V v), None, _, I8051.Add |
     None, Some (L.V v), _, I8051.Add )
     when Val.is_false v ->
    (* result unknown, but carry bit surely unset *)
    (None, Some (L.V (Val.of_bool false)))
  | (Some (L.V v), _, _, I8051.Add |
     _, Some (L.V v), _, I8051.Add )
     when Val.is_false v ->
    (* result variable, but carry bit surely unset *)
    (Some L.T, Some (L.V (Val.of_bool false)))
  | None, _, _, _ | _, None, _, _ | _, _, None, _ ->
    (* in these other cases, both are unknown *)
    (None, None)
  | _ ->
    (* otherwise, it means both are variable *)
    (Some L.T, Some L.T)

let do_the_opaccs
    (op : I8051.opaccs)
    (prop : F.property)
    (a : argument)
    (b : argument)
    : L.t option * L.t option =
  let x = find_arg_in a prop in
  let y = find_arg_in b prop in
  match x, y, op with
    | _, Some (L.V v2), I8051.DivuModu when Val.is_false v2 ->
      (* undefined, we put top *)
      (Some L.T, Some L.T)
    | Some (L.V v1), Some (L.V v2), _ ->
      let (a, b) = Eval.opaccs op v1 v2 in
      (Some (L.V a), Some (L.V b))
    (* some cases where the result is known regardless *)
    | (Some (L.V v), _, _ | _, Some (L.V v), _) when Val.is_false v ->
      (* case _ / 0 already crossed out *)
      let zero = Val.of_int 0 in
      (Some (L.V zero), Some (L.V zero))
    | (Some (L.V v), x, I8051.Mul | x, Some (L.V v), I8051.Mul)
      when Val.eq v (Val.of_int 1) ->
      (* second acc will be surely 0, first is equal to non-1 argument *)
      (x, Some (L.V (Val.of_int 0)))
    | None, _, _ | _, None, _ -> (None, None)
    | _ -> (Some L.T, Some L.T)

let print_deb x =
      (match x with
        | Some (L.V v) ->
          Printf.sprintf "%d" (Val.to_int v)
        | Some (L.T) ->
          Printf.sprintf "variable"
        | None ->
          Printf.sprintf "unknown")

let semantics
    (graph : statement Label.Map.t)
    (pred_table : Label.t list Label.Map.t)
    (lbl : Label.t)
    (valu : F.valuation)
    : F.property =
  let pred_prop = (* the situation at the entry of the statement (in [valu]) *)
    let f prop pred =
      L.join (valu pred) prop in
    List.fold_left f L.bottom (Label.Map.find lbl pred_table) in
  match Label.Map.find lbl graph with

    | St_move (r, a, _) -> L.bind r (find_arg_in a pred_prop) pred_prop
    | St_op1 (op, r, s, _) -> L.bind r (do_the_op1 op pred_prop s) pred_prop
    | St_op2 (op, r, a, b, _) ->
      let (x, c) = do_the_op2 op pred_prop a b in
      L.bind_reg_n_carry r (x, c) pred_prop
    | St_opaccs (op, r, s, a, b, _) ->
      L.clear_carry (L.bind_2 r s (do_the_opaccs op pred_prop a b) pred_prop)
    | St_clear_carry _ -> L.clear_carry pred_prop
    | St_set_carry _ -> L.set_carry pred_prop
    | St_load (r, _, _, _) -> L.bind r None pred_prop
    | St_call_id (_, _, rets, _)
    | St_call_ptr (_, _, _, rets, _) ->
      List.fold_left (fun p x -> L.bind x None p) pred_prop rets
    | St_addr (r, s, _, _)
    | St_stackaddr (r, s, _) -> L.bind_2 r s (None, None) pred_prop
    | _ -> pred_prop

let analyze
    (f_def : internal_function)
    : F.valuation =
  (* extract types of registers from the definition *)

  let graph = f_def.f_graph in

  let module U = GraphUtilities.Util(RTLGraph) in

  let pred_table = U.compute_predecessor_lists graph in

  F.lfp (semantics graph pred_table)

(* now that the info for constants can be gathered, let's put that to use *)

let find_cst_arg_in prop = function
  | Imm k -> Some k
  | Reg r -> L.find_cst_opt_in r prop

let arg_from_arg prop a =
  match find_cst_arg_in prop a with
    | Some k -> Imm k
    | None -> a

let move i a prop =
  match arg_from_arg prop a with
    | Reg j when i = j -> []
    | Imm k when L.find_cst_opt_in i prop = Some k -> []
    | a' -> [St_move (i, a', Label.dummy)]

let simpl_imm_op2 op i a b prop l =
  match find_cst_arg_in prop a, find_cst_arg_in prop b,
    L.find_cst_carry_in prop, op with
    | Some 0, _, _, (I8051.Or | I8051.Xor)
    | Some 0, _, Some 0, (I8051.Addc | I8051.Add)
      (* in the above case if carry is set add unsets it, that's why we must
         make sure it's unset *)

    | Some 255, _, Some 1, I8051.Addc
    | Some 255, _, _, I8051.And ->
      move i b prop
    | _, Some 0, _, (I8051.Or | I8051.Xor)
    | _, Some 0, Some 0, (I8051.Addc | I8051.Sub | I8051.Add)
    | _, Some 255, Some 1, I8051.Addc
    | _, Some 255, _, I8051.And ->
      move i a prop
    | _, _, Some 0, I8051.Addc ->
      (* does not change time, but maybe helps getting better results
         with liveness analysis *)
      [St_op2 (I8051.Add, i, arg_from_arg prop a, arg_from_arg prop b, l)]
    | _ ->
      [St_op2 (op, i, arg_from_arg prop a, arg_from_arg prop b, l)]

let simpl_imm_opaccs op i j a b prop l =
  match find_cst_arg_in prop a, find_cst_arg_in prop b, op with
    | Some 1, _, I8051.Mul ->
      move i b prop @ move j (Imm 0) prop
    |  _, Some 1, (I8051.Mul | I8051.DivuModu) ->
      move i a prop @ move j (Imm 0) prop
    | _ ->
      [St_opaccs (op, i, j, arg_from_arg prop a, arg_from_arg prop b, l)]


(* we transform statements according to the valuation found out by analyze *)
(* We also turn branchings into redirections if the guard is constant. We *)
(* need the label to extract the property. The label in the output is for *)
(* compliance with GraphUtilities. *)
(* we transform statements according to the valuation found out by analyze *)
(* We also turn branchings into redirections if the guard is constant. *)
let transform
    (valu : F.valuation)
    (p    : Label.t)
    (stmt : statement) : statement list * Label.t list option =
  match stmt with
    | St_move (i, a, l) ->
      (move i a (valu p), None)
    | (St_op1 (_,i,_,l) | St_op2(_,i,_,_,l))
        when L.is_cst_out i (valu p) ->
      (move i (Imm (L.find_cst_out i (valu p))) (valu p), None)
    | St_op2 (op, i, a, b, l) ->
      (simpl_imm_op2 op i a b (valu p) l, None)
    | St_opaccs (op, i, j, a, b, l) ->
      (simpl_imm_opaccs op i j a b (valu p) l, None)
    | St_set_carry l when L.find_cst_carry_in (valu p) = Some 1 -> ([], None)
    | St_clear_carry l when L.find_cst_carry_in (valu p) = Some 0 -> ([], None)
    | St_load (i, a, b, l) ->
      ([St_load(i, arg_from_arg (valu p) a, arg_from_arg (valu p) b, l)], None)
    | St_store (a, b, c, l) ->
      ([St_store (arg_from_arg (valu p) a,
                 arg_from_arg (valu p) b,
                 arg_from_arg (valu p) c, l)], None)
    | St_cond (i, if_true, if_false) as s ->
      (match L.find_cst_opt_in i (valu p) with
        | Some 0 -> ([], Some [if_false])
        | Some _ -> ([], Some [if_true])
        | None -> ([s], Some [if_true ; if_false]))
    | St_call_id (f, args, rets, l) ->
      let args' = List.map (arg_from_arg (valu p)) args in
      ([St_call_id (f, args', rets, l)], None)
    | St_call_ptr (f1, f2, args, rets, l) ->
      let args' = List.map (arg_from_arg (valu p)) args in
      ([St_call_ptr (f1, f2, args', rets, l)], None)
    | St_tailcall_id (f, args) ->
      let args' = List.map (arg_from_arg (valu p)) args in
      ([St_tailcall_id (f, args')], None)
    | St_tailcall_ptr (f1, f2, args) ->
      let args' = List.map (arg_from_arg (valu p)) args in
      ([St_tailcall_ptr (f1, f2, args')], None)
    | stmt -> ([stmt], None)

let transform_int_function
    (f_def  : internal_function)
    : internal_function =
  let valu = analyze f_def in
        (* we transform the graph according to the analysis *)
  let module U = GraphUtilities.Util(RTLGraph) in
  let module T = GraphUtilities.Trans(RTLGraph)(RTLGraph) in
  let trans = transform valu in
  let fresh () = Label.Gen.fresh f_def.f_luniverse in
  let graph = T.translate_pure_with_redirects fresh trans f_def.f_graph in
  (* and we eliminate resulting dead code *)
  let graph = U.dead_code_elim graph f_def.f_entry in
  {f_def with f_graph = graph}

let transform_function = function
  | (id, F_int f_def) -> (id, F_int (transform_int_function f_def))
  | f -> f

let trans = Languages.RTL, function
  | Languages.AstRTL p ->
    Languages.AstRTL {p with functs = List.map transform_function p.functs}
  | _ -> assert false