Project

General

Profile

Download (31.6 KB) Statistics
| Branch: | Tag: | Revision:
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
  | MSpec _ | 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
52
               expr
53
             else
54
               (try IMap.find v.var_id elim with Not_found -> expr)
55
  | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
56
  | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
57
  | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
58
  | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
59
  | Cst _ -> expr
60

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

    
68

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
462
(* variable substitution for optimizing purposes *)
463

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
605

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

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

    
673
(*** Main function ***)
674

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

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

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

    
686

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

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

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