Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / optimize_machine.ml @ 4f26dcf5

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