Project

General

Profile

Download (33.9 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

    
12
open Utils
13
open Lustre_types
14
open Spec_types
15
open Machine_code_types
16
open Corelang
17
open Causality
18
open Machine_code_common
19
module Mpfr = Lustrec_mpfr
20

    
21
let pp_elim m fmt elim =
22
  IMap.pp ~comment:"/* elim table: */" (pp_val m) fmt elim
23

    
24
let eliminate_var_decl elim m v f a =
25
  if is_memory m v then a
26
  else try
27
      f (IMap.find v.var_id elim)
28
    with Not_found -> a
29

    
30
let rec eliminate_val m elim expr =
31
  let eliminate_val = eliminate_val m in
32
  match expr.value_desc with
33
  | Var v ->
34
    eliminate_var_decl elim m v (fun x -> x) expr
35
  | Fun (id, vl) ->
36
    { expr with value_desc = Fun (id, List.map (eliminate_val elim) vl) }
37
  | Array vl ->
38
    { expr with value_desc = Array (List.map (eliminate_val elim) vl) }
39
  | Access (v1, v2) ->
40
    {
41
      expr with
42
      value_desc = Access (eliminate_val elim v1, eliminate_val elim v2);
43
    }
44
  | Power (v1, v2) ->
45
    {
46
      expr with
47
      value_desc = Power (eliminate_val elim v1, eliminate_val elim v2);
48
    }
49
  | Cst _ | ResetFlag ->
50
    expr
51

    
52
let eliminate_expr m elim e =
53
  let e_val = eliminate_val m elim in
54
  match e with
55
  | Val v -> Val (e_val v)
56
  | Var v -> eliminate_var_decl elim m v (fun x -> Val x) e
57
  | _ -> e
58

    
59
let eliminate_pred m elim = function
60
  | Transition (s, f, inst, i, vars, r, mems, insts) ->
61
    let vars = List.filter_map (function
62
        | Spec_types.Val v ->
63
          begin match v.value_desc with
64
            | Var vd when IMap.mem vd.var_id elim -> None
65
            | _ -> Some (Val v)
66
          end
67
        | Spec_types.Var vd when IMap.mem vd.var_id elim -> None
68
        | e -> Some (eliminate_expr m elim e)) vars
69
    in
70
    Transition (s, f, inst, i, vars, r, mems, insts)
71
  | p ->
72
    p
73

    
74
let rec eliminate_formula m elim =
75
  let e_expr = eliminate_expr m elim in
76
  let e_instr i = eliminate_formula m elim i in
77
  let e_pred = eliminate_pred m elim in
78
  function
79
  | Equal (e1, e2) ->
80
    Equal (e_expr e1, e_expr e2)
81
  | And f ->
82
    And (List.map e_instr f)
83
  | Or f ->
84
    Or (List.map e_instr f)
85
  | Imply (a, b) ->
86
    Imply (e_instr a, e_instr b)
87
  | Exists (xs, a) ->
88
    let xs = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) xs in
89
    Exists (xs, eliminate_formula m elim a)
90
  | Forall (xs, a) ->
91
    let xs = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) xs in
92
    Forall (xs, eliminate_formula m elim a)
93
  | Ternary (e, a, b) ->
94
    Ternary (e_expr e, e_instr a, e_instr b)
95
  | Predicate p ->
96
    Predicate (e_pred p)
97
  | ExistsMem (f, a, b) ->
98
    ExistsMem (f, e_instr a, e_instr b)
99
  | f ->
100
    f
101

    
102
let rec eliminate m elim instr =
103
  let e_val = eliminate_val m elim in
104
  let instr = { instr with instr_spec = List.map (eliminate_formula m elim) instr.instr_spec } in
105
  match get_instr_desc instr with
106
  | MLocalAssign (i, v) ->
107
    update_instr_desc instr (MLocalAssign (i, e_val v))
108
  | MStateAssign (i, v) ->
109
    update_instr_desc instr (MStateAssign (i, e_val v))
110
  | MSetReset _
111
  | MNoReset _
112
  | MClearReset
113
  | MResetAssign _
114
  | MSpec _
115
  | MComment _ ->
116
    instr
117
  | MStep (il, i, vl) ->
118
    update_instr_desc instr (MStep (il, i, List.map e_val vl))
119
  | MBranch (g, hl) ->
120
    update_instr_desc
121
      instr
122
      (MBranch
123
         ( e_val g,
124
           List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl ))
125

    
126
let eliminate_transition m elim t =
127
  { t with
128
    tvars = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) t.tvars;
129
    tformula = eliminate_formula m elim t.tformula }
130

    
131
(* XXX: UNUSED *)
132
(* let eliminate_dim elim dim =
133
 *   Dimension.expr_replace_expr
134
 *     (fun v ->
135
 *       try dimension_of_value (IMap.find v elim)
136
 *       with Not_found -> mkdim_ident dim.dim_loc v)
137
 *     dim *)
138

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

    
142
let unfold_expr_offset m offset expr =
143
  List.fold_left
144
    (fun res -> function
145
      | Index i ->
146
        mk_val
147
          (Access (res, value_of_dimension m i))
148
          (Types.array_element_type res.value_type)
149
      | Field _ ->
150
        Format.eprintf "internal error: not yet implemented !";
151
        assert false)
152
    expr
153
    offset
154

    
155
let rec simplify_cst_expr m offset typ cst =
156
  match offset, cst with
157
  | [], _ ->
158
    mk_val (Cst cst) typ
159
  | Index i :: q, Const_array cl when Dimension.is_const i ->
160
    let elt_typ = Types.array_element_type typ in
161
    simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const i))
162
  | Index i :: q, Const_array cl ->
163
    let elt_typ = Types.array_element_type typ in
164
    unfold_expr_offset
165
      m
166
      [ Index i ]
167
      (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
168
  | Field f :: q, Const_struct fl ->
169
    let fld_typ = Types.struct_field_type typ f in
170
    simplify_cst_expr m q fld_typ (List.assoc f fl)
171
  | _ ->
172
    Format.eprintf
173
      "internal error: Optimize_machine.simplify_cst_expr %a@."
174
      Printers.pp_const
175
      cst;
176
    assert false
177

    
178
let simplify_expr_offset m expr =
179
  let rec simplify offset expr =
180
    match offset, expr.value_desc with
181
    | Field _ :: _, _ ->
182
      failwith "not yet implemented"
183
    | _, Fun (id, vl) when Basic_library.is_value_internal_fun expr ->
184
      mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
185
    | _, Fun _ | _, Var _ ->
186
      unfold_expr_offset m offset expr
187
    | _, Cst cst ->
188
      simplify_cst_expr m offset expr.value_type cst
189
    | _, Access (expr, i) ->
190
      simplify (Index (dimension_of_value i) :: offset) expr
191
    | _, ResetFlag ->
192
      expr
193
    | [], _ ->
194
      expr
195
    | Index _ :: q, Power (expr, _) ->
196
      simplify q expr
197
    | Index i :: q, Array vl when Dimension.is_const i ->
198
      simplify q (List.nth vl (Dimension.size_const i))
199
    | Index i :: q, Array vl ->
200
      unfold_expr_offset
201
        m
202
        [ Index i ]
203
        (mk_val (Array (List.map (simplify q) vl)) expr.value_type)
204
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr
205
      (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
206
      with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr
207
      (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
208
  in
209
  simplify [] expr
210

    
211
let rec simplify_instr_offset m instr =
212
  match get_instr_desc instr with
213
  | MLocalAssign (v, expr) ->
214
    update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
215
  | MStateAssign (v, expr) ->
216
    update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
217
  | MSetReset _
218
  | MNoReset _
219
  | MClearReset
220
  | MResetAssign _
221
  | MSpec _
222
  | MComment _ ->
223
    instr
224
  | MStep (outputs, id, inputs) ->
225
    update_instr_desc
226
      instr
227
      (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
228
  | MBranch (cond, brl) ->
229
    update_instr_desc
230
      instr
231
      (MBranch
232
         ( simplify_expr_offset m cond,
233
           List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl ))
234

    
235
and simplify_instrs_offset m instrs = List.map (simplify_instr_offset m) instrs
236

    
237
(* XXX: UNUSED *)
238
(* let is_scalar_const c =
239
 *   match c with Const_real _ | Const_int _ | Const_tag _ -> true | _ -> false *)
240

    
241
(* An instruction v = expr may (and will) be unfolded iff: - either expr is
242
   atomic (no complex expressions, only const, vars and array/struct accesses) -
243
   or v has a fanin <= 1 (used at most once) *)
244
let is_unfoldable_expr fanin expr =
245
  let rec unfold_const offset cst =
246
    match offset, cst with
247
    | _, Const_int _ | _, Const_real _ | _, Const_tag _ ->
248
      true
249
    | Field f :: q, Const_struct fl ->
250
      unfold_const q (List.assoc f fl)
251
    | [], Const_struct _ ->
252
      false
253
    | Index i :: q, Const_array cl when Dimension.is_const i ->
254
      unfold_const q (List.nth cl (Dimension.size_const i))
255
    | _, Const_array _ ->
256
      false
257
    | _ ->
258
      assert false
259
  in
260
  let rec unfold offset expr =
261
    match offset, expr.value_desc with
262
    | _, Cst cst ->
263
      unfold_const offset cst
264
    | _, Var _ ->
265
      true
266
    | [], Power _ | [], Array _ ->
267
      false
268
    | Index _ :: q, Power (v, _) ->
269
      unfold q v
270
    | Index i :: q, Array vl when Dimension.is_const i ->
271
      unfold q (List.nth vl (Dimension.size_const i))
272
    | _, Array _ ->
273
      false
274
    | _, Access (v, i) ->
275
      unfold (Index (dimension_of_value i) :: offset) v
276
    | _, Fun (_, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
277
      ->
278
      List.for_all (unfold offset) vl
279
    | _, Fun _ ->
280
      false
281
    | _ ->
282
      assert false
283
  in
284
  unfold [] expr
285

    
286
let basic_unfoldable_assign fanin v expr =
287
  try
288
    let d = Hashtbl.find fanin v.var_id in
289
    is_unfoldable_expr d expr
290
  with Not_found -> false
291

    
292
let unfoldable_assign fanin v expr =
293
  (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
294
  && basic_unfoldable_assign fanin v expr
295

    
296
let merge_elim elim1 elim2 =
297
  let merge _ e1 e2 =
298
    match e1, e2 with
299
    | Some e1, Some e2 ->
300
      if e1 = e2 then Some e1 else None
301
    | _, Some e2 ->
302
      Some e2
303
    | Some e1, _ ->
304
      Some e1
305
    | _ ->
306
      None
307
  in
308
  IMap.merge merge elim1 elim2
309

    
310
(* see if elim has to take in account the provided instr: if so, update elim and
311
   return the remove flag, otherwise, the expression should be kept and elim is
312
   left untouched *)
313
let rec instrs_unfold m fanin elim instrs =
314
  let elim, rev_instrs =
315
    List.fold_left
316
      (fun (elim, instrs) instr ->
317
        (* each subexpression in instr that could be rewritten by the elim set
318
           is rewritten *)
319
        let instr = eliminate m (IMap.map fst elim) instr in
320
        (* if instr is a simple local assign, then (a) elim is simplified with
321
           it (b) it is stored as the elim set *)
322
        instr_unfold m fanin instrs elim instr)
323
      (elim, [])
324
      instrs
325
  in
326
  elim, List.rev rev_instrs
327

    
328
and instr_unfold m fanin instrs (elim : (value_t * eq) IMap.t) instr =
329
  (* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE
330
     IT@." pp_instr instr;*)
331
  match get_instr_desc instr with
332
  (* Simple cases*)
333
  | MStep ([ v ], id, vl)
334
    when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
335
    ->
336
    instr_unfold
337
      m
338
      fanin
339
      instrs
340
      elim
341
      (update_instr_desc
342
         instr
343
         (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
344
  | MLocalAssign (v, expr)
345
    when (not (is_clock_dec_type v.var_dec_type.ty_dec_desc))
346
         && unfoldable_assign fanin v expr ->
347
    (* we don't eliminate clock definitions *)
348
    let new_eq =
349
      Corelang.mkeq
350
        (desome instr.lustre_eq).eq_loc
351
        ([ v.var_id ], (desome instr.lustre_eq).eq_rhs)
352
    in
353
    IMap.add v.var_id (expr, new_eq) elim, instrs
354
  | MBranch (g, hl) when false ->
355
    let elim_branches =
356
      List.map (fun (h, l) -> h, instrs_unfold m fanin elim l) hl
357
    in
358
    let elim, branches =
359
      List.fold_right
360
        (fun (h, (e, l)) (elim, branches) ->
361
          merge_elim elim e, (h, l) :: branches)
362
        elim_branches
363
        (elim, [])
364
    in
365
    elim, update_instr_desc instr (MBranch (g, branches)) :: instrs
366
  | _ ->
367
    elim, instr :: instrs
368
(* default case, we keep the instruction and do not modify elim *)
369

    
370
(** We iterate in the order, recording simple local assigns in an accumulator 1.
371
    each expression is rewritten according to the accumulator 2. local assigns
372
    then rewrite occurrences of the lhs in the computed accumulator *)
373

    
374
let static_call_unfold elim (inst, (n, args)) =
375
  let replace v =
376
    try dimension_of_value (IMap.find v elim)
377
    with Not_found -> Dimension.mkdim_ident Location.dummy v
378
  in
379
  inst, (n, List.map (Dimension.expr_replace_expr replace) args)
380

    
381
(** Perform optimization on machine code: - iterate through step instructions
382
    and remove simple local assigns *)
383
let machine_unfold fanin elim machine =
384
  Log.report ~level:3 (fun fmt ->
385
      Format.fprintf
386
        fmt
387
        "machine_unfold %s %a@ "
388
        machine.mname.node_id
389
        (pp_elim machine)
390
        (IMap.map fst elim));
391
  let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
392
  let elim_vars, instrs =
393
    instrs_unfold machine fanin elim_consts machine.mstep.step_instrs
394
  in
395
  let step_instrs = simplify_instrs_offset machine instrs in
396
  let step_checks =
397
    List.map
398
      (fun (loc, check) ->
399
        loc, eliminate_val machine (IMap.map fst elim_vars) check)
400
      machine.mstep.step_checks
401
  in
402
  let step_locals =
403
    List.filter
404
      (fun v -> not (IMap.mem v.var_id elim_vars))
405
      machine.mstep.step_locals
406
  in
407
  let mtransitions = List.map (eliminate_transition machine (IMap.map fst elim_vars)) machine.mspec.mtransitions in
408
  let elim_consts = IMap.map fst elim_consts in
409
  let minstances =
410
    List.map (static_call_unfold elim_consts) machine.minstances
411
  in
412
  let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls in
413
  ( {
414
      machine with
415
      mstep =
416
        {
417
          machine.mstep with
418
          step_locals;
419
          step_instrs;
420
          step_checks;
421
        };
422
      mspec =
423
        {
424
          machine.mspec with
425
          mtransitions
426
        };
427
      mconst;
428
      minstances;
429
      mcalls;
430
    },
431
    elim_vars )
432

    
433
let instr_of_const top_const =
434
  let const = const_of_top top_const in
435
  let loc = const.const_loc in
436
  let id = const.const_id in
437
  let vdecl =
438
    mkvar_decl
439
      loc
440
      ( id,
441
        mktyp Location.dummy Tydec_any,
442
        mkclock loc Ckdec_any,
443
        true,
444
        None,
445
        None )
446
  in
447
  let vdecl = { vdecl with var_type = const.const_type } in
448
  let lustre_eq =
449
    mkeq loc ([ const.const_id ], mkexpr loc (Expr_const const.const_value))
450
  in
451
  mkinstr
452
    ~lustre_eq
453
    (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
454

    
455
(* We do not perform this optimization on contract nodes since there is not
456
   explicit dependence btw variables and their use in contracts. *)
457
let machines_unfold consts node_schs machines =
458
  List.fold_right
459
    (fun m (machines, removed) ->
460
      let is_contract =
461
        match m.mspec.mnode_spec with Some (Contract _) -> true | _ -> false
462
      in
463
      if is_contract then m :: machines, removed
464
      else
465
        let fanin =
466
          (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table
467
        in
468
        let elim_consts, _ =
469
          instrs_unfold m fanin IMap.empty (List.map instr_of_const consts)
470
        in
471
        let m, removed_m = machine_unfold fanin elim_consts m in
472
        m :: machines, IMap.add m.mname.node_id removed_m removed)
473
    machines
474
    ([], IMap.empty)
475

    
476
let get_assign_lhs instr =
477
  match get_instr_desc instr with
478
  | MLocalAssign (v, e) ->
479
    mk_val (Var v) e.value_type
480
  | MStateAssign (v, e) ->
481
    mk_val (Var v) e.value_type
482
  | _ ->
483
    assert false
484

    
485
let get_assign_rhs instr =
486
  match get_instr_desc instr with
487
  | MLocalAssign (_, e) | MStateAssign (_, e) ->
488
    e
489
  | _ ->
490
    assert false
491

    
492
let is_assign instr =
493
  match get_instr_desc instr with
494
  | MLocalAssign _ | MStateAssign _ ->
495
    true
496
  | _ ->
497
    false
498

    
499
let mk_assign m v e =
500
  match v.value_desc with
501
  | Var v ->
502
    if is_memory m v then MStateAssign (v, e) else MLocalAssign (v, e)
503
  | _ ->
504
    assert false
505

    
506
let rec assigns_instr instr assign =
507
  match get_instr_desc instr with
508
  | MLocalAssign (i, _) | MStateAssign (i, _) ->
509
    VSet.add i assign
510
  | MStep (ol, _, _) ->
511
    List.fold_right VSet.add ol assign
512
  | MBranch (_, hl) ->
513
    List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
514
  | _ ->
515
    assign
516

    
517
and assigns_instrs instrs assign =
518
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
519

    
520
(* and substitute_expr subst expr = match expr with | Var v -> (try IMap.find
521
   expr subst with Not_found -> expr) | Fun (id, vl) -> Fun (id, List.map
522
   (substitute_expr subst) vl) | Array(vl) -> Array(List.map (substitute_expr
523
   subst) vl) | Access(v1, v2) -> Access(substitute_expr subst v1,
524
   substitute_expr subst v2) | Power(v1, v2) -> Power(substitute_expr subst v1,
525
   substitute_expr subst v2) | Cst _ -> expr *)
526

    
527
(** Finds a substitute for [instr] in [instrs], i.e. another instr' with the
528
    same rhs expression. Then substitute this expression with the first assigned
529
    var *)
530
let subst_instr m subst instrs instr =
531
  (* Format.eprintf "subst instr: %a@." (pp_instr m) instr; *)
532
  let instr = eliminate m subst instr in
533
  let instr_v = get_assign_lhs instr in
534
  let instr_e = get_assign_rhs instr in
535
  try
536
    (* Searching for equivalent asssign *)
537
    let instr' =
538
      List.find
539
        (fun instr' -> is_assign instr' && get_assign_rhs instr' = instr_e)
540
        instrs
541
    in
542
    (* Registering the instr_v as instr'_v while replacing *)
543
    match instr_v.value_desc with
544
    | Var v -> (
545
      let instr'_v = get_assign_lhs instr' in
546
      if not (is_memory m v) then
547
        (* The current instruction defines a local variables, ie not memory, we
548
           can just record the relationship and continue *)
549
        IMap.add v.var_id instr'_v subst, instrs
550
      else
551
        (* The current instruction defines a memory. We need to keep the
552
           definition, simplified *)
553
        match instr'_v.value_desc with
554
        | Var v' ->
555
          if not (is_memory m v') then
556
            (* We define v' = v. Don't need to update the records. *)
557
            let instr =
558
              eliminate
559
                m
560
                subst
561
                (update_instr_desc instr (mk_assign m instr_v instr'_v))
562
            in
563
            subst, instr :: instrs
564
          else
565
            (* Last case, v', the lhs of the previous similar definition is,
566
               itself, a memory *)
567

    
568
            (* TODO regarder avec X. Il me semble qu'on peut faire plus
569
               simple: *)
570
            (* Filtering out the list of instructions: - we copy in the same
571
               order the list of instr in instrs (fold_right) - if the current
572
               instr is this instr' then apply the elimination with v' -> v on
573
               instr' before recording it as an instruction. *)
574
            let subst_v' = IMap.add v'.var_id instr_v IMap.empty in
575
            let instrs' =
576
              snd
577
                (List.fold_right
578
                   (fun instr (ok, instrs) ->
579
                     ( ok || instr = instr',
580
                       if ok then instr :: instrs
581
                       else if instr = instr' then instrs
582
                       else eliminate m subst_v' instr :: instrs ))
583
                   instrs
584
                   (false, []))
585
            in
586
            IMap.add v'.var_id instr_v subst, instr :: instrs'
587
        | _ ->
588
          assert false)
589
    | _ ->
590
      assert false
591
  with Not_found ->
592
    (* No such equivalent expr: keeping the definition *)
593
    subst, instr :: instrs
594

    
595
(* - [subst] : hashtable from ident to (simple) definition it is an equivalence
596
   table - [elim] : set of eliminated variables - [instrs] : previous
597
   instructions, which [instr] is compared against - [instr] : current
598
   instruction, normalized by [subst] *)
599

    
600
(** Common sub-expression elimination for machine instructions *)
601
let rec instr_cse m (subst, instrs) instr =
602
  match get_instr_desc instr with
603
  (* Simple cases*)
604
  | MStep ([ v ], id, vl)
605
    when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
606
    ->
607
    instr_cse
608
      m
609
      (subst, instrs)
610
      (update_instr_desc
611
         instr
612
         (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
613
  | MLocalAssign (v, expr) when is_unfoldable_expr 2 expr ->
614
    IMap.add v.var_id expr subst, instr :: instrs
615
  | _ when is_assign instr ->
616
    subst_instr m subst instrs instr
617
  | _ ->
618
    subst, instr :: instrs
619

    
620
(** Apply common sub-expression elimination to a sequence of instrs *)
621
let instrs_cse m subst instrs =
622
  let subst, rev_instrs = List.fold_left (instr_cse m) (subst, []) instrs in
623
  subst, List.rev rev_instrs
624

    
625
(** Apply common sub-expression elimination to a machine - iterate through step
626
    instructions and remove simple local assigns *)
627
let machine_cse subst machine =
628
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@."
629
    pp_elim subst);*)
630
  let _, instrs = instrs_cse machine subst machine.mstep.step_instrs in
631
  let assigned = assigns_instrs instrs VSet.empty in
632
  {
633
    machine with
634
    mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
635
    mstep =
636
      {
637
        machine.mstep with
638
        step_locals =
639
          List.filter
640
            (fun vdecl -> VSet.mem vdecl assigned)
641
            machine.mstep.step_locals;
642
        step_instrs = instrs;
643
      };
644
  }
645

    
646
let machines_cse machines = List.map (machine_cse IMap.empty) machines
647

    
648
(* variable substitution for optimizing purposes *)
649

    
650
(* checks whether an [instr] is skip and can be removed from program *)
651
let rec instr_is_skip instr =
652
  match get_instr_desc instr with
653
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
654
    true
655
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
656
    true
657
  | MBranch (_, hl) ->
658
    List.for_all (fun (_, il) -> instrs_are_skip il) hl
659
  | _ ->
660
    false
661

    
662
and instrs_are_skip instrs = List.for_all instr_is_skip instrs
663

    
664
let instr_cons instr cont = if instr_is_skip instr then cont else instr :: cont
665

    
666
(* XXX: UNUSED *)
667
(* let rec instr_remove_skip instr cont =
668
 *   match get_instr_desc instr with
669
 *   | MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
670
 *     cont
671
 *   | MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
672
 *     cont
673
 *   | MBranch (g, hl) ->
674
 *     update_instr_desc instr
675
 *       (MBranch (g, List.map (fun (h, il) -> h, instrs_remove_skip il []) hl))
676
 *     :: cont
677
 *   | _ ->
678
 *     instr :: cont
679
 *
680
 * and instrs_remove_skip instrs cont =
681
 *   List.fold_right instr_remove_skip instrs cont *)
682

    
683
let rec value_replace_var fvar value =
684
  match value.value_desc with
685
  | Cst _ | ResetFlag ->
686
    value
687
  | Var v ->
688
    { value with value_desc = Var (fvar v) }
689
  | Fun (id, args) ->
690
    { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
691
  | Array vl ->
692
    { value with value_desc = Array (List.map (value_replace_var fvar) vl) }
693
  | Access (t, i) ->
694
    { value with value_desc = Access (value_replace_var fvar t, i) }
695
  | Power (v, n) ->
696
    { value with value_desc = Power (value_replace_var fvar v, n) }
697

    
698
let expr_spec_replace fvar = function
699
  | Val v ->
700
    Val (value_replace_var fvar v)
701
  | Var v ->
702
    Var (fvar v)
703
  | e ->
704
    e
705

    
706
let predicate_spec_replace fvar = function
707
  | Transition (s, f, inst, i, vars, r, mems, insts) ->
708
    Transition
709
      (s, f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts)
710
  | p ->
711
    p
712

    
713
let rec instr_spec_replace fvar =
714
  let aux instr = instr_spec_replace fvar instr in
715
  function
716
  | Equal (e1, e2) ->
717
    Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
718
  | And f ->
719
    And (List.map aux f)
720
  | Or f ->
721
    Or (List.map aux f)
722
  | Imply (a, b) ->
723
    Imply (aux a, aux b)
724
  | Exists (xs, a) ->
725
    let fvar v = if List.mem v xs then v else fvar v in
726
    Exists (xs, instr_spec_replace fvar a)
727
  | Forall (xs, a) ->
728
    let fvar v = if List.mem v xs then v else fvar v in
729
    Forall (xs, instr_spec_replace fvar a)
730
  | Ternary (e, a, b) ->
731
    Ternary (expr_spec_replace fvar e, aux a, aux b)
732
  | Predicate p ->
733
    Predicate (predicate_spec_replace fvar p)
734
  | ExistsMem (f, a, b) ->
735
    ExistsMem (f, aux a, aux b)
736
  | f ->
737
    f
738

    
739
let rec instr_replace_var fvar instr =
740
  let instr_desc =
741
    match instr.instr_desc with
742
    | MLocalAssign (i, v) ->
743
      MLocalAssign (fvar i, value_replace_var fvar v)
744
    | MStateAssign (i, v) ->
745
      MStateAssign (i, value_replace_var fvar v)
746
    | MStep (il, i, vl) ->
747
      MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)
748
    | MBranch (g, hl) ->
749
      MBranch
750
        ( value_replace_var fvar g,
751
          List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )
752
    | MSetReset _
753
    | MNoReset _
754
    | MClearReset
755
    | MResetAssign _
756
    | MSpec _
757
    | MComment _ ->
758
      instr.instr_desc
759
  in
760
  let instr_spec = List.map (instr_spec_replace fvar) instr.instr_spec in
761
  instr_cons { instr with instr_desc; instr_spec }
762

    
763
and instrs_replace_var fvar instrs cont =
764
  List.fold_right (instr_replace_var fvar) instrs cont
765

    
766
let step_replace_var fvar step =
767
  (* Some outputs may have been replaced by locals. We then need to rename those
768
     outputs without changing their clocks, etc *)
769
  let outputs' =
770
    List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs
771
  in
772
  let locals' =
773
    List.fold_left
774
      (fun res l ->
775
        let l' = fvar l in
776
        if List.exists (fun o -> o.var_id = l'.var_id) outputs' then res
777
        else Utils.add_cons l' res)
778
      []
779
      step.step_locals
780
  in
781
  {
782
    step with
783
    step_checks =
784
      List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks;
785
    step_outputs = outputs';
786
    step_locals = locals';
787
    step_instrs = instrs_replace_var fvar step.step_instrs [];
788
  }
789

    
790
let machine_replace_variables fvar m =
791
  { m with mstep = step_replace_var fvar m.mstep }
792

    
793
let machine_reuse_variables reuse m =
794
  let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
795
  machine_replace_variables fvar m
796

    
797
let machines_reuse_variables reuse_tables =
798
  List.map (fun m ->
799
      machine_reuse_variables (Utils.IMap.find m.mname.node_id reuse_tables) m)
800

    
801
let rec instr_assign res instr =
802
  match get_instr_desc instr with
803
  | MLocalAssign (i, _) ->
804
    Disjunction.CISet.add i res
805
  | MStateAssign (i, _) ->
806
    Disjunction.CISet.add i res
807
  | MBranch (_, hl) ->
808
    List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
809
  | MStep (il, _, _) ->
810
    List.fold_right Disjunction.CISet.add il res
811
  | _ ->
812
    res
813

    
814
and instrs_assign res instrs = List.fold_left instr_assign res instrs
815

    
816
let rec instr_constant_assign var instr =
817
  match get_instr_desc instr with
818
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
819
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) ->
820
    i = var
821
  | MBranch (_, hl) ->
822
    List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
823
  | _ ->
824
    false
825

    
826
and instrs_constant_assign var instrs =
827
  List.fold_left
828
    (fun res i ->
829
      if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then
830
        instr_constant_assign var i
831
      else res)
832
    false
833
    instrs
834

    
835
let rec instr_reduce branches instr1 cont =
836
  match get_instr_desc instr1 with
837
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
838
    instr1 :: (List.assoc c branches @ cont)
839
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
840
    instr1 :: (List.assoc c branches @ cont)
841
  | MBranch (g, hl) ->
842
    update_instr_desc
843
      instr1
844
      (MBranch (g, List.map (fun (h, b) -> h, instrs_reduce branches b []) hl))
845
    :: cont
846
  | _ ->
847
    instr1 :: cont
848

    
849
and instrs_reduce branches instrs cont =
850
  match instrs with
851
  | [] ->
852
    cont
853
  | [ i ] ->
854
    instr_reduce branches i cont
855
  | i1 :: i2 :: q ->
856
    i1 :: instrs_reduce branches (i2 :: q) cont
857

    
858
let rec instrs_fusion instrs =
859
  match instrs with
860
  | [] | [ _ ] ->
861
    instrs
862
  | i1 :: i2 :: q -> (
863
    match i2.instr_desc with
864
    | MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 ->
865
      instr_reduce
866
        (List.map (fun (h, b) -> h, instrs_fusion b) hl)
867
        { i1 with instr_spec = i1.instr_spec @ i2.instr_spec }
868
        (instrs_fusion q)
869
    | _ ->
870
      i1 :: instrs_fusion (i2 :: q))
871

    
872
let step_fusion step =
873
  { step with step_instrs = instrs_fusion step.step_instrs }
874

    
875
let machine_fusion m = { m with mstep = step_fusion m.mstep }
876

    
877
let machines_fusion prog = List.map machine_fusion prog
878

    
879
(* Additional function to modify the prog according to removed variables map *)
880

    
881
let elim_prog_variables prog removed_table =
882
  List.map
883
    (fun t ->
884
      match t.top_decl_desc with
885
      | Node nd -> (
886
        match IMap.find_opt nd.node_id removed_table with
887
        | Some nd_elim_map ->
888
          (* Iterating through the elim map to compute - the list of variables
889
             to remove - the associated list of lustre definitions x = expr to
890
             be used when removing these variables *)
891
          let vars_to_replace, defs =
892
            (* Recovering vid from node locals *)
893
            IMap.fold
894
              (fun v (_, eq) (accu_locals, accu_defs) ->
895
                let locals =
896
                  try
897
                    List.find (fun v' -> v'.var_id = v) nd.node_locals
898
                    :: accu_locals
899
                  with Not_found -> accu_locals
900
                  (* Variable v shall be a global constant, we do no need to
901
                     eliminate it from the locals *)
902
                in
903
                (* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc =
904
                   e.expr_loc } in *)
905
                let defs = eq :: accu_defs in
906
                locals, defs)
907
              nd_elim_map
908
              ([], [])
909
          in
910
          let node_locals, node_stmts =
911
            List.fold_right
912
              (fun stmt (locals, res_stmts) ->
913
                match stmt with
914
                | Aut _ ->
915
                  assert false (* should be processed by now *)
916
                | Eq eq -> (
917
                  match eq.eq_lhs with
918
                  | [] ->
919
                    assert false (* shall not happen *)
920
                  | [lhs] when List.exists (fun v -> v.var_id = lhs) vars_to_replace ->
921
                    (* We remove the def *)
922
                    List.filter (fun v -> v.var_id <> lhs) locals, res_stmts
923
                  | _ ->
924
                    (* When more than one lhs we just keep the equation and do
925
                       not delete it *)
926
                    let eq_rhs =
927
                      substitute_expr vars_to_replace defs eq.eq_rhs
928
                    in
929
                    locals, Eq { eq with eq_rhs } :: res_stmts))
930
              nd.node_stmts
931
              (nd.node_locals, [])
932
          in
933
          let nd' = { nd with node_locals; node_stmts } in
934
          { t with top_decl_desc = Node nd' }
935
        | None ->
936
          t)
937
      | _ ->
938
        t)
939
    prog
940

    
941
(*** Main function ***)
942

    
943
(* This functions produces an optimzed prog * machines It 1- eliminates common
944
   sub-expressions (TODO how is this different from normalization?) 2- inline
945
   constants and eliminate duplicated variables 3- try to reuse variables
946
   whenever possible
947

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

    
952
   The function returns both the (possibly updated) prog as well as the
953
   machines *)
954
let optimize params prog node_schs machine_code =
955
  let machine_code =
956
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then (
957
      Log.report ~level:1 (fun fmt ->
958
          Format.fprintf
959
            fmt
960
            "@ @[<v 2>.. machines optimization: sub-expression elimination@ ");
961
      let machine_code = machines_cse machine_code in
962
      Log.report ~level:3 (fun fmt ->
963
          Format.fprintf
964
            fmt
965
            "@[<v 2>.. generated machines (sub-expr elim):@ %a@]@ "
966
            pp_machines
967
            machine_code);
968
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
969
      machine_code)
970
    else machine_code
971
  in
972
  (* Optimize machine code *)
973
  let prog, machine_code, removed_table =
974
    if
975
      !Options.optimization >= 2 && !Options.output <> Options.OutEMF
976
      (*&& !Options.output <> "horn"*)
977
    then (
978
      Log.report ~level:1 (fun fmt ->
979
          Format.fprintf
980
            fmt
981
            "@ @[<v 2>.. machines optimization: const. inlining (partial eval. \
982
             with const)@ ");
983
      let machine_code, removed_table =
984
        machines_unfold (Corelang.get_consts prog) node_schs machine_code
985
      in
986
      Log.report ~level:3 (fun fmt ->
987
          Format.fprintf
988
            fmt
989
            "@ Eliminated flows: %a@ "
990
            (IMap.pp (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m)))
991
            removed_table);
992
      (* If variables were eliminated, relaunch the normalization/machine
993
         generation *)
994
      let prog, machine_code, removed_table =
995
        if IMap.is_empty removed_table then
996
          (* stopping here, no need to reupdate the prog *)
997
          prog, machine_code, removed_table
998
        else
999
          let prog = elim_prog_variables prog removed_table in
1000
          (* Mini stage1 *)
1001
          let prog = Normalization.normalize_prog ~first:false params prog in
1002
          let prog = SortProg.sort_nodes_locals prog in
1003
          (* Mini stage2: note that we do not protect against alg. loop since
1004
             this should have been handled before *)
1005
          let prog, node_schs = Scheduling.schedule_prog prog in
1006
          let machine_code = Machine_code.translate_prog prog node_schs in
1007
          (* Mini stage2 machine optimiation *)
1008
          let machine_code, removed_table =
1009
            machines_unfold (Corelang.get_consts prog) node_schs machine_code
1010
          in
1011
          prog, machine_code, removed_table
1012
      in
1013
      Log.report ~level:3 (fun fmt ->
1014
          Format.fprintf
1015
            fmt
1016
            "@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "
1017
            pp_machines
1018
            machine_code);
1019
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
1020
      prog, machine_code, removed_table)
1021
    else prog, machine_code, IMap.empty
1022
  in
1023
  (* Optimize machine code *)
1024
  let machine_code =
1025
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then (
1026
      Log.report ~level:1 (fun fmt ->
1027
          Format.fprintf
1028
            fmt
1029
            ".. machines optimization: minimize stack usage by reusing \
1030
             variables@,");
1031
      let node_schs =
1032
        Scheduling.remove_prog_inlined_locals removed_table node_schs
1033
      in
1034
      let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
1035
      machines_fusion (machines_reuse_variables reuse_tables machine_code))
1036
    else machine_code
1037
  in
1038

    
1039
  prog, machine_code
1040

    
1041
(* Local Variables: *)
1042
(* compile-command:"make -C .." *)
1043
(* End: *)
(60-60/99)