Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / optimize_machine.ml @ f0195e96

History | View | Annotate | Download (31.6 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
module Mpfr = Lustrec_mpfr
20

    
21

    
22
let pp_elim m fmt elim =
23
  begin
24
    Format.fprintf fmt "@[{ /* elim table: */@ ";
25
    IMap.iter (fun v expr -> Format.fprintf fmt "%s |-> %a@ " v (pp_val m) expr) elim;
26
    Format.fprintf fmt "}@ @]";
27
  end
28

    
29
let rec eliminate m elim instr =
30
  let e_expr = eliminate_expr m elim in
31
  match get_instr_desc instr with
32
  | MSpec _ | MComment _         -> instr
33
  | MLocalAssign (i,v) -> update_instr_desc instr (MLocalAssign (i, e_expr v))
34
  | MStateAssign (i,v) -> update_instr_desc instr (MStateAssign (i, e_expr v))
35
  | MReset i           -> instr
36
  | MNoReset i         -> instr
37
  | MStep (il, i, vl)  -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
38
  | MBranch (g,hl)     -> 
39
     update_instr_desc instr (
40
       MBranch
41
	 (e_expr g, 
42
	  (List.map 
43
	     (fun (l, il) -> l, List.map (eliminate m elim) il) 
44
	     hl
45
	  )
46
	 )
47
     )
48
    
49
and eliminate_expr m elim expr =
50
  let eliminate_expr = eliminate_expr m in
51
  match expr.value_desc with
52
  | Var v -> if is_memory m v then
53
               expr
54
             else
55
               (try IMap.find v.var_id elim with Not_found -> expr)
56
  | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
57
  | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
58
  | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
59
  | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
60
  | Cst _ -> expr
61

    
62
let eliminate_dim elim dim =
63
  Dimension.expr_replace_expr 
64
    (fun v -> try
65
		dimension_of_value (IMap.find v elim) 
66
      with Not_found -> mkdim_ident dim.dim_loc v) 
67
    dim
68

    
69

    
70
(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following
71
   functions seem unsused. They have to be adapted to the new type for expr
72
*)
73

    
74
let unfold_expr_offset m offset expr =
75
  List.fold_left
76
    (fun res -> (function | Index i -> mk_val (Access (res, value_of_dimension m i))
77
					      (Types.array_element_type res.value_type)
78
                          | Field f -> Format.eprintf "internal error: not yet implemented !"; assert false))
79
    expr offset
80

    
81
let rec simplify_cst_expr m offset typ cst =
82
    match offset, cst with
83
    | []          , _
84
      -> mk_val (Cst cst) typ
85
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i
86
      -> let elt_typ = Types.array_element_type typ in
87
         simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const_dimension i))
88
    | Index i :: q, Const_array cl
89
      -> let elt_typ = Types.array_element_type typ in
90
         unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
91
    | Field f :: q, Const_struct fl
92
      -> let fld_typ = Types.struct_field_type typ f in
93
         simplify_cst_expr m q fld_typ (List.assoc f fl)
94
    | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false)
95

    
96
let simplify_expr_offset m expr =
97
  let rec simplify offset expr =
98
    match offset, expr.value_desc with
99
    | Field f ::q , _                -> failwith "not yet implemented"
100
    | _           , Fun (id, vl) when Basic_library.is_value_internal_fun expr
101
                                     -> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
102
    | _           , Fun _
103
    | _           , Var _            -> unfold_expr_offset m offset expr
104
    | _           , Cst cst          -> simplify_cst_expr m offset expr.value_type cst
105
    | _           , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr
106
    | []          , _                -> expr
107
    | Index _ :: q, Power (expr, _)  -> simplify q expr
108
    | Index i :: q, Array vl when Dimension.is_dimension_const i
109
                                     -> simplify q (List.nth vl (Dimension.size_const_dimension i))
110
    | Index i :: q, Array vl         -> unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type)
111
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
112
     with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
113
  in simplify [] expr
114

    
115
let rec simplify_instr_offset m instr =
116
  match get_instr_desc instr with
117
  | MLocalAssign (v, expr) -> update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
118
  | MStateAssign (v, expr) -> update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
119
  | MReset id              -> instr
120
  | MNoReset id            -> instr
121
  | MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
122
  | MBranch (cond, brl)
123
    -> update_instr_desc instr (
124
      MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
125
    )
126
  | MSpec _ | MComment _             -> instr
127

    
128
and simplify_instrs_offset m instrs =
129
  List.map (simplify_instr_offset m) instrs
130

    
131
let is_scalar_const c =
132
  match c with
133
  | Const_real _
134
  | Const_int _
135
  | Const_tag _   -> true
136
  | _             -> false
137

    
138
(* An instruction v = expr may (and will) be unfolded iff:
139
   - either expr is atomic
140
     (no complex expressions, only const, vars and array/struct accesses)
141
   - or v has a fanin <= 1 (used at most once)
142
*)
143
let is_unfoldable_expr fanin expr =
144
  let rec unfold_const offset cst =
145
    match offset, cst with
146
    | _           , Const_int _
147
    | _           , Const_real _
148
    | _           , Const_tag _     -> true
149
    | Field f :: q, Const_struct fl -> unfold_const q (List.assoc f fl)
150
    | []          , Const_struct _  -> false
151
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i
152
                                    -> unfold_const q (List.nth cl (Dimension.size_const_dimension i))
153
    | _           , Const_array _   -> false
154
    | _                             -> assert false in
155
  let rec unfold offset expr =
156
    match offset, expr.value_desc with
157
    | _           , Cst cst                      -> unfold_const offset cst
158
    | _           , Var _                        -> true
159
    | []          , Power _
160
    | []          , Array _                      -> false
161
    | Index i :: q, Power (v, _)                 -> unfold q v
162
    | Index i :: q, Array vl when Dimension.is_dimension_const i
163
                                                 -> unfold q (List.nth vl (Dimension.size_const_dimension i))
164
    | _           , Array _                      -> false
165
    | _           , Access (v, i)                -> unfold (Index (dimension_of_value i) :: offset) v
166
    | _           , Fun (id, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
167
                                                 -> List.for_all (unfold offset) vl
168
    | _           , Fun _                        -> false
169
    | _                                          -> assert false
170
  in unfold [] expr
171

    
172
let basic_unfoldable_assign fanin v expr =
173
  try
174
    let d = Hashtbl.find fanin v.var_id
175
    in is_unfoldable_expr d expr
176
  with Not_found -> false
177

    
178
let unfoldable_assign fanin v expr =
179
   (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
180
&& basic_unfoldable_assign fanin v expr
181

    
182
let merge_elim elim1 elim2 =
183
  let merge k e1 e2 =
184
    match e1, e2 with
185
    | Some e1, Some e2 -> if e1 = e2 then Some e1 else None
186
    | _      , Some e2 -> Some e2
187
    | Some e1, _       -> Some e1
188
    | _                -> None
189
  in IMap.merge merge elim1 elim2
190

    
191
(* see if elim has to take in account the provided instr:
192
   if so, update elim and return the remove flag,
193
   otherwise, the expression should be kept and elim is left untouched *)
194
let rec instrs_unfold m fanin elim instrs =
195
  let elim, rev_instrs = 
196
    List.fold_left (fun (elim, instrs) instr ->
197
      (* each subexpression in instr that could be rewritten by the elim set is
198
	 rewritten *)
199
      let instr = eliminate m (IMap.map fst elim) instr in
200
      (* if instr is a simple local assign, then (a) elim is simplified with it (b) it
201
	 is stored as the elim set *)
202
      instr_unfold m fanin instrs elim instr
203
    ) (elim, []) instrs
204
  in elim, List.rev rev_instrs
205

    
206
and instr_unfold m fanin instrs (elim:(value_t * eq) IMap.t) instr =
207
(*  Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*)
208
  match get_instr_desc instr with
209
  (* Simple cases*)
210
  | MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
211
    -> instr_unfold m fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
212
  | MLocalAssign(v, expr) when not (is_clock_dec_type v.var_dec_type.ty_dec_desc) && unfoldable_assign fanin v expr
213
    -> (* we don't eliminate clock definitions *)
214
     let new_eq =
215
       Corelang.mkeq
216
         (desome instr.lustre_eq).eq_loc
217
         ([v.var_id], (desome instr.lustre_eq).eq_rhs)
218
     in
219
     (IMap.add v.var_id (expr, new_eq )  elim, instrs)
220
  | MBranch(g, hl) when false
221
    -> let elim_branches = List.map (fun (h, l) -> (h, instrs_unfold m fanin elim l)) hl in
222
       let (elim, branches) =
223
	 List.fold_right
224
	   (fun (h, (e, l)) (elim, branches) -> (merge_elim elim e, (h, l)::branches))
225
	   elim_branches (elim, [])
226
       in elim, ((update_instr_desc instr (MBranch (g, branches))) :: instrs)
227
  | _
228
    -> (elim, instr :: instrs)
229
    (* default case, we keep the instruction and do not modify elim *)
230
  
231

    
232
(** We iterate in the order, recording simple local assigns in an accumulator
233
    1. each expression is rewritten according to the accumulator
234
    2. local assigns then rewrite occurrences of the lhs in the computed accumulator
235
*)
236

    
237
let static_call_unfold elim (inst, (n, args)) =
238
  let replace v =
239
    try
240
      dimension_of_value (IMap.find v elim)
241
    with Not_found -> Dimension.mkdim_ident Location.dummy_loc v
242
  in (inst, (n, List.map (Dimension.expr_replace_expr replace) args))
243

    
244
(** Perform optimization on machine code:
245
    - iterate through step instructions and remove simple local assigns
246
    
247
*)
248
let machine_unfold fanin elim machine =
249
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "machine_unfold %s %a@." machine.mname.node_id (pp_elim machine) (IMap.map fst elim)); 
250
  let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
251
  let elim_vars, instrs = instrs_unfold machine fanin elim_consts machine.mstep.step_instrs in
252
  let instrs = simplify_instrs_offset machine instrs in
253
  let checks = List.map
254
                 (fun (loc, check) ->
255
                   loc,
256
                   eliminate_expr machine (IMap.map fst elim_vars) check
257
                 ) machine.mstep.step_checks
258
  in
259
  let locals = List.filter (fun v -> not (IMap.mem v.var_id elim_vars)) machine.mstep.step_locals in
260
  let elim_consts = IMap.map fst elim_consts in
261
  let minstances = List.map (static_call_unfold elim_consts) machine.minstances in
262
  let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls
263
  in
264
  {
265
    machine with
266
      mstep = { 
267
	machine.mstep with 
268
	  step_locals = locals;
269
	  step_instrs = instrs;
270
	  step_checks = checks
271
      };
272
      mconst = mconst;
273
      minstances = minstances;
274
      mcalls = mcalls;
275
  },
276
  elim_vars
277

    
278
let instr_of_const top_const =
279
  let const = const_of_top top_const in
280
  let loc = const.const_loc in
281
  let id = const.const_id in
282
  let vdecl = mkvar_decl loc (id, mktyp Location.dummy_loc Tydec_any, mkclock loc Ckdec_any, true, None, None) in
283
  let vdecl = { vdecl with var_type = const.const_type } in
284
  let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in
285
  mkinstr
286
    ~lustre_eq:lustre_eq 
287
    (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
288

    
289
(* We do not perform this optimization on contract nodes since there
290
   is not explicit dependence btw variables and their use in
291
   contracts. *)
292
let machines_unfold consts node_schs machines =
293
  List.fold_right (fun m (machines, removed) ->
294
      let is_contract = match m.mspec with Some (Contract _) -> true | _ -> false in
295
      if is_contract then
296
        m::machines, removed
297
      else 
298
        let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in
299
        let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in
300
        let (m, removed_m) =  machine_unfold fanin elim_consts m in
301
        (m::machines, IMap.add m.mname.node_id removed_m removed)
302
    )
303
    machines
304
    ([], IMap.empty)
305

    
306
let get_assign_lhs instr =
307
  match get_instr_desc instr with
308
  | MLocalAssign(v, e) -> mk_val (Var v) e.value_type
309
  | MStateAssign(v, e) -> mk_val (Var v) e.value_type
310
  | _                  -> assert false
311

    
312
let get_assign_rhs instr =
313
  match get_instr_desc instr with
314
  | MLocalAssign(_, e)
315
  | MStateAssign(_, e) -> e
316
  | _                  -> assert false
317

    
318
let is_assign instr =
319
  match get_instr_desc instr with
320
  | MLocalAssign _
321
  | MStateAssign _ -> true
322
  | _              -> false
323

    
324
let mk_assign m v e =
325
 match v.value_desc with
326
 | Var v -> if is_memory m v then MStateAssign(v, e) else MLocalAssign(v, e)
327
 | _          -> assert false
328

    
329
let rec assigns_instr instr assign =
330
  match get_instr_desc instr with  
331
  | MLocalAssign (i,_)
332
  | MStateAssign (i,_) -> VSet.add i assign
333
  | MStep (ol, _, _)   -> List.fold_right VSet.add ol assign
334
  | MBranch (_,hl)     -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
335
  | _                  -> assign
336

    
337
and assigns_instrs instrs assign =
338
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
339

    
340
(*    
341
and substitute_expr subst expr =
342
  match expr with
343
  | Var v -> (try IMap.find expr subst with Not_found -> expr)
344
  | Fun (id, vl) -> Fun (id, List.map (substitute_expr subst) vl)
345
  | Array(vl) -> Array(List.map (substitute_expr subst) vl)
346
  | Access(v1, v2) -> Access(substitute_expr subst v1, substitute_expr subst v2)
347
  | Power(v1, v2) -> Power(substitute_expr subst v1, substitute_expr subst v2)
348
  | Cst _  -> expr
349
*)
350
(** Finds a substitute for [instr] in [instrs], 
351
   i.e. another instr' with the same rhs expression.
352
   Then substitute this expression with the first assigned var
353
*)
354
let subst_instr m subst instrs instr =
355
  (* Format.eprintf "subst instr: %a@." (pp_instr m) instr; *)
356
  let instr = eliminate m subst instr in
357
  let instr_v = get_assign_lhs instr in  
358
  let instr_e = get_assign_rhs instr in
359
  try
360
    (* Searching for equivalent asssign *)
361
    let instr' = List.find (fun instr' -> is_assign instr' &&
362
                                            get_assign_rhs instr' = instr_e) instrs in
363
    (* Registering the instr_v as instr'_v while replacing *)
364
    match instr_v.value_desc with
365
    | Var v ->
366
       let instr'_v = get_assign_lhs instr' in
367
         if not (is_memory m v) then
368
         (* The current instruction defines a local variables, ie not
369
            memory, we can just record the relationship and continue
370
          *)
371
         IMap.add v.var_id instr'_v subst, instrs
372
       else  (
373
         (* The current instruction defines a memory. We need to keep
374
            the definition, simplified *)
375
         (match instr'_v.value_desc with
376
          | Var v' ->
377
             if not (is_memory m v') then
378
               (* We define v' = v. Don't need to update the records. *)
379
               let instr = eliminate m subst (update_instr_desc instr (mk_assign m instr_v instr'_v)) in
380
	       subst, instr :: instrs
381
             else ( (* Last case, v', the lhs of the previous similar
382
                       definition is, itself, a memory *)
383

    
384
               (* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *)
385
               (* Filtering out the list of instructions: 
386
                  - we copy in the same order the list of instr in instrs (fold_right)
387
                  - if the current instr is this instr' then apply 
388
                    the elimination with v' -> v on instr' before recording it as an instruction.  
389
                *)
390
               let subst_v' = IMap.add v'.var_id instr_v IMap.empty in
391
	       let instrs' =
392
                 snd
393
                   (List.fold_right
394
                      (fun instr (ok, instrs) ->
395
                        (ok || instr = instr',
396
                         if ok then
397
                           instr :: instrs
398
                         else
399
                           if instr = instr' then
400
                             instrs
401
                           else
402
                             eliminate m subst_v' instr :: instrs))
403
                      instrs (false, []))
404
               in
405
	       IMap.add v'.var_id instr_v subst, instr :: instrs'
406
             )
407
          | _           -> assert false)
408
       )
409
    | _          -> assert false
410
                  
411
  with Not_found ->
412
    (* No such equivalent expr: keeping the definition *)
413
    subst, instr :: instrs
414
                
415
(** Common sub-expression elimination for machine instructions *)
416
(* - [subst] : hashtable from ident to (simple) definition
417
               it is an equivalence table
418
   - [elim]   : set of eliminated variables
419
   - [instrs] : previous instructions, which [instr] is compared against
420
   - [instr] : current instruction, normalized by [subst]
421
*)
422
let rec instr_cse m (subst, instrs) instr =
423
  match get_instr_desc instr with
424
  (* Simple cases*)
425
  | MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
426
      -> instr_cse m (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
427
  | MLocalAssign(v, expr) when is_unfoldable_expr 2 expr
428
      -> (IMap.add v.var_id expr subst, instr :: instrs)
429
  | _ when is_assign instr
430
      -> subst_instr m subst instrs instr
431
  | _ -> (subst, instr :: instrs)
432

    
433
(** Apply common sub-expression elimination to a sequence of instrs
434
*)
435
let instrs_cse m subst instrs =
436
  let subst, rev_instrs = 
437
    List.fold_left (instr_cse m) (subst, []) instrs
438
  in subst, List.rev rev_instrs
439

    
440
(** Apply common sub-expression elimination to a machine
441
    - iterate through step instructions and remove simple local assigns
442
*)
443
let machine_cse subst machine =
444
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)
445
  let subst, instrs = instrs_cse machine subst machine.mstep.step_instrs in
446
  let assigned = assigns_instrs instrs VSet.empty
447
  in
448
  {
449
    machine with
450
      mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
451
      mstep = { 
452
	machine.mstep with 
453
	  step_locals = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mstep.step_locals;
454
	  step_instrs = instrs
455
      }
456
  }
457

    
458
let machines_cse machines =
459
  List.map
460
    (machine_cse IMap.empty)
461
    machines
462

    
463
(* variable substitution for optimizing purposes *)
464

    
465
(* checks whether an [instr] is skip and can be removed from program *)
466
let rec instr_is_skip instr =
467
  match get_instr_desc instr with
468
  | MLocalAssign (i, { value_desc = (Var v) ; _}) when i = v -> true
469
  | MStateAssign (i, { value_desc = Var v; _}) when i = v -> true
470
  | MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
471
  | _               -> false
472
and instrs_are_skip instrs =
473
  List.for_all instr_is_skip instrs
474

    
475
let instr_cons instr cont =
476
 if instr_is_skip instr then cont else instr::cont
477

    
478
let rec instr_remove_skip instr cont =
479
  match get_instr_desc instr with
480
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v -> cont
481
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v -> cont
482
  | MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont
483
  | _               -> instr::cont
484

    
485
and instrs_remove_skip instrs cont =
486
  List.fold_right instr_remove_skip instrs cont
487

    
488
let rec value_replace_var fvar value =
489
  match value.value_desc with
490
  | Cst c -> value
491
  | Var v -> { value with value_desc = Var (fvar v) }
492
  | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
493
  | Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
494
  | Access (t, i) -> { value with value_desc = Access(value_replace_var fvar t, i)}
495
  | Power (v, n) -> { value with value_desc = Power(value_replace_var fvar v, n)}
496

    
497
let rec instr_replace_var fvar instr cont =
498
  match get_instr_desc instr with
499
  | MSpec _ | MComment _          -> instr_cons instr cont
500
  | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
501
  | MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
502
  | MReset i            -> instr_cons instr cont
503
  | MNoReset i          -> instr_cons instr cont
504
  | MStep (il, i, vl)   -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont
505
  | 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
506

    
507
and instrs_replace_var fvar instrs cont =
508
  List.fold_right (instr_replace_var fvar) instrs cont
509

    
510
let step_replace_var fvar step =
511
  (* Some outputs may have been replaced by locals.
512
     We then need to rename those outputs
513
     without changing their clocks, etc *)
514
  let outputs' =
515
    List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs in
516
  let locals'  =
517
    List.fold_left (fun res l ->
518
      let l' = fvar l in
519
      if List.exists (fun o -> o.var_id = l'.var_id) outputs'
520
      then res
521
      else Utils.add_cons l' res)
522
      [] step.step_locals in
523
  { step with
524
    step_checks = List.map (fun (l, v) -> (l, value_replace_var fvar v)) step.step_checks;
525
    step_outputs = outputs';
526
    step_locals = locals';
527
    step_instrs = instrs_replace_var fvar step.step_instrs [];
528
}
529

    
530
let rec machine_replace_variables fvar m =
531
  { m with
532
    mstep = step_replace_var fvar m.mstep
533
  }
534

    
535
let machine_reuse_variables m reuse =
536
  let fvar v =
537
    try
538
      Hashtbl.find reuse v.var_id
539
    with Not_found -> v in
540
  machine_replace_variables fvar m
541

    
542
let machines_reuse_variables prog reuse_tables =
543
  List.map 
544
    (fun m -> 
545
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables)
546
    ) prog
547

    
548
let rec instr_assign res instr =
549
  match get_instr_desc instr with
550
  | MLocalAssign (i, _) -> Disjunction.CISet.add i res
551
  | MStateAssign (i, _) -> Disjunction.CISet.add i res
552
  | MBranch (g, hl)     -> List.fold_left (fun res (h, b) -> instrs_assign res b) res hl
553
  | MStep (il, _, _)    -> List.fold_right Disjunction.CISet.add il res
554
  | _                   -> res
555

    
556
and instrs_assign res instrs =
557
  List.fold_left instr_assign res instrs
558

    
559
let rec instr_constant_assign var instr =
560
  match get_instr_desc instr with
561
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
562
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var
563
  | MBranch (g, hl)                     -> List.for_all (fun (h, b) -> instrs_constant_assign var b) hl
564
  | _                                   -> false
565

    
566
and instrs_constant_assign var instrs =
567
  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
568

    
569
let rec instr_reduce branches instr1 cont =
570
  match get_instr_desc instr1 with
571
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
572
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
573
  | MBranch (g, hl)                     -> (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl))) :: cont
574
  | _                                   -> instr1 :: cont
575

    
576
and instrs_reduce branches instrs cont =
577
 match instrs with
578
 | []        -> cont
579
 | [i]       -> instr_reduce branches i cont
580
 | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont
581

    
582
let rec instrs_fusion instrs =
583
  match instrs, List.map get_instr_desc instrs with
584
  | [], []
585
  | [_], [_]                                                               ->
586
    instrs
587
  | i1::i2::q, i1_desc::(MBranch ({ value_desc = Var v; _}, hl))::q_desc when instr_constant_assign v i1 ->
588
    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)
589
  | i1::i2::q, _                                                         ->
590
    i1 :: instrs_fusion (i2::q)
591
  | _ -> assert false (* Other cases should not happen since both lists are of same size *)
592
     
593
let step_fusion step =
594
  { step with
595
    step_instrs = instrs_fusion step.step_instrs;
596
  }
597

    
598
let rec machine_fusion m =
599
  { m with
600
    mstep = step_fusion m.mstep
601
  }
602

    
603
let machines_fusion prog =
604
  List.map machine_fusion prog
605

    
606

    
607
(* Additional function to modify the prog according to removed variables map *)
608

    
609
let elim_prog_variables prog removed_table =
610
  List.map (
611
      fun t ->
612
      match t.top_decl_desc with
613
        Node nd ->
614
         if IMap.mem nd.node_id removed_table then
615
           let nd_elim_map = IMap.find nd.node_id removed_table in
616
           (* Iterating through the elim map to compute
617
              - the list of variables to remove
618
              - the associated list of lustre definitions x = expr to
619
                be used when removing these variables *)
620
           let vars_to_replace, defs = (* Recovering vid from node locals *)
621
             IMap.fold (fun v (_,eq) (accu_locals, accu_defs) ->
622
                 let locals =
623
                   try
624
                     (List.find (fun v' -> v'.var_id = v) nd.node_locals)::accu_locals
625
                   with Not_found -> accu_locals (* Variable v shall
626
                                                    be a global
627
                                                    constant, we do no
628
                                                    need to eliminate
629
                                                    it from the locals
630
                                                    *)
631
                 in
632
                 (* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc = e.expr_loc } in *)
633
                 let defs = eq::accu_defs in
634
                 locals, defs
635
               ) nd_elim_map ([], [])
636
           in
637
            
638
           let new_locals, new_stmts =
639
             List.fold_right (fun stmt (locals, res_stmts) ->
640
                 match stmt with
641
                   Aut _ -> assert false (* should be processed by now *)
642
                 | Eq eq -> (
643
                   match eq.eq_lhs with
644
                   | [] -> assert false (* shall not happen *)
645
                   | _::_::_ ->
646
                      (* When more than one lhs we just keep the
647
                         equation and do not delete it *)
648
                      let eq_rhs' = substitute_expr vars_to_replace defs eq.eq_rhs in
649
                      locals, (Eq { eq with eq_rhs = eq_rhs' })::res_stmts
650
                   | [lhs] -> 
651
                      if List.exists (fun v -> v.var_id = lhs) vars_to_replace then 
652
                        (* We remove the def *)
653
                        List.filter (fun l -> l.var_id != lhs) locals,
654
                        res_stmts
655
                      else (* We keep it but modify any use of an eliminatend var *)
656
                        let eq_rhs' = substitute_expr vars_to_replace defs eq.eq_rhs in 
657
                        locals,
658
                        (Eq { eq with eq_rhs = eq_rhs' })::res_stmts
659
                        
660
                 )
661
               ) nd.node_stmts (nd.node_locals,[])
662
           in
663
           let nd' = { nd with
664
                       node_locals = new_locals;
665
                       node_stmts = new_stmts;
666
                     }
667
           in
668
           { t with top_decl_desc = Node nd' }
669
         else
670
           t
671
      | _ -> t
672
    ) prog
673

    
674
(*** Main function ***)
675

    
676
(* 
677
This functions produces an optimzed prog * machines
678
It 
679
1- eliminates common sub-expressions (TODO how is this different from normalization?)
680
2- inline constants and eliminate duplicated variables 
681
3- try to reuse variables whenever possible
682

    
683
When item (2) identified eliminated variables, the initial prog is modified, its normalized recomputed, as well as its scheduling, before regenerating the machines.
684

    
685
The function returns both the (possibly updated) prog as well as the machines 
686

    
687

    
688
*)
689
let optimize params prog node_schs machine_code =
690
  let machine_code =
691
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
692
      begin
693
	Log.report ~level:1 
694
	  (fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,");
695
	let machine_code = machines_cse machine_code in
696
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "pp_machines machine_code);
697
	machine_code
698
      end
699
    else
700
      machine_code
701
  in
702
  (* Optimize machine code *)
703
  let prog, machine_code, removed_table = 
704
    if !Options.optimization >= 2
705
       && !Options.output <> "emf" (*&& !Options.output <> "horn"*)
706
    then
707
      begin
708
	Log.report ~level:1
709
          (fun fmt ->
710
            Format.fprintf fmt 
711
	      ".. machines optimization: const. inlining (partial eval. with const)@,");
712
	let machine_code, removed_table =
713
          machines_unfold (Corelang.get_consts prog) node_schs machine_code in
714
  Log.report ~level:3
715
          (fun fmt ->
716
            Format.fprintf fmt "\t@[Eliminated flows: @[%a@]@]@ "
717
	      (pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m))) removed_table); 
718
	Log.report ~level:3
719
          (fun fmt ->
720
            Format.fprintf fmt
721
              ".. generated machines (const inlining):@ %a@ "
722
              pp_machines machine_code);
723
        (* If variables were eliminated, relaunch the
724
           normalization/machine generation *)
725
        if IMap.is_empty removed_table then
726
	  (* stopping here, no need to reupdate the prog *)
727
          prog, machine_code, removed_table
728
        else (
729
          let prog = elim_prog_variables prog removed_table in
730
          (* Mini stage1 *)
731
          let prog = Normalization.normalize_prog params prog in
732
          let prog = SortProg.sort_nodes_locals prog in
733
          (* Mini stage2: note that we do not protect against
734
             alg. loop since this should have been handled before *)
735
          let prog, node_schs = Scheduling.schedule_prog prog in
736
          let machine_code = Machine_code.translate_prog prog node_schs in
737
	  (* Mini stage2 machine optimiation *)
738
          let machine_code, removed_table =
739
            machines_unfold (Corelang.get_consts prog) node_schs machine_code in
740
	  prog, machine_code, removed_table
741
        )
742

    
743
      end
744
    else
745
      prog, machine_code, IMap.empty
746
  in  
747
  (* Optimize machine code *)
748
  let machine_code =
749
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then
750
      begin
751
	Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
752
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
753
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
754
	machines_fusion (machines_reuse_variables machine_code reuse_tables)
755
      end
756
    else
757
      machine_code
758
  in
759
  
760

    
761
  prog, List.rev machine_code  
762
          
763
          
764
                 (* Local Variables: *)
765
                 (* compile-command:"make -C .." *)
766
                 (* End: *)