source: Deliverables/D2.2/8051/src/RTLabs/copyPropagation.ml @ 2169

open RTLabs
open AST

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.RTLabsMemory

module L  = struct

  type property =
      Register.t Register.FlexMap.t

  let bottom : property =
    Register.FlexMap.empty

  let meet =
    let choose r ro1 ro2 = match ro1, ro2 with
      | Some r1, Some r2 when r1 = r2 -> Some r1
      | _ -> None in
    Register.FlexMap.merge choose

  let big_meet f = function
    | [] -> bottom
    | x :: xs ->
      let f' s y = meet s (f y) in
      List.fold_left f' (f x) xs

  let equal : property -> property -> bool =
    Register.FlexMap.equal Register.equal

  let is_maximal _ = false

end

let ( --* ) m = function
  | None -> m
  | Some r ->
    let filter s t = not (Register.equal s r || Register.equal t r) in
    Register.FlexMap.filter filter m

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

let semantics
    (graph : statement Label.Map.t)
    (pred_table : Label.t list Label.Map.t)
    (lbl : Label.t)
    (valu : F.valuation)
    : F.property =
  let copies_out l =
    let copies_out = valu l in
    match Label.Map.find l graph with
      | St_op1 (Op_id, r, s, _) ->
        let copy_of x =
          (try
             Register.FlexMap.find x copies_out
           with
             | Not_found -> x) in
        if Register.equal (copy_of r) (copy_of s) then copies_out else
          Register.FlexMap.add r s (copies_out --* (Some r))
      | stmt -> copies_out --* RTLabsGraph.modified_at_stmt stmt in
  L.big_meet copies_out (Label.Map.find lbl pred_table)

let analyze
    (f_def : internal_function)
    : F.valuation =

  let graph = f_def.f_graph in

  let pred_table =
    let module U = GraphUtilities.Util(RTLabsGraph) in
    U.compute_predecessor_lists graph in

  F.lfp (semantics graph pred_table)

(* we transform statements according to the valuation found out by analyze *)
let transform_statement
    (valu : F.valuation)
    (p    : Label.t)
    : statement -> statement =
  let copy_of x =
    try
      Register.FlexMap.find x (valu p)
    with
      | Not_found -> x in
  let copy_of_arg = function
    | Reg x -> Reg (copy_of x)
    | Imm _ as a -> a in
  function
    | St_op1 (o,i,j,next) -> St_op1(o,i,copy_of j,next)
    | St_op2 (o,i,j,k,next) -> St_op2(o,i,copy_of_arg j, copy_of_arg k,next)
    | St_load (q, a, j, l) -> St_load (q, copy_of_arg a, j, l)
    | St_store (q, a1, a2, l) -> St_store(q, copy_of_arg a1, copy_of_arg a2, l)
    | St_cond (i, if_true, if_false) -> St_cond (copy_of i, if_true, if_false)
    | St_call_id (f, args, ret, sign, l) ->
      St_call_id (f, List.map copy_of_arg args, ret, sign, l)
    | St_call_ptr (f, args, ret, sign, l) ->
      St_call_ptr (f, List.map copy_of_arg args, ret, sign, l)
    | stmt -> stmt

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 graph = Label.Map.mapi (transform_statement valu) f_def.f_graph 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.RTLabs, function
  | Languages.AstRTLabs p ->
    Languages.AstRTLabs {p with functs = List.map transform_function p.functs}
  | _ -> assert false