lustrec / src / optimize_machine.ml @ e7cc5186
History | View | Annotate | Download (26.4 KB)
1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|
2 | (* *) |
||
3 | (* The LustreC compiler toolset / The LustreC Development Team *) |
||
4 | (* Copyright 2012 - -- ONERA - CNRS - INPT *) |
||
5 | (* *) |
||
6 | (* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
||
7 | (* under the terms of the GNU Lesser General Public License *) |
||
8 | (* version 2.1. *) |
||
9 | (* *) |
||
10 | (********************************************************************) |
||
11 | |||
12 | d0b1ec56 | xthirioux | open Utils |
13 | cf78a589 | ploc | open LustreSpec |
14 | open Corelang |
||
15 | b1655a21 | xthirioux | open Causality |
16 | cf78a589 | ploc | open Machine_code |
17 | ec433d69 | xthirioux | open Dimension |
18 | cf78a589 | ploc | |
19 | 55537f48 | xthirioux | |
20 | d0b1ec56 | xthirioux | let pp_elim fmt elim = |
21 | begin |
||
22 | 521e2a6b | ploc | Format.fprintf fmt "@[{ /* elim table: */@ "; |
23 | IMap.iter (fun v expr -> Format.fprintf fmt "%s |-> %a@ " v pp_val expr) elim; |
||
24 | Format.fprintf fmt "}@ @]"; |
||
25 | d0b1ec56 | xthirioux | end |
26 | |||
27 | cf78a589 | ploc | let rec eliminate elim instr = |
28 | let e_expr = eliminate_expr elim in |
||
29 | 3ca27bc7 | ploc | match get_instr_desc instr with |
30 | 04a63d25 | xthirioux | | MComment _ -> instr |
31 | 3ca27bc7 | ploc | | MLocalAssign (i,v) -> update_instr_desc instr (MLocalAssign (i, e_expr v)) |
32 | | MStateAssign (i,v) -> update_instr_desc instr (MStateAssign (i, e_expr v)) |
||
33 | cf78a589 | ploc | | MReset i -> instr |
34 | 45f0f48d | xthirioux | | MNoReset i -> instr |
35 | 3ca27bc7 | ploc | | MStep (il, i, vl) -> update_instr_desc instr (MStep(il, i, List.map e_expr vl)) |
36 | cf78a589 | ploc | | MBranch (g,hl) -> |
37 | 3ca27bc7 | ploc | update_instr_desc instr ( |
38 | MBranch |
||
39 | (e_expr g, |
||
40 | (List.map |
||
41 | (fun (l, il) -> l, List.map (eliminate elim) il) |
||
42 | hl |
||
43 | ) |
||
44 | ) |
||
45 | ) |
||
46 | cf78a589 | ploc | |
47 | and eliminate_expr elim expr = |
||
48 | 04a63d25 | xthirioux | match expr.value_desc with |
49 | d0b1ec56 | xthirioux | | LocalVar v -> (try IMap.find v.var_id elim with Not_found -> expr) |
50 | 04a63d25 | xthirioux | | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)} |
51 | | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)} |
||
52 | | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)} |
||
53 | | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)} |
||
54 | | Cst _ | StateVar _ -> expr |
||
55 | cf78a589 | ploc | |
56 | ec433d69 | xthirioux | let eliminate_dim elim dim = |
57 | 45f0f48d | xthirioux | Dimension.expr_replace_expr |
58 | (fun v -> try |
||
59 | dimension_of_value (IMap.find v elim) |
||
60 | with Not_found -> mkdim_ident dim.dim_loc v) |
||
61 | dim |
||
62 | ec433d69 | xthirioux | |
63 | ca88e660 | Ploc | |
64 | (* 8th Jan 2016: issues when merging salsa with horn_encoding: The following |
||
65 | functions seem unsused. They have to be adapted to the new type for expr |
||
66 | d2d9d4cb | ploc | *) |
67 | ca88e660 | Ploc | |
68 | d7b73fed | xthirioux | let unfold_expr_offset m offset expr = |
69 | 04a63d25 | xthirioux | List.fold_left |
70 | (fun res -> (function | Index i -> mk_val (Access (res, value_of_dimension m i)) |
||
71 | (Types.array_element_type res.value_type) |
||
72 | | Field f -> Format.eprintf "internal error: not yet implemented !"; assert false)) |
||
73 | expr offset |
||
74 | d7b73fed | xthirioux | |
75 | 04a63d25 | xthirioux | let rec simplify_cst_expr m offset typ cst = |
76 | d7b73fed | xthirioux | match offset, cst with |
77 | | [] , _ |
||
78 | 04a63d25 | xthirioux | -> mk_val (Cst cst) typ |
79 | d7b73fed | xthirioux | | Index i :: q, Const_array cl when Dimension.is_dimension_const i |
80 | 04a63d25 | xthirioux | -> let elt_typ = Types.array_element_type typ in |
81 | simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const_dimension i)) |
||
82 | d7b73fed | xthirioux | | Index i :: q, Const_array cl |
83 | 04a63d25 | xthirioux | -> let elt_typ = Types.array_element_type typ in |
84 | unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ) |
||
85 | d7b73fed | xthirioux | | Field f :: q, Const_struct fl |
86 | 04a63d25 | xthirioux | -> let fld_typ = Types.struct_field_type typ f in |
87 | simplify_cst_expr m q fld_typ (List.assoc f fl) |
||
88 | d7b73fed | xthirioux | | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false) |
89 | |||
90 | let simplify_expr_offset m expr = |
||
91 | let rec simplify offset expr = |
||
92 | 04a63d25 | xthirioux | match offset, expr.value_desc with |
93 | d7b73fed | xthirioux | | Field f ::q , _ -> failwith "not yet implemented" |
94 | 04a63d25 | xthirioux | | _ , Fun (id, vl) when Basic_library.is_value_internal_fun expr |
95 | -> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type |
||
96 | d7b73fed | xthirioux | | _ , Fun _ |
97 | | _ , StateVar _ |
||
98 | | _ , LocalVar _ -> unfold_expr_offset m offset expr |
||
99 | 04a63d25 | xthirioux | | _ , Cst cst -> simplify_cst_expr m offset expr.value_type cst |
100 | d7b73fed | xthirioux | | _ , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr |
101 | | [] , _ -> expr |
||
102 | | Index _ :: q, Power (expr, _) -> simplify q expr |
||
103 | | Index i :: q, Array vl when Dimension.is_dimension_const i |
||
104 | -> simplify q (List.nth vl (Dimension.size_const_dimension i)) |
||
105 | 04a63d25 | xthirioux | | Index i :: q, Array vl -> unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type) |
106 | d7b73fed | xthirioux | (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res) |
107 | with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*) |
||
108 | in simplify [] expr |
||
109 | |||
110 | let rec simplify_instr_offset m instr = |
||
111 | 3ca27bc7 | ploc | match get_instr_desc instr with |
112 | | MLocalAssign (v, expr) -> update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr)) |
||
113 | | MStateAssign (v, expr) -> update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr)) |
||
114 | d7b73fed | xthirioux | | MReset id -> instr |
115 | 45f0f48d | xthirioux | | MNoReset id -> instr |
116 | 3ca27bc7 | ploc | | MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs)) |
117 | d7b73fed | xthirioux | | MBranch (cond, brl) |
118 | 3ca27bc7 | ploc | -> update_instr_desc instr ( |
119 | MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl) |
||
120 | ) |
||
121 | 04a63d25 | xthirioux | | MComment _ -> instr |
122 | d7b73fed | xthirioux | |
123 | and simplify_instrs_offset m instrs = |
||
124 | List.map (simplify_instr_offset m) instrs |
||
125 | |||
126 | d0b1ec56 | xthirioux | let is_scalar_const c = |
127 | match c with |
||
128 | | Const_real _ |
||
129 | 04a63d25 | xthirioux | | Const_int _ |
130 | d0b1ec56 | xthirioux | | Const_tag _ -> true |
131 | | _ -> false |
||
132 | |||
133 | d7b73fed | xthirioux | (* An instruction v = expr may (and will) be unfolded iff: |
134 | - either expr is atomic |
||
135 | (no complex expressions, only const, vars and array/struct accesses) |
||
136 | - or v has a fanin <= 1 (used at most once) |
||
137 | *) |
||
138 | let is_unfoldable_expr fanin expr = |
||
139 | let rec unfold_const offset cst = |
||
140 | match offset, cst with |
||
141 | | _ , Const_int _ |
||
142 | | _ , Const_real _ |
||
143 | | _ , Const_tag _ -> true |
||
144 | | Field f :: q, Const_struct fl -> unfold_const q (List.assoc f fl) |
||
145 | | [] , Const_struct _ -> false |
||
146 | | Index i :: q, Const_array cl when Dimension.is_dimension_const i |
||
147 | -> unfold_const q (List.nth cl (Dimension.size_const_dimension i)) |
||
148 | | _ , Const_array _ -> false |
||
149 | | _ -> assert false in |
||
150 | let rec unfold offset expr = |
||
151 | 04a63d25 | xthirioux | match offset, expr.value_desc with |
152 | d7b73fed | xthirioux | | _ , Cst cst -> unfold_const offset cst |
153 | | _ , LocalVar _ |
||
154 | | _ , StateVar _ -> true |
||
155 | | [] , Power _ |
||
156 | | [] , Array _ -> false |
||
157 | | Index i :: q, Power (v, _) -> unfold q v |
||
158 | | Index i :: q, Array vl when Dimension.is_dimension_const i |
||
159 | -> unfold q (List.nth vl (Dimension.size_const_dimension i)) |
||
160 | | _ , Array _ -> false |
||
161 | | _ , Access (v, i) -> unfold (Index (dimension_of_value i) :: offset) v |
||
162 | 04a63d25 | xthirioux | | _ , Fun (id, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr |
163 | d7b73fed | xthirioux | -> List.for_all (unfold offset) vl |
164 | | _ , Fun _ -> false |
||
165 | | _ -> assert false |
||
166 | in unfold [] expr |
||
167 | c287ba28 | xthirioux | |
168 | 04a63d25 | xthirioux | let basic_unfoldable_assign fanin v expr = |
169 | d0b1ec56 | xthirioux | try |
170 | let d = Hashtbl.find fanin v.var_id |
||
171 | d7b73fed | xthirioux | in is_unfoldable_expr d expr |
172 | with Not_found -> false |
||
173 | 04a63d25 | xthirioux | |
174 | d7b73fed | xthirioux | let unfoldable_assign fanin v expr = |
175 | 04a63d25 | xthirioux | (if !Options.mpfr then Mpfr.unfoldable_value expr else true) |
176 | && basic_unfoldable_assign fanin v expr |
||
177 | |||
178 | d0b1ec56 | xthirioux | let merge_elim elim1 elim2 = |
179 | let merge k e1 e2 = |
||
180 | match e1, e2 with |
||
181 | | Some e1, Some e2 -> if e1 = e2 then Some e1 else None |
||
182 | | _ , Some e2 -> Some e2 |
||
183 | | Some e1, _ -> Some e1 |
||
184 | | _ -> None |
||
185 | in IMap.merge merge elim1 elim2 |
||
186 | |||
187 | cf78a589 | ploc | (* see if elim has to take in account the provided instr: |
188 | 54d032f5 | xthirioux | if so, update elim and return the remove flag, |
189 | cf78a589 | ploc | otherwise, the expression should be kept and elim is left untouched *) |
190 | d0b1ec56 | xthirioux | let rec instrs_unfold fanin elim instrs = |
191 | let elim, rev_instrs = |
||
192 | List.fold_left (fun (elim, instrs) instr -> |
||
193 | (* each subexpression in instr that could be rewritten by the elim set is |
||
194 | rewritten *) |
||
195 | let instr = eliminate elim instr in |
||
196 | (* if instr is a simple local assign, then (a) elim is simplified with it (b) it |
||
197 | is stored as the elim set *) |
||
198 | instr_unfold fanin instrs elim instr |
||
199 | ) (elim, []) instrs |
||
200 | in elim, List.rev rev_instrs |
||
201 | |||
202 | and instr_unfold fanin instrs elim instr = |
||
203 | 429ab729 | ploc | (* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*) |
204 | 3ca27bc7 | ploc | match get_instr_desc instr with |
205 | cf78a589 | ploc | (* Simple cases*) |
206 | 04a63d25 | xthirioux | | MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type) |
207 | 3ca27bc7 | ploc | -> instr_unfold fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))) |
208 | d0b1ec56 | xthirioux | | MLocalAssign(v, expr) when unfoldable_assign fanin v expr |
209 | -> (IMap.add v.var_id expr elim, instrs) |
||
210 | | MBranch(g, hl) when false |
||
211 | -> let elim_branches = List.map (fun (h, l) -> (h, instrs_unfold fanin elim l)) hl in |
||
212 | let (elim, branches) = |
||
213 | List.fold_right |
||
214 | (fun (h, (e, l)) (elim, branches) -> (merge_elim elim e, (h, l)::branches)) |
||
215 | elim_branches (elim, []) |
||
216 | 3ca27bc7 | ploc | in elim, ((update_instr_desc instr (MBranch (g, branches))) :: instrs) |
217 | d0b1ec56 | xthirioux | | _ |
218 | -> (elim, instr :: instrs) |
||
219 | cf78a589 | ploc | (* default case, we keep the instruction and do not modify elim *) |
220 | |||
221 | |||
222 | (** We iterate in the order, recording simple local assigns in an accumulator |
||
223 | 1. each expression is rewritten according to the accumulator |
||
224 | 2. local assigns then rewrite occurrences of the lhs in the computed accumulator |
||
225 | *) |
||
226 | |||
227 | ec433d69 | xthirioux | let static_call_unfold elim (inst, (n, args)) = |
228 | let replace v = |
||
229 | try |
||
230 | Machine_code.dimension_of_value (IMap.find v elim) |
||
231 | with Not_found -> Dimension.mkdim_ident Location.dummy_loc v |
||
232 | in (inst, (n, List.map (Dimension.expr_replace_expr replace) args)) |
||
233 | |||
234 | cf78a589 | ploc | (** Perform optimization on machine code: |
235 | - iterate through step instructions and remove simple local assigns |
||
236 | |||
237 | *) |
||
238 | d0b1ec56 | xthirioux | let machine_unfold fanin elim machine = |
239 | (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_unfold %a@." pp_elim elim);*) |
||
240 | ec433d69 | xthirioux | let elim_consts, mconst = instrs_unfold fanin elim machine.mconst in |
241 | let elim_vars, instrs = instrs_unfold fanin elim_consts machine.mstep.step_instrs in |
||
242 | d7b73fed | xthirioux | let instrs = simplify_instrs_offset machine instrs in |
243 | let checks = List.map (fun (loc, check) -> loc, eliminate_expr elim_vars check) machine.mstep.step_checks in |
||
244 | ec433d69 | xthirioux | let locals = List.filter (fun v -> not (IMap.mem v.var_id elim_vars)) machine.mstep.step_locals in |
245 | let minstances = List.map (static_call_unfold elim_consts) machine.minstances in |
||
246 | let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls |
||
247 | cf78a589 | ploc | in |
248 | { |
||
249 | machine with |
||
250 | mstep = { |
||
251 | machine.mstep with |
||
252 | ec433d69 | xthirioux | step_locals = locals; |
253 | d7b73fed | xthirioux | step_instrs = instrs; |
254 | step_checks = checks |
||
255 | ec433d69 | xthirioux | }; |
256 | mconst = mconst; |
||
257 | minstances = minstances; |
||
258 | mcalls = mcalls; |
||
259 | 04a63d25 | xthirioux | }, |
260 | elim_vars |
||
261 | cf78a589 | ploc | |
262 | d0b1ec56 | xthirioux | let instr_of_const top_const = |
263 | let const = const_of_top top_const in |
||
264 | ec433d69 | xthirioux | let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true, None) in |
265 | d0b1ec56 | xthirioux | let vdecl = { vdecl with var_type = const.const_type } |
266 | 3ca27bc7 | ploc | in mkinstr (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type)) |
267 | cf78a589 | ploc | |
268 | d0b1ec56 | xthirioux | let machines_unfold consts node_schs machines = |
269 | 04a63d25 | xthirioux | List.fold_right (fun m (machines, removed) -> |
270 | let fanin = (IMap.find m.mname.node_id node_schs).Scheduling.fanin_table in |
||
271 | let elim_consts, _ = instrs_unfold fanin IMap.empty (List.map instr_of_const consts) in |
||
272 | let (m, removed_m) = machine_unfold fanin elim_consts m in |
||
273 | (m::machines, IMap.add m.mname.node_id removed_m removed) |
||
274 | ) |
||
275 | d0b1ec56 | xthirioux | machines |
276 | 04a63d25 | xthirioux | ([], IMap.empty) |
277 | cf78a589 | ploc | |
278 | c287ba28 | xthirioux | let get_assign_lhs instr = |
279 | 3ca27bc7 | ploc | match get_instr_desc instr with |
280 | 04a63d25 | xthirioux | | MLocalAssign(v, e) -> mk_val (LocalVar v) e.value_type |
281 | | MStateAssign(v, e) -> mk_val (StateVar v) e.value_type |
||
282 | c287ba28 | xthirioux | | _ -> assert false |
283 | |||
284 | let get_assign_rhs instr = |
||
285 | 3ca27bc7 | ploc | match get_instr_desc instr with |
286 | c287ba28 | xthirioux | | MLocalAssign(_, e) |
287 | | MStateAssign(_, e) -> e |
||
288 | | _ -> assert false |
||
289 | |||
290 | let is_assign instr = |
||
291 | 3ca27bc7 | ploc | match get_instr_desc instr with |
292 | c287ba28 | xthirioux | | MLocalAssign _ |
293 | | MStateAssign _ -> true |
||
294 | | _ -> false |
||
295 | |||
296 | let mk_assign v e = |
||
297 | 04a63d25 | xthirioux | match v.value_desc with |
298 | c287ba28 | xthirioux | | LocalVar v -> MLocalAssign(v, e) |
299 | | StateVar v -> MStateAssign(v, e) |
||
300 | | _ -> assert false |
||
301 | |||
302 | let rec assigns_instr instr assign = |
||
303 | 3ca27bc7 | ploc | match get_instr_desc instr with |
304 | c287ba28 | xthirioux | | MLocalAssign (i,_) |
305 | 017eec6a | ploc | | MStateAssign (i,_) -> VSet.add i assign |
306 | | MStep (ol, _, _) -> List.fold_right VSet.add ol assign |
||
307 | c287ba28 | xthirioux | | MBranch (_,hl) -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign |
308 | | _ -> assign |
||
309 | |||
310 | and assigns_instrs instrs assign = |
||
311 | List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs |
||
312 | |||
313 | (* |
||
314 | and substitute_expr subst expr = |
||
315 | match expr with |
||
316 | | StateVar v |
||
317 | | LocalVar v -> (try IMap.find expr subst with Not_found -> expr) |
||
318 | | Fun (id, vl) -> Fun (id, List.map (substitute_expr subst) vl) |
||
319 | | Array(vl) -> Array(List.map (substitute_expr subst) vl) |
||
320 | | Access(v1, v2) -> Access(substitute_expr subst v1, substitute_expr subst v2) |
||
321 | | Power(v1, v2) -> Power(substitute_expr subst v1, substitute_expr subst v2) |
||
322 | | Cst _ -> expr |
||
323 | *) |
||
324 | (** Finds a substitute for [instr] in [instrs], |
||
325 | i.e. another instr' with the same rhs expression. |
||
326 | Then substitute this expression with the first assigned var |
||
327 | *) |
||
328 | let subst_instr subst instrs instr = |
||
329 | (*Format.eprintf "subst instr: %a@." Machine_code.pp_instr instr;*) |
||
330 | let instr = eliminate subst instr in |
||
331 | let v = get_assign_lhs instr in |
||
332 | let e = get_assign_rhs instr in |
||
333 | 85da3a4b | ploc | (* Difficulties to merge with unstable. Here is the other code: |
334 | |||
335 | try |
||
336 | c287ba28 | xthirioux | let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in |
337 | 53206908 | xthirioux | match v.value_desc with |
338 | c287ba28 | xthirioux | | LocalVar v -> |
339 | IMap.add v.var_id (get_assign_lhs instr') subst, instrs |
||
340 | | StateVar v -> |
||
341 | 53206908 | xthirioux | let lhs' = get_assign_lhs instr' in |
342 | let typ' = lhs'.value_type in |
||
343 | (match lhs'.value_desc with |
||
344 | c287ba28 | xthirioux | | LocalVar v' -> |
345 | 53206908 | xthirioux | let instr = eliminate subst (mk_assign (mk_val (StateVar v) typ') (mk_val (LocalVar v') typ')) in |
346 | c287ba28 | xthirioux | subst, instr :: instrs |
347 | | StateVar v' -> |
||
348 | 53206908 | xthirioux | let subst_v' = IMap.add v'.var_id (mk_val (StateVar v) typ') IMap.empty in |
349 | let instrs' = snd (List.fold_right (fun instr (ok, instrs) -> (ok || instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in |
||
350 | IMap.add v'.var_id (mk_val (StateVar v) typ') subst, instr :: instrs' |
||
351 | c287ba28 | xthirioux | | _ -> assert false) |
352 | | _ -> assert false |
||
353 | with Not_found -> subst, instr :: instrs |
||
354 | |||
355 | 85da3a4b | ploc | *) |
356 | |||
357 | try |
||
358 | c287ba28 | xthirioux | let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in |
359 | 04a63d25 | xthirioux | match v.value_desc with |
360 | c287ba28 | xthirioux | | LocalVar v -> |
361 | IMap.add v.var_id (get_assign_lhs instr') subst, instrs |
||
362 | 04a63d25 | xthirioux | | StateVar stv -> |
363 | let lhs = get_assign_lhs instr' in |
||
364 | (match lhs.value_desc with |
||
365 | c287ba28 | xthirioux | | LocalVar v' -> |
366 | 3ca27bc7 | ploc | let instr = eliminate subst (update_instr_desc instr (mk_assign v lhs)) in |
367 | c287ba28 | xthirioux | subst, instr :: instrs |
368 | 04a63d25 | xthirioux | | StateVar stv' -> |
369 | let subst_v' = IMap.add stv'.var_id v IMap.empty in |
||
370 | c287ba28 | xthirioux | let instrs' = snd (List.fold_right (fun instr (ok, instrs) -> (ok || instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in |
371 | 04a63d25 | xthirioux | IMap.add stv'.var_id v subst, instr :: instrs' |
372 | c287ba28 | xthirioux | | _ -> assert false) |
373 | | _ -> assert false |
||
374 | with Not_found -> subst, instr :: instrs |
||
375 | |||
376 | (** Common sub-expression elimination for machine instructions *) |
||
377 | (* - [subst] : hashtable from ident to (simple) definition |
||
378 | it is an equivalence table |
||
379 | - [elim] : set of eliminated variables |
||
380 | - [instrs] : previous instructions, which [instr] is compared against |
||
381 | - [instr] : current instruction, normalized by [subst] |
||
382 | *) |
||
383 | let rec instr_cse (subst, instrs) instr = |
||
384 | 3ca27bc7 | ploc | match get_instr_desc instr with |
385 | c287ba28 | xthirioux | (* Simple cases*) |
386 | 04a63d25 | xthirioux | | MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl) |
387 | 3ca27bc7 | ploc | -> instr_cse (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))) |
388 | d7b73fed | xthirioux | | MLocalAssign(v, expr) when is_unfoldable_expr 2 expr |
389 | c287ba28 | xthirioux | -> (IMap.add v.var_id expr subst, instr :: instrs) |
390 | | _ when is_assign instr |
||
391 | -> subst_instr subst instrs instr |
||
392 | | _ -> (subst, instr :: instrs) |
||
393 | |||
394 | (** Apply common sub-expression elimination to a sequence of instrs |
||
395 | *) |
||
396 | let rec instrs_cse subst instrs = |
||
397 | let subst, rev_instrs = |
||
398 | List.fold_left instr_cse (subst, []) instrs |
||
399 | in subst, List.rev rev_instrs |
||
400 | |||
401 | (** Apply common sub-expression elimination to a machine |
||
402 | - iterate through step instructions and remove simple local assigns |
||
403 | *) |
||
404 | let machine_cse subst machine = |
||
405 | (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*) |
||
406 | let subst, instrs = instrs_cse subst machine.mstep.step_instrs in |
||
407 | 017eec6a | ploc | let assigned = assigns_instrs instrs VSet.empty |
408 | c287ba28 | xthirioux | in |
409 | { |
||
410 | machine with |
||
411 | 017eec6a | ploc | mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory; |
412 | c287ba28 | xthirioux | mstep = { |
413 | machine.mstep with |
||
414 | 017eec6a | ploc | step_locals = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mstep.step_locals; |
415 | c287ba28 | xthirioux | step_instrs = instrs |
416 | } |
||
417 | } |
||
418 | |||
419 | let machines_cse machines = |
||
420 | List.map |
||
421 | (machine_cse IMap.empty) |
||
422 | machines |
||
423 | |||
424 | 45c13277 | xthirioux | (* variable substitution for optimizing purposes *) |
425 | |||
426 | (* checks whether an [instr] is skip and can be removed from program *) |
||
427 | let rec instr_is_skip instr = |
||
428 | 3ca27bc7 | ploc | match get_instr_desc instr with |
429 | 04a63d25 | xthirioux | | MLocalAssign (i, { value_desc = (LocalVar v) ; _}) when i = v -> true |
430 | | MStateAssign (i, { value_desc = StateVar v; _}) when i = v -> true |
||
431 | 45c13277 | xthirioux | | MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl |
432 | | _ -> false |
||
433 | and instrs_are_skip instrs = |
||
434 | List.for_all instr_is_skip instrs |
||
435 | |||
436 | let instr_cons instr cont = |
||
437 | if instr_is_skip instr then cont else instr::cont |
||
438 | |||
439 | let rec instr_remove_skip instr cont = |
||
440 | 3ca27bc7 | ploc | match get_instr_desc instr with |
441 | 04a63d25 | xthirioux | | MLocalAssign (i, { value_desc = LocalVar v; _ }) when i = v -> cont |
442 | | MStateAssign (i, { value_desc = StateVar v; _ }) when i = v -> cont |
||
443 | 3ca27bc7 | ploc | | MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont |
444 | 45c13277 | xthirioux | | _ -> instr::cont |
445 | |||
446 | and instrs_remove_skip instrs cont = |
||
447 | List.fold_right instr_remove_skip instrs cont |
||
448 | |||
449 | let rec value_replace_var fvar value = |
||
450 | 04a63d25 | xthirioux | match value.value_desc with |
451 | 45c13277 | xthirioux | | Cst c -> value |
452 | 04a63d25 | xthirioux | | LocalVar v -> { value with value_desc = LocalVar (fvar v) } |
453 | 45c13277 | xthirioux | | StateVar v -> value |
454 | 04a63d25 | xthirioux | | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) } |
455 | | Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)} |
||
456 | | Access (t, i) -> { value with value_desc = Access(value_replace_var fvar t, i)} |
||
457 | | Power (v, n) -> { value with value_desc = Power(value_replace_var fvar v, n)} |
||
458 | 45c13277 | xthirioux | |
459 | let rec instr_replace_var fvar instr cont = |
||
460 | 3ca27bc7 | ploc | match get_instr_desc instr with |
461 | 04a63d25 | xthirioux | | MComment _ -> instr_cons instr cont |
462 | 3ca27bc7 | ploc | | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont |
463 | | MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont |
||
464 | 45c13277 | xthirioux | | MReset i -> instr_cons instr cont |
465 | eb837d74 | xthirioux | | MNoReset i -> instr_cons instr cont |
466 | 3ca27bc7 | ploc | | MStep (il, i, vl) -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont |
467 | | MBranch (g, hl) -> instr_cons (update_instr_desc instr (MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il [])) hl))) cont |
||
468 | 45c13277 | xthirioux | |
469 | and instrs_replace_var fvar instrs cont = |
||
470 | List.fold_right (instr_replace_var fvar) instrs cont |
||
471 | |||
472 | let step_replace_var fvar step = |
||
473 | (* Some outputs may have been replaced by locals. |
||
474 | We then need to rename those outputs |
||
475 | without changing their clocks, etc *) |
||
476 | let outputs' = |
||
477 | List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs in |
||
478 | let locals' = |
||
479 | List.fold_left (fun res l -> |
||
480 | let l' = fvar l in |
||
481 | if List.exists (fun o -> o.var_id = l'.var_id) outputs' |
||
482 | then res |
||
483 | else Utils.add_cons l' res) |
||
484 | [] step.step_locals in |
||
485 | { step with |
||
486 | step_checks = List.map (fun (l, v) -> (l, value_replace_var fvar v)) step.step_checks; |
||
487 | step_outputs = outputs'; |
||
488 | step_locals = locals'; |
||
489 | step_instrs = instrs_replace_var fvar step.step_instrs []; |
||
490 | } |
||
491 | |||
492 | let rec machine_replace_variables fvar m = |
||
493 | { m with |
||
494 | mstep = step_replace_var fvar m.mstep |
||
495 | } |
||
496 | |||
497 | let machine_reuse_variables m reuse = |
||
498 | let fvar v = |
||
499 | try |
||
500 | Hashtbl.find reuse v.var_id |
||
501 | with Not_found -> v in |
||
502 | machine_replace_variables fvar m |
||
503 | |||
504 | 04a63d25 | xthirioux | let machines_reuse_variables prog reuse_tables = |
505 | 45c13277 | xthirioux | List.map |
506 | (fun m -> |
||
507 | 04a63d25 | xthirioux | machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables) |
508 | 45c13277 | xthirioux | ) prog |
509 | |||
510 | b1655a21 | xthirioux | let rec instr_assign res instr = |
511 | 3ca27bc7 | ploc | match get_instr_desc instr with |
512 | b1655a21 | xthirioux | | MLocalAssign (i, _) -> Disjunction.CISet.add i res |
513 | | MStateAssign (i, _) -> Disjunction.CISet.add i res |
||
514 | | MBranch (g, hl) -> List.fold_left (fun res (h, b) -> instrs_assign res b) res hl |
||
515 | | MStep (il, _, _) -> List.fold_right Disjunction.CISet.add il res |
||
516 | | _ -> res |
||
517 | |||
518 | and instrs_assign res instrs = |
||
519 | List.fold_left instr_assign res instrs |
||
520 | |||
521 | let rec instr_constant_assign var instr = |
||
522 | 3ca27bc7 | ploc | match get_instr_desc instr with |
523 | 04a63d25 | xthirioux | | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ }) |
524 | | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var |
||
525 | b1655a21 | xthirioux | | MBranch (g, hl) -> List.for_all (fun (h, b) -> instrs_constant_assign var b) hl |
526 | | _ -> false |
||
527 | |||
528 | and instrs_constant_assign var instrs = |
||
529 | List.fold_left (fun res i -> if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then instr_constant_assign var i else res) false instrs |
||
530 | |||
531 | let rec instr_reduce branches instr1 cont = |
||
532 | 3ca27bc7 | ploc | match get_instr_desc instr1 with |
533 | 04a63d25 | xthirioux | | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont) |
534 | | MStateAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont) |
||
535 | 3ca27bc7 | ploc | | MBranch (g, hl) -> (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl))) :: cont |
536 | b1655a21 | xthirioux | | _ -> instr1 :: cont |
537 | |||
538 | and instrs_reduce branches instrs cont = |
||
539 | match instrs with |
||
540 | | [] -> cont |
||
541 | | [i] -> instr_reduce branches i cont |
||
542 | | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont |
||
543 | |||
544 | let rec instrs_fusion instrs = |
||
545 | 3ca27bc7 | ploc | match instrs, List.map get_instr_desc instrs with |
546 | | [], [] |
||
547 | | [_], [_] -> |
||
548 | b1655a21 | xthirioux | instrs |
549 | 3ca27bc7 | ploc | | i1::i2::q, i1_desc::(MBranch ({ value_desc = LocalVar v; _}, hl))::q_desc when instr_constant_assign v i1 -> |
550 | b1655a21 | xthirioux | instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q) |
551 | 3ca27bc7 | ploc | | i1::i2::q, i1_desc::(MBranch ({ value_desc = StateVar v; _}, hl))::q_desc when instr_constant_assign v i1 -> |
552 | b1655a21 | xthirioux | instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q) |
553 | 3ca27bc7 | ploc | | i1::i2::q, _ -> |
554 | b1655a21 | xthirioux | i1 :: instrs_fusion (i2::q) |
555 | 3ca27bc7 | ploc | | _ -> assert false (* Other cases should not happen since both lists are of same size *) |
556 | |||
557 | b1655a21 | xthirioux | let step_fusion step = |
558 | { step with |
||
559 | step_instrs = instrs_fusion step.step_instrs; |
||
560 | } |
||
561 | |||
562 | let rec machine_fusion m = |
||
563 | { m with |
||
564 | mstep = step_fusion m.mstep |
||
565 | } |
||
566 | |||
567 | let machines_fusion prog = |
||
568 | List.map machine_fusion prog |
||
569 | cf78a589 | ploc | |
570 | 13507742 | ploc | |
571 | (*** Main function ***) |
||
572 | |||
573 | let optimize prog node_schs machine_code = |
||
574 | let machine_code = |
||
575 | if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then |
||
576 | begin |
||
577 | Log.report ~level:1 |
||
578 | (fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,"); |
||
579 | let machine_code = machines_cse machine_code in |
||
580 | Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code); |
||
581 | machine_code |
||
582 | end |
||
583 | else |
||
584 | machine_code |
||
585 | in |
||
586 | (* Optimize machine code *) |
||
587 | let machine_code, removed_table = |
||
588 | if !Options.optimization >= 2 && !Options.output <> "emf" (*&& !Options.output <> "horn"*) then |
||
589 | begin |
||
590 | Log.report ~level:1 (fun fmt -> Format.fprintf fmt |
||
591 | ".. machines optimization: const. inlining (partial eval. with const)@,"); |
||
592 | let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in |
||
593 | Log.report ~level:3 (fun fmt -> Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ " |
||
594 | (pp_imap pp_elim) removed_table); |
||
595 | Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code); |
||
596 | machine_code, removed_table |
||
597 | end |
||
598 | else |
||
599 | machine_code, IMap.empty |
||
600 | in |
||
601 | (* Optimize machine code *) |
||
602 | let machine_code = |
||
603 | if !Options.optimization >= 3 && not (Backends.is_functional ()) then |
||
604 | begin |
||
605 | Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,"); |
||
606 | let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in |
||
607 | let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in |
||
608 | machines_fusion (machines_reuse_variables machine_code reuse_tables) |
||
609 | end |
||
610 | else |
||
611 | machine_code |
||
612 | in |
||
613 | |||
614 | (* Salsa optimize machine code *) |
||
615 | (* |
||
616 | let machine_code = |
||
617 | if !Options.salsa_enabled then |
||
618 | begin |
||
619 | check_main (); |
||
620 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,"); |
||
621 | (* Selecting float constants for Salsa *) |
||
622 | let constEnv = List.fold_left ( |
||
623 | fun accu c_topdecl -> |
||
624 | match c_topdecl.top_decl_desc with |
||
625 | | Const c when Types.is_real_type c.const_type -> |
||
626 | (c.const_id, c.const_value) :: accu |
||
627 | | _ -> accu |
||
628 | ) [] (Corelang.get_consts prog) |
||
629 | in |
||
630 | List.map |
||
631 | (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) |
||
632 | machine_code |
||
633 | end |
||
634 | else |
||
635 | machine_code |
||
636 | in |
||
637 | Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ " |
||
638 | (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
||
639 | machine_code); |
||
640 | *) |
||
641 | |||
642 | |||
643 | machine_code |
||
644 | |||
645 | |||
646 | cf78a589 | ploc | (* Local Variables: *) |
647 | (* compile-command:"make -C .." *) |
||
648 | (* End: *) |