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
  | 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
  | MResetAssign _
37
  | MSpec _
38
  | MComment _         -> instr
39
  | MStep (il, i, vl)  -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
40
  | MBranch (g,hl)     -> 
41
     update_instr_desc instr (
42
       MBranch
43
	 (e_expr g, 
44
	  (List.map 
45
	     (fun (l, il) -> l, List.map (eliminate m elim) il) 
46
	     hl
47
	  )
48
	 )
49
     )
50
    
51
and eliminate_expr m elim expr =
52
  let eliminate_expr = eliminate_expr m in
53
  match expr.value_desc with
54
  | Var v -> if is_memory m v then
55
               expr
56
             else
57
               (try IMap.find v.var_id elim with Not_found -> expr)
58
  | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
59
  | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
60
  | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
61
  | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
62
  | Cst _ | ResetFlag -> expr
63

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

    
71

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

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

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

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

    
122
let rec simplify_instr_offset m instr =
123
  match get_instr_desc instr with
124
  | MLocalAssign (v, expr) -> update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
125
  | MStateAssign (v, expr) -> update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
126
  | MSetReset _
127
  | MNoReset _
128
  | MClearReset
129
  | MResetAssign _
130
  | MSpec _
131
  | MComment _             -> instr
132
  | MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
133
  | MBranch (cond, brl)
134
    -> update_instr_desc instr (
135
      MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
136
    )
137

    
138
and simplify_instrs_offset m instrs =
139
  List.map (simplify_instr_offset m) instrs
140

    
141
let is_scalar_const c =
142
  match c with
143
  | Const_real _
144
  | Const_int _
145
  | Const_tag _   -> true
146
  | _             -> false
147

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

    
182
let basic_unfoldable_assign fanin v expr =
183
  try
184
    let d = Hashtbl.find fanin v.var_id
185
    in is_unfoldable_expr d expr
186
  with Not_found -> false
187

    
188
let unfoldable_assign fanin v expr =
189
   (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
190
&& basic_unfoldable_assign fanin v expr
191

    
192
let merge_elim elim1 elim2 =
193
  let merge _ e1 e2 =
194
    match e1, e2 with
195
    | Some e1, Some e2 -> if e1 = e2 then Some e1 else None
196
    | _      , Some e2 -> Some e2
197
    | Some e1, _       -> Some e1
198
    | _                -> None
199
  in IMap.merge merge elim1 elim2
200

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

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

    
242
(** We iterate in the order, recording simple local assigns in an accumulator
243
    1. each expression is rewritten according to the accumulator
244
    2. local assigns then rewrite occurrences of the lhs in the computed accumulator
245
*)
246

    
247
let static_call_unfold elim (inst, (n, args)) =
248
  let replace v =
249
    try
250
      dimension_of_value (IMap.find v elim)
251
    with Not_found -> Dimension.mkdim_ident Location.dummy_loc v
252
  in (inst, (n, List.map (Dimension.expr_replace_expr replace) args))
253

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

    
289
let instr_of_const top_const =
290
  let const = const_of_top top_const in
291
  let loc = const.const_loc in
292
  let id = const.const_id in
293
  let vdecl = mkvar_decl loc (id, mktyp Location.dummy_loc Tydec_any, mkclock loc Ckdec_any, true, None, None) in
294
  let vdecl = { vdecl with var_type = const.const_type } in
295
  let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in
296
  mkinstr
297
    ~lustre_eq
298
    (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
299

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

    
319
let get_assign_lhs instr =
320
  match get_instr_desc instr with
321
  | MLocalAssign(v, e) -> mk_val (Var v) e.value_type
322
  | MStateAssign(v, e) -> mk_val (Var v) e.value_type
323
  | _                  -> assert false
324

    
325
let get_assign_rhs instr =
326
  match get_instr_desc instr with
327
  | MLocalAssign(_, e)
328
  | MStateAssign(_, e) -> e
329
  | _                  -> assert false
330

    
331
let is_assign instr =
332
  match get_instr_desc instr with
333
  | MLocalAssign _
334
  | MStateAssign _ -> true
335
  | _              -> false
336

    
337
let mk_assign m v e =
338
 match v.value_desc with
339
 | Var v -> if is_memory m v then MStateAssign(v, e) else MLocalAssign(v, e)
340
 | _          -> assert false
341

    
342
let rec assigns_instr instr assign =
343
  match get_instr_desc instr with  
344
  | MLocalAssign (i,_)
345
  | MStateAssign (i,_) -> VSet.add i assign
346
  | MStep (ol, _, _)   -> List.fold_right VSet.add ol assign
347
  | MBranch (_,hl)     -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
348
  | _                  -> assign
349

    
350
and assigns_instrs instrs assign =
351
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
352

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

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

    
446
(** Apply common sub-expression elimination to a sequence of instrs
447
*)
448
let instrs_cse m subst instrs =
449
  let subst, rev_instrs = 
450
    List.fold_left (instr_cse m) (subst, []) instrs
451
  in subst, List.rev rev_instrs
452

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

    
471
let machines_cse machines =
472
  List.map
473
    (machine_cse IMap.empty)
474
    machines
475

    
476
(* variable substitution for optimizing purposes *)
477

    
478
(* checks whether an [instr] is skip and can be removed from program *)
479
let rec instr_is_skip instr =
480
  match get_instr_desc instr with
481
  | MLocalAssign (i, { value_desc = (Var v) ; _}) when i = v -> true
482
  | MStateAssign (i, { value_desc = Var v; _}) when i = v -> true
483
  | MBranch (_, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
484
  | _               -> false
485
and instrs_are_skip instrs =
486
  List.for_all instr_is_skip instrs
487

    
488
let instr_cons instr cont =
489
 if instr_is_skip instr then cont else instr::cont
490

    
491
let rec instr_remove_skip instr cont =
492
  match get_instr_desc instr with
493
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v -> cont
494
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v -> cont
495
  | MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont
496
  | _               -> instr::cont
497

    
498
and instrs_remove_skip instrs cont =
499
  List.fold_right instr_remove_skip instrs cont
500

    
501
let rec value_replace_var fvar value =
502
  match value.value_desc with
503
  | Cst _ | ResetFlag -> value
504
  | Var v -> { value with value_desc = Var (fvar v) }
505
  | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
506
  | Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
507
  | Access (t, i) -> { value with value_desc = Access(value_replace_var fvar t, i)}
508
  | Power (v, n) -> { value with value_desc = Power(value_replace_var fvar v, n)}
509

    
510
let rec instr_replace_var fvar instr cont =
511
  match get_instr_desc instr with
512
  | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
513
  | MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
514
  | MSetReset _
515
  | MNoReset _
516
  | MClearReset
517
  | MResetAssign _
518
  | MSpec _
519
  | MComment _          -> instr_cons instr cont
520
  | MStep (il, i, vl)   -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont
521
  | 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
522

    
523
and instrs_replace_var fvar instrs cont =
524
  List.fold_right (instr_replace_var fvar) instrs cont
525

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

    
546
let machine_replace_variables fvar m =
547
  { m with
548
    mstep = step_replace_var fvar m.mstep
549
  }
550

    
551
let machine_reuse_variables m reuse =
552
  let fvar v =
553
    try
554
      Hashtbl.find reuse v.var_id
555
    with Not_found -> v in
556
  machine_replace_variables fvar m
557

    
558
let machines_reuse_variables prog reuse_tables =
559
  List.map 
560
    (fun m -> 
561
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables)
562
    ) prog
563

    
564
let rec instr_assign res instr =
565
  match get_instr_desc instr with
566
  | MLocalAssign (i, _) -> Disjunction.CISet.add i res
567
  | MStateAssign (i, _) -> Disjunction.CISet.add i res
568
  | MBranch (_, hl)     -> List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
569
  | MStep (il, _, _)    -> List.fold_right Disjunction.CISet.add il res
570
  | _                   -> res
571

    
572
and instrs_assign res instrs =
573
  List.fold_left instr_assign res instrs
574

    
575
let rec instr_constant_assign var instr =
576
  match get_instr_desc instr with
577
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
578
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var
579
  | MBranch (_, hl)                     -> List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
580
  | _                                   -> false
581

    
582
and instrs_constant_assign var instrs =
583
  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
584

    
585
let rec instr_reduce branches instr1 cont =
586
  match get_instr_desc instr1 with
587
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
588
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
589
  | MBranch (g, hl)                     -> (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl))) :: cont
590
  | _                                   -> instr1 :: cont
591

    
592
and instrs_reduce branches instrs cont =
593
 match instrs with
594
 | []        -> cont
595
 | [i]       -> instr_reduce branches i cont
596
 | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont
597

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

    
614
let machine_fusion m =
615
  { m with
616
    mstep = step_fusion m.mstep
617
  }
618

    
619
let machines_fusion prog =
620
  List.map machine_fusion prog
621

    
622

    
623
(* Additional function to modify the prog according to removed variables map *)
624

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

    
690
(*** Main function ***)
691

    
692
(* 
693
This functions produces an optimzed prog * machines
694
It 
695
1- eliminates common sub-expressions (TODO how is this different from normalization?)
696
2- inline constants and eliminate duplicated variables 
697
3- try to reuse variables whenever possible
698

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

    
701
The function returns both the (possibly updated) prog as well as the machines 
702

    
703

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

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

    
778

    
779
  prog, machine_code
780

    
781
          
782
                 (* Local Variables: *)
783
                 (* compile-command:"make -C .." *)
784
                 (* End: *)
(45-45/66)