Project

General

Profile

Download (31.9 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
module Mpfr = Lustrec_mpfr
20

    
21

    
22
let pp_elim m fmt elim =
23
  pp_imap ~comment:"/* elim table: */" (pp_val m) fmt elim
24
  (* Format.fprintf fmt "@[<hv 0>@[<hv 2>{ /* elim table: */";
25
   * IMap.iter (fun v expr -> Format.fprintf fmt "@ %s |-> %a," v (pp_val m) expr) elim;
26
   * Format.fprintf fmt "@]@ }@]" *)
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
  | MLocalAssign (i,v) -> update_instr_desc instr (MLocalAssign (i, e_expr v))
32
  | MStateAssign (i,v) -> update_instr_desc instr (MStateAssign (i, e_expr v))
33
  | MSetReset _
34
  | MNoReset _
35
  | MClearReset
36
  | MSpec _
37
  | MComment _         -> instr
38
  | MStep (il, i, vl)  -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
39
  | MBranch (g,hl)     -> 
40
     update_instr_desc instr (
41
       MBranch
42
	 (e_expr g, 
43
	  (List.map 
44
	     (fun (l, il) -> l, List.map (eliminate m elim) il) 
45
	     hl
46
	  )
47
	 )
48
     )
49
    
50
and eliminate_expr m elim expr =
51
  let eliminate_expr = eliminate_expr m in
52
  match expr.value_desc with
53
  | Var v -> if is_memory m v then
54
               expr
55
             else
56
               (try IMap.find v.var_id elim with Not_found -> expr)
57
  | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
58
  | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
59
  | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
60
  | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
61
  | Cst _ -> expr
62

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

    
70

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

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

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

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

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

    
131
and simplify_instrs_offset m instrs =
132
  List.map (simplify_instr_offset m) instrs
133

    
134
let is_scalar_const c =
135
  match c with
136
  | Const_real _
137
  | Const_int _
138
  | Const_tag _   -> true
139
  | _             -> false
140

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

    
175
let basic_unfoldable_assign fanin v expr =
176
  try
177
    let d = Hashtbl.find fanin v.var_id
178
    in is_unfoldable_expr d expr
179
  with Not_found -> false
180

    
181
let unfoldable_assign fanin v expr =
182
   (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
183
&& basic_unfoldable_assign fanin v expr
184

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

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

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

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

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

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

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

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

    
312
let get_assign_lhs instr =
313
  match get_instr_desc instr with
314
  | MLocalAssign(v, e) -> mk_val (Var v) e.value_type
315
  | MStateAssign(v, e) -> mk_val (Var v) e.value_type
316
  | _                  -> assert false
317

    
318
let get_assign_rhs instr =
319
  match get_instr_desc instr with
320
  | MLocalAssign(_, e)
321
  | MStateAssign(_, e) -> e
322
  | _                  -> assert false
323

    
324
let is_assign instr =
325
  match get_instr_desc instr with
326
  | MLocalAssign _
327
  | MStateAssign _ -> true
328
  | _              -> false
329

    
330
let mk_assign m v e =
331
 match v.value_desc with
332
 | Var v -> if is_memory m v then MStateAssign(v, e) else MLocalAssign(v, e)
333
 | _          -> assert false
334

    
335
let rec assigns_instr instr assign =
336
  match get_instr_desc instr with  
337
  | MLocalAssign (i,_)
338
  | MStateAssign (i,_) -> VSet.add i assign
339
  | MStep (ol, _, _)   -> List.fold_right VSet.add ol assign
340
  | MBranch (_,hl)     -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
341
  | _                  -> assign
342

    
343
and assigns_instrs instrs assign =
344
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
345

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

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

    
439
(** Apply common sub-expression elimination to a sequence of instrs
440
*)
441
let instrs_cse m subst instrs =
442
  let subst, rev_instrs = 
443
    List.fold_left (instr_cse m) (subst, []) instrs
444
  in subst, List.rev rev_instrs
445

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

    
464
let machines_cse machines =
465
  List.map
466
    (machine_cse IMap.empty)
467
    machines
468

    
469
(* variable substitution for optimizing purposes *)
470

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

    
481
let instr_cons instr cont =
482
 if instr_is_skip instr then cont else instr::cont
483

    
484
let rec instr_remove_skip instr cont =
485
  match get_instr_desc instr with
486
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v -> cont
487
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v -> cont
488
  | MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont
489
  | _               -> instr::cont
490

    
491
and instrs_remove_skip instrs cont =
492
  List.fold_right instr_remove_skip instrs cont
493

    
494
let rec value_replace_var fvar value =
495
  match value.value_desc with
496
  | Cst _ -> value
497
  | Var v -> { value with value_desc = Var (fvar v) }
498
  | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
499
  | Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
500
  | Access (t, i) -> { value with value_desc = Access(value_replace_var fvar t, i)}
501
  | Power (v, n) -> { value with value_desc = Power(value_replace_var fvar v, n)}
502

    
503
let rec instr_replace_var fvar instr cont =
504
  match get_instr_desc instr with
505
  | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
506
  | MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
507
  | MSetReset _
508
  | MNoReset _
509
  | MClearReset
510
  | MSpec _
511
  | MComment _          -> instr_cons instr cont
512
  | MStep (il, i, vl)   -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont
513
  | 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
514

    
515
and instrs_replace_var fvar instrs cont =
516
  List.fold_right (instr_replace_var fvar) instrs cont
517

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

    
538
let machine_replace_variables fvar m =
539
  { m with
540
    mstep = step_replace_var fvar m.mstep
541
  }
542

    
543
let machine_reuse_variables m reuse =
544
  let fvar v =
545
    try
546
      Hashtbl.find reuse v.var_id
547
    with Not_found -> v in
548
  machine_replace_variables fvar m
549

    
550
let machines_reuse_variables prog reuse_tables =
551
  List.map 
552
    (fun m -> 
553
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables)
554
    ) prog
555

    
556
let rec instr_assign res instr =
557
  match get_instr_desc instr with
558
  | MLocalAssign (i, _) -> Disjunction.CISet.add i res
559
  | MStateAssign (i, _) -> Disjunction.CISet.add i res
560
  | MBranch (_, hl)     -> List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
561
  | MStep (il, _, _)    -> List.fold_right Disjunction.CISet.add il res
562
  | _                   -> res
563

    
564
and instrs_assign res instrs =
565
  List.fold_left instr_assign res instrs
566

    
567
let rec instr_constant_assign var instr =
568
  match get_instr_desc instr with
569
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
570
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var
571
  | MBranch (_, hl)                     -> List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
572
  | _                                   -> false
573

    
574
and instrs_constant_assign var instrs =
575
  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
576

    
577
let rec instr_reduce branches instr1 cont =
578
  match get_instr_desc instr1 with
579
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
580
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
581
  | MBranch (g, hl)                     -> (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl))) :: cont
582
  | _                                   -> instr1 :: cont
583

    
584
and instrs_reduce branches instrs cont =
585
 match instrs with
586
 | []        -> cont
587
 | [i]       -> instr_reduce branches i cont
588
 | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont
589

    
590
let rec instrs_fusion instrs =
591
  match instrs, List.map get_instr_desc instrs with
592
  | [], []
593
  | [_], [_]                                                               ->
594
    instrs
595
  | i1::_::q, _::(MBranch ({ value_desc = Var v; _}, hl))::_ when instr_constant_assign v i1 ->
596
    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)
597
  | i1::i2::q, _                                                         ->
598
    i1 :: instrs_fusion (i2::q)
599
  | _ -> assert false (* Other cases should not happen since both lists are of same size *)
600
     
601
let step_fusion step =
602
  { step with
603
    step_instrs = instrs_fusion step.step_instrs;
604
  }
605

    
606
let machine_fusion m =
607
  { m with
608
    mstep = step_fusion m.mstep
609
  }
610

    
611
let machines_fusion prog =
612
  List.map machine_fusion prog
613

    
614

    
615
(* Additional function to modify the prog according to removed variables map *)
616

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

    
682
(*** Main function ***)
683

    
684
(* 
685
This functions produces an optimzed prog * machines
686
It 
687
1- eliminates common sub-expressions (TODO how is this different from normalization?)
688
2- inline constants and eliminate duplicated variables 
689
3- try to reuse variables whenever possible
690

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

    
693
The function returns both the (possibly updated) prog as well as the machines 
694

    
695

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

    
754
    end else
755
      prog, machine_code, IMap.empty
756
  in  
757
  (* Optimize machine code *)
758
  let machine_code =
759
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then
760
      begin
761
        Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
762
        let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
763
        let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
764
        machines_fusion (machines_reuse_variables machine_code reuse_tables)
765
      end
766
    else
767
      machine_code
768
  in
769

    
770

    
771
  prog, machine_code
772

    
773
          
774
                 (* Local Variables: *)
775
                 (* compile-command:"make -C .." *)
776
                 (* End: *)
(45-45/66)