1 | |
---|
2 | let int_size = Driver.CminorMemory.int_size |
---|
3 | |
---|
4 | let funct_vars (id, fun_def) = match fun_def with |
---|
5 | | Cminor.F_int def -> |
---|
6 | id :: (List.map fst (def.Cminor.f_params @ def.Cminor.f_vars)) |
---|
7 | | _ -> [id] |
---|
8 | |
---|
9 | let prog_idents p = |
---|
10 | let vars = List.map (fun (x, _, _) -> x) p.Cminor.vars in |
---|
11 | let f vars funct = vars @ (funct_vars funct) in |
---|
12 | let vars = List.fold_left f vars p.Cminor.functs in |
---|
13 | let f vars var = StringTools.Set.add var vars in |
---|
14 | List.fold_left f StringTools.Set.empty vars |
---|
15 | |
---|
16 | let fresh_cost_id prefix p = |
---|
17 | let vars = prog_idents p in |
---|
18 | StringTools.Gen.fresh_prefix vars prefix |
---|
19 | |
---|
20 | |
---|
21 | (* |
---|
22 | let increment cost_id incr = |
---|
23 | let cost = |
---|
24 | Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol cost_id), AST.Sig_ptr) in |
---|
25 | let load = Cminor.Expr (Cminor.Mem (Memory.QInt 4, cost), AST.Sig_int 4) in |
---|
26 | let incr = Cminor.Expr (Cminor.Cst (AST.Cst_int incr), AST.Sig_int 4) in |
---|
27 | let incr = Cminor.Expr (Cminor.Op2 (AST.Op_add, load, incr), AST.Sig_int 4) in |
---|
28 | Cminor.St_store (Memory.QInt 4, cost, incr) |
---|
29 | |
---|
30 | |
---|
31 | let f_remove_cost_labels_exp e subexp_res = match e, subexp_res with |
---|
32 | | Cminor.Id _, _ | Cminor.Cst _, _ -> e |
---|
33 | | Cminor.Op1 (op, _), [e1] -> Cminor.Op1 (op, e1) |
---|
34 | | Cminor.Op2 (op, _, _), [e1 ; e2] -> Cminor.Op2 (op, e1, e2) |
---|
35 | | Cminor.Mem (chunk, _), [e] -> Cminor.Mem (chunk, e) |
---|
36 | | Cminor.Cond (_, _, _), [e1 ; e2 ; e3] -> Cminor.Cond (e1, e2, e3) |
---|
37 | | Cminor.Exp_cost _, [e] -> e |
---|
38 | | _ -> assert false (* wrong number of arguments *) |
---|
39 | |
---|
40 | let remove_cost_labels_exp e = |
---|
41 | CminorFold.expression f_remove_cost_labels_exp e |
---|
42 | |
---|
43 | let remove_cost_labels_exps exps = |
---|
44 | List.map remove_cost_labels_exp exps |
---|
45 | |
---|
46 | |
---|
47 | let list_seq l = |
---|
48 | let f res stmt = Cminor.St_seq (res, stmt) in |
---|
49 | List.fold_left f Cminor.St_skip l |
---|
50 | |
---|
51 | let f_update_cost_exp costs_mapping cost_id e subexp_res = |
---|
52 | match e, subexp_res with |
---|
53 | | Cminor.Cond (e1, _, _), [stmt1 ; stmt2 ; stmt3] -> |
---|
54 | Cminor.St_seq (stmt1, Cminor.St_ifthenelse (e1, stmt2, stmt3)) |
---|
55 | | Cminor.Exp_cost (lbl, _), [stmt2] -> |
---|
56 | let incr = |
---|
57 | if CostLabel.Map.mem lbl costs_mapping then |
---|
58 | CostLabel.Map.find lbl costs_mapping |
---|
59 | else 0 in |
---|
60 | let stmt1 = increment cost_id incr in |
---|
61 | Cminor.St_seq (stmt1, stmt2) |
---|
62 | | _ -> list_seq subexp_res |
---|
63 | |
---|
64 | let update_cost_exp costs_mapping cost_id e = |
---|
65 | CminorFold.expression (f_update_cost_exp costs_mapping cost_id) e |
---|
66 | |
---|
67 | let update_cost_exps costs_mapping cost_id exps = |
---|
68 | let l = List.map (update_cost_exp costs_mapping cost_id) exps in |
---|
69 | let f stmt upd = Cminor.St_seq (stmt, upd) in |
---|
70 | List.fold_left f Cminor.St_skip l |
---|
71 | |
---|
72 | |
---|
73 | let rec instrument_stmt costs_mapping cost_id body = match body with |
---|
74 | | Cminor.St_skip | Cminor.St_exit _ | Cminor.St_return None -> body |
---|
75 | | Cminor.St_assign (x, e) -> |
---|
76 | let upd = update_cost_exp costs_mapping cost_id e in |
---|
77 | let e = remove_cost_labels_exp e in |
---|
78 | Cminor.St_seq (upd, Cminor.St_assign (x, e)) |
---|
79 | | Cminor.St_store (chunk, e1, e2) -> |
---|
80 | let upd = update_cost_exps costs_mapping cost_id [e1 ; e2] in |
---|
81 | let e1 = remove_cost_labels_exp e1 in |
---|
82 | let e2 = remove_cost_labels_exp e2 in |
---|
83 | Cminor.St_seq (upd, Cminor.St_store (chunk, e1, e2)) |
---|
84 | | Cminor.St_call (ox, f, args, sg) -> |
---|
85 | let upd = update_cost_exps costs_mapping cost_id (f :: args) in |
---|
86 | let f = remove_cost_labels_exp f in |
---|
87 | let args = remove_cost_labels_exps args in |
---|
88 | Cminor.St_seq (upd, Cminor.St_call (ox, f, args, sg)) |
---|
89 | | Cminor.St_tailcall (f, args, sg) -> |
---|
90 | let upd = update_cost_exps costs_mapping cost_id (f :: args) in |
---|
91 | let f = remove_cost_labels_exp f in |
---|
92 | let args = remove_cost_labels_exps args in |
---|
93 | Cminor.St_seq (upd, Cminor.St_tailcall (f, args, sg)) |
---|
94 | | Cminor.St_seq (stmt1, stmt2) -> |
---|
95 | let stmt1 = instrument_stmt costs_mapping cost_id stmt1 in |
---|
96 | let stmt2 = instrument_stmt costs_mapping cost_id stmt2 in |
---|
97 | Cminor.St_seq (stmt1, stmt2) |
---|
98 | | Cminor.St_ifthenelse (e, stmt1, stmt2) -> |
---|
99 | let upd = update_cost_exp costs_mapping cost_id e in |
---|
100 | let e = remove_cost_labels_exp e in |
---|
101 | let stmt1 = instrument_stmt costs_mapping cost_id stmt1 in |
---|
102 | let stmt2 = instrument_stmt costs_mapping cost_id stmt2 in |
---|
103 | Cminor.St_seq (upd, Cminor.St_ifthenelse (e, stmt1, stmt2)) |
---|
104 | | Cminor.St_loop stmt -> |
---|
105 | Cminor.St_loop (instrument_stmt costs_mapping cost_id stmt) |
---|
106 | | Cminor.St_block stmt -> |
---|
107 | Cminor.St_block (instrument_stmt costs_mapping cost_id stmt) |
---|
108 | | Cminor.St_switch (e, tbl, dflt) -> |
---|
109 | let upd = update_cost_exp costs_mapping cost_id e in |
---|
110 | let e = remove_cost_labels_exp e in |
---|
111 | Cminor.St_seq (upd, Cminor.St_switch (e, tbl, dflt)) |
---|
112 | | Cminor.St_label (lbl, stmt) -> |
---|
113 | Cminor.St_label (lbl, instrument_stmt costs_mapping cost_id stmt) |
---|
114 | | Cminor.St_goto lbl -> body |
---|
115 | | Cminor.St_return (Some e) -> |
---|
116 | let upd = update_cost_exp costs_mapping cost_id e in |
---|
117 | let e = remove_cost_labels_exp e in |
---|
118 | Cminor.St_seq (upd, Cminor.St_return (Some e)) |
---|
119 | | Cminor.St_cost (lbl, stmt) -> |
---|
120 | let incr = |
---|
121 | if CostLabel.Map.mem lbl costs_mapping then |
---|
122 | CostLabel.Map.find lbl costs_mapping |
---|
123 | else 0 in |
---|
124 | let stmt = instrument_stmt costs_mapping cost_id stmt in |
---|
125 | if incr = 0 then stmt |
---|
126 | else Cminor.St_seq (increment cost_id incr, stmt) |
---|
127 | |
---|
128 | |
---|
129 | let instrument_function costs_mapping cost_id = function |
---|
130 | | Cminor.F_int int_def -> |
---|
131 | let body = instrument_stmt costs_mapping cost_id int_def.Cminor.f_body in |
---|
132 | let def = { int_def with Cminor.f_body = body} in |
---|
133 | Cminor.F_int def |
---|
134 | | def -> def |
---|
135 | |
---|
136 | |
---|
137 | (** [instrument prog cost_map] instruments the program [prog]. First a fresh |
---|
138 | global variable --- the so-called cost variable --- is added to the program. |
---|
139 | Then, each cost label in the program is replaced by an increment of the cost |
---|
140 | variable, following the mapping [cost_map]. The function also returns the |
---|
141 | name of the cost variable and the name of the cost increment function. *) |
---|
142 | |
---|
143 | let instrument p costs_mapping = |
---|
144 | let cost_id = fresh_cost_id "_cost" p in |
---|
145 | let vars = (cost_id, [AST.Data_int32 0]) :: p.Cminor.vars in |
---|
146 | let f (f_name, f_def) = |
---|
147 | (f_name, instrument_function costs_mapping cost_id f_def) in |
---|
148 | let functs = List.map f p.Cminor.functs in |
---|
149 | ({ Cminor.vars = vars ; |
---|
150 | Cminor.functs = functs ; |
---|
151 | Cminor.main = p.Cminor.main }, |
---|
152 | "" (* TODO *), |
---|
153 | "" (* TODO *)) |
---|
154 | *) |
---|
155 | |
---|
156 | |
---|
157 | (* Program cost labels and labels *) |
---|
158 | |
---|
159 | let labels_empty = (CostLabel.Set.empty, Label.Set.empty) |
---|
160 | |
---|
161 | let add_cost_label lbl (cost_label, user_label) = |
---|
162 | (CostLabel.Set.add lbl cost_label, user_label) |
---|
163 | |
---|
164 | let add_label lbl (cost_label, user_label) = |
---|
165 | (cost_label, Label.Set.add lbl user_label) |
---|
166 | |
---|
167 | let labels_union (cost_labels1, user_labels1) (cost_labels2, user_labels2) = |
---|
168 | (CostLabel.Set.union cost_labels1 cost_labels2, |
---|
169 | Label.Set.union user_labels1 user_labels2) |
---|
170 | |
---|
171 | let labels_union_list l = |
---|
172 | let f res labels = labels_union res labels in |
---|
173 | List.fold_left f labels_empty l |
---|
174 | |
---|
175 | let f_exp_labels (Cminor.Expr (ed, _)) subexp_res = |
---|
176 | let labels1 = labels_union_list subexp_res in |
---|
177 | let labels2 = match ed with |
---|
178 | | Cminor.Exp_cost (lbl, _) -> add_cost_label lbl labels_empty |
---|
179 | | _ -> labels_empty in |
---|
180 | labels_union labels1 labels2 |
---|
181 | |
---|
182 | let f_body_labels stmt subexp_res substmt_res = |
---|
183 | let labels1 = labels_union_list subexp_res in |
---|
184 | let labels2 = labels_union_list substmt_res in |
---|
185 | let labels = labels_union labels1 labels2 in |
---|
186 | let labels3 = match stmt with |
---|
187 | | Cminor.St_label (lbl, _) -> add_label lbl labels_empty |
---|
188 | | Cminor.St_cost (lbl, _) -> add_cost_label lbl labels_empty |
---|
189 | | _ -> labels_empty in |
---|
190 | labels_union labels labels3 |
---|
191 | |
---|
192 | let body_labels stmt = CminorFold.statement f_exp_labels f_body_labels stmt |
---|
193 | |
---|
194 | let prog_labels p = |
---|
195 | let f lbls (_, f_def) = match f_def with |
---|
196 | | Cminor.F_int def -> |
---|
197 | labels_union lbls (body_labels def.Cminor.f_body) |
---|
198 | | _ -> lbls in |
---|
199 | List.fold_left f (CostLabel.Set.empty, Label.Set.empty) p.Cminor.functs |
---|
200 | |
---|
201 | let cost_labels p = fst (prog_labels p) |
---|
202 | let user_labels p = snd (prog_labels p) |
---|
203 | |
---|
204 | let all_labels p = |
---|
205 | let (cost_labels, user_labels) = prog_labels p in |
---|
206 | let f lbl = StringTools.Set.add (CostLabel.string_of_cost_label lbl) in |
---|
207 | let all = CostLabel.Set.fold f cost_labels StringTools.Set.empty in |
---|
208 | Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all |
---|