source: Deliverables/D2.2/8051/src/RTLabs/RTLabsUtilities.ml @ 1572

(** this module provides some utilities relative to RTLabs graphs *)

open RTLabs

type node = Label.t

(** Successors of a statement *)
let statement_successors (stmt : statement) =
  match stmt with
  | St_return _ 
  | St_tailcall_id _
  | St_tailcall_ptr _ ->
    []
  | St_skip l
  | St_cost (_, l)
  | St_ind_0 (_, l)
  | St_ind_inc (_, l)
  | St_cst (_, _, l)
  | St_op1 (_, _, _, l)
  | St_op2 (_, _, _, _, l)
  | St_load (_, _, _, l)
  | St_store (_, _, _, l)
  | St_call_ptr (_, _, _, _, l)
  | St_call_id (_, _, _, _, l) ->
    [l]
  | St_cond (_, l1, l2) ->
    [l1 ; l2]
  | St_jumptable (_, ls) -> ls

let count_statement_successors (stmt : statement) =
  match stmt with
  | St_return _ 
  | St_tailcall_id _
  | St_tailcall_ptr _ -> 0
  | St_skip _
  | St_cost _
  | St_ind_0 _
  | St_ind_inc _
  | St_cst _
  | St_op1 _
  | St_op2 _
  | St_load _
  | St_store _
  | St_call_ptr _
  | St_call_id _ -> 1
  | St_cond _ -> 2
  | St_jumptable (_, ls) -> List.length ls

(** computes a map binding the set of predecessors to each node. The domain 
    is guaranteed to be equal to the domain of graph *)
let compute_predecessors graph =
  let add_to_preds pred map lbl =
    let preds =
        try
          Label.Set.add pred (Label.Map.find lbl map)
    with
          | Not_found -> Label.Set.singleton pred in
    Label.Map.add lbl preds map in
  let add_predecessor lbl stmt map =
        (* make sure the domain of the map will be equal to dom graph, adding *)
        (* empty sets if need be *)
    let map = if Label.Map.mem lbl map then map else
            Label.Map.add lbl Label.Set.empty map in
        List.fold_left (add_to_preds lbl) map (statement_successors stmt) in 
  Label.Map.fold add_predecessor graph Label.Map.empty

let compute_predecessor_lists graph =
  let add_to_preds pred map lbl =
    let preds =
      try
        pred :: Label.Map.find lbl map
      with
        | Not_found -> [pred] in
    Label.Map.add lbl preds map in
  let add_predecessors lbl stmt map =
        (* make sure the domain of the map will be equal to dom graph, adding *)
        (* empty sets if need be *)
    let map = if Label.Map.mem lbl map then map else
            Label.Map.add lbl [] map in
        List.fold_left (add_to_preds lbl) map (statement_successors stmt) in 
  Label.Map.fold add_predecessors graph Label.Map.empty

let fill_labels stmt lbls = match stmt, lbls with
  | St_return _, _ 
  | St_tailcall_id _, _
  | St_tailcall_ptr _, _ -> stmt
  | St_skip _, lbl :: _ -> St_skip lbl
  | St_cost (cost_lbl, _), lbl :: _ -> St_cost (cost_lbl, lbl) 
  | St_ind_0 (i, _), lbl :: _ -> St_ind_0 (i, lbl) 
  | St_ind_inc (i, _), lbl :: _ -> St_ind_inc (i, lbl) 
  | St_cst (r, c, _), lbl :: _ -> St_cst (r, c, lbl) 
  | St_op1 (op, r, s, _), lbl :: _ -> St_op1 (op, r, s, lbl) 
  | St_op2 (op, r, s, t, _), lbl :: _ -> St_op2 (op, r, s, t, lbl) 
  | St_load (q, r, s, _), lbl :: _ -> St_load (q, r, s, lbl) 
  | St_store (q, r, s, _), lbl :: _ -> St_store (q, r, s, lbl) 
  | St_call_ptr (r, args, ret, sg, _), lbl :: _ ->
    St_call_ptr (r, args, ret, sg, lbl) 
  | St_call_id (i, args, ret, sg, _), lbl :: _ ->
    St_call_id (i, args, ret, sg, lbl) 
  | St_cond (r, _, _), lbl1 :: lbl2 :: _ -> St_cond (r, lbl1, lbl2)
  | St_jumptable (r, _), lbls -> St_jumptable (r, lbls)
  | _ -> invalid_arg "fill_labels: not enough successors to fill"

(** [insert_in_between u g src tgt s] inserts [s] between [src] and [tgt].
    [tgt] should be a successor of [src], and the provided [s] should already be
    linked to [tgt]. This function just generates a new node containing [s]
    and updates [src]'s links to [tgt] to be pointing to this new node.
    If [src] is linked to [tgt] multiple times, all such links are updated. *)
let insert_in_between
    (fresh : unit -> node)
    (g : graph)
    (src : node)
    (tgt : node)
    (s : statement)
    : Label.t * graph =
  let new_lbl = fresh () in 
  let src_stmt = Label.Map.find src g in
  let succs = statement_successors src_stmt in
  let repl lbl = if lbl = tgt then new_lbl else lbl in
  let new_succs = List.map repl succs in 
  let new_src_stmt = fill_labels src_stmt new_succs in
  (new_lbl, Label.Map.add new_lbl s (Label.Map.add src new_src_stmt g))

let dfs_fold
    (f : node -> statement -> 'a -> 'a)
    (g : graph)
    (entry : node)
    (init : 'a)
    : 'a =
  assert (Label.Map.mem entry g);
  let rec process done_set = function
    | [] -> init
    | next :: worklist when Label.Set.mem next done_set ->
      process done_set worklist
    | next :: worklist ->
      let stmt = Label.Map.find next g in
      let succs = statement_successors stmt in
      f next stmt (process (Label.Set.add next done_set) (succs @ worklist)) in
  process Label.Set.empty [entry]
    
let dead_code_elim
    (g     : graph)
    (entry : node)
    : graph =
  let add lbl _ = Label.Set.add lbl in
  let reachable = dfs_fold add g entry Label.Set.empty in
  let is_reachable x _ = Label.Set.mem x reachable in
  Label.Map.filter is_reachable g

let dfs_iter
    (f : node -> statement -> unit)
    (g : graph)
    (entry : node)
    : unit =
  assert (Label.Map.mem entry g);
  let rec process done_set = function
    | [] -> ();
    | next :: worklist when Label.Set.mem next done_set ->
      process done_set worklist
    | next :: worklist ->
      let stmt = Label.Map.find next g in
      let succs = statement_successors stmt in
      f next stmt;
      process (Label.Set.add next done_set) (succs @ worklist) in
  process Label.Set.empty [entry]

let computes_type_map
    (f_def : internal_function)
    : AST.sig_type Register.Map.t =
  let types = Register.Map.empty in 
  let add map (r, typ)  = Register.Map.add r typ map in
  let types = List.fold_left add types f_def.f_params in
  let types = List.fold_left add types f_def.f_locals in
  match f_def.f_result with
    | None -> types
    | Some x -> add types x

(* the register modified by a node *)
let modified_at_stmt stmt =
  match stmt with
    | St_op1 (_, r, _, _)
    | St_op2 (_, r, _, _, _)
    | St_cst (r, _, _)
    | St_load (_, _, r, _)
    | St_call_id (_, _, Some r, _, _)
    | St_call_ptr (_, _, Some r, _, _) -> Some r
    | _ -> None

let modified_at (g : graph) (n : Label.t) : Register.t option =
  modified_at_stmt (Label.Map.find n g)