Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / optimize_machine.ml @ ef8a361a

History | View | Annotate | Download (26.4 KB)

1 a2d97a3e ploc
(********************************************************************)
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 d0b1ec56 xthirioux
open Utils
13 cf78a589 ploc
open LustreSpec 
14
open Corelang
15 b1655a21 xthirioux
open Causality
16 cf78a589 ploc
open Machine_code 
17 ec433d69 xthirioux
open Dimension
18 cf78a589 ploc
19 55537f48 xthirioux
20 d0b1ec56 xthirioux
let pp_elim fmt elim =
21
  begin
22 521e2a6b ploc
    Format.fprintf fmt "@[{ /* elim table: */@ ";
23
    IMap.iter (fun v expr -> Format.fprintf fmt "%s |-> %a@ " v pp_val expr) elim;
24
    Format.fprintf fmt "}@ @]";
25 d0b1ec56 xthirioux
  end
26
27 cf78a589 ploc
let rec eliminate elim instr =
28
  let e_expr = eliminate_expr elim in
29 3ca27bc7 ploc
  match get_instr_desc instr with
30 04a63d25 xthirioux
  | MComment _         -> instr
31 3ca27bc7 ploc
  | MLocalAssign (i,v) -> update_instr_desc instr (MLocalAssign (i, e_expr v))
32
  | MStateAssign (i,v) -> update_instr_desc instr (MStateAssign (i, e_expr v))
33 cf78a589 ploc
  | MReset i           -> instr
34 45f0f48d xthirioux
  | MNoReset i         -> instr
35 3ca27bc7 ploc
  | MStep (il, i, vl)  -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
36 cf78a589 ploc
  | MBranch (g,hl)     -> 
37 3ca27bc7 ploc
     update_instr_desc instr (
38
       MBranch
39
	 (e_expr g, 
40
	  (List.map 
41
	     (fun (l, il) -> l, List.map (eliminate elim) il) 
42
	     hl
43
	  )
44
	 )
45
     )
46 cf78a589 ploc
    
47
and eliminate_expr elim expr =
48 04a63d25 xthirioux
  match expr.value_desc with
49 d0b1ec56 xthirioux
  | LocalVar v -> (try IMap.find v.var_id elim with Not_found -> expr)
50 04a63d25 xthirioux
  | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
51
  | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
52
  | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
53
  | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
54
  | Cst _ | StateVar _ -> expr
55 cf78a589 ploc
56 ec433d69 xthirioux
let eliminate_dim elim dim =
57 45f0f48d xthirioux
  Dimension.expr_replace_expr 
58
    (fun v -> try
59
		dimension_of_value (IMap.find v elim) 
60
      with Not_found -> mkdim_ident dim.dim_loc v) 
61
    dim
62 ec433d69 xthirioux
63 ca88e660 Ploc
64
(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following
65
   functions seem unsused. They have to be adapted to the new type for expr
66 d2d9d4cb ploc
*)
67 ca88e660 Ploc
68 d7b73fed xthirioux
let unfold_expr_offset m offset expr =
69 04a63d25 xthirioux
  List.fold_left
70
    (fun res -> (function | Index i -> mk_val (Access (res, value_of_dimension m i))
71
					      (Types.array_element_type res.value_type)
72
                          | Field f -> Format.eprintf "internal error: not yet implemented !"; assert false))
73
    expr offset
74 d7b73fed xthirioux
75 04a63d25 xthirioux
let rec simplify_cst_expr m offset typ cst =
76 d7b73fed xthirioux
    match offset, cst with
77
    | []          , _
78 04a63d25 xthirioux
      -> mk_val (Cst cst) typ
79 d7b73fed xthirioux
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i
80 04a63d25 xthirioux
      -> let elt_typ = Types.array_element_type typ in
81
         simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const_dimension i))
82 d7b73fed xthirioux
    | Index i :: q, Const_array cl
83 04a63d25 xthirioux
      -> let elt_typ = Types.array_element_type typ in
84
         unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
85 d7b73fed xthirioux
    | Field f :: q, Const_struct fl
86 04a63d25 xthirioux
      -> let fld_typ = Types.struct_field_type typ f in
87
         simplify_cst_expr m q fld_typ (List.assoc f fl)
88 d7b73fed xthirioux
    | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false)
89
90
let simplify_expr_offset m expr =
91
  let rec simplify offset expr =
92 04a63d25 xthirioux
    match offset, expr.value_desc with
93 d7b73fed xthirioux
    | Field f ::q , _                -> failwith "not yet implemented"
94 04a63d25 xthirioux
    | _           , Fun (id, vl) when Basic_library.is_value_internal_fun expr
95
                                     -> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
96 d7b73fed xthirioux
    | _           , Fun _
97
    | _           , StateVar _
98
    | _           , LocalVar _       -> unfold_expr_offset m offset expr
99 04a63d25 xthirioux
    | _           , Cst cst          -> simplify_cst_expr m offset expr.value_type cst
100 d7b73fed xthirioux
    | _           , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr
101
    | []          , _                -> expr
102
    | Index _ :: q, Power (expr, _)  -> simplify q expr
103
    | Index i :: q, Array vl when Dimension.is_dimension_const i
104
                                     -> simplify q (List.nth vl (Dimension.size_const_dimension i))
105 04a63d25 xthirioux
    | Index i :: q, Array vl         -> unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type)
106 d7b73fed xthirioux
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
107
     with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
108
  in simplify [] expr
109
110
let rec simplify_instr_offset m instr =
111 3ca27bc7 ploc
  match get_instr_desc instr with
112
  | MLocalAssign (v, expr) -> update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
113
  | MStateAssign (v, expr) -> update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
114 d7b73fed xthirioux
  | MReset id              -> instr
115 45f0f48d xthirioux
  | MNoReset id            -> instr
116 3ca27bc7 ploc
  | MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
117 d7b73fed xthirioux
  | MBranch (cond, brl)
118 3ca27bc7 ploc
    -> update_instr_desc instr (
119
      MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
120
    )
121 04a63d25 xthirioux
  | MComment _             -> instr
122 d7b73fed xthirioux
123
and simplify_instrs_offset m instrs =
124
  List.map (simplify_instr_offset m) instrs
125
126 d0b1ec56 xthirioux
let is_scalar_const c =
127
  match c with
128
  | Const_real _
129 04a63d25 xthirioux
  | Const_int _
130 d0b1ec56 xthirioux
  | Const_tag _   -> true
131
  | _             -> false
132
133 d7b73fed xthirioux
(* An instruction v = expr may (and will) be unfolded iff:
134
   - either expr is atomic
135
     (no complex expressions, only const, vars and array/struct accesses)
136
   - or v has a fanin <= 1 (used at most once)
137
*)
138
let is_unfoldable_expr fanin expr =
139
  let rec unfold_const offset cst =
140
    match offset, cst with
141
    | _           , Const_int _
142
    | _           , Const_real _
143
    | _           , Const_tag _     -> true
144
    | Field f :: q, Const_struct fl -> unfold_const q (List.assoc f fl)
145
    | []          , Const_struct _  -> false
146
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i
147
                                    -> unfold_const q (List.nth cl (Dimension.size_const_dimension i))
148
    | _           , Const_array _   -> false
149
    | _                             -> assert false in
150
  let rec unfold offset expr =
151 04a63d25 xthirioux
    match offset, expr.value_desc with
152 d7b73fed xthirioux
    | _           , Cst cst                      -> unfold_const offset cst
153
    | _           , LocalVar _
154
    | _           , StateVar _                   -> true
155
    | []          , Power _
156
    | []          , Array _                      -> false
157
    | Index i :: q, Power (v, _)                 -> unfold q v
158
    | Index i :: q, Array vl when Dimension.is_dimension_const i
159
                                                 -> unfold q (List.nth vl (Dimension.size_const_dimension i))
160
    | _           , Array _                      -> false
161
    | _           , Access (v, i)                -> unfold (Index (dimension_of_value i) :: offset) v
162 04a63d25 xthirioux
    | _           , Fun (id, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
163 d7b73fed xthirioux
                                                 -> List.for_all (unfold offset) vl
164
    | _           , Fun _                        -> false
165
    | _                                          -> assert false
166
  in unfold [] expr
167 c287ba28 xthirioux
168 04a63d25 xthirioux
let basic_unfoldable_assign fanin v expr =
169 d0b1ec56 xthirioux
  try
170
    let d = Hashtbl.find fanin v.var_id
171 d7b73fed xthirioux
    in is_unfoldable_expr d expr
172
  with Not_found -> false
173 04a63d25 xthirioux
174 d7b73fed xthirioux
let unfoldable_assign fanin v expr =
175 04a63d25 xthirioux
   (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
176
&& basic_unfoldable_assign fanin v expr
177
178 d0b1ec56 xthirioux
let merge_elim elim1 elim2 =
179
  let merge k e1 e2 =
180
    match e1, e2 with
181
    | Some e1, Some e2 -> if e1 = e2 then Some e1 else None
182
    | _      , Some e2 -> Some e2
183
    | Some e1, _       -> Some e1
184
    | _                -> None
185
  in IMap.merge merge elim1 elim2
186
187 cf78a589 ploc
(* see if elim has to take in account the provided instr:
188 54d032f5 xthirioux
   if so, update elim and return the remove flag,
189 cf78a589 ploc
   otherwise, the expression should be kept and elim is left untouched *)
190 d0b1ec56 xthirioux
let rec instrs_unfold fanin elim instrs =
191
  let elim, rev_instrs = 
192
    List.fold_left (fun (elim, instrs) instr ->
193
      (* each subexpression in instr that could be rewritten by the elim set is
194
	 rewritten *)
195
      let instr = eliminate elim instr in
196
      (* if instr is a simple local assign, then (a) elim is simplified with it (b) it
197
	 is stored as the elim set *)
198
      instr_unfold fanin instrs elim instr
199
    ) (elim, []) instrs
200
  in elim, List.rev rev_instrs
201
202
and instr_unfold fanin instrs elim instr =
203 429ab729 ploc
(*  Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*)
204 3ca27bc7 ploc
  match get_instr_desc instr with
205 cf78a589 ploc
  (* Simple cases*)
206 04a63d25 xthirioux
  | MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
207 3ca27bc7 ploc
    -> instr_unfold fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
208 d0b1ec56 xthirioux
  | MLocalAssign(v, expr) when unfoldable_assign fanin v expr
209
    -> (IMap.add v.var_id expr elim, instrs)
210
  | MBranch(g, hl) when false
211
    -> let elim_branches = List.map (fun (h, l) -> (h, instrs_unfold fanin elim l)) hl in
212
       let (elim, branches) =
213
	 List.fold_right
214
	   (fun (h, (e, l)) (elim, branches) -> (merge_elim elim e, (h, l)::branches))
215
	   elim_branches (elim, [])
216 3ca27bc7 ploc
       in elim, ((update_instr_desc instr (MBranch (g, branches))) :: instrs)
217 d0b1ec56 xthirioux
  | _
218
    -> (elim, instr :: instrs)
219 cf78a589 ploc
    (* default case, we keep the instruction and do not modify elim *)
220
  
221
222
(** We iterate in the order, recording simple local assigns in an accumulator
223
    1. each expression is rewritten according to the accumulator
224
    2. local assigns then rewrite occurrences of the lhs in the computed accumulator
225
*)
226
227 ec433d69 xthirioux
let static_call_unfold elim (inst, (n, args)) =
228
  let replace v =
229
    try
230
      Machine_code.dimension_of_value (IMap.find v elim)
231
    with Not_found -> Dimension.mkdim_ident Location.dummy_loc v
232
  in (inst, (n, List.map (Dimension.expr_replace_expr replace) args))
233
234 cf78a589 ploc
(** Perform optimization on machine code:
235
    - iterate through step instructions and remove simple local assigns
236
    
237
*)
238 d0b1ec56 xthirioux
let machine_unfold fanin elim machine =
239
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_unfold %a@." pp_elim elim);*)
240 ec433d69 xthirioux
  let elim_consts, mconst = instrs_unfold fanin elim machine.mconst in
241
  let elim_vars, instrs = instrs_unfold fanin elim_consts machine.mstep.step_instrs in
242 d7b73fed xthirioux
  let instrs = simplify_instrs_offset machine instrs in
243
  let checks = List.map (fun (loc, check) -> loc, eliminate_expr elim_vars check) machine.mstep.step_checks in
244 ec433d69 xthirioux
  let locals = List.filter (fun v -> not (IMap.mem v.var_id elim_vars)) machine.mstep.step_locals in
245
  let minstances = List.map (static_call_unfold elim_consts) machine.minstances in
246
  let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls
247 cf78a589 ploc
  in
248
  {
249
    machine with
250
      mstep = { 
251
	machine.mstep with 
252 ec433d69 xthirioux
	  step_locals = locals;
253 d7b73fed xthirioux
	  step_instrs = instrs;
254
	  step_checks = checks
255 ec433d69 xthirioux
      };
256
      mconst = mconst;
257
      minstances = minstances;
258
      mcalls = mcalls;
259 04a63d25 xthirioux
  },
260
  elim_vars
261 cf78a589 ploc
262 d0b1ec56 xthirioux
let instr_of_const top_const =
263
  let const = const_of_top top_const in
264 ec433d69 xthirioux
  let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true, None) in
265 d0b1ec56 xthirioux
  let vdecl = { vdecl with var_type = const.const_type }
266 3ca27bc7 ploc
  in mkinstr (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
267 cf78a589 ploc
268 d0b1ec56 xthirioux
let machines_unfold consts node_schs machines =
269 04a63d25 xthirioux
  List.fold_right (fun m (machines, removed) ->
270
    let fanin = (IMap.find m.mname.node_id node_schs).Scheduling.fanin_table in
271
    let elim_consts, _ = instrs_unfold fanin IMap.empty (List.map instr_of_const consts) in
272
    let (m, removed_m) =  machine_unfold fanin elim_consts m in
273
    (m::machines, IMap.add m.mname.node_id removed_m removed)
274
    )
275 d0b1ec56 xthirioux
    machines
276 04a63d25 xthirioux
    ([], IMap.empty)
277 cf78a589 ploc
278 c287ba28 xthirioux
let get_assign_lhs instr =
279 3ca27bc7 ploc
  match get_instr_desc instr with
280 04a63d25 xthirioux
  | MLocalAssign(v, e) -> mk_val (LocalVar v) e.value_type
281
  | MStateAssign(v, e) -> mk_val (StateVar v) e.value_type
282 c287ba28 xthirioux
  | _                  -> assert false
283
284
let get_assign_rhs instr =
285 3ca27bc7 ploc
  match get_instr_desc instr with
286 c287ba28 xthirioux
  | MLocalAssign(_, e)
287
  | MStateAssign(_, e) -> e
288
  | _                  -> assert false
289
290
let is_assign instr =
291 3ca27bc7 ploc
  match get_instr_desc instr with
292 c287ba28 xthirioux
  | MLocalAssign _
293
  | MStateAssign _ -> true
294
  | _              -> false
295
296
let mk_assign v e =
297 04a63d25 xthirioux
 match v.value_desc with
298 c287ba28 xthirioux
 | LocalVar v -> MLocalAssign(v, e)
299
 | StateVar v -> MStateAssign(v, e)
300
 | _          -> assert false
301
302
let rec assigns_instr instr assign =
303 3ca27bc7 ploc
  match get_instr_desc instr with  
304 c287ba28 xthirioux
  | MLocalAssign (i,_)
305 017eec6a ploc
  | MStateAssign (i,_) -> VSet.add i assign
306
  | MStep (ol, _, _)   -> List.fold_right VSet.add ol assign
307 c287ba28 xthirioux
  | MBranch (_,hl)     -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
308
  | _                  -> assign
309
310
and assigns_instrs instrs assign =
311
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
312
313
(*    
314
and substitute_expr subst expr =
315
  match expr with
316
  | StateVar v
317
  | LocalVar v -> (try IMap.find expr subst with Not_found -> expr)
318
  | Fun (id, vl) -> Fun (id, List.map (substitute_expr subst) vl)
319
  | Array(vl) -> Array(List.map (substitute_expr subst) vl)
320
  | Access(v1, v2) -> Access(substitute_expr subst v1, substitute_expr subst v2)
321
  | Power(v1, v2) -> Power(substitute_expr subst v1, substitute_expr subst v2)
322
  | Cst _  -> expr
323
*)
324
(** Finds a substitute for [instr] in [instrs], 
325
   i.e. another instr' with the same rhs expression.
326
   Then substitute this expression with the first assigned var
327
*)
328
let subst_instr subst instrs instr =
329
  (*Format.eprintf "subst instr: %a@." Machine_code.pp_instr instr;*)
330
  let instr = eliminate subst instr in
331
  let v = get_assign_lhs instr in
332
  let e = get_assign_rhs instr in
333 85da3a4b ploc
  (* Difficulties to merge with unstable. Here is the other code:
334
335
try
336 c287ba28 xthirioux
    let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in
337 53206908 xthirioux
    match v.value_desc with
338 c287ba28 xthirioux
    | LocalVar v ->
339
      IMap.add v.var_id (get_assign_lhs instr') subst, instrs
340
    | StateVar v ->
341 53206908 xthirioux
      let lhs' = get_assign_lhs instr' in
342
      let typ' = lhs'.value_type in
343
      (match lhs'.value_desc with
344 c287ba28 xthirioux
      | LocalVar v' ->
345 53206908 xthirioux
	let instr = eliminate subst (mk_assign (mk_val (StateVar v) typ') (mk_val (LocalVar v') typ')) in
346 c287ba28 xthirioux
	subst, instr :: instrs
347
      | StateVar v' ->
348 53206908 xthirioux
	let subst_v' = IMap.add v'.var_id (mk_val (StateVar v) typ') IMap.empty in
349
let instrs' = snd (List.fold_right (fun instr (ok, instrs) -> (ok || instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in
350
	IMap.add v'.var_id (mk_val (StateVar v) typ') subst, instr :: instrs'
351 c287ba28 xthirioux
      | _           -> assert false)
352
    | _          -> assert false
353
  with Not_found -> subst, instr :: instrs
354
 
355 85da3a4b ploc
*)
356
357
try
358 c287ba28 xthirioux
    let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in
359 04a63d25 xthirioux
    match v.value_desc with
360 c287ba28 xthirioux
    | LocalVar v ->
361
      IMap.add v.var_id (get_assign_lhs instr') subst, instrs
362 04a63d25 xthirioux
    | StateVar stv ->
363
       let lhs = get_assign_lhs instr' in
364
      (match lhs.value_desc with
365 c287ba28 xthirioux
      | LocalVar v' ->
366 3ca27bc7 ploc
        let instr = eliminate subst (update_instr_desc instr (mk_assign v lhs)) in
367 c287ba28 xthirioux
	subst, instr :: instrs
368 04a63d25 xthirioux
      | StateVar stv' ->
369
	let subst_v' = IMap.add stv'.var_id v IMap.empty in
370 c287ba28 xthirioux
	let instrs' = snd (List.fold_right (fun instr (ok, instrs) -> (ok || instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in
371 04a63d25 xthirioux
	IMap.add stv'.var_id v subst, instr :: instrs'
372 c287ba28 xthirioux
      | _           -> assert false)
373
    | _          -> assert false
374
  with Not_found -> subst, instr :: instrs
375
 
376
(** Common sub-expression elimination for machine instructions *)
377
(* - [subst] : hashtable from ident to (simple) definition
378
               it is an equivalence table
379
   - [elim]   : set of eliminated variables
380
   - [instrs] : previous instructions, which [instr] is compared against
381
   - [instr] : current instruction, normalized by [subst]
382
*)
383
let rec instr_cse (subst, instrs) instr =
384 3ca27bc7 ploc
  match get_instr_desc instr with
385 c287ba28 xthirioux
  (* Simple cases*)
386 04a63d25 xthirioux
  | MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
387 3ca27bc7 ploc
      -> instr_cse (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
388 d7b73fed xthirioux
  | MLocalAssign(v, expr) when is_unfoldable_expr 2 expr
389 c287ba28 xthirioux
      -> (IMap.add v.var_id expr subst, instr :: instrs)
390
  | _ when is_assign instr
391
      -> subst_instr subst instrs instr
392
  | _ -> (subst, instr :: instrs)
393
394
(** Apply common sub-expression elimination to a sequence of instrs
395
*)
396
let rec instrs_cse subst instrs =
397
  let subst, rev_instrs = 
398
    List.fold_left instr_cse (subst, []) instrs
399
  in subst, List.rev rev_instrs
400
401
(** Apply common sub-expression elimination to a machine
402
    - iterate through step instructions and remove simple local assigns
403
*)
404
let machine_cse subst machine =
405
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)
406
  let subst, instrs = instrs_cse subst machine.mstep.step_instrs in
407 017eec6a ploc
  let assigned = assigns_instrs instrs VSet.empty
408 c287ba28 xthirioux
  in
409
  {
410
    machine with
411 017eec6a ploc
      mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
412 c287ba28 xthirioux
      mstep = { 
413
	machine.mstep with 
414 017eec6a ploc
	  step_locals = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mstep.step_locals;
415 c287ba28 xthirioux
	  step_instrs = instrs
416
      }
417
  }
418
419
let machines_cse machines =
420
  List.map
421
    (machine_cse IMap.empty)
422
    machines
423
424 45c13277 xthirioux
(* variable substitution for optimizing purposes *)
425
426
(* checks whether an [instr] is skip and can be removed from program *)
427
let rec instr_is_skip instr =
428 3ca27bc7 ploc
  match get_instr_desc instr with
429 04a63d25 xthirioux
  | MLocalAssign (i, { value_desc = (LocalVar v) ; _}) when i = v -> true
430
  | MStateAssign (i, { value_desc = StateVar v; _}) when i = v -> true
431 45c13277 xthirioux
  | MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
432
  | _               -> false
433
and instrs_are_skip instrs =
434
  List.for_all instr_is_skip instrs
435
436
let instr_cons instr cont =
437
 if instr_is_skip instr then cont else instr::cont
438
439
let rec instr_remove_skip instr cont =
440 3ca27bc7 ploc
  match get_instr_desc instr with
441 04a63d25 xthirioux
  | MLocalAssign (i, { value_desc = LocalVar v; _ }) when i = v -> cont
442
  | MStateAssign (i, { value_desc = StateVar v; _ }) when i = v -> cont
443 3ca27bc7 ploc
  | MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont
444 45c13277 xthirioux
  | _               -> instr::cont
445
446
and instrs_remove_skip instrs cont =
447
  List.fold_right instr_remove_skip instrs cont
448
449
let rec value_replace_var fvar value =
450 04a63d25 xthirioux
  match value.value_desc with
451 45c13277 xthirioux
  | Cst c -> value
452 04a63d25 xthirioux
  | LocalVar v -> { value with value_desc = LocalVar (fvar v) }
453 45c13277 xthirioux
  | StateVar v -> value
454 04a63d25 xthirioux
  | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
455
  | Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
456
  | Access (t, i) -> { value with value_desc = Access(value_replace_var fvar t, i)}
457
  | Power (v, n) -> { value with value_desc = Power(value_replace_var fvar v, n)}
458 45c13277 xthirioux
459
let rec instr_replace_var fvar instr cont =
460 3ca27bc7 ploc
  match get_instr_desc instr with
461 04a63d25 xthirioux
  | MComment _          -> instr_cons instr cont
462 3ca27bc7 ploc
  | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
463
  | MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
464 45c13277 xthirioux
  | MReset i            -> instr_cons instr cont
465 eb837d74 xthirioux
  | MNoReset i          -> instr_cons instr cont
466 3ca27bc7 ploc
  | MStep (il, i, vl)   -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont
467
  | MBranch (g, hl)     -> instr_cons (update_instr_desc instr (MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il [])) hl))) cont
468 45c13277 xthirioux
469
and instrs_replace_var fvar instrs cont =
470
  List.fold_right (instr_replace_var fvar) instrs cont
471
472
let step_replace_var fvar step =
473
  (* Some outputs may have been replaced by locals.
474
     We then need to rename those outputs
475
     without changing their clocks, etc *)
476
  let outputs' =
477
    List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs in
478
  let locals'  =
479
    List.fold_left (fun res l ->
480
      let l' = fvar l in
481
      if List.exists (fun o -> o.var_id = l'.var_id) outputs'
482
      then res
483
      else Utils.add_cons l' res)
484
      [] step.step_locals in
485
  { step with
486
    step_checks = List.map (fun (l, v) -> (l, value_replace_var fvar v)) step.step_checks;
487
    step_outputs = outputs';
488
    step_locals = locals';
489
    step_instrs = instrs_replace_var fvar step.step_instrs [];
490
}
491
492
let rec machine_replace_variables fvar m =
493
  { m with
494
    mstep = step_replace_var fvar m.mstep
495
  }
496
497
let machine_reuse_variables m reuse =
498
  let fvar v =
499
    try
500
      Hashtbl.find reuse v.var_id
501
    with Not_found -> v in
502
  machine_replace_variables fvar m
503
504 04a63d25 xthirioux
let machines_reuse_variables prog reuse_tables =
505 45c13277 xthirioux
  List.map 
506
    (fun m -> 
507 04a63d25 xthirioux
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables)
508 45c13277 xthirioux
    ) prog
509
510 b1655a21 xthirioux
let rec instr_assign res instr =
511 3ca27bc7 ploc
  match get_instr_desc instr with
512 b1655a21 xthirioux
  | MLocalAssign (i, _) -> Disjunction.CISet.add i res
513
  | MStateAssign (i, _) -> Disjunction.CISet.add i res
514
  | MBranch (g, hl)     -> List.fold_left (fun res (h, b) -> instrs_assign res b) res hl
515
  | MStep (il, _, _)    -> List.fold_right Disjunction.CISet.add il res
516
  | _                   -> res
517
518
and instrs_assign res instrs =
519
  List.fold_left instr_assign res instrs
520
521
let rec instr_constant_assign var instr =
522 3ca27bc7 ploc
  match get_instr_desc instr with
523 04a63d25 xthirioux
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
524
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var
525 b1655a21 xthirioux
  | MBranch (g, hl)                     -> List.for_all (fun (h, b) -> instrs_constant_assign var b) hl
526
  | _                                   -> false
527
528
and instrs_constant_assign var instrs =
529
  List.fold_left (fun res i -> if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then instr_constant_assign var i else res) false instrs
530
531
let rec instr_reduce branches instr1 cont =
532 3ca27bc7 ploc
  match get_instr_desc instr1 with
533 04a63d25 xthirioux
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
534
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
535 3ca27bc7 ploc
  | MBranch (g, hl)                     -> (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl))) :: cont
536 b1655a21 xthirioux
  | _                                   -> instr1 :: cont
537
538
and instrs_reduce branches instrs cont =
539
 match instrs with
540
 | []        -> cont
541
 | [i]       -> instr_reduce branches i cont
542
 | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont
543
544
let rec instrs_fusion instrs =
545 3ca27bc7 ploc
  match instrs, List.map get_instr_desc instrs with
546
  | [], []
547
  | [_], [_]                                                               ->
548 b1655a21 xthirioux
    instrs
549 3ca27bc7 ploc
  | i1::i2::q, i1_desc::(MBranch ({ value_desc = LocalVar v; _}, hl))::q_desc when instr_constant_assign v i1 ->
550 b1655a21 xthirioux
    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)
551 3ca27bc7 ploc
  | i1::i2::q, i1_desc::(MBranch ({ value_desc = StateVar v; _}, hl))::q_desc when instr_constant_assign v i1 ->
552 b1655a21 xthirioux
    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q) 
553 3ca27bc7 ploc
  | i1::i2::q, _                                                         ->
554 b1655a21 xthirioux
    i1 :: instrs_fusion (i2::q)
555 3ca27bc7 ploc
  | _ -> assert false (* Other cases should not happen since both lists are of same size *)
556
     
557 b1655a21 xthirioux
let step_fusion step =
558
  { step with
559
    step_instrs = instrs_fusion step.step_instrs;
560
  }
561
562
let rec machine_fusion m =
563
  { m with
564
    mstep = step_fusion m.mstep
565
  }
566
567
let machines_fusion prog =
568
  List.map machine_fusion prog
569 cf78a589 ploc
570 13507742 ploc
571
(*** Main function ***)
572
    
573
let optimize prog node_schs machine_code =
574
  let machine_code =
575
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
576
      begin
577
	Log.report ~level:1 
578
	  (fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,");
579
	let machine_code = machines_cse machine_code in
580
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code);
581
	machine_code
582
      end
583
    else
584
      machine_code
585
  in
586
  (* Optimize machine code *)
587
  let machine_code, removed_table = 
588
    if !Options.optimization >= 2 && !Options.output <> "emf" (*&& !Options.output <> "horn"*) then
589
      begin
590
	Log.report ~level:1 (fun fmt -> Format.fprintf fmt 
591
	  ".. machines optimization: const. inlining (partial eval. with const)@,");
592
	let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in
593
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ "
594
	  (pp_imap pp_elim) removed_table);
595
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code);	
596
	machine_code, removed_table
597
      end
598
    else
599
      machine_code, IMap.empty
600
  in  
601
  (* Optimize machine code *)
602
  let machine_code =
603
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then
604
      begin
605
	Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
606
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
607
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
608
	machines_fusion (machines_reuse_variables machine_code reuse_tables)
609
      end
610
    else
611
      machine_code
612
  in
613
  
614
  (* Salsa optimize machine code *)
615
  (*
616
  let machine_code = 
617
    if !Options.salsa_enabled then
618
      begin
619
	check_main ();
620
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
621
	(* Selecting float constants for Salsa *)
622
	let constEnv = List.fold_left (
623
	  fun accu c_topdecl ->
624
	    match c_topdecl.top_decl_desc with
625
	    | Const c when Types.is_real_type c.const_type  ->
626
	      (c.const_id, c.const_value) :: accu
627
	    | _ -> accu
628
	) [] (Corelang.get_consts prog) 
629
	in
630
	List.map 
631
	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) 
632
	  machine_code 
633
      end
634
    else
635
      machine_code
636
  in
637
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
638
    (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
639
    machine_code);
640
  *)
641
642
643
    machine_code  
644
    
645
    
646 cf78a589 ploc
(* Local Variables: *)
647
(* compile-command:"make -C .." *)
648
(* End: *)