2 let int_size = Driver.CminorMemory.int_size
4 let funct_vars (id, fun_def) = match fun_def with
6 id :: (List.map fst (def.Cminor.f_params @ def.Cminor.f_vars))
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
16 let fresh_cost_id prefix p =
17 let vars = prog_idents p in
18 StringTools.Gen.fresh_prefix vars prefix
22 let increment cost_id incr =
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)
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 *)
40 let remove_cost_labels_exp e =
41 CminorFold.expression f_remove_cost_labels_exp e
43 let remove_cost_labels_exps exps =
44 List.map remove_cost_labels_exp exps
48 let f res stmt = Cminor.St_seq (res, stmt) in
49 List.fold_left f Cminor.St_skip l
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] ->
57 if CostLabel.Map.mem lbl costs_mapping then
58 CostLabel.Map.find lbl costs_mapping
60 let stmt1 = increment cost_id incr in
61 Cminor.St_seq (stmt1, stmt2)
62 | _ -> list_seq subexp_res
64 let update_cost_exp costs_mapping cost_id e =
65 CminorFold.expression (f_update_cost_exp costs_mapping cost_id) e
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
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) ->
121 if CostLabel.Map.mem lbl costs_mapping then
122 CostLabel.Map.find lbl costs_mapping
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)
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
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. *)
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 },
157 (* Program cost labels and labels *)
159 let labels_empty = (CostLabel.Set.empty, Label.Set.empty)
161 let add_cost_label lbl (cost_label, user_label) =
162 (CostLabel.Set.add lbl cost_label, user_label)
164 let add_label lbl (cost_label, user_label) =
165 (cost_label, Label.Set.add lbl user_label)
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)
171 let labels_union_list l =
172 let f res labels = labels_union res labels in
173 List.fold_left f labels_empty l
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
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
192 let body_labels stmt = CminorFold.statement f_exp_labels f_body_labels stmt
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)
199 List.fold_left f (CostLabel.Set.empty, Label.Set.empty) p.Cminor.functs
201 let cost_labels p = fst (prog_labels p)
202 let user_labels p = snd (prog_labels p)
205 let (cost_labels, user_labels) = prog_labels p in
207 CostLabel.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls)
208 cost_labels StringTools.Set.empty in
209 Label.Set.fold (fun lbl lbls -> StringTools.Set.add lbl lbls) user_labels all