Project

General

Profile

Download (36.5 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 f (IMap.find v.var_id elim) with Not_found -> a
27

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

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

    
60
let eliminate_pred m elim = function
61
  (* the transition is local to the machine *)
62
  | Transition (s, f, inst, Some i, vars, r, mems, insts) ->
63
    let vars =
64
      List.filter_map
65
        (function
66
          | Spec_types.Val v -> (
67
            match v.value_desc with
68
            | Var vd when IMap.mem vd.var_id elim ->
69
              None
70
            | _ ->
71
              Some (Val v))
72
          | Spec_types.Var vd when IMap.mem vd.var_id elim ->
73
            None
74
          | e ->
75
            Some (eliminate_expr m elim e))
76
        vars
77
    in
78
    Transition (s, f, inst, Some i, vars, r, mems, insts)
79
  (* the transition is not local to the machine *)
80
  | Transition (s, f, inst, None, vars, r, mems, insts) ->
81
    let vars = List.map (eliminate_expr m elim) vars in
82
    Transition (s, f, inst, None, vars, r, mems, insts)
83
  | p ->
84
    p
85

    
86
let rec eliminate_formula m elim =
87
  let e_expr = eliminate_expr m elim in
88
  let e_instr i = eliminate_formula m elim i in
89
  let e_pred = eliminate_pred m elim in
90
  function
91
  | Equal (e1, e2) ->
92
    Equal (e_expr e1, e_expr e2)
93
  | GEqual (e1, e2) ->
94
    GEqual (e_expr e1, e_expr e2)
95
  | And f ->
96
    And (List.map e_instr f)
97
  | Or f ->
98
    Or (List.map e_instr f)
99
  | Imply (a, b) ->
100
    Imply (e_instr a, e_instr b)
101
  | Exists (xs, a) ->
102
    let xs = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) xs in
103
    Exists (xs, eliminate_formula m elim a)
104
  | Forall (xs, a) ->
105
    let xs = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) xs in
106
    Forall (xs, eliminate_formula m elim a)
107
  | Ternary (e, a, b) ->
108
    Ternary (e_expr e, e_instr a, e_instr b)
109
  | Predicate p ->
110
    Predicate (e_pred p)
111
  | ExistsMem (f, a, b) ->
112
    ExistsMem (f, e_instr a, e_instr b)
113
  | Value v ->
114
    Value (eliminate_val m elim v)
115
  | f ->
116
    f
117

    
118
let rec eliminate m elim instr =
119
  let e_val = eliminate_val m elim in
120
  let instr =
121
    {
122
      instr with
123
      instr_spec = List.map (eliminate_formula m elim) instr.instr_spec;
124
    }
125
  in
126
  match get_instr_desc instr with
127
  | MLocalAssign (i, v) ->
128
    update_instr_desc instr (MLocalAssign (i, e_val v))
129
  | MStateAssign (i, v) ->
130
    update_instr_desc instr (MStateAssign (i, e_val v))
131
  | MSetReset _
132
  | MNoReset _
133
  | MClearReset
134
  | MResetAssign _
135
  | MSpec _
136
  | MComment _ ->
137
    instr
138
  | MStep (il, i, vl) ->
139
    update_instr_desc instr (MStep (il, i, List.map e_val vl))
140
  | MBranch (g, hl) ->
141
    update_instr_desc
142
      instr
143
      (MBranch
144
         ( e_val g,
145
           List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl ))
146

    
147
let rec fv_value m s v =
148
  match v.value_desc with
149
  | Var v ->
150
    if is_memory m v then s else VSet.add v s
151
  | Fun (_, vl) | Array vl ->
152
    List.fold_left (fv_value m) s vl
153
  | Access (v1, v2) | Power (v1, v2) ->
154
    fv_value m (fv_value m s v1) v2
155
  | _ ->
156
    s
157

    
158
let fv_expr m s = function
159
  | Val v ->
160
    fv_value m s v
161
  | Var v ->
162
    if is_memory m v then s else VSet.add v s
163
  | _ ->
164
    s
165

    
166
let fv_predicate m s = function
167
  | Transition (_, _, _, _, vars, _, _, _) ->
168
    List.fold_left (fv_expr m) s vars
169
  | _ ->
170
    s
171

    
172
let rec fv_formula m s = function
173
  | Equal (e1, e2) | GEqual (e1, e2) ->
174
    fv_expr m (fv_expr m s e1) e2
175
  | And f | Or f ->
176
    List.fold_left (fv_formula m) s f
177
  | Imply (a, b) | ExistsMem (_, a, b) ->
178
    fv_formula m (fv_formula m s a) b
179
  | Exists (xs, a) | Forall (xs, a) ->
180
    VSet.filter (fun v -> not (List.mem v xs)) (fv_formula m s a)
181
  | Ternary (e, a, b) ->
182
    fv_expr m (fv_formula m (fv_formula m s a) b) e
183
  | Predicate p ->
184
    fv_predicate m s p
185
  | Value v ->
186
    fv_value m s v
187
  | _ ->
188
    s
189

    
190
let eliminate_transition m elim t =
191
  let tvars = List.filter (fun vd -> not (IMap.mem vd.var_id elim)) t.tvars in
192
  let tformula = eliminate_formula m elim t.tformula in
193
  let fv =
194
    VSet.(elements (diff (fv_formula m empty tformula) (of_list tvars)))
195
  in
196
  let tformula = Exists (fv, tformula) in
197
  { t with tvars; tformula }
198

    
199
(* XXX: UNUSED *)
200
(* let eliminate_dim elim dim =
201
 *   Dimension.expr_replace_expr
202
 *     (fun v ->
203
 *       try dimension_of_value (IMap.find v elim)
204
 *       with Not_found -> mkdim_ident dim.dim_loc v)
205
 *     dim *)
206

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

    
210
let unfold_expr_offset m offset expr =
211
  List.fold_left
212
    (fun res -> function
213
      | Index i ->
214
        mk_val
215
          (Access (res, value_of_dimension m i))
216
          (Types.array_element_type res.value_type)
217
      | Field _ ->
218
        Format.eprintf "internal error: not yet implemented !";
219
        assert false)
220
    expr
221
    offset
222

    
223
let rec simplify_cst_expr m offset typ cst =
224
  match offset, cst with
225
  | [], _ ->
226
    mk_val (Cst cst) typ
227
  | Index i :: q, Const_array cl when Dimension.is_const i ->
228
    let elt_typ = Types.array_element_type typ in
229
    simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const i))
230
  | Index i :: q, Const_array cl ->
231
    let elt_typ = Types.array_element_type typ in
232
    unfold_expr_offset
233
      m
234
      [ Index i ]
235
      (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
236
  | Field f :: q, Const_struct fl ->
237
    let fld_typ = Types.struct_field_type typ f in
238
    simplify_cst_expr m q fld_typ (List.assoc f fl)
239
  | _ ->
240
    Format.eprintf
241
      "internal error: Optimize_machine.simplify_cst_expr %a@."
242
      Printers.pp_const
243
      cst;
244
    assert false
245

    
246
let simplify_expr_offset m expr =
247
  let rec simplify offset expr =
248
    match offset, expr.value_desc with
249
    | Field _ :: _, _ ->
250
      failwith "not yet implemented"
251
    | _, Fun (id, vl) when Basic_library.is_value_internal_fun expr ->
252
      mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
253
    | _, Fun _ | _, Var _ ->
254
      unfold_expr_offset m offset expr
255
    | _, Cst cst ->
256
      simplify_cst_expr m offset expr.value_type cst
257
    | _, Access (expr, i) ->
258
      simplify (Index (dimension_of_value i) :: offset) expr
259
    | _, ResetFlag ->
260
      expr
261
    | [], _ ->
262
      expr
263
    | Index _ :: q, Power (expr, _) ->
264
      simplify q expr
265
    | Index i :: q, Array vl when Dimension.is_const i ->
266
      simplify q (List.nth vl (Dimension.size_const i))
267
    | Index i :: q, Array vl ->
268
      unfold_expr_offset
269
        m
270
        [ Index i ]
271
        (mk_val (Array (List.map (simplify q) vl)) expr.value_type)
272
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr
273
      (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
274
      with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr
275
      (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
276
  in
277
  simplify [] expr
278

    
279
let rec simplify_instr_offset m instr =
280
  match get_instr_desc instr with
281
  | MLocalAssign (v, expr) ->
282
    update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
283
  | MStateAssign (v, expr) ->
284
    update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
285
  | MSetReset _
286
  | MNoReset _
287
  | MClearReset
288
  | MResetAssign _
289
  | MSpec _
290
  | MComment _ ->
291
    instr
292
  | MStep (outputs, id, inputs) ->
293
    update_instr_desc
294
      instr
295
      (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
296
  | MBranch (cond, brl) ->
297
    update_instr_desc
298
      instr
299
      (MBranch
300
         ( simplify_expr_offset m cond,
301
           List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl ))
302

    
303
and simplify_instrs_offset m instrs = List.map (simplify_instr_offset m) instrs
304

    
305
(* XXX: UNUSED *)
306
(* let is_scalar_const c =
307
 *   match c with Const_real _ | Const_int _ | Const_tag _ -> true | _ -> false *)
308

    
309
(* An instruction v = expr may (and will) be unfolded iff: - either expr is
310
   atomic (no complex expressions, only const, vars and array/struct accesses) -
311
   or v has a fanin <= 1 (used at most once) *)
312
let is_unfoldable_expr fanin expr =
313
  let rec unfold_const offset cst =
314
    match offset, cst with
315
    | _, Const_int _ | _, Const_real _ | _, Const_tag _ ->
316
      true
317
    | Field f :: q, Const_struct fl ->
318
      unfold_const q (List.assoc f fl)
319
    | [], Const_struct _ ->
320
      false
321
    | Index i :: q, Const_array cl when Dimension.is_const i ->
322
      unfold_const q (List.nth cl (Dimension.size_const i))
323
    | _, Const_array _ ->
324
      false
325
    | _ ->
326
      assert false
327
  in
328
  let rec unfold offset expr =
329
    match offset, expr.value_desc with
330
    | _, Cst cst ->
331
      unfold_const offset cst
332
    | _, Var _ ->
333
      true
334
    | [], Power _ | [], Array _ ->
335
      false
336
    | Index _ :: q, Power (v, _) ->
337
      unfold q v
338
    | Index i :: q, Array vl when Dimension.is_const i ->
339
      unfold q (List.nth vl (Dimension.size_const i))
340
    | _, Array _ ->
341
      false
342
    | _, Access (v, i) ->
343
      unfold (Index (dimension_of_value i) :: offset) v
344
    | _, Fun (_, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
345
      ->
346
      List.for_all (unfold offset) vl
347
    | _, Fun _ ->
348
      false
349
    | _ ->
350
      assert false
351
  in
352
  unfold [] expr
353

    
354
let basic_unfoldable_assign fanin v expr =
355
  try
356
    let d = Hashtbl.find fanin v.var_id in
357
    is_unfoldable_expr d expr
358
  with Not_found -> false
359

    
360
let unfoldable_assign fanin v expr =
361
  (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
362
  && basic_unfoldable_assign fanin v expr
363

    
364
let merge_elim elim1 elim2 =
365
  let merge _ e1 e2 =
366
    match e1, e2 with
367
    | Some e1, Some e2 ->
368
      if e1 = e2 then Some e1 else None
369
    | _, Some e2 ->
370
      Some e2
371
    | Some e1, _ ->
372
      Some e1
373
    | _ ->
374
      None
375
  in
376
  IMap.merge merge elim1 elim2
377

    
378
(* see if elim has to take in account the provided instr: if so, update elim and
379
   return the remove flag, otherwise, the expression should be kept and elim is
380
   left untouched *)
381
let instrs_unfold m fanin elim instrs =
382
  let rec gather_elim ((elim, instrs) as acc) instr =
383
    match get_instr_desc instr with
384
    | MStep ([ v ], id, vl)
385
      when Basic_library.is_value_internal_fun
386
             (mk_val (Fun (id, vl)) v.var_type) ->
387
      gather_elim
388
        acc
389
        (update_instr_desc
390
           instr
391
           (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
392
    | MLocalAssign (v, expr)
393
      when (not (is_clock_dec_type v.var_dec_type.ty_dec_desc))
394
           && unfoldable_assign fanin v expr ->
395
      (* we don't eliminate clock definitions *)
396
      let new_eq =
397
        Corelang.mkeq
398
          (desome instr.lustre_eq).eq_loc
399
          ([ v.var_id ], (desome instr.lustre_eq).eq_rhs)
400
      in
401
      IMap.add v.var_id (expr, new_eq) elim, instr :: instrs
402
    | MBranch (g, hl) ->
403
      let elim, hl =
404
        List.fold_left
405
          (fun (elim', hl) (h, l) ->
406
            let elim, l = List.fold_left gather_elim (elim, []) l in
407
            merge_elim elim' elim, (h, List.rev l) :: hl)
408
          (elim, [])
409
          hl
410
      in
411
      elim, update_instr_desc instr (MBranch (g, List.rev hl)) :: instrs
412
    | _ ->
413
      elim, instr :: instrs
414
  in
415
  let elim, instrs = List.fold_left gather_elim (elim, []) instrs in
416
  let rec filter instrs =
417
    List.filter_map
418
      (fun instr ->
419
        match get_instr_desc instr with
420
        | MLocalAssign (v, expr)
421
          when (not (is_clock_dec_type v.var_dec_type.ty_dec_desc))
422
               && unfoldable_assign fanin v expr
423
               && IMap.mem v.var_id elim ->
424
          None
425
        | MBranch (g, hl) ->
426
          let instr =
427
            update_instr_desc
428
              instr
429
              (MBranch (g, List.map (fun (h, l) -> h, filter l) hl))
430
          in
431
          Some (eliminate m (IMap.map fst elim) instr)
432
        | _ ->
433
          Some (eliminate m (IMap.map fst elim) instr))
434
      instrs
435
  in
436
  elim, List.rev (filter instrs)
437

    
438
(** We iterate in the order, recording simple local assigns in an accumulator 1.
439
    each expression is rewritten according to the accumulator 2. local assigns
440
    then rewrite occurrences of the lhs in the computed accumulator *)
441

    
442
let static_call_unfold elim (inst, (n, args)) =
443
  let replace v =
444
    try dimension_of_value (IMap.find v elim)
445
    with Not_found -> Dimension.mkdim_ident Location.dummy v
446
  in
447
  inst, (n, List.map (Dimension.expr_replace_expr replace) args)
448

    
449
(** Perform optimization on machine code: - iterate through step instructions
450
    and remove simple local assigns *)
451
let machine_unfold fanin elim machine =
452
  let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
453
  let elim_vars, instrs =
454
    instrs_unfold machine fanin elim_consts machine.mstep.step_instrs
455
  in
456
  Log.report ~level:3 (fun fmt ->
457
      Format.fprintf
458
        fmt
459
        "@[<v 2>machine_unfold %s@;from %a@;to   %a@]"
460
        machine.mname.node_id
461
        (pp_elim machine)
462
        (IMap.map fst elim)
463
        (pp_elim machine)
464
        (IMap.map fst elim_vars));
465
  let step_instrs = simplify_instrs_offset machine instrs in
466
  let step_checks =
467
    List.map
468
      (fun (loc, check) ->
469
        loc, eliminate_val machine (IMap.map fst elim_vars) check)
470
      machine.mstep.step_checks
471
  in
472
  let step_locals =
473
    List.filter
474
      (fun v -> not (IMap.mem v.var_id elim_vars))
475
      machine.mstep.step_locals
476
  in
477
  let mtransitions =
478
    List.map
479
      (eliminate_transition machine (IMap.map fst elim_vars))
480
      machine.mspec.mtransitions
481
  in
482
  let elim_consts = IMap.map fst elim_consts in
483
  let minstances =
484
    List.map (static_call_unfold elim_consts) machine.minstances
485
  in
486
  let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls in
487
  ( {
488
      machine with
489
      mstep = { machine.mstep with step_locals; step_instrs; step_checks };
490
      mspec = { machine.mspec with mtransitions };
491
      mconst;
492
      minstances;
493
      mcalls;
494
    },
495
    elim_vars )
496

    
497
let instr_of_const top_const =
498
  let const = const_of_top top_const in
499
  let loc = const.const_loc in
500
  let id = const.const_id in
501
  let vdecl =
502
    mkvar_decl
503
      loc
504
      ( id,
505
        mktyp Location.dummy Tydec_any,
506
        mkclock loc Ckdec_any,
507
        true,
508
        None,
509
        None )
510
  in
511
  let vdecl = { vdecl with var_type = const.const_type } in
512
  let lustre_eq =
513
    mkeq loc ([ const.const_id ], mkexpr loc (Expr_const const.const_value))
514
  in
515
  mkinstr
516
    ~lustre_eq
517
    (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
518

    
519
(* We do not perform this optimization on contract nodes since there is not
520
   explicit dependence btw variables and their use in contracts. *)
521
let machines_unfold consts node_schs machines =
522
  List.fold_right
523
    (fun m (machines, removed) ->
524
      let is_contract =
525
        match m.mspec.mnode_spec with Some (Contract _) -> true | _ -> false
526
      in
527
      if is_contract then m :: machines, removed
528
      else
529
        let fanin =
530
          (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table
531
        in
532
        let elim_consts, _ =
533
          instrs_unfold m fanin IMap.empty (List.map instr_of_const consts)
534
        in
535
        let m, removed_m = machine_unfold fanin elim_consts m in
536
        m :: machines, IMap.add m.mname.node_id removed_m removed)
537
    machines
538
    ([], IMap.empty)
539

    
540
let get_assign_lhs instr =
541
  match get_instr_desc instr with
542
  | MLocalAssign (v, e) ->
543
    mk_val (Var v) e.value_type
544
  | MStateAssign (v, e) ->
545
    mk_val (Var v) e.value_type
546
  | _ ->
547
    assert false
548

    
549
let get_assign_rhs instr =
550
  match get_instr_desc instr with
551
  | MLocalAssign (_, e) | MStateAssign (_, e) ->
552
    e
553
  | _ ->
554
    assert false
555

    
556
let is_assign instr =
557
  match get_instr_desc instr with
558
  | MLocalAssign _ | MStateAssign _ ->
559
    true
560
  | _ ->
561
    false
562

    
563
let mk_assign m v e =
564
  match v.value_desc with
565
  | Var v ->
566
    if is_memory m v then MStateAssign (v, e) else MLocalAssign (v, e)
567
  | _ ->
568
    assert false
569

    
570
let rec assigns_instr instr assign =
571
  match get_instr_desc instr with
572
  | MLocalAssign (i, _) | MStateAssign (i, _) ->
573
    VSet.add i assign
574
  | MStep (ol, _, _) ->
575
    List.fold_right VSet.add ol assign
576
  | MBranch (_, hl) ->
577
    List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
578
  | _ ->
579
    assign
580

    
581
and assigns_instrs instrs assign =
582
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
583

    
584
(* and substitute_expr subst expr = match expr with | Var v -> (try IMap.find
585
   expr subst with Not_found -> expr) | Fun (id, vl) -> Fun (id, List.map
586
   (substitute_expr subst) vl) | Array(vl) -> Array(List.map (substitute_expr
587
   subst) vl) | Access(v1, v2) -> Access(substitute_expr subst v1,
588
   substitute_expr subst v2) | Power(v1, v2) -> Power(substitute_expr subst v1,
589
   substitute_expr subst v2) | Cst _ -> expr *)
590

    
591
(** Finds a substitute for [instr] in [instrs], i.e. another instr' with the
592
    same rhs expression. Then substitute this expression with the first assigned
593
    var *)
594
let subst_instr m subst instrs instr =
595
  (* Format.eprintf "subst instr: %a@." (pp_instr m) instr; *)
596
  let instr = eliminate m subst instr in
597
  let instr_v = get_assign_lhs instr in
598
  let instr_e = get_assign_rhs instr in
599
  try
600
    (* Searching for equivalent asssign *)
601
    let instr' =
602
      List.find
603
        (fun instr' -> is_assign instr' && get_assign_rhs instr' = instr_e)
604
        instrs
605
    in
606
    (* Registering the instr_v as instr'_v while replacing *)
607
    match instr_v.value_desc with
608
    | Var v -> (
609
      let instr'_v = get_assign_lhs instr' in
610
      if not (is_memory m v) then
611
        (* The current instruction defines a local variables, ie not memory, we
612
           can just record the relationship and continue *)
613
        IMap.add v.var_id instr'_v subst, instrs
614
      else
615
        (* The current instruction defines a memory. We need to keep the
616
           definition, simplified *)
617
        match instr'_v.value_desc with
618
        | Var v' ->
619
          if not (is_memory m v') then
620
            (* We define v' = v. Don't need to update the records. *)
621
            let instr =
622
              eliminate
623
                m
624
                subst
625
                (update_instr_desc instr (mk_assign m instr_v instr'_v))
626
            in
627
            subst, instr :: instrs
628
          else
629
            (* Last case, v', the lhs of the previous similar definition is,
630
               itself, a memory *)
631

    
632
            (* TODO regarder avec X. Il me semble qu'on peut faire plus
633
               simple: *)
634
            (* Filtering out the list of instructions: - we copy in the same
635
               order the list of instr in instrs (fold_right) - if the current
636
               instr is this instr' then apply the elimination with v' -> v on
637
               instr' before recording it as an instruction. *)
638
            let subst_v' = IMap.add v'.var_id instr_v IMap.empty in
639
            let instrs' =
640
              snd
641
                (List.fold_right
642
                   (fun instr (ok, instrs) ->
643
                     ( ok || instr = instr',
644
                       if ok then instr :: instrs
645
                       else if instr = instr' then instrs
646
                       else eliminate m subst_v' instr :: instrs ))
647
                   instrs
648
                   (false, []))
649
            in
650
            IMap.add v'.var_id instr_v subst, instr :: instrs'
651
        | _ ->
652
          assert false)
653
    | _ ->
654
      assert false
655
  with Not_found ->
656
    (* No such equivalent expr: keeping the definition *)
657
    subst, instr :: instrs
658

    
659
(* - [subst] : hashtable from ident to (simple) definition it is an equivalence
660
   table - [elim] : set of eliminated variables - [instrs] : previous
661
   instructions, which [instr] is compared against - [instr] : current
662
   instruction, normalized by [subst] *)
663

    
664
(** Common sub-expression elimination for machine instructions *)
665
let rec instr_cse m (subst, instrs) instr =
666
  match get_instr_desc instr with
667
  (* Simple cases*)
668
  | MStep ([ v ], id, vl)
669
    when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
670
    ->
671
    instr_cse
672
      m
673
      (subst, instrs)
674
      (update_instr_desc
675
         instr
676
         (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
677
  | MLocalAssign (v, expr) when is_unfoldable_expr 2 expr ->
678
    IMap.add v.var_id expr subst, instr :: instrs
679
  | _ when is_assign instr ->
680
    subst_instr m subst instrs instr
681
  | _ ->
682
    subst, instr :: instrs
683

    
684
(** Apply common sub-expression elimination to a sequence of instrs *)
685
let instrs_cse m subst instrs =
686
  let subst, rev_instrs = List.fold_left (instr_cse m) (subst, []) instrs in
687
  subst, List.rev rev_instrs
688

    
689
(** Apply common sub-expression elimination to a machine - iterate through step
690
    instructions and remove simple local assigns *)
691
let machine_cse subst machine =
692
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@."
693
    pp_elim subst);*)
694
  let _, instrs = instrs_cse machine subst machine.mstep.step_instrs in
695
  let assigned = assigns_instrs instrs VSet.empty in
696
  {
697
    machine with
698
    mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
699
    mstep =
700
      {
701
        machine.mstep with
702
        step_locals =
703
          List.filter
704
            (fun vdecl -> VSet.mem vdecl assigned)
705
            machine.mstep.step_locals;
706
        step_instrs = instrs;
707
      };
708
  }
709

    
710
let machines_cse machines = List.map (machine_cse IMap.empty) machines
711

    
712
(* variable substitution for optimizing purposes *)
713

    
714
(* checks whether an [instr] is skip and can be removed from program *)
715
let rec instr_is_skip instr =
716
  match get_instr_desc instr with
717
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
718
    true
719
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
720
    true
721
  | MBranch (_, hl) ->
722
    List.for_all (fun (_, il) -> instrs_are_skip il) hl
723
  | _ ->
724
    false
725

    
726
and instrs_are_skip instrs = List.for_all instr_is_skip instrs
727

    
728
let instr_cons instr cont = if instr_is_skip instr then cont else instr :: cont
729

    
730
(* XXX: UNUSED *)
731
(* let rec instr_remove_skip instr cont =
732
 *   match get_instr_desc instr with
733
 *   | MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
734
 *     cont
735
 *   | MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
736
 *     cont
737
 *   | MBranch (g, hl) ->
738
 *     update_instr_desc instr
739
 *       (MBranch (g, List.map (fun (h, il) -> h, instrs_remove_skip il []) hl))
740
 *     :: cont
741
 *   | _ ->
742
 *     instr :: cont
743
 *
744
 * and instrs_remove_skip instrs cont =
745
 *   List.fold_right instr_remove_skip instrs cont *)
746

    
747
let rec value_replace_var fvar value =
748
  match value.value_desc with
749
  | Cst _ | ResetFlag ->
750
    value
751
  | Var v ->
752
    { value with value_desc = Var (fvar v) }
753
  | Fun (id, args) ->
754
    { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
755
  | Array vl ->
756
    { value with value_desc = Array (List.map (value_replace_var fvar) vl) }
757
  | Access (t, i) ->
758
    { value with value_desc = Access (value_replace_var fvar t, i) }
759
  | Power (v, n) ->
760
    { value with value_desc = Power (value_replace_var fvar v, n) }
761

    
762
let expr_spec_replace fvar = function
763
  | Val v ->
764
    Val (value_replace_var fvar v)
765
  | Var v ->
766
    Var (fvar v)
767
  | e ->
768
    e
769

    
770
let predicate_spec_replace fvar = function
771
  | Transition (s, f, inst, i, vars, r, mems, insts) ->
772
    Transition
773
      (s, f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts)
774
  | p ->
775
    p
776

    
777
let rec instr_spec_replace fvar =
778
  let aux instr = instr_spec_replace fvar instr in
779
  function
780
  | Equal (e1, e2) ->
781
    Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
782
  | GEqual (e1, e2) ->
783
    GEqual (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
784
  | And f ->
785
    And (List.map aux f)
786
  | Or f ->
787
    Or (List.map aux f)
788
  | Imply (a, b) ->
789
    Imply (aux a, aux b)
790
  | Exists (xs, a) ->
791
    let fvar v = if List.mem v xs then v else fvar v in
792
    Exists (xs, instr_spec_replace fvar a)
793
  | Forall (xs, a) ->
794
    let fvar v = if List.mem v xs then v else fvar v in
795
    Forall (xs, instr_spec_replace fvar a)
796
  | Ternary (e, a, b) ->
797
    Ternary (expr_spec_replace fvar e, aux a, aux b)
798
  | Predicate p ->
799
    Predicate (predicate_spec_replace fvar p)
800
  | ExistsMem (f, a, b) ->
801
    ExistsMem (f, aux a, aux b)
802
  | f ->
803
    f
804

    
805
let rec instr_replace_var fvar instr =
806
  let instr_desc =
807
    match instr.instr_desc with
808
    | MLocalAssign (i, v) ->
809
      MLocalAssign (fvar i, value_replace_var fvar v)
810
    | MStateAssign (i, v) ->
811
      MStateAssign (i, value_replace_var fvar v)
812
    | MStep (il, i, vl) ->
813
      MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)
814
    | MBranch (g, hl) ->
815
      MBranch
816
        ( value_replace_var fvar g,
817
          List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )
818
    | MSetReset _
819
    | MNoReset _
820
    | MClearReset
821
    | MResetAssign _
822
    | MSpec _
823
    | MComment _ ->
824
      instr.instr_desc
825
  in
826
  let instr_spec = List.map (instr_spec_replace fvar) instr.instr_spec in
827
  instr_cons { instr with instr_desc; instr_spec }
828

    
829
and instrs_replace_var fvar instrs cont =
830
  List.fold_right (instr_replace_var fvar) instrs cont
831

    
832
let step_replace_var fvar step =
833
  (* Some outputs may have been replaced by locals. We then need to rename those
834
     outputs without changing their clocks, etc *)
835
  let outputs' =
836
    List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs
837
  in
838
  let locals' =
839
    List.fold_left
840
      (fun res l ->
841
        let l' = fvar l in
842
        if List.exists (fun o -> o.var_id = l'.var_id) outputs' then res
843
        else Utils.add_cons l' res)
844
      []
845
      step.step_locals
846
  in
847
  {
848
    step with
849
    step_checks =
850
      List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks;
851
    step_outputs = outputs';
852
    step_locals = locals';
853
    step_instrs = instrs_replace_var fvar step.step_instrs [];
854
  }
855

    
856
let machine_replace_variables fvar m =
857
  { m with mstep = step_replace_var fvar m.mstep }
858

    
859
let machine_reuse_variables reuse m =
860
  let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
861
  machine_replace_variables fvar m
862

    
863
let machines_reuse_variables reuse_tables =
864
  List.map (fun m ->
865
      machine_reuse_variables (Utils.IMap.find m.mname.node_id reuse_tables) m)
866

    
867
let rec instr_assign res instr =
868
  match get_instr_desc instr with
869
  | MLocalAssign (i, _) ->
870
    Disjunction.CISet.add i res
871
  | MStateAssign (i, _) ->
872
    Disjunction.CISet.add i res
873
  | MBranch (_, hl) ->
874
    List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
875
  | MStep (il, _, _) ->
876
    List.fold_right Disjunction.CISet.add il res
877
  | _ ->
878
    res
879

    
880
and instrs_assign res instrs = List.fold_left instr_assign res instrs
881

    
882
let rec instr_constant_assign var instr =
883
  match get_instr_desc instr with
884
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
885
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) ->
886
    i = var
887
  | MBranch (_, hl) ->
888
    List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
889
  | _ ->
890
    false
891

    
892
and instrs_constant_assign var instrs =
893
  List.fold_left
894
    (fun res i ->
895
      if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then
896
        instr_constant_assign var i
897
      else res)
898
    false
899
    instrs
900

    
901
let rec instr_reduce branches instr1 cont =
902
  match get_instr_desc instr1 with
903
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _ })
904
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
905
    instr1 :: (List.assoc c branches @ cont)
906
  | MBranch (g, hl) ->
907
    update_instr_desc
908
      instr1
909
      (MBranch (g, List.map (fun (h, b) -> h, instrs_reduce branches b []) hl))
910
    :: cont
911
  | _ ->
912
    instr1 :: cont
913

    
914
and instrs_reduce branches instrs cont =
915
  match instrs with
916
  | [] ->
917
    cont
918
  | [ i ] ->
919
    instr_reduce branches i cont
920
  | i1 :: i2 :: q ->
921
    i1 :: instrs_reduce branches (i2 :: q) cont
922

    
923
let rec instrs_fusion instrs =
924
  match instrs with
925
  | [] | [ _ ] ->
926
    instrs
927
  | i1 :: i2 :: q -> (
928
    match i2.instr_desc with
929
    | MBranch ({ value_desc = Var v; _ }, hl) when instr_constant_assign v i1 ->
930
      instr_reduce
931
        (List.map (fun (h, b) -> h, instrs_fusion b) hl)
932
        { i1 with instr_spec = i1.instr_spec @ i2.instr_spec }
933
        (instrs_fusion q)
934
    | _ ->
935
      i1 :: instrs_fusion (i2 :: q))
936

    
937
let step_fusion step =
938
  { step with step_instrs = instrs_fusion step.step_instrs }
939

    
940
let machine_fusion m =
941
  let m = { m with mstep = step_fusion m.mstep } in
942
  let unused = Machine_code_dep.compute_unused_variables m in
943
  let is_used v = not (ISet.mem v.var_id unused) in
944
  let step_locals = List.filter is_used m.mstep.step_locals in
945
  let rec filter_instrs instrs =
946
    List.filter_map (fun instr -> match get_instr_desc instr with
947
        | MLocalAssign (v, _) ->
948
          if is_used v then Some instr else None
949
        | MBranch (e, hl) ->
950
          Some (update_instr_desc instr
951
                  (MBranch (e, List.map (fun (h, l) -> h, filter_instrs l) hl)))
952
        | _ -> Some instr) instrs
953
  in
954
  let step_instrs = filter_instrs m.mstep.step_instrs in
955
  { m with mstep = { m.mstep with step_locals; step_instrs }}
956
  (* List.iter (fun (g, u) -> Format.printf "%a@;%a@." pp_dep_graph g ISet.pp u) gs; *)
957

    
958
let machines_fusion prog = List.map machine_fusion prog
959

    
960
(* Additional function to modify the prog according to removed variables map *)
961

    
962
let elim_prog_variables prog removed_table =
963
  List.map
964
    (fun t ->
965
      match t.top_decl_desc with
966
      | Node nd -> (
967
        match IMap.find_opt nd.node_id removed_table with
968
        | Some nd_elim_map ->
969
          (* Iterating through the elim map to compute - the list of variables
970
             to remove - the associated list of lustre definitions x = expr to
971
             be used when removing these variables *)
972
          let vars_to_replace, defs =
973
            (* Recovering vid from node locals *)
974
            IMap.fold
975
              (fun v (_, eq) (accu_locals, accu_defs) ->
976
                let locals =
977
                  try
978
                    List.find (fun v' -> v'.var_id = v) nd.node_locals
979
                    :: accu_locals
980
                  with Not_found -> accu_locals
981
                  (* Variable v shall be a global constant, we do no need to
982
                     eliminate it from the locals *)
983
                in
984
                (* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc =
985
                   e.expr_loc } in *)
986
                let defs = eq :: accu_defs in
987
                locals, defs)
988
              nd_elim_map
989
              ([], [])
990
          in
991
          let node_locals, node_stmts =
992
            List.fold_right
993
              (fun stmt (locals, res_stmts) ->
994
                match stmt with
995
                | Aut _ ->
996
                  assert false (* should be processed by now *)
997
                | Eq eq -> (
998
                  match eq.eq_lhs with
999
                  | [] ->
1000
                    assert false (* shall not happen *)
1001
                  | [ lhs ]
1002
                    when List.exists (fun v -> v.var_id = lhs) vars_to_replace
1003
                    ->
1004
                    (* We remove the def *)
1005
                    List.filter (fun v -> v.var_id <> lhs) locals, res_stmts
1006
                  | _ ->
1007
                    (* When more than one lhs we just keep the equation and do
1008
                       not delete it *)
1009
                    let eq_rhs =
1010
                      substitute_expr vars_to_replace defs eq.eq_rhs
1011
                    in
1012
                    locals, Eq { eq with eq_rhs } :: res_stmts))
1013
              nd.node_stmts
1014
              (nd.node_locals, [])
1015
          in
1016
          let nd' = { nd with node_locals; node_stmts } in
1017
          { t with top_decl_desc = Node nd' }
1018
        | None ->
1019
          t)
1020
      | _ ->
1021
        t)
1022
    prog
1023

    
1024
(*** Main function ***)
1025

    
1026
(* This functions produces an optimzed prog * machines It 1- eliminates common
1027
   sub-expressions (TODO how is this different from normalization?) 2- inline
1028
   constants and eliminate duplicated variables 3- try to reuse variables
1029
   whenever possible
1030

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

    
1035
   The function returns both the (possibly updated) prog as well as the
1036
   machines *)
1037
let optimize params prog node_schs machine_code =
1038
  let machine_code =
1039
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then (
1040
      Log.report ~level:1 (fun fmt ->
1041
          Format.fprintf
1042
            fmt
1043
            "@ @[<v 2>.. machines optimization: sub-expression elimination@ ");
1044
      let machine_code = machines_cse machine_code in
1045
      Log.report ~level:3 (fun fmt ->
1046
          Format.fprintf
1047
            fmt
1048
            "@[<v 2>.. generated machines (sub-expr elim):@ %a@]@ "
1049
            pp_machines
1050
            machine_code);
1051
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
1052
      machine_code)
1053
    else machine_code
1054
  in
1055
  (* Optimize machine code *)
1056
  let prog, machine_code, removed_table =
1057
    if
1058
      !Options.optimization >= 2 && !Options.output <> Options.OutEMF
1059
      (*&& !Options.output <> "horn"*)
1060
    then (
1061
      Log.report ~level:1 (fun fmt ->
1062
          Format.fprintf
1063
            fmt
1064
            "@ @[<v 2>.. machines optimization: const. inlining (partial eval. \
1065
             with const)@ ");
1066
      let machine_code, removed_table =
1067
        machines_unfold (Corelang.get_consts prog) node_schs machine_code
1068
      in
1069
      Log.report ~level:3 (fun fmt ->
1070
          Format.fprintf
1071
            fmt
1072
            "@ Eliminated flows: %a@ "
1073
            (IMap.pp (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m)))
1074
            removed_table);
1075
      (* If variables were eliminated, relaunch the normalization/machine
1076
         generation *)
1077
      let prog, machine_code, removed_table =
1078
        if IMap.is_empty removed_table then
1079
          (* stopping here, no need to reupdate the prog *)
1080
          prog, machine_code, removed_table
1081
        else
1082
          let prog = elim_prog_variables prog removed_table in
1083
          (* Mini stage1 *)
1084
          let prog = Normalization.normalize_prog ~first:false params prog in
1085
          let prog = SortProg.sort_nodes_locals prog in
1086
          (* Mini stage2: note that we do not protect against alg. loop since
1087
             this should have been handled before *)
1088
          let prog, node_schs = Scheduling.schedule_prog prog in
1089
          let machine_code = Machine_code.translate_prog prog node_schs in
1090
          (* Mini stage2 machine optimiation *)
1091
          let machine_code, removed_table =
1092
            machines_unfold (Corelang.get_consts prog) node_schs machine_code
1093
          in
1094
          prog, machine_code, removed_table
1095
      in
1096
      Log.report ~level:3 (fun fmt ->
1097
          Format.fprintf
1098
            fmt
1099
            "@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "
1100
            pp_machines
1101
            machine_code);
1102
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
1103
      prog, machine_code, removed_table)
1104
    else prog, machine_code, IMap.empty
1105
  in
1106
  (* Optimize machine code *)
1107
  let machine_code =
1108
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then (
1109
      Log.report ~level:1 (fun fmt ->
1110
          Format.fprintf
1111
            fmt
1112
            ".. machines optimization: minimize stack usage by reusing \
1113
             variables@,");
1114
      let node_schs =
1115
        Scheduling.remove_prog_inlined_locals removed_table node_schs
1116
      in
1117
      let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
1118
      let machine_code = machines_fusion (machines_reuse_variables reuse_tables machine_code) in
1119
      machine_code)
1120
    else machine_code
1121
  in
1122

    
1123
  prog, machine_code
1124

    
1125
(* Local Variables: *)
1126
(* compile-command:"make -C .." *)
1127
(* End: *)
(62-62/101)