Project

General

Profile

Download (32.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 Spec_types
15
open Machine_code_types
16
open Corelang
17
open Causality
18
open Machine_code_common
19
open Dimension
20
module Mpfr = Lustrec_mpfr
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) ->
32
    update_instr_desc instr (MLocalAssign (i, e_expr v))
33
  | MStateAssign (i, v) ->
34
    update_instr_desc instr (MStateAssign (i, e_expr v))
35
  | MSetReset _
36
  | MNoReset _
37
  | MClearReset
38
  | MResetAssign _
39
  | MSpec _
40
  | MComment _ ->
41
    instr
42
  | MStep (il, i, vl) ->
43
    update_instr_desc instr (MStep (il, i, List.map e_expr vl))
44
  | MBranch (g, hl) ->
45
    update_instr_desc instr
46
      (MBranch
47
         ( e_expr g,
48
           List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl ))
49

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
552
(* variable substitution for optimizing purposes *)
553

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

    
566
and instrs_are_skip instrs = List.for_all instr_is_skip instrs
567

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

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

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

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

    
601
let expr_spec_replace :
602
    type a.
603
    (var_decl -> var_decl) ->
604
    (value_t, a) expression_t ->
605
    (value_t, a) expression_t =
606
 fun fvar -> function
607
  | Val v ->
608
    Val (value_replace_var fvar v)
609
  | Var v ->
610
    Var (fvar v)
611
  | e ->
612
    e
613

    
614
let predicate_spec_replace fvar = function
615
  | Transition (f, inst, i, vars, r, mems, insts) ->
616
    Transition
617
      (f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts)
618
  | p ->
619
    p
620

    
621
let rec instr_spec_replace fvar =
622
  let aux instr = instr_spec_replace fvar instr in
623
  function
624
  | Equal (e1, e2) ->
625
    Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
626
  | And f ->
627
    And (List.map aux f)
628
  | Or f ->
629
    Or (List.map aux f)
630
  | Imply (a, b) ->
631
    Imply (aux a, aux b)
632
  | Exists (xs, a) ->
633
    let fvar v = if List.mem v xs then v else fvar v in
634
    Exists (xs, instr_spec_replace fvar a)
635
  | Forall (xs, a) ->
636
    let fvar v = if List.mem v xs then v else fvar v in
637
    Forall (xs, instr_spec_replace fvar a)
638
  | Ternary (e, a, b) ->
639
    Ternary (expr_spec_replace fvar e, aux a, aux b)
640
  | Predicate p ->
641
    Predicate (predicate_spec_replace fvar p)
642
  | ExistsMem (f, a, b) ->
643
    ExistsMem (f, aux a, aux b)
644
  | f ->
645
    f
646

    
647
let rec instr_replace_var fvar instr =
648
  let instr_desc =
649
    match instr.instr_desc with
650
    | MLocalAssign (i, v) ->
651
      MLocalAssign (fvar i, value_replace_var fvar v)
652
    | MStateAssign (i, v) ->
653
      MStateAssign (i, value_replace_var fvar v)
654
    | MStep (il, i, vl) ->
655
      MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)
656
    | MBranch (g, hl) ->
657
      MBranch
658
        ( value_replace_var fvar g,
659
          List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )
660
    | MSetReset _
661
    | MNoReset _
662
    | MClearReset
663
    | MResetAssign _
664
    | MSpec _
665
    | MComment _ ->
666
      instr.instr_desc
667
  in
668
  let instr_spec = List.map (instr_spec_replace fvar) instr.instr_spec in
669
  instr_cons { instr with instr_desc; instr_spec }
670

    
671
and instrs_replace_var fvar instrs cont =
672
  List.fold_right (instr_replace_var fvar) instrs cont
673

    
674
let step_replace_var fvar step =
675
  (* Some outputs may have been replaced by locals. We then need to rename those
676
     outputs without changing their clocks, etc *)
677
  let outputs' =
678
    List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs
679
  in
680
  let locals' =
681
    List.fold_left
682
      (fun res l ->
683
        let l' = fvar l in
684
        if List.exists (fun o -> o.var_id = l'.var_id) outputs' then res
685
        else Utils.add_cons l' res)
686
      [] step.step_locals
687
  in
688
  {
689
    step with
690
    step_checks =
691
      List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks;
692
    step_outputs = outputs';
693
    step_locals = locals';
694
    step_instrs = instrs_replace_var fvar step.step_instrs [];
695
  }
696

    
697
let machine_replace_variables fvar m =
698
  { m with mstep = step_replace_var fvar m.mstep }
699

    
700
let machine_reuse_variables reuse m =
701
  let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
702
  machine_replace_variables fvar m
703

    
704
let machines_reuse_variables reuse_tables =
705
  List.map (fun m ->
706
      machine_reuse_variables (Utils.IMap.find m.mname.node_id reuse_tables) m)
707

    
708
let rec instr_assign res instr =
709
  match get_instr_desc instr with
710
  | MLocalAssign (i, _) ->
711
    Disjunction.CISet.add i res
712
  | MStateAssign (i, _) ->
713
    Disjunction.CISet.add i res
714
  | MBranch (_, hl) ->
715
    List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
716
  | MStep (il, _, _) ->
717
    List.fold_right Disjunction.CISet.add il res
718
  | _ ->
719
    res
720

    
721
and instrs_assign res instrs = List.fold_left instr_assign res instrs
722

    
723
let rec instr_constant_assign var instr =
724
  match get_instr_desc instr with
725
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
726
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) ->
727
    i = var
728
  | MBranch (_, hl) ->
729
    List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
730
  | _ ->
731
    false
732

    
733
and instrs_constant_assign var instrs =
734
  List.fold_left
735
    (fun res i ->
736
      if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then
737
        instr_constant_assign var i
738
      else res)
739
    false instrs
740

    
741
let rec instr_reduce branches instr1 cont =
742
  match get_instr_desc instr1 with
743
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
744
    instr1 :: (List.assoc c branches @ cont)
745
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
746
    instr1 :: (List.assoc c branches @ cont)
747
  | MBranch (g, hl) ->
748
    update_instr_desc instr1
749
      (MBranch (g, List.map (fun (h, b) -> h, instrs_reduce branches b []) hl))
750
    :: cont
751
  | _ ->
752
    instr1 :: cont
753

    
754
and instrs_reduce branches instrs cont =
755
  match instrs with
756
  | [] ->
757
    cont
758
  | [ i ] ->
759
    instr_reduce branches i cont
760
  | i1 :: i2 :: q ->
761
    i1 :: instrs_reduce branches (i2 :: q) cont
762

    
763
let rec instrs_fusion instrs =
764
  match instrs with
765
  | [] | [ _ ] ->
766
    instrs
767
  | i1 :: i2 :: q -> (
768
    match i2.instr_desc with
769
    | MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 ->
770
      instr_reduce
771
        (List.map (fun (h, b) -> h, instrs_fusion b) hl)
772
        { i1 with instr_spec = i1.instr_spec @ i2.instr_spec }
773
        (instrs_fusion q)
774
    | _ ->
775
      i1 :: instrs_fusion (i2 :: q))
776

    
777
let step_fusion step =
778
  { step with step_instrs = instrs_fusion step.step_instrs }
779

    
780
let machine_fusion m = { m with mstep = step_fusion m.mstep }
781

    
782
let machines_fusion prog = List.map machine_fusion prog
783

    
784
(* Additional function to modify the prog according to removed variables map *)
785

    
786
let elim_prog_variables prog removed_table =
787
  List.map
788
    (fun t ->
789
      match t.top_decl_desc with
790
      | Node nd -> (
791
        match IMap.find_opt nd.node_id removed_table with
792
        | Some nd_elim_map ->
793
          (* Iterating through the elim map to compute - the list of variables
794
             to remove - the associated list of lustre definitions x = expr to
795
             be used when removing these variables *)
796
          let vars_to_replace, defs =
797
            (* Recovering vid from node locals *)
798
            IMap.fold
799
              (fun v (_, eq) (accu_locals, accu_defs) ->
800
                let locals =
801
                  try
802
                    List.find (fun v' -> v'.var_id = v) nd.node_locals
803
                    :: accu_locals
804
                  with Not_found -> accu_locals
805
                  (* Variable v shall be a global constant, we do no need to
806
                     eliminate it from the locals *)
807
                in
808
                (* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc =
809
                   e.expr_loc } in *)
810
                let defs = eq :: accu_defs in
811
                locals, defs)
812
              nd_elim_map ([], [])
813
          in
814

    
815
          let node_locals, node_stmts =
816
            List.fold_right
817
              (fun stmt (locals, res_stmts) ->
818
                match stmt with
819
                | Aut _ ->
820
                  assert false (* should be processed by now *)
821
                | Eq eq -> (
822
                  match eq.eq_lhs with
823
                  | [] ->
824
                    assert false (* shall not happen *)
825
                  | _ :: _ :: _ ->
826
                    (* When more than one lhs we just keep the equation and do
827
                       not delete it *)
828
                    let eq_rhs' =
829
                      substitute_expr vars_to_replace defs eq.eq_rhs
830
                    in
831
                    locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts
832
                  | [ lhs ] ->
833
                    if List.exists (fun v -> v.var_id = lhs) vars_to_replace
834
                    then
835
                      (* We remove the def *)
836
                      List.filter (fun v -> v.var_id <> lhs) locals, res_stmts
837
                    else
838
                      (* We keep it but modify any use of an eliminatend var *)
839
                      let eq_rhs' =
840
                        substitute_expr vars_to_replace defs eq.eq_rhs
841
                      in
842
                      locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts))
843
              nd.node_stmts (nd.node_locals, [])
844
          in
845
          let nd' = { nd with node_locals; node_stmts } in
846
          { t with top_decl_desc = Node nd' }
847
        | None ->
848
          t)
849
      | _ ->
850
        t)
851
    prog
852

    
853
(*** Main function ***)
854

    
855
(* This functions produces an optimzed prog * machines It 1- eliminates common
856
   sub-expressions (TODO how is this different from normalization?) 2- inline
857
   constants and eliminate duplicated variables 3- try to reuse variables
858
   whenever possible
859

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

    
864
   The function returns both the (possibly updated) prog as well as the machines *)
865
let optimize params prog node_schs machine_code =
866
  let machine_code =
867
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then (
868
      Log.report ~level:1 (fun fmt ->
869
          Format.fprintf fmt
870
            "@ @[<v 2>.. machines optimization: sub-expression elimination@ ");
871
      let machine_code = machines_cse machine_code in
872
      Log.report ~level:3 (fun fmt ->
873
          Format.fprintf fmt
874
            "@[<v 2>.. generated machines (sub-expr elim):@ %a@]@ " pp_machines
875
            machine_code);
876
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
877
      machine_code)
878
    else machine_code
879
  in
880
  (* Optimize machine code *)
881
  let prog, machine_code, removed_table =
882
    if
883
      !Options.optimization >= 2 && !Options.output <> "emf"
884
      (*&& !Options.output <> "horn"*)
885
    then (
886
      Log.report ~level:1 (fun fmt ->
887
          Format.fprintf fmt
888
            "@ @[<v 2>.. machines optimization: const. inlining (partial eval. \
889
             with const)@ ");
890
      let machine_code, removed_table =
891
        machines_unfold (Corelang.get_consts prog) node_schs machine_code
892
      in
893
      Log.report ~level:3 (fun fmt ->
894
          Format.fprintf fmt "@ Eliminated flows: %a@ "
895
            (pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m)))
896
            removed_table);
897
      Log.report ~level:3 (fun fmt ->
898
          Format.fprintf fmt
899
            "@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "
900
            pp_machines machine_code);
901
      (* If variables were eliminated, relaunch the normalization/machine
902
         generation *)
903
      let prog, machine_code, removed_table =
904
        if IMap.is_empty removed_table then
905
          (* stopping here, no need to reupdate the prog *)
906
          prog, machine_code, removed_table
907
        else
908
          let prog = elim_prog_variables prog removed_table in
909
          (* Mini stage1 *)
910
          let prog = Normalization.normalize_prog params prog in
911
          let prog = SortProg.sort_nodes_locals prog in
912
          (* Mini stage2: note that we do not protect against alg. loop since
913
             this should have been handled before *)
914
          let prog, node_schs = Scheduling.schedule_prog prog in
915
          let machine_code = Machine_code.translate_prog prog node_schs in
916
          (* Mini stage2 machine optimiation *)
917
          let machine_code, removed_table =
918
            machines_unfold (Corelang.get_consts prog) node_schs machine_code
919
          in
920
          prog, machine_code, removed_table
921
      in
922
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
923
      prog, machine_code, removed_table)
924
    else prog, machine_code, IMap.empty
925
  in
926
  (* Optimize machine code *)
927
  let machine_code =
928
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then (
929
      Log.report ~level:1 (fun fmt ->
930
          Format.fprintf fmt
931
            ".. machines optimization: minimize stack usage by reusing \
932
             variables@,");
933
      let node_schs =
934
        Scheduling.remove_prog_inlined_locals removed_table node_schs
935
      in
936
      let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
937
      machines_fusion (machines_reuse_variables reuse_tables machine_code))
938
    else machine_code
939
  in
940

    
941
  prog, machine_code
942

    
943
(* Local Variables: *)
944
(* compile-command:"make -C .." *)
945
(* End: *)
(45-45/66)