1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
open Utils
|
13
|
open Lustre_types
|
14
|
open Machine_code_types
|
15
|
open Corelang
|
16
|
open Causality
|
17
|
open Machine_code_common
|
18
|
open Dimension
|
19
|
module Mpfr = Lustrec_mpfr
|
20
|
|
21
|
let pp_elim m fmt elim =
|
22
|
pp_imap ~comment:"/* elim table: */" (pp_val m) fmt elim
|
23
|
(* Format.fprintf fmt "@[<hv 0>@[<hv 2>{ /* elim table: */";
|
24
|
* IMap.iter (fun v expr -> Format.fprintf fmt "@ %s |-> %a," v (pp_val m) expr) elim;
|
25
|
* Format.fprintf fmt "@]@ }@]" *)
|
26
|
|
27
|
let rec eliminate m elim instr =
|
28
|
let e_expr = eliminate_expr m elim in
|
29
|
match get_instr_desc instr with
|
30
|
| MLocalAssign (i, v) ->
|
31
|
update_instr_desc instr (MLocalAssign (i, e_expr v))
|
32
|
| MStateAssign (i, v) ->
|
33
|
update_instr_desc instr (MStateAssign (i, e_expr v))
|
34
|
| MSetReset _
|
35
|
| MNoReset _
|
36
|
| MClearReset
|
37
|
| MResetAssign _
|
38
|
| MSpec _
|
39
|
| MComment _ ->
|
40
|
instr
|
41
|
| MStep (il, i, vl) ->
|
42
|
update_instr_desc instr (MStep (il, i, List.map e_expr vl))
|
43
|
| MBranch (g, hl) ->
|
44
|
update_instr_desc instr
|
45
|
(MBranch
|
46
|
( e_expr g,
|
47
|
List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl ))
|
48
|
|
49
|
and eliminate_expr m elim expr =
|
50
|
let eliminate_expr = eliminate_expr m in
|
51
|
match expr.value_desc with
|
52
|
| Var v -> (
|
53
|
if is_memory m v then expr
|
54
|
else try IMap.find v.var_id elim with Not_found -> expr)
|
55
|
| Fun (id, vl) ->
|
56
|
{ expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl) }
|
57
|
| Array vl ->
|
58
|
{ expr with value_desc = Array (List.map (eliminate_expr elim) vl) }
|
59
|
| Access (v1, v2) ->
|
60
|
{
|
61
|
expr with
|
62
|
value_desc = Access (eliminate_expr elim v1, eliminate_expr elim v2);
|
63
|
}
|
64
|
| Power (v1, v2) ->
|
65
|
{
|
66
|
expr with
|
67
|
value_desc = Power (eliminate_expr elim v1, eliminate_expr elim v2);
|
68
|
}
|
69
|
| Cst _ | ResetFlag ->
|
70
|
expr
|
71
|
|
72
|
let eliminate_dim elim dim =
|
73
|
Dimension.expr_replace_expr
|
74
|
(fun v ->
|
75
|
try dimension_of_value (IMap.find v elim)
|
76
|
with Not_found -> mkdim_ident dim.dim_loc v)
|
77
|
dim
|
78
|
|
79
|
(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following
|
80
|
functions seem unsused. They have to be adapted to the new type for expr *)
|
81
|
|
82
|
let unfold_expr_offset m offset expr =
|
83
|
List.fold_left
|
84
|
(fun res -> function
|
85
|
| Index i ->
|
86
|
mk_val
|
87
|
(Access (res, value_of_dimension m i))
|
88
|
(Types.array_element_type res.value_type)
|
89
|
| Field _ ->
|
90
|
Format.eprintf "internal error: not yet implemented !";
|
91
|
assert false)
|
92
|
expr offset
|
93
|
|
94
|
let rec simplify_cst_expr m offset typ cst =
|
95
|
match offset, cst with
|
96
|
| [], _ ->
|
97
|
mk_val (Cst cst) typ
|
98
|
| Index i :: q, Const_array cl when Dimension.is_dimension_const i ->
|
99
|
let elt_typ = Types.array_element_type typ in
|
100
|
simplify_cst_expr m q elt_typ
|
101
|
(List.nth cl (Dimension.size_const_dimension i))
|
102
|
| Index i :: q, Const_array cl ->
|
103
|
let elt_typ = Types.array_element_type typ in
|
104
|
unfold_expr_offset m [ Index i ]
|
105
|
(mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
|
106
|
| Field f :: q, Const_struct fl ->
|
107
|
let fld_typ = Types.struct_field_type typ f in
|
108
|
simplify_cst_expr m q fld_typ (List.assoc f fl)
|
109
|
| _ ->
|
110
|
Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@."
|
111
|
Printers.pp_const cst;
|
112
|
assert false
|
113
|
|
114
|
let simplify_expr_offset m expr =
|
115
|
let rec simplify offset expr =
|
116
|
match offset, expr.value_desc with
|
117
|
| Field _ :: _, _ ->
|
118
|
failwith "not yet implemented"
|
119
|
| _, Fun (id, vl) when Basic_library.is_value_internal_fun expr ->
|
120
|
mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
|
121
|
| _, Fun _ | _, Var _ ->
|
122
|
unfold_expr_offset m offset expr
|
123
|
| _, Cst cst ->
|
124
|
simplify_cst_expr m offset expr.value_type cst
|
125
|
| _, Access (expr, i) ->
|
126
|
simplify (Index (dimension_of_value i) :: offset) expr
|
127
|
| _, ResetFlag ->
|
128
|
expr
|
129
|
| [], _ ->
|
130
|
expr
|
131
|
| Index _ :: q, Power (expr, _) ->
|
132
|
simplify q expr
|
133
|
| Index i :: q, Array vl when Dimension.is_dimension_const i ->
|
134
|
simplify q (List.nth vl (Dimension.size_const_dimension i))
|
135
|
| Index i :: q, Array vl ->
|
136
|
unfold_expr_offset m [ Index i ]
|
137
|
(mk_val (Array (List.map (simplify q) vl)) expr.value_type)
|
138
|
(*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr
|
139
|
(Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
|
140
|
with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr
|
141
|
(Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
|
142
|
in
|
143
|
simplify [] expr
|
144
|
|
145
|
let rec simplify_instr_offset m instr =
|
146
|
match get_instr_desc instr with
|
147
|
| MLocalAssign (v, expr) ->
|
148
|
update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
|
149
|
| MStateAssign (v, expr) ->
|
150
|
update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
|
151
|
| MSetReset _
|
152
|
| MNoReset _
|
153
|
| MClearReset
|
154
|
| MResetAssign _
|
155
|
| MSpec _
|
156
|
| MComment _ ->
|
157
|
instr
|
158
|
| MStep (outputs, id, inputs) ->
|
159
|
update_instr_desc instr
|
160
|
(MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
|
161
|
| MBranch (cond, brl) ->
|
162
|
update_instr_desc instr
|
163
|
(MBranch
|
164
|
( simplify_expr_offset m cond,
|
165
|
List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl ))
|
166
|
|
167
|
and simplify_instrs_offset m instrs = List.map (simplify_instr_offset m) instrs
|
168
|
|
169
|
let is_scalar_const c =
|
170
|
match c with Const_real _ | Const_int _ | Const_tag _ -> true | _ -> false
|
171
|
|
172
|
(* An instruction v = expr may (and will) be unfolded iff: - either expr is
|
173
|
atomic (no complex expressions, only const, vars and array/struct accesses) -
|
174
|
or v has a fanin <= 1 (used at most once) *)
|
175
|
let is_unfoldable_expr fanin expr =
|
176
|
let rec unfold_const offset cst =
|
177
|
match offset, cst with
|
178
|
| _, Const_int _ | _, Const_real _ | _, Const_tag _ ->
|
179
|
true
|
180
|
| Field f :: q, Const_struct fl ->
|
181
|
unfold_const q (List.assoc f fl)
|
182
|
| [], Const_struct _ ->
|
183
|
false
|
184
|
| Index i :: q, Const_array cl when Dimension.is_dimension_const i ->
|
185
|
unfold_const q (List.nth cl (Dimension.size_const_dimension i))
|
186
|
| _, Const_array _ ->
|
187
|
false
|
188
|
| _ ->
|
189
|
assert false
|
190
|
in
|
191
|
let rec unfold offset expr =
|
192
|
match offset, expr.value_desc with
|
193
|
| _, Cst cst ->
|
194
|
unfold_const offset cst
|
195
|
| _, Var _ ->
|
196
|
true
|
197
|
| [], Power _ | [], Array _ ->
|
198
|
false
|
199
|
| Index _ :: q, Power (v, _) ->
|
200
|
unfold q v
|
201
|
| Index i :: q, Array vl when Dimension.is_dimension_const i ->
|
202
|
unfold q (List.nth vl (Dimension.size_const_dimension i))
|
203
|
| _, Array _ ->
|
204
|
false
|
205
|
| _, Access (v, i) ->
|
206
|
unfold (Index (dimension_of_value i) :: offset) v
|
207
|
| _, Fun (_, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
|
208
|
->
|
209
|
List.for_all (unfold offset) vl
|
210
|
| _, Fun _ ->
|
211
|
false
|
212
|
| _ ->
|
213
|
assert false
|
214
|
in
|
215
|
unfold [] expr
|
216
|
|
217
|
let basic_unfoldable_assign fanin v expr =
|
218
|
try
|
219
|
let d = Hashtbl.find fanin v.var_id in
|
220
|
is_unfoldable_expr d expr
|
221
|
with Not_found -> false
|
222
|
|
223
|
let unfoldable_assign fanin v expr =
|
224
|
(if !Options.mpfr then Mpfr.unfoldable_value expr else true)
|
225
|
&& basic_unfoldable_assign fanin v expr
|
226
|
|
227
|
let merge_elim elim1 elim2 =
|
228
|
let merge _ e1 e2 =
|
229
|
match e1, e2 with
|
230
|
| Some e1, Some e2 ->
|
231
|
if e1 = e2 then Some e1 else None
|
232
|
| _, Some e2 ->
|
233
|
Some e2
|
234
|
| Some e1, _ ->
|
235
|
Some e1
|
236
|
| _ ->
|
237
|
None
|
238
|
in
|
239
|
IMap.merge merge elim1 elim2
|
240
|
|
241
|
(* see if elim has to take in account the provided instr: if so, update elim and
|
242
|
return the remove flag, otherwise, the expression should be kept and elim is
|
243
|
left untouched *)
|
244
|
let rec instrs_unfold m fanin elim instrs =
|
245
|
let elim, rev_instrs =
|
246
|
List.fold_left
|
247
|
(fun (elim, instrs) instr ->
|
248
|
(* each subexpression in instr that could be rewritten by the elim set
|
249
|
is rewritten *)
|
250
|
let instr = eliminate m (IMap.map fst elim) instr in
|
251
|
(* if instr is a simple local assign, then (a) elim is simplified with
|
252
|
it (b) it is stored as the elim set *)
|
253
|
instr_unfold m fanin instrs elim instr)
|
254
|
(elim, []) instrs
|
255
|
in
|
256
|
elim, List.rev rev_instrs
|
257
|
|
258
|
and instr_unfold m fanin instrs (elim : (value_t * eq) IMap.t) instr =
|
259
|
(* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE
|
260
|
IT@." pp_instr instr;*)
|
261
|
match get_instr_desc instr with
|
262
|
(* Simple cases*)
|
263
|
| MStep ([ v ], id, vl)
|
264
|
when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
|
265
|
->
|
266
|
instr_unfold m fanin instrs elim
|
267
|
(update_instr_desc instr
|
268
|
(MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
|
269
|
| MLocalAssign (v, expr)
|
270
|
when (not (is_clock_dec_type v.var_dec_type.ty_dec_desc))
|
271
|
&& unfoldable_assign fanin v expr ->
|
272
|
(* we don't eliminate clock definitions *)
|
273
|
let new_eq =
|
274
|
Corelang.mkeq (desome instr.lustre_eq).eq_loc
|
275
|
([ v.var_id ], (desome instr.lustre_eq).eq_rhs)
|
276
|
in
|
277
|
IMap.add v.var_id (expr, new_eq) elim, instrs
|
278
|
| MBranch (g, hl) when false ->
|
279
|
let elim_branches =
|
280
|
List.map (fun (h, l) -> h, instrs_unfold m fanin elim l) hl
|
281
|
in
|
282
|
let elim, branches =
|
283
|
List.fold_right
|
284
|
(fun (h, (e, l)) (elim, branches) ->
|
285
|
merge_elim elim e, (h, l) :: branches)
|
286
|
elim_branches (elim, [])
|
287
|
in
|
288
|
elim, update_instr_desc instr (MBranch (g, branches)) :: instrs
|
289
|
| _ ->
|
290
|
elim, instr :: instrs
|
291
|
(* default case, we keep the instruction and do not modify elim *)
|
292
|
|
293
|
(** We iterate in the order, recording simple local assigns in an accumulator 1.
|
294
|
each expression is rewritten according to the accumulator 2. local assigns
|
295
|
then rewrite occurrences of the lhs in the computed accumulator *)
|
296
|
|
297
|
let static_call_unfold elim (inst, (n, args)) =
|
298
|
let replace v =
|
299
|
try dimension_of_value (IMap.find v elim)
|
300
|
with Not_found -> Dimension.mkdim_ident Location.dummy_loc v
|
301
|
in
|
302
|
inst, (n, List.map (Dimension.expr_replace_expr replace) args)
|
303
|
|
304
|
(** Perform optimization on machine code: - iterate through step instructions
|
305
|
and remove simple local assigns *)
|
306
|
let machine_unfold fanin elim machine =
|
307
|
Log.report ~level:3 (fun fmt ->
|
308
|
Format.fprintf fmt "machine_unfold %s %a@ " machine.mname.node_id
|
309
|
(pp_elim machine) (IMap.map fst elim));
|
310
|
let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
|
311
|
let elim_vars, instrs =
|
312
|
instrs_unfold machine fanin elim_consts machine.mstep.step_instrs
|
313
|
in
|
314
|
let instrs = simplify_instrs_offset machine instrs in
|
315
|
let checks =
|
316
|
List.map
|
317
|
(fun (loc, check) ->
|
318
|
loc, eliminate_expr machine (IMap.map fst elim_vars) check)
|
319
|
machine.mstep.step_checks
|
320
|
in
|
321
|
let locals =
|
322
|
List.filter
|
323
|
(fun v -> not (IMap.mem v.var_id elim_vars))
|
324
|
machine.mstep.step_locals
|
325
|
in
|
326
|
let elim_consts = IMap.map fst elim_consts in
|
327
|
let minstances =
|
328
|
List.map (static_call_unfold elim_consts) machine.minstances
|
329
|
in
|
330
|
let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls in
|
331
|
( {
|
332
|
machine with
|
333
|
mstep =
|
334
|
{
|
335
|
machine.mstep with
|
336
|
step_locals = locals;
|
337
|
step_instrs = instrs;
|
338
|
step_checks = checks;
|
339
|
};
|
340
|
mconst;
|
341
|
minstances;
|
342
|
mcalls;
|
343
|
},
|
344
|
elim_vars )
|
345
|
|
346
|
let instr_of_const top_const =
|
347
|
let const = const_of_top top_const in
|
348
|
let loc = const.const_loc in
|
349
|
let id = const.const_id in
|
350
|
let vdecl =
|
351
|
mkvar_decl loc
|
352
|
( id,
|
353
|
mktyp Location.dummy_loc Tydec_any,
|
354
|
mkclock loc Ckdec_any,
|
355
|
true,
|
356
|
None,
|
357
|
None )
|
358
|
in
|
359
|
let vdecl = { vdecl with var_type = const.const_type } in
|
360
|
let lustre_eq =
|
361
|
mkeq loc ([ const.const_id ], mkexpr loc (Expr_const const.const_value))
|
362
|
in
|
363
|
mkinstr ~lustre_eq
|
364
|
(MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
|
365
|
|
366
|
(* We do not perform this optimization on contract nodes since there is not
|
367
|
explicit dependence btw variables and their use in contracts. *)
|
368
|
let machines_unfold consts node_schs machines =
|
369
|
List.fold_right
|
370
|
(fun m (machines, removed) ->
|
371
|
let is_contract =
|
372
|
match m.mspec.mnode_spec with Some (Contract _) -> true | _ -> false
|
373
|
in
|
374
|
if is_contract then m :: machines, removed
|
375
|
else
|
376
|
let fanin =
|
377
|
(IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table
|
378
|
in
|
379
|
let elim_consts, _ =
|
380
|
instrs_unfold m fanin IMap.empty (List.map instr_of_const consts)
|
381
|
in
|
382
|
let m, removed_m = machine_unfold fanin elim_consts m in
|
383
|
m :: machines, IMap.add m.mname.node_id removed_m removed)
|
384
|
machines ([], IMap.empty)
|
385
|
|
386
|
let get_assign_lhs instr =
|
387
|
match get_instr_desc instr with
|
388
|
| MLocalAssign (v, e) ->
|
389
|
mk_val (Var v) e.value_type
|
390
|
| MStateAssign (v, e) ->
|
391
|
mk_val (Var v) e.value_type
|
392
|
| _ ->
|
393
|
assert false
|
394
|
|
395
|
let get_assign_rhs instr =
|
396
|
match get_instr_desc instr with
|
397
|
| MLocalAssign (_, e) | MStateAssign (_, e) ->
|
398
|
e
|
399
|
| _ ->
|
400
|
assert false
|
401
|
|
402
|
let is_assign instr =
|
403
|
match get_instr_desc instr with
|
404
|
| MLocalAssign _ | MStateAssign _ ->
|
405
|
true
|
406
|
| _ ->
|
407
|
false
|
408
|
|
409
|
let mk_assign m v e =
|
410
|
match v.value_desc with
|
411
|
| Var v ->
|
412
|
if is_memory m v then MStateAssign (v, e) else MLocalAssign (v, e)
|
413
|
| _ ->
|
414
|
assert false
|
415
|
|
416
|
let rec assigns_instr instr assign =
|
417
|
match get_instr_desc instr with
|
418
|
| MLocalAssign (i, _) | MStateAssign (i, _) ->
|
419
|
VSet.add i assign
|
420
|
| MStep (ol, _, _) ->
|
421
|
List.fold_right VSet.add ol assign
|
422
|
| MBranch (_, hl) ->
|
423
|
List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
|
424
|
| _ ->
|
425
|
assign
|
426
|
|
427
|
and assigns_instrs instrs assign =
|
428
|
List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
|
429
|
|
430
|
(* and substitute_expr subst expr = match expr with | Var v -> (try IMap.find
|
431
|
expr subst with Not_found -> expr) | Fun (id, vl) -> Fun (id, List.map
|
432
|
(substitute_expr subst) vl) | Array(vl) -> Array(List.map (substitute_expr
|
433
|
subst) vl) | Access(v1, v2) -> Access(substitute_expr subst v1,
|
434
|
substitute_expr subst v2) | Power(v1, v2) -> Power(substitute_expr subst v1,
|
435
|
substitute_expr subst v2) | Cst _ -> expr *)
|
436
|
|
437
|
(** Finds a substitute for [instr] in [instrs], i.e. another instr' with the
|
438
|
same rhs expression. Then substitute this expression with the first assigned
|
439
|
var *)
|
440
|
let subst_instr m subst instrs instr =
|
441
|
(* Format.eprintf "subst instr: %a@." (pp_instr m) instr; *)
|
442
|
let instr = eliminate m subst instr in
|
443
|
let instr_v = get_assign_lhs instr in
|
444
|
let instr_e = get_assign_rhs instr in
|
445
|
try
|
446
|
(* Searching for equivalent asssign *)
|
447
|
let instr' =
|
448
|
List.find
|
449
|
(fun instr' -> is_assign instr' && get_assign_rhs instr' = instr_e)
|
450
|
instrs
|
451
|
in
|
452
|
(* Registering the instr_v as instr'_v while replacing *)
|
453
|
match instr_v.value_desc with
|
454
|
| Var v -> (
|
455
|
let instr'_v = get_assign_lhs instr' in
|
456
|
if not (is_memory m v) then
|
457
|
(* The current instruction defines a local variables, ie not memory, we
|
458
|
can just record the relationship and continue *)
|
459
|
IMap.add v.var_id instr'_v subst, instrs
|
460
|
else
|
461
|
(* The current instruction defines a memory. We need to keep the
|
462
|
definition, simplified *)
|
463
|
match instr'_v.value_desc with
|
464
|
| Var v' ->
|
465
|
if not (is_memory m v') then
|
466
|
(* We define v' = v. Don't need to update the records. *)
|
467
|
let instr =
|
468
|
eliminate m subst
|
469
|
(update_instr_desc instr (mk_assign m instr_v instr'_v))
|
470
|
in
|
471
|
subst, instr :: instrs
|
472
|
else
|
473
|
(* Last case, v', the lhs of the previous similar definition is,
|
474
|
itself, a memory *)
|
475
|
|
476
|
(* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *)
|
477
|
(* Filtering out the list of instructions: - we copy in the same
|
478
|
order the list of instr in instrs (fold_right) - if the current
|
479
|
instr is this instr' then apply the elimination with v' -> v on
|
480
|
instr' before recording it as an instruction. *)
|
481
|
let subst_v' = IMap.add v'.var_id instr_v IMap.empty in
|
482
|
let instrs' =
|
483
|
snd
|
484
|
(List.fold_right
|
485
|
(fun instr (ok, instrs) ->
|
486
|
( ok || instr = instr',
|
487
|
if ok then instr :: instrs
|
488
|
else if instr = instr' then instrs
|
489
|
else eliminate m subst_v' instr :: instrs ))
|
490
|
instrs (false, []))
|
491
|
in
|
492
|
IMap.add v'.var_id instr_v subst, instr :: instrs'
|
493
|
| _ ->
|
494
|
assert false)
|
495
|
| _ ->
|
496
|
assert false
|
497
|
with Not_found ->
|
498
|
(* No such equivalent expr: keeping the definition *)
|
499
|
subst, instr :: instrs
|
500
|
|
501
|
(* - [subst] : hashtable from ident to (simple) definition it is an equivalence
|
502
|
table - [elim] : set of eliminated variables - [instrs] : previous
|
503
|
instructions, which [instr] is compared against - [instr] : current
|
504
|
instruction, normalized by [subst] *)
|
505
|
|
506
|
(** Common sub-expression elimination for machine instructions *)
|
507
|
let rec instr_cse m (subst, instrs) instr =
|
508
|
match get_instr_desc instr with
|
509
|
(* Simple cases*)
|
510
|
| MStep ([ v ], id, vl)
|
511
|
when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
|
512
|
->
|
513
|
instr_cse m (subst, instrs)
|
514
|
(update_instr_desc instr
|
515
|
(MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
|
516
|
| MLocalAssign (v, expr) when is_unfoldable_expr 2 expr ->
|
517
|
IMap.add v.var_id expr subst, instr :: instrs
|
518
|
| _ when is_assign instr ->
|
519
|
subst_instr m subst instrs instr
|
520
|
| _ ->
|
521
|
subst, instr :: instrs
|
522
|
|
523
|
(** Apply common sub-expression elimination to a sequence of instrs *)
|
524
|
let instrs_cse m subst instrs =
|
525
|
let subst, rev_instrs = List.fold_left (instr_cse m) (subst, []) instrs in
|
526
|
subst, List.rev rev_instrs
|
527
|
|
528
|
(** Apply common sub-expression elimination to a machine - iterate through step
|
529
|
instructions and remove simple local assigns *)
|
530
|
let machine_cse subst machine =
|
531
|
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@."
|
532
|
pp_elim subst);*)
|
533
|
let _, instrs = instrs_cse machine subst machine.mstep.step_instrs in
|
534
|
let assigned = assigns_instrs instrs VSet.empty in
|
535
|
{
|
536
|
machine with
|
537
|
mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
|
538
|
mstep =
|
539
|
{
|
540
|
machine.mstep with
|
541
|
step_locals =
|
542
|
List.filter
|
543
|
(fun vdecl -> VSet.mem vdecl assigned)
|
544
|
machine.mstep.step_locals;
|
545
|
step_instrs = instrs;
|
546
|
};
|
547
|
}
|
548
|
|
549
|
let machines_cse machines = List.map (machine_cse IMap.empty) machines
|
550
|
|
551
|
(* variable substitution for optimizing purposes *)
|
552
|
|
553
|
(* checks whether an [instr] is skip and can be removed from program *)
|
554
|
let rec instr_is_skip instr =
|
555
|
match get_instr_desc instr with
|
556
|
| MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
|
557
|
true
|
558
|
| MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
|
559
|
true
|
560
|
| MBranch (_, hl) ->
|
561
|
List.for_all (fun (_, il) -> instrs_are_skip il) hl
|
562
|
| _ ->
|
563
|
false
|
564
|
|
565
|
and instrs_are_skip instrs = List.for_all instr_is_skip instrs
|
566
|
|
567
|
let instr_cons instr cont = if instr_is_skip instr then cont else instr :: cont
|
568
|
|
569
|
let rec instr_remove_skip instr cont =
|
570
|
match get_instr_desc instr with
|
571
|
| MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
|
572
|
cont
|
573
|
| MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
|
574
|
cont
|
575
|
| MBranch (g, hl) ->
|
576
|
update_instr_desc instr
|
577
|
(MBranch (g, List.map (fun (h, il) -> h, instrs_remove_skip il []) hl))
|
578
|
:: cont
|
579
|
| _ ->
|
580
|
instr :: cont
|
581
|
|
582
|
and instrs_remove_skip instrs cont =
|
583
|
List.fold_right instr_remove_skip instrs cont
|
584
|
|
585
|
let rec value_replace_var fvar value =
|
586
|
match value.value_desc with
|
587
|
| Cst _ | ResetFlag ->
|
588
|
value
|
589
|
| Var v ->
|
590
|
{ value with value_desc = Var (fvar v) }
|
591
|
| Fun (id, args) ->
|
592
|
{ value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
|
593
|
| Array vl ->
|
594
|
{ value with value_desc = Array (List.map (value_replace_var fvar) vl) }
|
595
|
| Access (t, i) ->
|
596
|
{ value with value_desc = Access (value_replace_var fvar t, i) }
|
597
|
| Power (v, n) ->
|
598
|
{ value with value_desc = Power (value_replace_var fvar v, n) }
|
599
|
|
600
|
let rec instr_replace_var fvar instr cont =
|
601
|
match get_instr_desc instr with
|
602
|
| MLocalAssign (i, v) ->
|
603
|
instr_cons
|
604
|
(update_instr_desc instr
|
605
|
(MLocalAssign (fvar i, value_replace_var fvar v)))
|
606
|
cont
|
607
|
| MStateAssign (i, v) ->
|
608
|
instr_cons
|
609
|
(update_instr_desc instr (MStateAssign (i, value_replace_var fvar v)))
|
610
|
cont
|
611
|
| MSetReset _
|
612
|
| MNoReset _
|
613
|
| MClearReset
|
614
|
| MResetAssign _
|
615
|
| MSpec _
|
616
|
| MComment _ ->
|
617
|
instr_cons instr cont
|
618
|
| MStep (il, i, vl) ->
|
619
|
instr_cons
|
620
|
(update_instr_desc instr
|
621
|
(MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)))
|
622
|
cont
|
623
|
| MBranch (g, hl) ->
|
624
|
instr_cons
|
625
|
(update_instr_desc instr
|
626
|
(MBranch
|
627
|
( value_replace_var fvar g,
|
628
|
List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )))
|
629
|
cont
|
630
|
|
631
|
and instrs_replace_var fvar instrs cont =
|
632
|
List.fold_right (instr_replace_var fvar) instrs cont
|
633
|
|
634
|
let step_replace_var fvar step =
|
635
|
(* Some outputs may have been replaced by locals. We then need to rename those
|
636
|
outputs without changing their clocks, etc *)
|
637
|
let outputs' =
|
638
|
List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs
|
639
|
in
|
640
|
let locals' =
|
641
|
List.fold_left
|
642
|
(fun res l ->
|
643
|
let l' = fvar l in
|
644
|
if List.exists (fun o -> o.var_id = l'.var_id) outputs' then res
|
645
|
else Utils.add_cons l' res)
|
646
|
[] step.step_locals
|
647
|
in
|
648
|
{
|
649
|
step with
|
650
|
step_checks =
|
651
|
List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks;
|
652
|
step_outputs = outputs';
|
653
|
step_locals = locals';
|
654
|
step_instrs = instrs_replace_var fvar step.step_instrs [];
|
655
|
}
|
656
|
|
657
|
let machine_replace_variables fvar m =
|
658
|
{ m with mstep = step_replace_var fvar m.mstep }
|
659
|
|
660
|
let machine_reuse_variables m reuse =
|
661
|
let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
|
662
|
machine_replace_variables fvar m
|
663
|
|
664
|
let machines_reuse_variables prog reuse_tables =
|
665
|
List.map
|
666
|
(fun m ->
|
667
|
machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables))
|
668
|
prog
|
669
|
|
670
|
let rec instr_assign res instr =
|
671
|
match get_instr_desc instr with
|
672
|
| MLocalAssign (i, _) ->
|
673
|
Disjunction.CISet.add i res
|
674
|
| MStateAssign (i, _) ->
|
675
|
Disjunction.CISet.add i res
|
676
|
| MBranch (_, hl) ->
|
677
|
List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
|
678
|
| MStep (il, _, _) ->
|
679
|
List.fold_right Disjunction.CISet.add il res
|
680
|
| _ ->
|
681
|
res
|
682
|
|
683
|
and instrs_assign res instrs = List.fold_left instr_assign res instrs
|
684
|
|
685
|
let rec instr_constant_assign var instr =
|
686
|
match get_instr_desc instr with
|
687
|
| MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
|
688
|
| MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) ->
|
689
|
i = var
|
690
|
| MBranch (_, hl) ->
|
691
|
List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
|
692
|
| _ ->
|
693
|
false
|
694
|
|
695
|
and instrs_constant_assign var instrs =
|
696
|
List.fold_left
|
697
|
(fun res i ->
|
698
|
if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then
|
699
|
instr_constant_assign var i
|
700
|
else res)
|
701
|
false instrs
|
702
|
|
703
|
let rec instr_reduce branches instr1 cont =
|
704
|
match get_instr_desc instr1 with
|
705
|
| MLocalAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
|
706
|
instr1 :: (List.assoc c branches @ cont)
|
707
|
| MStateAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
|
708
|
instr1 :: (List.assoc c branches @ cont)
|
709
|
| MBranch (g, hl) ->
|
710
|
update_instr_desc instr1
|
711
|
(MBranch (g, List.map (fun (h, b) -> h, instrs_reduce branches b []) hl))
|
712
|
:: cont
|
713
|
| _ ->
|
714
|
instr1 :: cont
|
715
|
|
716
|
and instrs_reduce branches instrs cont =
|
717
|
match instrs with
|
718
|
| [] ->
|
719
|
cont
|
720
|
| [ i ] ->
|
721
|
instr_reduce branches i cont
|
722
|
| i1 :: i2 :: q ->
|
723
|
i1 :: instrs_reduce branches (i2 :: q) cont
|
724
|
|
725
|
let rec instrs_fusion instrs =
|
726
|
match instrs, List.map get_instr_desc instrs with
|
727
|
| [], [] | [ _ ], [ _ ] ->
|
728
|
instrs
|
729
|
| i1 :: _ :: q, _ :: MBranch ({ value_desc = Var v; _ }, hl) :: _
|
730
|
when instr_constant_assign v i1 ->
|
731
|
instr_reduce
|
732
|
(List.map (fun (h, b) -> h, instrs_fusion b) hl)
|
733
|
i1 (instrs_fusion q)
|
734
|
| i1 :: i2 :: q, _ ->
|
735
|
i1 :: instrs_fusion (i2 :: q)
|
736
|
| _ ->
|
737
|
assert false
|
738
|
(* Other cases should not happen since both lists are of same size *)
|
739
|
|
740
|
let step_fusion step =
|
741
|
{ step with step_instrs = instrs_fusion step.step_instrs }
|
742
|
|
743
|
let machine_fusion m = { m with mstep = step_fusion m.mstep }
|
744
|
|
745
|
let machines_fusion prog = List.map machine_fusion prog
|
746
|
|
747
|
(* Additional function to modify the prog according to removed variables map *)
|
748
|
|
749
|
let elim_prog_variables prog removed_table =
|
750
|
List.map
|
751
|
(fun t ->
|
752
|
match t.top_decl_desc with
|
753
|
| Node nd -> (
|
754
|
match IMap.find_opt nd.node_id removed_table with
|
755
|
| Some nd_elim_map ->
|
756
|
(* Iterating through the elim map to compute - the list of variables
|
757
|
to remove - the associated list of lustre definitions x = expr to
|
758
|
be used when removing these variables *)
|
759
|
let vars_to_replace, defs =
|
760
|
(* Recovering vid from node locals *)
|
761
|
IMap.fold
|
762
|
(fun v (_, eq) (accu_locals, accu_defs) ->
|
763
|
let locals =
|
764
|
try
|
765
|
List.find (fun v' -> v'.var_id = v) nd.node_locals
|
766
|
:: accu_locals
|
767
|
with Not_found -> accu_locals
|
768
|
(* Variable v shall be a global constant, we do no need to
|
769
|
eliminate it from the locals *)
|
770
|
in
|
771
|
(* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc =
|
772
|
e.expr_loc } in *)
|
773
|
let defs = eq :: accu_defs in
|
774
|
locals, defs)
|
775
|
nd_elim_map ([], [])
|
776
|
in
|
777
|
|
778
|
let node_locals, node_stmts =
|
779
|
List.fold_right
|
780
|
(fun stmt (locals, res_stmts) ->
|
781
|
match stmt with
|
782
|
| Aut _ ->
|
783
|
assert false (* should be processed by now *)
|
784
|
| Eq eq -> (
|
785
|
match eq.eq_lhs with
|
786
|
| [] ->
|
787
|
assert false (* shall not happen *)
|
788
|
| _ :: _ :: _ ->
|
789
|
(* When more than one lhs we just keep the equation and do
|
790
|
not delete it *)
|
791
|
let eq_rhs' =
|
792
|
substitute_expr vars_to_replace defs eq.eq_rhs
|
793
|
in
|
794
|
locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts
|
795
|
| [ lhs ] ->
|
796
|
if List.exists (fun v -> v.var_id = lhs) vars_to_replace
|
797
|
then
|
798
|
(* We remove the def *)
|
799
|
List.filter (fun v -> v.var_id <> lhs) locals, res_stmts
|
800
|
else
|
801
|
(* We keep it but modify any use of an eliminatend var *)
|
802
|
let eq_rhs' =
|
803
|
substitute_expr vars_to_replace defs eq.eq_rhs
|
804
|
in
|
805
|
locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts))
|
806
|
nd.node_stmts (nd.node_locals, [])
|
807
|
in
|
808
|
let nd' = { nd with node_locals; node_stmts } in
|
809
|
{ t with top_decl_desc = Node nd' }
|
810
|
| None ->
|
811
|
t)
|
812
|
| _ ->
|
813
|
t)
|
814
|
prog
|
815
|
|
816
|
(*** Main function ***)
|
817
|
|
818
|
(* This functions produces an optimzed prog * machines It 1- eliminates common
|
819
|
sub-expressions (TODO how is this different from normalization?) 2- inline
|
820
|
constants and eliminate duplicated variables 3- try to reuse variables
|
821
|
whenever possible
|
822
|
|
823
|
When item (2) identified eliminated variables, the initial prog is modified,
|
824
|
its normalized recomputed, as well as its scheduling, before regenerating the
|
825
|
machines.
|
826
|
|
827
|
The function returns both the (possibly updated) prog as well as the machines *)
|
828
|
let optimize params prog node_schs machine_code =
|
829
|
let machine_code =
|
830
|
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then (
|
831
|
Log.report ~level:1 (fun fmt ->
|
832
|
Format.fprintf fmt
|
833
|
"@ @[<v 2>.. machines optimization: sub-expression elimination@ ");
|
834
|
let machine_code = machines_cse machine_code in
|
835
|
Log.report ~level:3 (fun fmt ->
|
836
|
Format.fprintf fmt
|
837
|
"@[<v 2>.. generated machines (sub-expr elim):@ %a@]@ " pp_machines
|
838
|
machine_code);
|
839
|
Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
|
840
|
machine_code)
|
841
|
else machine_code
|
842
|
in
|
843
|
(* Optimize machine code *)
|
844
|
let prog, machine_code, removed_table =
|
845
|
if
|
846
|
!Options.optimization >= 2 && !Options.output <> "emf"
|
847
|
(*&& !Options.output <> "horn"*)
|
848
|
then (
|
849
|
Log.report ~level:1 (fun fmt ->
|
850
|
Format.fprintf fmt
|
851
|
"@ @[<v 2>.. machines optimization: const. inlining (partial eval. \
|
852
|
with const)@ ");
|
853
|
let machine_code, removed_table =
|
854
|
machines_unfold (Corelang.get_consts prog) node_schs machine_code
|
855
|
in
|
856
|
Log.report ~level:3 (fun fmt ->
|
857
|
Format.fprintf fmt "@ Eliminated flows: %a@ "
|
858
|
(pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m)))
|
859
|
removed_table);
|
860
|
Log.report ~level:3 (fun fmt ->
|
861
|
Format.fprintf fmt
|
862
|
"@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "
|
863
|
pp_machines machine_code);
|
864
|
(* If variables were eliminated, relaunch the normalization/machine
|
865
|
generation *)
|
866
|
let prog, machine_code, removed_table =
|
867
|
if IMap.is_empty removed_table then
|
868
|
(* stopping here, no need to reupdate the prog *)
|
869
|
prog, machine_code, removed_table
|
870
|
else
|
871
|
let prog = elim_prog_variables prog removed_table in
|
872
|
(* Mini stage1 *)
|
873
|
let prog = Normalization.normalize_prog params prog in
|
874
|
let prog = SortProg.sort_nodes_locals prog in
|
875
|
(* Mini stage2: note that we do not protect against alg. loop since
|
876
|
this should have been handled before *)
|
877
|
let prog, node_schs = Scheduling.schedule_prog prog in
|
878
|
let machine_code = Machine_code.translate_prog prog node_schs in
|
879
|
(* Mini stage2 machine optimiation *)
|
880
|
let machine_code, removed_table =
|
881
|
machines_unfold (Corelang.get_consts prog) node_schs machine_code
|
882
|
in
|
883
|
prog, machine_code, removed_table
|
884
|
in
|
885
|
Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
|
886
|
prog, machine_code, removed_table)
|
887
|
else prog, machine_code, IMap.empty
|
888
|
in
|
889
|
(* Optimize machine code *)
|
890
|
let machine_code =
|
891
|
if !Options.optimization >= 3 && not (Backends.is_functional ()) then (
|
892
|
Log.report ~level:1 (fun fmt ->
|
893
|
Format.fprintf fmt
|
894
|
".. machines optimization: minimize stack usage by reusing \
|
895
|
variables@,");
|
896
|
let node_schs =
|
897
|
Scheduling.remove_prog_inlined_locals removed_table node_schs
|
898
|
in
|
899
|
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
|
900
|
machines_fusion (machines_reuse_variables machine_code reuse_tables))
|
901
|
else machine_code
|
902
|
in
|
903
|
|
904
|
prog, machine_code
|
905
|
|
906
|
(* Local Variables: *)
|
907
|
(* compile-command:"make -C .." *)
|
908
|
(* End: *)
|