lustrec / src / optimize_machine.ml @ e8250987
History  View  Annotate  Download (26 KB)
1 
(********************************************************************) 

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 
open Utils 
13 
open Lustre_types 
14 
open Machine_code_types 
15 
open Corelang 
16 
open Causality 
17 
open Machine_code_common 
18 
open Dimension 
19  
20  
21 
let pp_elim m fmt elim = 
22 
begin 
23 
Format.fprintf fmt "@[{ /* elim table: */@ "; 
24 
IMap.iter (fun v expr > Format.fprintf fmt "%s > %a@ " v (pp_val m) expr) elim; 
25 
Format.fprintf fmt "}@ @]"; 
26 
end 
27  
28 
let rec eliminate m elim instr = 
29 
let e_expr = eliminate_expr m elim in 
30 
match get_instr_desc instr with 
31 
 MComment _ > instr 
32 
 MLocalAssign (i,v) > update_instr_desc instr (MLocalAssign (i, e_expr v)) 
33 
 MStateAssign (i,v) > update_instr_desc instr (MStateAssign (i, e_expr v)) 
34 
 MReset i > instr 
35 
 MNoReset i > instr 
36 
 MStep (il, i, vl) > update_instr_desc instr (MStep(il, i, List.map e_expr vl)) 
37 
 MBranch (g,hl) > 
38 
update_instr_desc instr ( 
39 
MBranch 
40 
(e_expr g, 
41 
(List.map 
42 
(fun (l, il) > l, List.map (eliminate m elim) il) 
43 
hl 
44 
) 
45 
) 
46 
) 
47 

48 
and eliminate_expr m elim expr = 
49 
let eliminate_expr = eliminate_expr m in 
50 
match expr.value_desc with 
51 
 Var v > if is_memory m v then expr else (try IMap.find v.var_id elim with Not_found > expr) 
52 
 Fun (id, vl) > {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)} 
53 
 Array(vl) > {expr with value_desc = Array(List.map (eliminate_expr elim) vl)} 
54 
 Access(v1, v2) > { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)} 
55 
 Power(v1, v2) > { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)} 
56 
 Cst _ > expr 
57  
58 
let eliminate_dim elim dim = 
59 
Dimension.expr_replace_expr 
60 
(fun v > try 
61 
dimension_of_value (IMap.find v elim) 
62 
with Not_found > mkdim_ident dim.dim_loc v) 
63 
dim 
64  
65  
66 
(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following 
67 
functions seem unsused. They have to be adapted to the new type for expr 
68 
*) 
69  
70 
let unfold_expr_offset m offset expr = 
71 
List.fold_left 
72 
(fun res > (function  Index i > mk_val (Access (res, value_of_dimension m i)) 
73 
(Types.array_element_type res.value_type) 
74 
 Field f > Format.eprintf "internal error: not yet implemented !"; assert false)) 
75 
expr offset 
76  
77 
let rec simplify_cst_expr m offset typ cst = 
78 
match offset, cst with 
79 
 [] , _ 
80 
> mk_val (Cst cst) typ 
81 
 Index i :: q, Const_array cl when Dimension.is_dimension_const i 
82 
> let elt_typ = Types.array_element_type typ in 
83 
simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const_dimension i)) 
84 
 Index i :: q, Const_array cl 
85 
> let elt_typ = Types.array_element_type typ in 
86 
unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ) 
87 
 Field f :: q, Const_struct fl 
88 
> let fld_typ = Types.struct_field_type typ f in 
89 
simplify_cst_expr m q fld_typ (List.assoc f fl) 
90 
 _ > (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false) 
91  
92 
let simplify_expr_offset m expr = 
93 
let rec simplify offset expr = 
94 
match offset, expr.value_desc with 
95 
 Field f ::q , _ > failwith "not yet implemented" 
96 
 _ , Fun (id, vl) when Basic_library.is_value_internal_fun expr 
97 
> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type 
98 
 _ , Fun _ 
99 
 _ , Var _ > unfold_expr_offset m offset expr 
100 
 _ , Cst cst > simplify_cst_expr m offset expr.value_type cst 
101 
 _ , Access (expr, i) > simplify (Index (dimension_of_value i) :: offset) expr 
102 
 [] , _ > expr 
103 
 Index _ :: q, Power (expr, _) > simplify q expr 
104 
 Index i :: q, Array vl when Dimension.is_dimension_const i 
105 
> simplify q (List.nth vl (Dimension.size_const_dimension i)) 
106 
 Index i :: q, Array vl > unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type) 
107 
(*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res) 
108 
with e > (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*) 
109 
in simplify [] expr 
110  
111 
let rec simplify_instr_offset m instr = 
112 
match get_instr_desc instr with 
113 
 MLocalAssign (v, expr) > update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr)) 
114 
 MStateAssign (v, expr) > update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr)) 
115 
 MReset id > instr 
116 
 MNoReset id > instr 
117 
 MStep (outputs, id, inputs) > update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs)) 
118 
 MBranch (cond, brl) 
119 
> update_instr_desc instr ( 
120 
MBranch(simplify_expr_offset m cond, List.map (fun (l, il) > l, simplify_instrs_offset m il) brl) 
121 
) 
122 
 MComment _ > instr 
123  
124 
and simplify_instrs_offset m instrs = 
125 
List.map (simplify_instr_offset m) instrs 
126  
127 
let is_scalar_const c = 
128 
match c with 
129 
 Const_real _ 
130 
 Const_int _ 
131 
 Const_tag _ > true 
132 
 _ > false 
133  
134 
(* An instruction v = expr may (and will) be unfolded iff: 
135 
 either expr is atomic 
136 
(no complex expressions, only const, vars and array/struct accesses) 
137 
 or v has a fanin <= 1 (used at most once) 
138 
*) 
139 
let is_unfoldable_expr fanin expr = 
140 
let rec unfold_const offset cst = 
141 
match offset, cst with 
142 
 _ , Const_int _ 
143 
 _ , Const_real _ 
144 
 _ , Const_tag _ > true 
145 
 Field f :: q, Const_struct fl > unfold_const q (List.assoc f fl) 
146 
 [] , Const_struct _ > false 
147 
 Index i :: q, Const_array cl when Dimension.is_dimension_const i 
148 
> unfold_const q (List.nth cl (Dimension.size_const_dimension i)) 
149 
 _ , Const_array _ > false 
150 
 _ > assert false in 
151 
let rec unfold offset expr = 
152 
match offset, expr.value_desc with 
153 
 _ , Cst cst > unfold_const offset cst 
154 
 _ , Var _ > 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 
 _ , Fun (id, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr 
163 
> List.for_all (unfold offset) vl 
164 
 _ , Fun _ > false 
165 
 _ > assert false 
166 
in unfold [] expr 
167  
168 
let basic_unfoldable_assign fanin v expr = 
169 
try 
170 
let d = Hashtbl.find fanin v.var_id 
171 
in is_unfoldable_expr d expr 
172 
with Not_found > false 
173  
174 
let unfoldable_assign fanin v expr = 
175 
(if !Options.mpfr then Mpfr.unfoldable_value expr else true) 
176 
&& basic_unfoldable_assign fanin v expr 
177  
178 
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 
(* see if elim has to take in account the provided instr: 
188 
if so, update elim and return the remove flag, 
189 
otherwise, the expression should be kept and elim is left untouched *) 
190 
let rec instrs_unfold m 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 m 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 m fanin instrs elim instr 
199 
) (elim, []) instrs 
200 
in elim, List.rev rev_instrs 
201  
202 
and instr_unfold m fanin instrs elim instr = 
203 
(* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*) 
204 
match get_instr_desc instr with 
205 
(* Simple cases*) 
206 
 MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type) 
207 
> instr_unfold m fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))) 
208 
 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 m 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 
in elim, ((update_instr_desc instr (MBranch (g, branches))) :: instrs) 
217 
 _ 
218 
> (elim, instr :: instrs) 
219 
(* 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 
let static_call_unfold elim (inst, (n, args)) = 
228 
let replace v = 
229 
try 
230 
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 
(** Perform optimization on machine code: 
235 
 iterate through step instructions and remove simple local assigns 
236 

237 
*) 
238 
let machine_unfold fanin elim machine = 
239 
(*Log.report ~level:1 (fun fmt > Format.fprintf fmt "machine_unfold %a@." pp_elim elim);*) 
240 
let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in 
241 
let elim_vars, instrs = instrs_unfold machine fanin elim_consts machine.mstep.step_instrs in 
242 
let instrs = simplify_instrs_offset machine instrs in 
243 
let checks = List.map (fun (loc, check) > loc, eliminate_expr machine elim_vars check) machine.mstep.step_checks in 
244 
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 
in 
248 
{ 
249 
machine with 
250 
mstep = { 
251 
machine.mstep with 
252 
step_locals = locals; 
253 
step_instrs = instrs; 
254 
step_checks = checks 
255 
}; 
256 
mconst = mconst; 
257 
minstances = minstances; 
258 
mcalls = mcalls; 
259 
}, 
260 
elim_vars 
261  
262 
let instr_of_const top_const = 
263 
let const = const_of_top top_const in 
264 
let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true, None, None) in 
265 
let vdecl = { vdecl with var_type = const.const_type } 
266 
in mkinstr (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type)) 
267  
268 
let machines_unfold consts node_schs machines = 
269 
List.fold_right (fun m (machines, removed) > 
270 
let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in 
271 
let elim_consts, _ = instrs_unfold m 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 
machines 
276 
([], IMap.empty) 
277  
278 
let get_assign_lhs instr = 
279 
match get_instr_desc instr with 
280 
 MLocalAssign(v, e) > mk_val (Var v) e.value_type 
281 
 MStateAssign(v, e) > mk_val (Var v) e.value_type 
282 
 _ > assert false 
283  
284 
let get_assign_rhs instr = 
285 
match get_instr_desc instr with 
286 
 MLocalAssign(_, e) 
287 
 MStateAssign(_, e) > e 
288 
 _ > assert false 
289  
290 
let is_assign instr = 
291 
match get_instr_desc instr with 
292 
 MLocalAssign _ 
293 
 MStateAssign _ > true 
294 
 _ > false 
295  
296 
let mk_assign m v e = 
297 
match v.value_desc with 
298 
 Var v > if is_memory m v then MStateAssign(v, e) else MLocalAssign(v, e) 
299 
 _ > assert false 
300  
301 
let rec assigns_instr instr assign = 
302 
match get_instr_desc instr with 
303 
 MLocalAssign (i,_) 
304 
 MStateAssign (i,_) > VSet.add i assign 
305 
 MStep (ol, _, _) > List.fold_right VSet.add ol assign 
306 
 MBranch (_,hl) > List.fold_right (fun (_, il) > assigns_instrs il) hl assign 
307 
 _ > assign 
308  
309 
and assigns_instrs instrs assign = 
310 
List.fold_left (fun assign instr > assigns_instr instr assign) assign instrs 
311  
312 
(* 
313 
and substitute_expr subst expr = 
314 
match expr with 
315 
 Var v > (try IMap.find expr subst with Not_found > expr) 
316 
 Fun (id, vl) > Fun (id, List.map (substitute_expr subst) vl) 
317 
 Array(vl) > Array(List.map (substitute_expr subst) vl) 
318 
 Access(v1, v2) > Access(substitute_expr subst v1, substitute_expr subst v2) 
319 
 Power(v1, v2) > Power(substitute_expr subst v1, substitute_expr subst v2) 
320 
 Cst _ > expr 
321 
*) 
322 
(** Finds a substitute for [instr] in [instrs], 
323 
i.e. another instr' with the same rhs expression. 
324 
Then substitute this expression with the first assigned var 
325 
*) 
326 
let subst_instr m subst instrs instr = 
327 
(*Format.eprintf "subst instr: %a@." Machine_code.pp_instr instr;*) 
328 
let instr = eliminate m subst instr in 
329 
let instr_v = get_assign_lhs instr in 
330 
let instr_e = get_assign_rhs instr in 
331 
try 
332 
(* Searching for equivalent asssign *) 
333 
let instr' = List.find (fun instr' > is_assign instr' && 
334 
get_assign_rhs instr' = instr_e) instrs in 
335 
(* Registering the instr_v as instr'_v while replacing *) 
336 
match instr_v.value_desc with 
337 
 Var v > 
338 
if not (is_memory m v) then 
339 
(* The current instruction defines a local variables, ie not 
340 
memory, we can just record the relationship and continue 
341 
*) 
342 
IMap.add v.var_id (get_assign_lhs instr') subst, instrs 
343 
else ( 
344 
(* The current instruction defines a memory. We need to keep 
345 
the definition, simplified *) 
346 
let instr'_v = get_assign_lhs instr' in 
347 
(match instr'_v.value_desc with 
348 
 Var v' > 
349 
if not (is_memory m v') then 
350 
(* We define v' = v. Don't need to update the records. *) 
351 
let instr = eliminate m subst (update_instr_desc instr (mk_assign m instr_v instr'_v)) in 
352 
subst, instr :: instrs 
353 
else ( (* Last case, v', the lhs of the previous similar 
354 
definition is, itself, a memory *) 
355  
356 
(* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *) 
357 
(* Filtering out the list of instructions: 
358 
 we copy in the same order the list of instr in instrs (fold_right) 
359 
 if the current instr is this instr' then apply 
360 
the elimination with v' > v on instr' before recording it as an instruction. 
361 
*) 
362 
let subst_v' = IMap.add v'.var_id instr_v IMap.empty in 
363 
let instrs' = 
364 
snd 
365 
(List.fold_right 
366 
(fun instr (ok, instrs) > 
367 
(ok  instr = instr', 
368 
if ok then 
369 
instr :: instrs 
370 
else 
371 
if instr = instr' then 
372 
instrs 
373 
else 
374 
eliminate m subst_v' instr :: instrs)) 
375 
instrs (false, [])) 
376 
in 
377 
IMap.add v'.var_id instr_v subst, instr :: instrs' 
378 
) 
379 
 _ > assert false) 
380 
) 
381 
 _ > assert false 
382 

383 
with Not_found > 
384 
(* No such equivalent expr: keeping the definition *) 
385 
subst, instr :: instrs 
386 

387 
(** Common subexpression elimination for machine instructions *) 
388 
(*  [subst] : hashtable from ident to (simple) definition 
389 
it is an equivalence table 
390 
 [elim] : set of eliminated variables 
391 
 [instrs] : previous instructions, which [instr] is compared against 
392 
 [instr] : current instruction, normalized by [subst] 
393 
*) 
394 
let rec instr_cse m (subst, instrs) instr = 
395 
match get_instr_desc instr with 
396 
(* Simple cases*) 
397 
 MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v > v.value_type) vl) 
398 
> instr_cse m (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))) 
399 
 MLocalAssign(v, expr) when is_unfoldable_expr 2 expr 
400 
> (IMap.add v.var_id expr subst, instr :: instrs) 
401 
 _ when is_assign instr 
402 
> subst_instr m subst instrs instr 
403 
 _ > (subst, instr :: instrs) 
404  
405 
(** Apply common subexpression elimination to a sequence of instrs 
406 
*) 
407 
let instrs_cse m subst instrs = 
408 
let subst, rev_instrs = 
409 
List.fold_left (instr_cse m) (subst, []) instrs 
410 
in subst, List.rev rev_instrs 
411  
412 
(** Apply common subexpression elimination to a machine 
413 
 iterate through step instructions and remove simple local assigns 
414 
*) 
415 
let machine_cse subst machine = 
416 
(*Log.report ~level:1 (fun fmt > Format.fprintf fmt "machine_cse %a@." pp_elim subst);*) 
417 
let subst, instrs = instrs_cse machine subst machine.mstep.step_instrs in 
418 
let assigned = assigns_instrs instrs VSet.empty 
419 
in 
420 
{ 
421 
machine with 
422 
mmemory = List.filter (fun vdecl > VSet.mem vdecl assigned) machine.mmemory; 
423 
mstep = { 
424 
machine.mstep with 
425 
step_locals = List.filter (fun vdecl > VSet.mem vdecl assigned) machine.mstep.step_locals; 
426 
step_instrs = instrs 
427 
} 
428 
} 
429  
430 
let machines_cse machines = 
431 
List.map 
432 
(machine_cse IMap.empty) 
433 
machines 
434  
435 
(* variable substitution for optimizing purposes *) 
436  
437 
(* checks whether an [instr] is skip and can be removed from program *) 
438 
let rec instr_is_skip instr = 
439 
match get_instr_desc instr with 
440 
 MLocalAssign (i, { value_desc = (Var v) ; _}) when i = v > true 
441 
 MStateAssign (i, { value_desc = Var v; _}) when i = v > true 
442 
 MBranch (g, hl) > List.for_all (fun (_, il) > instrs_are_skip il) hl 
443 
 _ > false 
444 
and instrs_are_skip instrs = 
445 
List.for_all instr_is_skip instrs 
446  
447 
let instr_cons instr cont = 
448 
if instr_is_skip instr then cont else instr::cont 
449  
450 
let rec instr_remove_skip instr cont = 
451 
match get_instr_desc instr with 
452 
 MLocalAssign (i, { value_desc = Var v; _ }) when i = v > cont 
453 
 MStateAssign (i, { value_desc = Var v; _ }) when i = v > cont 
454 
 MBranch (g, hl) > update_instr_desc instr (MBranch (g, List.map (fun (h, il) > (h, instrs_remove_skip il [])) hl)) :: cont 
455 
 _ > instr::cont 
456  
457 
and instrs_remove_skip instrs cont = 
458 
List.fold_right instr_remove_skip instrs cont 
459  
460 
let rec value_replace_var fvar value = 
461 
match value.value_desc with 
462 
 Cst c > value 
463 
 Var v > { value with value_desc = Var (fvar v) } 
464 
 Fun (id, args) > { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) } 
465 
 Array vl > { value with value_desc = Array (List.map (value_replace_var fvar) vl)} 
466 
 Access (t, i) > { value with value_desc = Access(value_replace_var fvar t, i)} 
467 
 Power (v, n) > { value with value_desc = Power(value_replace_var fvar v, n)} 
468  
469 
let rec instr_replace_var fvar instr cont = 
470 
match get_instr_desc instr with 
471 
 MComment _ > instr_cons instr cont 
472 
 MLocalAssign (i, v) > instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont 
473 
 MStateAssign (i, v) > instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont 
474 
 MReset i > instr_cons instr cont 
475 
 MNoReset i > instr_cons instr cont 
476 
 MStep (il, i, vl) > instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont 
477 
 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 
478  
479 
and instrs_replace_var fvar instrs cont = 
480 
List.fold_right (instr_replace_var fvar) instrs cont 
481  
482 
let step_replace_var fvar step = 
483 
(* Some outputs may have been replaced by locals. 
484 
We then need to rename those outputs 
485 
without changing their clocks, etc *) 
486 
let outputs' = 
487 
List.map (fun o > { o with var_id = (fvar o).var_id }) step.step_outputs in 
488 
let locals' = 
489 
List.fold_left (fun res l > 
490 
let l' = fvar l in 
491 
if List.exists (fun o > o.var_id = l'.var_id) outputs' 
492 
then res 
493 
else Utils.add_cons l' res) 
494 
[] step.step_locals in 
495 
{ step with 
496 
step_checks = List.map (fun (l, v) > (l, value_replace_var fvar v)) step.step_checks; 
497 
step_outputs = outputs'; 
498 
step_locals = locals'; 
499 
step_instrs = instrs_replace_var fvar step.step_instrs []; 
500 
} 
501  
502 
let rec machine_replace_variables fvar m = 
503 
{ m with 
504 
mstep = step_replace_var fvar m.mstep 
505 
} 
506  
507 
let machine_reuse_variables m reuse = 
508 
let fvar v = 
509 
try 
510 
Hashtbl.find reuse v.var_id 
511 
with Not_found > v in 
512 
machine_replace_variables fvar m 
513  
514 
let machines_reuse_variables prog reuse_tables = 
515 
List.map 
516 
(fun m > 
517 
machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables) 
518 
) prog 
519  
520 
let rec instr_assign res instr = 
521 
match get_instr_desc instr with 
522 
 MLocalAssign (i, _) > Disjunction.CISet.add i res 
523 
 MStateAssign (i, _) > Disjunction.CISet.add i res 
524 
 MBranch (g, hl) > List.fold_left (fun res (h, b) > instrs_assign res b) res hl 
525 
 MStep (il, _, _) > List.fold_right Disjunction.CISet.add il res 
526 
 _ > res 
527  
528 
and instrs_assign res instrs = 
529 
List.fold_left instr_assign res instrs 
530  
531 
let rec instr_constant_assign var instr = 
532 
match get_instr_desc instr with 
533 
 MLocalAssign (i, { value_desc = Cst (Const_tag _); _ }) 
534 
 MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) > i = var 
535 
 MBranch (g, hl) > List.for_all (fun (h, b) > instrs_constant_assign var b) hl 
536 
 _ > false 
537  
538 
and instrs_constant_assign var instrs = 
539 
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 
540  
541 
let rec instr_reduce branches instr1 cont = 
542 
match get_instr_desc instr1 with 
543 
 MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) > instr1 :: (List.assoc c branches @ cont) 
544 
 MStateAssign (_, { value_desc = Cst (Const_tag c); _}) > instr1 :: (List.assoc c branches @ cont) 
545 
 MBranch (g, hl) > (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) > (h, instrs_reduce branches b [])) hl))) :: cont 
546 
 _ > instr1 :: cont 
547  
548 
and instrs_reduce branches instrs cont = 
549 
match instrs with 
550 
 [] > cont 
551 
 [i] > instr_reduce branches i cont 
552 
 i1::i2::q > i1 :: instrs_reduce branches (i2::q) cont 
553  
554 
let rec instrs_fusion instrs = 
555 
match instrs, List.map get_instr_desc instrs with 
556 
 [], [] 
557 
 [_], [_] > 
558 
instrs 
559 
 i1::i2::q, i1_desc::(MBranch ({ value_desc = Var v; _}, hl))::q_desc when instr_constant_assign v i1 > 
560 
instr_reduce (List.map (fun (h, b) > h, instrs_fusion b) hl) i1 (instrs_fusion q) 
561 
 i1::i2::q, _ > 
562 
i1 :: instrs_fusion (i2::q) 
563 
 _ > assert false (* Other cases should not happen since both lists are of same size *) 
564 

565 
let step_fusion step = 
566 
{ step with 
567 
step_instrs = instrs_fusion step.step_instrs; 
568 
} 
569  
570 
let rec machine_fusion m = 
571 
{ m with 
572 
mstep = step_fusion m.mstep 
573 
} 
574  
575 
let machines_fusion prog = 
576 
List.map machine_fusion prog 
577  
578  
579 
(*** Main function ***) 
580 

581 
let optimize prog node_schs machine_code = 
582 
let machine_code = 
583 
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then 
584 
begin 
585 
Log.report ~level:1 
586 
(fun fmt > Format.fprintf fmt ".. machines optimization: subexpression elimination@,"); 
587 
let machine_code = machines_cse machine_code in 
588 
Log.report ~level:3 (fun fmt > Format.fprintf fmt ".. generated machines (subexpr elim):@ %a@ "pp_machines machine_code); 
589 
machine_code 
590 
end 
591 
else 
592 
machine_code 
593 
in 
594 
(* Optimize machine code *) 
595 
let machine_code, removed_table = 
596 
if !Options.optimization >= 2 && !Options.output <> "emf" (*&& !Options.output <> "horn"*) then 
597 
begin 
598 
Log.report ~level:1 (fun fmt > Format.fprintf fmt 
599 
".. machines optimization: const. inlining (partial eval. with const)@,"); 
600 
let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in 
601 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ " 
602 
(pp_imap (pp_elim empty_machine)) removed_table); 
603 
Log.report ~level:3 (fun fmt > Format.fprintf fmt ".. generated machines (const inlining):@ %a@ "pp_machines machine_code); 
604 
machine_code, removed_table 
605 
end 
606 
else 
607 
machine_code, IMap.empty 
608 
in 
609 
(* Optimize machine code *) 
610 
let machine_code = 
611 
if !Options.optimization >= 3 && not (Backends.is_functional ()) then 
612 
begin 
613 
Log.report ~level:1 (fun fmt > Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,"); 
614 
let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in 
615 
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in 
616 
machines_fusion (machines_reuse_variables machine_code reuse_tables) 
617 
end 
618 
else 
619 
machine_code 
620 
in 
621 

622  
623 
machine_code 
624 

625 

626 
(* Local Variables: *) 
627 
(* compilecommand:"make C .." *) 
628 
(* End: *) 