Project

General

Profile

Download (32 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
  | 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 _           -> instr
35
  | MNoReset _         -> 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 _ -> 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 _ ::_ , _                -> 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 _               -> instr
119
  | MNoReset _             -> 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 _ :: 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 (_, 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 _ 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@ "
249
                          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.mnode_spec with
295
        | Some (Contract _) -> true
296
        | _ -> false in
297
      if is_contract then
298
        m :: machines, removed
299
      else 
300
        let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in
301
        let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in
302
        let (m, removed_m) =  machine_unfold fanin elim_consts m in
303
        (m::machines, IMap.add m.mname.node_id removed_m removed)
304
    )
305
    machines
306
    ([], IMap.empty)
307

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

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

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

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

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

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

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

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

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

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

    
460
let machines_cse machines =
461
  List.map
462
    (machine_cse IMap.empty)
463
    machines
464

    
465
(* variable substitution for optimizing purposes *)
466

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

    
477
let instr_cons instr cont =
478
 if instr_is_skip instr then cont else instr::cont
479

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

    
487
and instrs_remove_skip instrs cont =
488
  List.fold_right instr_remove_skip instrs cont
489

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

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

    
509
and instrs_replace_var fvar instrs cont =
510
  List.fold_right (instr_replace_var fvar) instrs cont
511

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

    
532
let machine_replace_variables fvar m =
533
  { m with
534
    mstep = step_replace_var fvar m.mstep
535
  }
536

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

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

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

    
558
and instrs_assign res instrs =
559
  List.fold_left instr_assign res instrs
560

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

    
568
and instrs_constant_assign var instrs =
569
  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
570

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

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

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

    
600
let machine_fusion m =
601
  { m with
602
    mstep = step_fusion m.mstep
603
  }
604

    
605
let machines_fusion prog =
606
  List.map machine_fusion prog
607

    
608

    
609
(* Additional function to modify the prog according to removed variables map *)
610

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

    
676
(*** Main function ***)
677

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

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

    
687
The function returns both the (possibly updated) prog as well as the machines 
688

    
689

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

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

    
764

    
765
  prog, List.rev machine_code  
766

    
767
          
768
                 (* Local Variables: *)
769
                 (* compile-command:"make -C .." *)
770
                 (* End: *)
(44-44/63)