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

Last change on this file since 1569 was 1569, checked in by tranquil, 9 years ago
  • added in repository some missing files...
File size: 6.2 KB
Line 
1(** this module provides some utilities relative to RTLabs graphs *)
2
3open RTLabs
4
5type node = Label.t
6
7(** Successors of a statement *)
8let statement_successors (stmt : statement) =
9  match stmt with
10  | St_return _ 
11        | St_tailcall_id _
12        | St_tailcall_ptr _ ->
13          []
14  | St_skip l
15  | St_cost (_, l)
16  | St_ind_0 (_, l)
17  | St_ind_inc (_, l)
18  | St_cst (_, _, l)
19  | St_op1 (_, _, _, l)
20  | St_op2 (_, _, _, _, l)
21  | St_load (_, _, _, l)
22  | St_store (_, _, _, l)
23  | St_call_ptr (_, _, _, _, l)
24  | St_call_id (_, _, _, _, l) ->
25    [l]
26  | St_cond (_, l1, l2) ->
27    [l1 ; l2]
28  | St_jumptable (_, ls) -> ls
29
30let count_statement_successors (stmt : statement) =
31  match stmt with
32  | St_return _ 
33        | St_tailcall_id _
34        | St_tailcall_ptr _ -> 0
35  | St_skip _
36  | St_cost _
37  | St_ind_0 _
38  | St_ind_inc _
39  | St_cst _
40  | St_op1 _
41  | St_op2 _
42  | St_load _
43  | St_store _
44  | St_call_ptr _
45  | St_call_id _ -> 1
46  | St_cond _ -> 2
47  | St_jumptable (_, ls) -> List.length ls
48
49(** computes a map binding the set of predecessors to each node. The domain
50    is guaranteed to be equal to the domain of graph *)
51let compute_predecessors graph =
52  let add_to_preds pred map lbl =
53    let preds =
54        try
55          Label.Set.add pred (Label.Map.find lbl map)
56    with
57          | Not_found -> Label.Set.singleton pred in
58    Label.Map.add lbl preds map in
59  let add_predecessor lbl stmt map =
60        (* make sure the domain of the map will be equal to dom graph, adding *)
61        (* empty sets if need be *)
62    let map = if Label.Map.mem lbl map then map else
63            Label.Map.add lbl Label.Set.empty map in
64        List.fold_left (add_to_preds lbl) map (statement_successors stmt) in 
65  Label.Map.fold add_predecessor graph Label.Map.empty
66
67let compute_predecessor_lists graph =
68  let add_to_preds pred map lbl =
69    let preds =
70      try
71        pred :: Label.Map.find lbl map
72      with
73        | Not_found -> [pred] in
74    Label.Map.add lbl preds map in
75  let add_predecessors lbl stmt map =
76        (* make sure the domain of the map will be equal to dom graph, adding *)
77        (* empty sets if need be *)
78    let map = if Label.Map.mem lbl map then map else
79            Label.Map.add lbl [] map in
80        List.fold_left (add_to_preds lbl) map (statement_successors stmt) in 
81  Label.Map.fold add_predecessors graph Label.Map.empty
82
83let fill_labels stmt lbls = match stmt, lbls with
84  | St_return _, _ 
85        | St_tailcall_id _, _
86        | St_tailcall_ptr _, _ -> stmt
87  | St_skip _, lbl :: _ -> St_skip lbl
88  | St_cost (cost_lbl, _), lbl :: _ -> St_cost (cost_lbl, lbl) 
89  | St_ind_0 (i, _), lbl :: _ -> St_ind_0 (i, lbl) 
90  | St_ind_inc (i, _), lbl :: _ -> St_ind_inc (i, lbl) 
91  | St_cst (r, c, _), lbl :: _ -> St_cst (r, c, lbl) 
92  | St_op1 (op, r, s, _), lbl :: _ -> St_op1 (op, r, s, lbl) 
93  | St_op2 (op, r, s, t, _), lbl :: _ -> St_op2 (op, r, s, t, lbl) 
94  | St_load (q, r, s, _), lbl :: _ -> St_load (q, r, s, lbl) 
95  | St_store (q, r, s, _), lbl :: _ -> St_store (q, r, s, lbl) 
96  | St_call_ptr (r, args, ret, sg, _), lbl :: _ ->
97                St_call_ptr (r, args, ret, sg, lbl) 
98  | St_call_id (i, args, ret, sg, _), lbl :: _ ->
99    St_call_id (i, args, ret, sg, lbl) 
100  | St_cond (r, _, _), lbl1 :: lbl2 :: _ -> St_cond (r, lbl1, lbl2)
101  | St_jumptable (r, _), lbls -> St_jumptable (r, lbls)
102        | _ -> invalid_arg "fill_labels: not enough successors to fill"
103
104(** [insert_in_between u g src tgt s] inserts [s] between [src] and [tgt].
105    [tgt] should be a successor of [src], and the provided [s] should already be
106    linked to [tgt]. This function just generates a new node containing [s]
107    and updates [src]'s links to [tgt] to be pointing to this new node.
108    If [src] is linked to [tgt] multiple times, all such links are updated. *)
109let insert_in_between
110    (fresh : unit -> node)
111                (g : graph)
112                (src : node)
113                (tgt : node)
114                (s : statement)
115                : Label.t * graph =
116                let new_lbl = fresh () in 
117                let src_stmt = Label.Map.find src g in
118                let succs = statement_successors src_stmt in
119                let repl lbl = if lbl = tgt then new_lbl else lbl in
120                let new_succs = List.map repl succs in 
121                let new_src_stmt = fill_labels src_stmt new_succs in
122                (new_lbl, Label.Map.add new_lbl s (Label.Map.add src new_src_stmt g))
123
124let dfs_fold
125    (f : node -> statement -> 'a -> 'a)
126                (g : graph)
127                (entry : node)
128                (init : 'a)
129                : 'a =
130        assert (Label.Map.mem entry g);
131        let rec process done_set = function
132                | [] -> init
133                | next :: worklist when Label.Set.mem next done_set ->
134                        process done_set worklist
135                | next :: worklist ->
136                        let stmt = Label.Map.find next g in
137                        let succs = statement_successors stmt in
138                        f next stmt (process (Label.Set.add next done_set) (succs @ worklist)) in
139        process Label.Set.empty [entry]
140       
141let dead_code_elim
142    (g     : graph)
143    (entry : node)
144    : graph =
145                let add lbl _ = Label.Set.add lbl in
146                let reachable = dfs_fold add g entry Label.Set.empty in
147    let is_reachable x _ = Label.Set.mem x reachable in
148    Label.Map.filter is_reachable g
149
150let dfs_iter
151    (f : node -> statement -> unit)
152    (g : graph)
153    (entry : node)
154    : unit =
155    assert (Label.Map.mem entry g);
156    let rec process done_set = function
157        | [] -> ();
158        | next :: worklist when Label.Set.mem next done_set ->
159            process done_set worklist
160        | next :: worklist ->
161            let stmt = Label.Map.find next g in
162            let succs = statement_successors stmt in
163            f next stmt;
164                                                process (Label.Set.add next done_set) (succs @ worklist) in
165    process Label.Set.empty [entry]
166   
167let computes_type_map
168    (f_def : internal_function)
169                : AST.sig_type Register.Map.t =
170        let types = Register.Map.empty in 
171        let add map (r, typ)  = Register.Map.add r typ map in
172        let types = List.fold_left add types f_def.f_params in
173        let types = List.fold_left add types f_def.f_locals in
174        match f_def.f_result with
175    | None -> types
176    | Some x -> add types x
177
178(* the register modified by a node *)
179let modified_at_stmt stmt =
180  match stmt with
181        | St_op1 (_, r, _, _)
182        | St_op2 (_, r, _, _, _)
183        | St_cst (r, _, _)
184        | St_load (_, _, r, _)
185        | St_call_id (_, _, Some r, _, _)
186        | St_call_ptr (_, _, Some r, _, _) -> Some r
187        | _ -> None
188
189let modified_at (g : graph) (n : Label.t) : Register.t option =
190    modified_at_stmt (Label.Map.find n g)
191
Note: See TracBrowser for help on using the repository browser.