Project

General

Profile

Download (31.1 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
let pp_elim m fmt elim =
22
  pp_imap ~comment:"/* elim table: */" (pp_val m) fmt elim
23
(* Format.fprintf fmt "@[<hv 0>@[<hv 2>{ /* elim table: */";
24
 * IMap.iter (fun v expr -> Format.fprintf fmt "@ %s |-> %a," v (pp_val m) expr) elim;
25
 * Format.fprintf fmt "@]@ }@]" *)
26

    
27
let rec eliminate m elim instr =
28
  let e_expr = eliminate_expr m elim in
29
  match get_instr_desc instr with
30
  | MLocalAssign (i, v) ->
31
    update_instr_desc instr (MLocalAssign (i, e_expr v))
32
  | MStateAssign (i, v) ->
33
    update_instr_desc instr (MStateAssign (i, e_expr v))
34
  | MSetReset _
35
  | MNoReset _
36
  | MClearReset
37
  | MResetAssign _
38
  | MSpec _
39
  | MComment _ ->
40
    instr
41
  | MStep (il, i, vl) ->
42
    update_instr_desc instr (MStep (il, i, List.map e_expr vl))
43
  | MBranch (g, hl) ->
44
    update_instr_desc instr
45
      (MBranch
46
         ( e_expr g,
47
           List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl ))
48

    
49
and eliminate_expr m elim expr =
50
  let eliminate_expr = eliminate_expr m in
51
  match expr.value_desc with
52
  | Var v -> (
53
    if is_memory m v then expr
54
    else try IMap.find v.var_id elim with Not_found -> expr)
55
  | Fun (id, vl) ->
56
    { expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl) }
57
  | Array vl ->
58
    { expr with value_desc = Array (List.map (eliminate_expr elim) vl) }
59
  | Access (v1, v2) ->
60
    {
61
      expr with
62
      value_desc = Access (eliminate_expr elim v1, eliminate_expr elim v2);
63
    }
64
  | Power (v1, v2) ->
65
    {
66
      expr with
67
      value_desc = Power (eliminate_expr elim v1, eliminate_expr elim v2);
68
    }
69
  | Cst _ | ResetFlag ->
70
    expr
71

    
72
let eliminate_dim elim dim =
73
  Dimension.expr_replace_expr
74
    (fun v ->
75
      try dimension_of_value (IMap.find v elim)
76
      with Not_found -> mkdim_ident dim.dim_loc v)
77
    dim
78

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

    
82
let unfold_expr_offset m offset expr =
83
  List.fold_left
84
    (fun res -> function
85
      | Index i ->
86
        mk_val
87
          (Access (res, value_of_dimension m i))
88
          (Types.array_element_type res.value_type)
89
      | Field _ ->
90
        Format.eprintf "internal error: not yet implemented !";
91
        assert false)
92
    expr offset
93

    
94
let rec simplify_cst_expr m offset typ cst =
95
  match offset, cst with
96
  | [], _ ->
97
    mk_val (Cst cst) typ
98
  | Index i :: q, Const_array cl when Dimension.is_dimension_const i ->
99
    let elt_typ = Types.array_element_type typ in
100
    simplify_cst_expr m q elt_typ
101
      (List.nth cl (Dimension.size_const_dimension i))
102
  | Index i :: q, Const_array cl ->
103
    let elt_typ = Types.array_element_type typ in
104
    unfold_expr_offset m [ Index i ]
105
      (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
106
  | Field f :: q, Const_struct fl ->
107
    let fld_typ = Types.struct_field_type typ f in
108
    simplify_cst_expr m q fld_typ (List.assoc f fl)
109
  | _ ->
110
    Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@."
111
      Printers.pp_const cst;
112
    assert false
113

    
114
let simplify_expr_offset m expr =
115
  let rec simplify offset expr =
116
    match offset, expr.value_desc with
117
    | Field _ :: _, _ ->
118
      failwith "not yet implemented"
119
    | _, Fun (id, vl) when Basic_library.is_value_internal_fun expr ->
120
      mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
121
    | _, Fun _ | _, Var _ ->
122
      unfold_expr_offset m offset expr
123
    | _, Cst cst ->
124
      simplify_cst_expr m offset expr.value_type cst
125
    | _, Access (expr, i) ->
126
      simplify (Index (dimension_of_value i) :: offset) expr
127
    | _, ResetFlag ->
128
      expr
129
    | [], _ ->
130
      expr
131
    | Index _ :: q, Power (expr, _) ->
132
      simplify q expr
133
    | Index i :: q, Array vl when Dimension.is_dimension_const i ->
134
      simplify q (List.nth vl (Dimension.size_const_dimension i))
135
    | Index i :: q, Array vl ->
136
      unfold_expr_offset m [ Index i ]
137
        (mk_val (Array (List.map (simplify q) vl)) expr.value_type)
138
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr
139
      (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
140
      with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr
141
      (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
142
  in
143
  simplify [] expr
144

    
145
let rec simplify_instr_offset m instr =
146
  match get_instr_desc instr with
147
  | MLocalAssign (v, expr) ->
148
    update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
149
  | MStateAssign (v, expr) ->
150
    update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
151
  | MSetReset _
152
  | MNoReset _
153
  | MClearReset
154
  | MResetAssign _
155
  | MSpec _
156
  | MComment _ ->
157
    instr
158
  | MStep (outputs, id, inputs) ->
159
    update_instr_desc instr
160
      (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
161
  | MBranch (cond, brl) ->
162
    update_instr_desc instr
163
      (MBranch
164
         ( simplify_expr_offset m cond,
165
           List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl ))
166

    
167
and simplify_instrs_offset m instrs = List.map (simplify_instr_offset m) instrs
168

    
169
let is_scalar_const c =
170
  match c with Const_real _ | Const_int _ | Const_tag _ -> true | _ -> false
171

    
172
(* An instruction v = expr may (and will) be unfolded iff: - either expr is
173
   atomic (no complex expressions, only const, vars and array/struct accesses) -
174
   or v has a fanin <= 1 (used at most once) *)
175
let is_unfoldable_expr fanin expr =
176
  let rec unfold_const offset cst =
177
    match offset, cst with
178
    | _, Const_int _ | _, Const_real _ | _, Const_tag _ ->
179
      true
180
    | Field f :: q, Const_struct fl ->
181
      unfold_const q (List.assoc f fl)
182
    | [], Const_struct _ ->
183
      false
184
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i ->
185
      unfold_const q (List.nth cl (Dimension.size_const_dimension i))
186
    | _, Const_array _ ->
187
      false
188
    | _ ->
189
      assert false
190
  in
191
  let rec unfold offset expr =
192
    match offset, expr.value_desc with
193
    | _, Cst cst ->
194
      unfold_const offset cst
195
    | _, Var _ ->
196
      true
197
    | [], Power _ | [], Array _ ->
198
      false
199
    | Index _ :: q, Power (v, _) ->
200
      unfold q v
201
    | Index i :: q, Array vl when Dimension.is_dimension_const i ->
202
      unfold q (List.nth vl (Dimension.size_const_dimension i))
203
    | _, Array _ ->
204
      false
205
    | _, Access (v, i) ->
206
      unfold (Index (dimension_of_value i) :: offset) v
207
    | _, Fun (_, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
208
      ->
209
      List.for_all (unfold offset) vl
210
    | _, Fun _ ->
211
      false
212
    | _ ->
213
      assert false
214
  in
215
  unfold [] expr
216

    
217
let basic_unfoldable_assign fanin v expr =
218
  try
219
    let d = Hashtbl.find fanin v.var_id in
220
    is_unfoldable_expr d expr
221
  with Not_found -> false
222

    
223
let unfoldable_assign fanin v expr =
224
  (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
225
  && basic_unfoldable_assign fanin v expr
226

    
227
let merge_elim elim1 elim2 =
228
  let merge _ e1 e2 =
229
    match e1, e2 with
230
    | Some e1, Some e2 ->
231
      if e1 = e2 then Some e1 else None
232
    | _, Some e2 ->
233
      Some e2
234
    | Some e1, _ ->
235
      Some e1
236
    | _ ->
237
      None
238
  in
239
  IMap.merge merge elim1 elim2
240

    
241
(* see if elim has to take in account the provided instr: if so, update elim and
242
   return the remove flag, otherwise, the expression should be kept and elim is
243
   left untouched *)
244
let rec instrs_unfold m fanin elim instrs =
245
  let elim, rev_instrs =
246
    List.fold_left
247
      (fun (elim, instrs) instr ->
248
        (* each subexpression in instr that could be rewritten by the elim set
249
           is rewritten *)
250
        let instr = eliminate m (IMap.map fst elim) instr in
251
        (* if instr is a simple local assign, then (a) elim is simplified with
252
           it (b) it is stored as the elim set *)
253
        instr_unfold m fanin instrs elim instr)
254
      (elim, []) instrs
255
  in
256
  elim, List.rev rev_instrs
257

    
258
and instr_unfold m fanin instrs (elim : (value_t * eq) IMap.t) instr =
259
  (* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE
260
     IT@." pp_instr instr;*)
261
  match get_instr_desc instr with
262
  (* Simple cases*)
263
  | MStep ([ v ], id, vl)
264
    when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
265
    ->
266
    instr_unfold m fanin instrs elim
267
      (update_instr_desc instr
268
         (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
269
  | MLocalAssign (v, expr)
270
    when (not (is_clock_dec_type v.var_dec_type.ty_dec_desc))
271
         && unfoldable_assign fanin v expr ->
272
    (* we don't eliminate clock definitions *)
273
    let new_eq =
274
      Corelang.mkeq (desome instr.lustre_eq).eq_loc
275
        ([ v.var_id ], (desome instr.lustre_eq).eq_rhs)
276
    in
277
    IMap.add v.var_id (expr, new_eq) elim, instrs
278
  | MBranch (g, hl) when false ->
279
    let elim_branches =
280
      List.map (fun (h, l) -> h, instrs_unfold m fanin elim l) hl
281
    in
282
    let elim, branches =
283
      List.fold_right
284
        (fun (h, (e, l)) (elim, branches) ->
285
          merge_elim elim e, (h, l) :: branches)
286
        elim_branches (elim, [])
287
    in
288
    elim, update_instr_desc instr (MBranch (g, branches)) :: instrs
289
  | _ ->
290
    elim, instr :: instrs
291
(* default case, we keep the instruction and do not modify elim *)
292

    
293
(** We iterate in the order, recording simple local assigns in an accumulator 1.
294
    each expression is rewritten according to the accumulator 2. local assigns
295
    then rewrite occurrences of the lhs in the computed accumulator *)
296

    
297
let static_call_unfold elim (inst, (n, args)) =
298
  let replace v =
299
    try dimension_of_value (IMap.find v elim)
300
    with Not_found -> Dimension.mkdim_ident Location.dummy_loc v
301
  in
302
  inst, (n, List.map (Dimension.expr_replace_expr replace) args)
303

    
304
(** Perform optimization on machine code: - iterate through step instructions
305
    and remove simple local assigns *)
306
let machine_unfold fanin elim machine =
307
  Log.report ~level:3 (fun fmt ->
308
      Format.fprintf fmt "machine_unfold %s %a@ " machine.mname.node_id
309
        (pp_elim machine) (IMap.map fst elim));
310
  let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
311
  let elim_vars, instrs =
312
    instrs_unfold machine fanin elim_consts machine.mstep.step_instrs
313
  in
314
  let instrs = simplify_instrs_offset machine instrs in
315
  let checks =
316
    List.map
317
      (fun (loc, check) ->
318
        loc, eliminate_expr machine (IMap.map fst elim_vars) check)
319
      machine.mstep.step_checks
320
  in
321
  let locals =
322
    List.filter
323
      (fun v -> not (IMap.mem v.var_id elim_vars))
324
      machine.mstep.step_locals
325
  in
326
  let elim_consts = IMap.map fst elim_consts in
327
  let minstances =
328
    List.map (static_call_unfold elim_consts) machine.minstances
329
  in
330
  let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls in
331
  ( {
332
      machine with
333
      mstep =
334
        {
335
          machine.mstep with
336
          step_locals = locals;
337
          step_instrs = instrs;
338
          step_checks = checks;
339
        };
340
      mconst;
341
      minstances;
342
      mcalls;
343
    },
344
    elim_vars )
345

    
346
let instr_of_const top_const =
347
  let const = const_of_top top_const in
348
  let loc = const.const_loc in
349
  let id = const.const_id in
350
  let vdecl =
351
    mkvar_decl loc
352
      ( id,
353
        mktyp Location.dummy_loc Tydec_any,
354
        mkclock loc Ckdec_any,
355
        true,
356
        None,
357
        None )
358
  in
359
  let vdecl = { vdecl with var_type = const.const_type } in
360
  let lustre_eq =
361
    mkeq loc ([ const.const_id ], mkexpr loc (Expr_const const.const_value))
362
  in
363
  mkinstr ~lustre_eq
364
    (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
365

    
366
(* We do not perform this optimization on contract nodes since there is not
367
   explicit dependence btw variables and their use in contracts. *)
368
let machines_unfold consts node_schs machines =
369
  List.fold_right
370
    (fun m (machines, removed) ->
371
      let is_contract =
372
        match m.mspec.mnode_spec with Some (Contract _) -> true | _ -> false
373
      in
374
      if is_contract then m :: machines, removed
375
      else
376
        let fanin =
377
          (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table
378
        in
379
        let elim_consts, _ =
380
          instrs_unfold m fanin IMap.empty (List.map instr_of_const consts)
381
        in
382
        let m, removed_m = machine_unfold fanin elim_consts m in
383
        m :: machines, IMap.add m.mname.node_id removed_m removed)
384
    machines ([], IMap.empty)
385

    
386
let get_assign_lhs instr =
387
  match get_instr_desc instr with
388
  | MLocalAssign (v, e) ->
389
    mk_val (Var v) e.value_type
390
  | MStateAssign (v, e) ->
391
    mk_val (Var v) e.value_type
392
  | _ ->
393
    assert false
394

    
395
let get_assign_rhs instr =
396
  match get_instr_desc instr with
397
  | MLocalAssign (_, e) | MStateAssign (_, e) ->
398
    e
399
  | _ ->
400
    assert false
401

    
402
let is_assign instr =
403
  match get_instr_desc instr with
404
  | MLocalAssign _ | MStateAssign _ ->
405
    true
406
  | _ ->
407
    false
408

    
409
let mk_assign m v e =
410
  match v.value_desc with
411
  | Var v ->
412
    if is_memory m v then MStateAssign (v, e) else MLocalAssign (v, e)
413
  | _ ->
414
    assert false
415

    
416
let rec assigns_instr instr assign =
417
  match get_instr_desc instr with
418
  | MLocalAssign (i, _) | MStateAssign (i, _) ->
419
    VSet.add i assign
420
  | MStep (ol, _, _) ->
421
    List.fold_right VSet.add ol assign
422
  | MBranch (_, hl) ->
423
    List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
424
  | _ ->
425
    assign
426

    
427
and assigns_instrs instrs assign =
428
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
429

    
430
(* and substitute_expr subst expr = match expr with | Var v -> (try IMap.find
431
   expr subst with Not_found -> expr) | Fun (id, vl) -> Fun (id, List.map
432
   (substitute_expr subst) vl) | Array(vl) -> Array(List.map (substitute_expr
433
   subst) vl) | Access(v1, v2) -> Access(substitute_expr subst v1,
434
   substitute_expr subst v2) | Power(v1, v2) -> Power(substitute_expr subst v1,
435
   substitute_expr subst v2) | Cst _ -> expr *)
436

    
437
(** Finds a substitute for [instr] in [instrs], i.e. another instr' with the
438
    same rhs expression. Then substitute this expression with the first assigned
439
    var *)
440
let subst_instr m subst instrs instr =
441
  (* Format.eprintf "subst instr: %a@." (pp_instr m) instr; *)
442
  let instr = eliminate m subst instr in
443
  let instr_v = get_assign_lhs instr in
444
  let instr_e = get_assign_rhs instr in
445
  try
446
    (* Searching for equivalent asssign *)
447
    let instr' =
448
      List.find
449
        (fun instr' -> is_assign instr' && get_assign_rhs instr' = instr_e)
450
        instrs
451
    in
452
    (* Registering the instr_v as instr'_v while replacing *)
453
    match instr_v.value_desc with
454
    | Var v -> (
455
      let instr'_v = get_assign_lhs instr' in
456
      if not (is_memory m v) then
457
        (* The current instruction defines a local variables, ie not memory, we
458
           can just record the relationship and continue *)
459
        IMap.add v.var_id instr'_v subst, instrs
460
      else
461
        (* The current instruction defines a memory. We need to keep the
462
           definition, simplified *)
463
        match instr'_v.value_desc with
464
        | Var v' ->
465
          if not (is_memory m v') then
466
            (* We define v' = v. Don't need to update the records. *)
467
            let instr =
468
              eliminate m subst
469
                (update_instr_desc instr (mk_assign m instr_v instr'_v))
470
            in
471
            subst, instr :: instrs
472
          else
473
            (* Last case, v', the lhs of the previous similar definition is,
474
               itself, a memory *)
475

    
476
            (* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *)
477
            (* Filtering out the list of instructions: - we copy in the same
478
               order the list of instr in instrs (fold_right) - if the current
479
               instr is this instr' then apply the elimination with v' -> v on
480
               instr' before recording it as an instruction. *)
481
            let subst_v' = IMap.add v'.var_id instr_v IMap.empty in
482
            let instrs' =
483
              snd
484
                (List.fold_right
485
                   (fun instr (ok, instrs) ->
486
                     ( ok || instr = instr',
487
                       if ok then instr :: instrs
488
                       else if instr = instr' then instrs
489
                       else eliminate m subst_v' instr :: instrs ))
490
                   instrs (false, []))
491
            in
492
            IMap.add v'.var_id instr_v subst, instr :: instrs'
493
        | _ ->
494
          assert false)
495
    | _ ->
496
      assert false
497
  with Not_found ->
498
    (* No such equivalent expr: keeping the definition *)
499
    subst, instr :: instrs
500

    
501
(* - [subst] : hashtable from ident to (simple) definition it is an equivalence
502
   table - [elim] : set of eliminated variables - [instrs] : previous
503
   instructions, which [instr] is compared against - [instr] : current
504
   instruction, normalized by [subst] *)
505

    
506
(** Common sub-expression elimination for machine instructions *)
507
let rec instr_cse m (subst, instrs) instr =
508
  match get_instr_desc instr with
509
  (* Simple cases*)
510
  | MStep ([ v ], id, vl)
511
    when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
512
    ->
513
    instr_cse m (subst, instrs)
514
      (update_instr_desc instr
515
         (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
516
  | MLocalAssign (v, expr) when is_unfoldable_expr 2 expr ->
517
    IMap.add v.var_id expr subst, instr :: instrs
518
  | _ when is_assign instr ->
519
    subst_instr m subst instrs instr
520
  | _ ->
521
    subst, instr :: instrs
522

    
523
(** Apply common sub-expression elimination to a sequence of instrs *)
524
let instrs_cse m subst instrs =
525
  let subst, rev_instrs = List.fold_left (instr_cse m) (subst, []) instrs in
526
  subst, List.rev rev_instrs
527

    
528
(** Apply common sub-expression elimination to a machine - iterate through step
529
    instructions and remove simple local assigns *)
530
let machine_cse subst machine =
531
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@."
532
    pp_elim subst);*)
533
  let _, instrs = instrs_cse machine subst machine.mstep.step_instrs in
534
  let assigned = assigns_instrs instrs VSet.empty in
535
  {
536
    machine with
537
    mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
538
    mstep =
539
      {
540
        machine.mstep with
541
        step_locals =
542
          List.filter
543
            (fun vdecl -> VSet.mem vdecl assigned)
544
            machine.mstep.step_locals;
545
        step_instrs = instrs;
546
      };
547
  }
548

    
549
let machines_cse machines = List.map (machine_cse IMap.empty) machines
550

    
551
(* variable substitution for optimizing purposes *)
552

    
553
(* checks whether an [instr] is skip and can be removed from program *)
554
let rec instr_is_skip instr =
555
  match get_instr_desc instr with
556
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
557
    true
558
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
559
    true
560
  | MBranch (_, hl) ->
561
    List.for_all (fun (_, il) -> instrs_are_skip il) hl
562
  | _ ->
563
    false
564

    
565
and instrs_are_skip instrs = List.for_all instr_is_skip instrs
566

    
567
let instr_cons instr cont = if instr_is_skip instr then cont else instr :: cont
568

    
569
let rec instr_remove_skip instr cont =
570
  match get_instr_desc instr with
571
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
572
    cont
573
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
574
    cont
575
  | MBranch (g, hl) ->
576
    update_instr_desc instr
577
      (MBranch (g, List.map (fun (h, il) -> h, instrs_remove_skip il []) hl))
578
    :: cont
579
  | _ ->
580
    instr :: cont
581

    
582
and instrs_remove_skip instrs cont =
583
  List.fold_right instr_remove_skip instrs cont
584

    
585
let rec value_replace_var fvar value =
586
  match value.value_desc with
587
  | Cst _ | ResetFlag ->
588
    value
589
  | Var v ->
590
    { value with value_desc = Var (fvar v) }
591
  | Fun (id, args) ->
592
    { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
593
  | Array vl ->
594
    { value with value_desc = Array (List.map (value_replace_var fvar) vl) }
595
  | Access (t, i) ->
596
    { value with value_desc = Access (value_replace_var fvar t, i) }
597
  | Power (v, n) ->
598
    { value with value_desc = Power (value_replace_var fvar v, n) }
599

    
600
let rec instr_replace_var fvar instr cont =
601
  match get_instr_desc instr with
602
  | MLocalAssign (i, v) ->
603
    instr_cons
604
      (update_instr_desc instr
605
         (MLocalAssign (fvar i, value_replace_var fvar v)))
606
      cont
607
  | MStateAssign (i, v) ->
608
    instr_cons
609
      (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v)))
610
      cont
611
  | MSetReset _
612
  | MNoReset _
613
  | MClearReset
614
  | MResetAssign _
615
  | MSpec _
616
  | MComment _ ->
617
    instr_cons instr cont
618
  | MStep (il, i, vl) ->
619
    instr_cons
620
      (update_instr_desc instr
621
         (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)))
622
      cont
623
  | MBranch (g, hl) ->
624
    instr_cons
625
      (update_instr_desc instr
626
         (MBranch
627
            ( value_replace_var fvar g,
628
              List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )))
629
      cont
630

    
631
and instrs_replace_var fvar instrs cont =
632
  List.fold_right (instr_replace_var fvar) instrs cont
633

    
634
let step_replace_var fvar step =
635
  (* Some outputs may have been replaced by locals. We then need to rename those
636
     outputs without changing their clocks, etc *)
637
  let outputs' =
638
    List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs
639
  in
640
  let locals' =
641
    List.fold_left
642
      (fun res l ->
643
        let l' = fvar l in
644
        if List.exists (fun o -> o.var_id = l'.var_id) outputs' then res
645
        else Utils.add_cons l' res)
646
      [] step.step_locals
647
  in
648
  {
649
    step with
650
    step_checks =
651
      List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks;
652
    step_outputs = outputs';
653
    step_locals = locals';
654
    step_instrs = instrs_replace_var fvar step.step_instrs [];
655
  }
656

    
657
let machine_replace_variables fvar m =
658
  { m with mstep = step_replace_var fvar m.mstep }
659

    
660
let machine_reuse_variables m reuse =
661
  let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
662
  machine_replace_variables fvar m
663

    
664
let machines_reuse_variables prog reuse_tables =
665
  List.map
666
    (fun m ->
667
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables))
668
    prog
669

    
670
let rec instr_assign res instr =
671
  match get_instr_desc instr with
672
  | MLocalAssign (i, _) ->
673
    Disjunction.CISet.add i res
674
  | MStateAssign (i, _) ->
675
    Disjunction.CISet.add i res
676
  | MBranch (_, hl) ->
677
    List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
678
  | MStep (il, _, _) ->
679
    List.fold_right Disjunction.CISet.add il res
680
  | _ ->
681
    res
682

    
683
and instrs_assign res instrs = List.fold_left instr_assign res instrs
684

    
685
let rec instr_constant_assign var instr =
686
  match get_instr_desc instr with
687
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
688
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) ->
689
    i = var
690
  | MBranch (_, hl) ->
691
    List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
692
  | _ ->
693
    false
694

    
695
and instrs_constant_assign var instrs =
696
  List.fold_left
697
    (fun res i ->
698
      if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then
699
        instr_constant_assign var i
700
      else res)
701
    false instrs
702

    
703
let rec instr_reduce branches instr1 cont =
704
  match get_instr_desc instr1 with
705
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
706
    instr1 :: (List.assoc c branches @ cont)
707
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
708
    instr1 :: (List.assoc c branches @ cont)
709
  | MBranch (g, hl) ->
710
    update_instr_desc instr1
711
      (MBranch (g, List.map (fun (h, b) -> h, instrs_reduce branches b []) hl))
712
    :: cont
713
  | _ ->
714
    instr1 :: cont
715

    
716
and instrs_reduce branches instrs cont =
717
  match instrs with
718
  | [] ->
719
    cont
720
  | [ i ] ->
721
    instr_reduce branches i cont
722
  | i1 :: i2 :: q ->
723
    i1 :: instrs_reduce branches (i2 :: q) cont
724

    
725
let rec instrs_fusion instrs =
726
  match instrs, List.map get_instr_desc instrs with
727
  | [], [] | [ _ ], [ _ ] ->
728
    instrs
729
  | i1 :: _ :: q, _ :: MBranch ({ value_desc = Var v; _ }, hl) :: _
730
    when instr_constant_assign v i1 ->
731
    instr_reduce
732
      (List.map (fun (h, b) -> h, instrs_fusion b) hl)
733
      i1 (instrs_fusion q)
734
  | i1 :: i2 :: q, _ ->
735
    i1 :: instrs_fusion (i2 :: q)
736
  | _ ->
737
    assert false
738
(* Other cases should not happen since both lists are of same size *)
739

    
740
let step_fusion step =
741
  { step with step_instrs = instrs_fusion step.step_instrs }
742

    
743
let machine_fusion m = { m with mstep = step_fusion m.mstep }
744

    
745
let machines_fusion prog = List.map machine_fusion prog
746

    
747
(* Additional function to modify the prog according to removed variables map *)
748

    
749
let elim_prog_variables prog removed_table =
750
  List.map
751
    (fun t ->
752
      match t.top_decl_desc with
753
      | Node nd -> (
754
        match IMap.find_opt nd.node_id removed_table with
755
        | Some nd_elim_map ->
756
          (* Iterating through the elim map to compute - the list of variables
757
             to remove - the associated list of lustre definitions x = expr to
758
             be used when removing these variables *)
759
          let vars_to_replace, defs =
760
            (* Recovering vid from node locals *)
761
            IMap.fold
762
              (fun v (_, eq) (accu_locals, accu_defs) ->
763
                let locals =
764
                  try
765
                    List.find (fun v' -> v'.var_id = v) nd.node_locals
766
                    :: accu_locals
767
                  with Not_found -> accu_locals
768
                  (* Variable v shall be a global constant, we do no need to
769
                     eliminate it from the locals *)
770
                in
771
                (* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc =
772
                   e.expr_loc } in *)
773
                let defs = eq :: accu_defs in
774
                locals, defs)
775
              nd_elim_map ([], [])
776
          in
777

    
778
          let node_locals, node_stmts =
779
            List.fold_right
780
              (fun stmt (locals, res_stmts) ->
781
                match stmt with
782
                | Aut _ ->
783
                  assert false (* should be processed by now *)
784
                | Eq eq -> (
785
                  match eq.eq_lhs with
786
                  | [] ->
787
                    assert false (* shall not happen *)
788
                  | _ :: _ :: _ ->
789
                    (* When more than one lhs we just keep the equation and do
790
                       not delete it *)
791
                    let eq_rhs' =
792
                      substitute_expr vars_to_replace defs eq.eq_rhs
793
                    in
794
                    locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts
795
                  | [ lhs ] ->
796
                    if List.exists (fun v -> v.var_id = lhs) vars_to_replace
797
                    then
798
                      (* We remove the def *)
799
                      List.filter (fun v -> v.var_id <> lhs) locals, res_stmts
800
                    else
801
                      (* We keep it but modify any use of an eliminatend var *)
802
                      let eq_rhs' =
803
                        substitute_expr vars_to_replace defs eq.eq_rhs
804
                      in
805
                      locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts))
806
              nd.node_stmts (nd.node_locals, [])
807
          in
808
          let nd' = { nd with node_locals; node_stmts } in
809
          { t with top_decl_desc = Node nd' }
810
        | None ->
811
          t)
812
      | _ ->
813
        t)
814
    prog
815

    
816
(*** Main function ***)
817

    
818
(* This functions produces an optimzed prog * machines It 1- eliminates common
819
   sub-expressions (TODO how is this different from normalization?) 2- inline
820
   constants and eliminate duplicated variables 3- try to reuse variables
821
   whenever possible
822

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

    
827
   The function returns both the (possibly updated) prog as well as the machines *)
828
let optimize params prog node_schs machine_code =
829
  let machine_code =
830
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then (
831
      Log.report ~level:1 (fun fmt ->
832
          Format.fprintf fmt
833
            "@ @[<v 2>.. machines optimization: sub-expression elimination@ ");
834
      let machine_code = machines_cse machine_code in
835
      Log.report ~level:3 (fun fmt ->
836
          Format.fprintf fmt
837
            "@[<v 2>.. generated machines (sub-expr elim):@ %a@]@ " pp_machines
838
            machine_code);
839
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
840
      machine_code)
841
    else machine_code
842
  in
843
  (* Optimize machine code *)
844
  let prog, machine_code, removed_table =
845
    if
846
      !Options.optimization >= 2 && !Options.output <> "emf"
847
      (*&& !Options.output <> "horn"*)
848
    then (
849
      Log.report ~level:1 (fun fmt ->
850
          Format.fprintf fmt
851
            "@ @[<v 2>.. machines optimization: const. inlining (partial eval. \
852
             with const)@ ");
853
      let machine_code, removed_table =
854
        machines_unfold (Corelang.get_consts prog) node_schs machine_code
855
      in
856
      Log.report ~level:3 (fun fmt ->
857
          Format.fprintf fmt "@ Eliminated flows: %a@ "
858
            (pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m)))
859
            removed_table);
860
      Log.report ~level:3 (fun fmt ->
861
          Format.fprintf fmt
862
            "@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "
863
            pp_machines machine_code);
864
      (* If variables were eliminated, relaunch the normalization/machine
865
         generation *)
866
      let prog, machine_code, removed_table =
867
        if IMap.is_empty removed_table then
868
          (* stopping here, no need to reupdate the prog *)
869
          prog, machine_code, removed_table
870
        else
871
          let prog = elim_prog_variables prog removed_table in
872
          (* Mini stage1 *)
873
          let prog = Normalization.normalize_prog params prog in
874
          let prog = SortProg.sort_nodes_locals prog in
875
          (* Mini stage2: note that we do not protect against alg. loop since
876
             this should have been handled before *)
877
          let prog, node_schs = Scheduling.schedule_prog prog in
878
          let machine_code = Machine_code.translate_prog prog node_schs in
879
          (* Mini stage2 machine optimiation *)
880
          let machine_code, removed_table =
881
            machines_unfold (Corelang.get_consts prog) node_schs machine_code
882
          in
883
          prog, machine_code, removed_table
884
      in
885
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
886
      prog, machine_code, removed_table)
887
    else prog, machine_code, IMap.empty
888
  in
889
  (* Optimize machine code *)
890
  let machine_code =
891
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then (
892
      Log.report ~level:1 (fun fmt ->
893
          Format.fprintf fmt
894
            ".. machines optimization: minimize stack usage by reusing \
895
             variables@,");
896
      let node_schs =
897
        Scheduling.remove_prog_inlined_locals removed_table node_schs
898
      in
899
      let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
900
      machines_fusion (machines_reuse_variables machine_code reuse_tables))
901
    else machine_code
902
  in
903

    
904
  prog, machine_code
905

    
906
(* Local Variables: *)
907
(* compile-command:"make -C .." *)
908
(* End: *)
(45-45/66)