source: Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml @ 740

Last change on this file since 740 was 740, checked in by ayache, 10 years ago

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

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