1 | (** this module provides some utilities relative to RTLabs graphs *) |
---|
2 | |
---|
3 | open RTLabs |
---|
4 | |
---|
5 | type node = Label.t |
---|
6 | |
---|
7 | (** Successors of a statement *) |
---|
8 | let 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 | |
---|
30 | let 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 *) |
---|
51 | let 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 | |
---|
67 | let 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 | |
---|
83 | let 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. *) |
---|
109 | let 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 | |
---|
124 | let 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 | |
---|
141 | let 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 | |
---|
150 | let 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 | |
---|
167 | let 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 *) |
---|
179 | let 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 | |
---|
189 | let modified_at (g : graph) (n : Label.t) : Register.t option = |
---|
190 | modified_at_stmt (Label.Map.find n g) |
---|
191 | |
---|