Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / optimize_machine.ml @ e6b644f4

History | View | Annotate | Download (26.3 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 c35de73b ploc
let pp_elim m fmt elim =
22 d0b1ec56 xthirioux
  begin
23 521e2a6b ploc
    Format.fprintf fmt "@[{ /* elim table: */@ ";
24 c35de73b ploc
    IMap.iter (fun v expr -> Format.fprintf fmt "%s |-> %a@ " v (pp_val m) expr) elim;
25 521e2a6b ploc
    Format.fprintf fmt "}@ @]";
26 d0b1ec56 xthirioux
  end
27
28 c35de73b ploc
let rec eliminate m elim instr =
29
  let e_expr = eliminate_expr m elim in
30 3ca27bc7 ploc
  match get_instr_desc instr with
31 1fd3d002 ploc
  | MSpec _ | 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 c35de73b ploc
	     (fun (l, il) -> l, List.map (eliminate m elim) il) 
43 3ca27bc7 ploc
	     hl
44
	  )
45
	 )
46
     )
47 cf78a589 ploc
    
48 c35de73b ploc
and eliminate_expr m elim expr =
49
  let eliminate_expr = eliminate_expr m in
50 04a63d25 xthirioux
  match expr.value_desc with
51 c35de73b ploc
  | Var v -> if is_memory m v then expr else (try IMap.find v.var_id elim with Not_found -> expr)
52 04a63d25 xthirioux
  | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
53
  | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
54
  | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
55
  | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
56 c35de73b ploc
  | Cst _ -> expr
57 cf78a589 ploc
58 ec433d69 xthirioux
let eliminate_dim elim dim =
59 45f0f48d xthirioux
  Dimension.expr_replace_expr 
60
    (fun v -> try
61
		dimension_of_value (IMap.find v elim) 
62
      with Not_found -> mkdim_ident dim.dim_loc v) 
63
    dim
64 ec433d69 xthirioux
65 ca88e660 Ploc
66
(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following
67
   functions seem unsused. They have to be adapted to the new type for expr
68 d2d9d4cb ploc
*)
69 ca88e660 Ploc
70 d7b73fed xthirioux
let unfold_expr_offset m offset expr =
71 04a63d25 xthirioux
  List.fold_left
72
    (fun res -> (function | Index i -> mk_val (Access (res, value_of_dimension m i))
73
					      (Types.array_element_type res.value_type)
74
                          | Field f -> Format.eprintf "internal error: not yet implemented !"; assert false))
75
    expr offset
76 d7b73fed xthirioux
77 04a63d25 xthirioux
let rec simplify_cst_expr m offset typ cst =
78 d7b73fed xthirioux
    match offset, cst with
79
    | []          , _
80 04a63d25 xthirioux
      -> mk_val (Cst cst) typ
81 d7b73fed xthirioux
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i
82 04a63d25 xthirioux
      -> let elt_typ = Types.array_element_type typ in
83
         simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const_dimension i))
84 d7b73fed xthirioux
    | Index i :: q, Const_array cl
85 04a63d25 xthirioux
      -> let elt_typ = Types.array_element_type typ in
86
         unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
87 d7b73fed xthirioux
    | Field f :: q, Const_struct fl
88 04a63d25 xthirioux
      -> let fld_typ = Types.struct_field_type typ f in
89
         simplify_cst_expr m q fld_typ (List.assoc f fl)
90 d7b73fed xthirioux
    | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false)
91
92
let simplify_expr_offset m expr =
93
  let rec simplify offset expr =
94 04a63d25 xthirioux
    match offset, expr.value_desc with
95 d7b73fed xthirioux
    | Field f ::q , _                -> failwith "not yet implemented"
96 04a63d25 xthirioux
    | _           , Fun (id, vl) when Basic_library.is_value_internal_fun expr
97
                                     -> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
98 d7b73fed xthirioux
    | _           , Fun _
99 c35de73b ploc
    | _           , Var _            -> 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 1fd3d002 ploc
  | MSpec _ | 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 c35de73b ploc
    | _           , Var _                        -> true
155 d7b73fed xthirioux
    | []          , 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 c35de73b ploc
let rec instrs_unfold m fanin elim instrs =
191 d0b1ec56 xthirioux
  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 c35de73b ploc
      let instr = eliminate m elim instr in
196 d0b1ec56 xthirioux
      (* if instr is a simple local assign, then (a) elim is simplified with it (b) it
197
	 is stored as the elim set *)
198 c35de73b ploc
      instr_unfold m fanin instrs elim instr
199 d0b1ec56 xthirioux
    ) (elim, []) instrs
200
  in elim, List.rev rev_instrs
201
202 c35de73b ploc
and instr_unfold m 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 c35de73b ploc
    -> instr_unfold m 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 c35de73b ploc
    -> let elim_branches = List.map (fun (h, l) -> (h, instrs_unfold m fanin elim l)) hl in
212 d0b1ec56 xthirioux
       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 2863281f ploc
      dimension_of_value (IMap.find v elim)
231 ec433d69 xthirioux
    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 c35de73b ploc
  let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
241
  let elim_vars, instrs = instrs_unfold machine fanin elim_consts machine.mstep.step_instrs in
242 d7b73fed xthirioux
  let instrs = simplify_instrs_offset machine instrs in
243 c35de73b ploc
  let checks = List.map (fun (loc, check) -> loc, eliminate_expr machine 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 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
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 1fd3d002 ploc
(* We do not perform this optimization on contract nodes since there
269
   is not explicit dependence btw variables and their use in
270
   contracts. *)
271 d0b1ec56 xthirioux
let machines_unfold consts node_schs machines =
272 04a63d25 xthirioux
  List.fold_right (fun m (machines, removed) ->
273 1fd3d002 ploc
      let is_contract = match m.mspec with Some (Contract _) -> true | _ -> false in
274
      if is_contract then
275
        m::machines, removed
276
      else
277
        let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in
278
        let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in
279
        let (m, removed_m) =  machine_unfold fanin elim_consts m in
280
        (m::machines, IMap.add m.mname.node_id removed_m removed)
281 04a63d25 xthirioux
    )
282 d0b1ec56 xthirioux
    machines
283 04a63d25 xthirioux
    ([], IMap.empty)
284 cf78a589 ploc
285 c287ba28 xthirioux
let get_assign_lhs instr =
286 3ca27bc7 ploc
  match get_instr_desc instr with
287 c35de73b ploc
  | MLocalAssign(v, e) -> mk_val (Var v) e.value_type
288
  | MStateAssign(v, e) -> mk_val (Var v) e.value_type
289 c287ba28 xthirioux
  | _                  -> assert false
290
291
let get_assign_rhs instr =
292 3ca27bc7 ploc
  match get_instr_desc instr with
293 c287ba28 xthirioux
  | MLocalAssign(_, e)
294
  | MStateAssign(_, e) -> e
295
  | _                  -> assert false
296
297
let is_assign instr =
298 3ca27bc7 ploc
  match get_instr_desc instr with
299 c287ba28 xthirioux
  | MLocalAssign _
300
  | MStateAssign _ -> true
301
  | _              -> false
302
303 c35de73b ploc
let mk_assign m v e =
304 04a63d25 xthirioux
 match v.value_desc with
305 c35de73b ploc
 | Var v -> if is_memory m v then MStateAssign(v, e) else MLocalAssign(v, e)
306 c287ba28 xthirioux
 | _          -> assert false
307
308
let rec assigns_instr instr assign =
309 3ca27bc7 ploc
  match get_instr_desc instr with  
310 c287ba28 xthirioux
  | MLocalAssign (i,_)
311 017eec6a ploc
  | MStateAssign (i,_) -> VSet.add i assign
312
  | MStep (ol, _, _)   -> List.fold_right VSet.add ol assign
313 c287ba28 xthirioux
  | MBranch (_,hl)     -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
314
  | _                  -> assign
315
316
and assigns_instrs instrs assign =
317
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
318
319
(*    
320
and substitute_expr subst expr =
321
  match expr with
322 c35de73b ploc
  | Var v -> (try IMap.find expr subst with Not_found -> expr)
323 c287ba28 xthirioux
  | Fun (id, vl) -> Fun (id, List.map (substitute_expr subst) vl)
324
  | Array(vl) -> Array(List.map (substitute_expr subst) vl)
325
  | Access(v1, v2) -> Access(substitute_expr subst v1, substitute_expr subst v2)
326
  | Power(v1, v2) -> Power(substitute_expr subst v1, substitute_expr subst v2)
327
  | Cst _  -> expr
328
*)
329
(** Finds a substitute for [instr] in [instrs], 
330
   i.e. another instr' with the same rhs expression.
331
   Then substitute this expression with the first assigned var
332
*)
333 c35de73b ploc
let subst_instr m subst instrs instr =
334 c287ba28 xthirioux
  (*Format.eprintf "subst instr: %a@." Machine_code.pp_instr instr;*)
335 c35de73b ploc
  let instr = eliminate m subst instr in
336
  let instr_v = get_assign_lhs instr in  
337
  let instr_e = get_assign_rhs instr in
338
  try
339
    (* Searching for equivalent asssign *)
340
    let instr' = List.find (fun instr' -> is_assign instr' &&
341
                                            get_assign_rhs instr' = instr_e) instrs in
342
    (* Registering the instr_v as instr'_v while replacing *)
343
    match instr_v.value_desc with
344
    | Var v ->
345
       if not (is_memory m v) then
346
         (* The current instruction defines a local variables, ie not
347
            memory, we can just record the relationship and continue
348
          *)
349
         IMap.add v.var_id (get_assign_lhs instr') subst, instrs
350
       else  (
351
         (* The current instruction defines a memory. We need to keep
352
            the definition, simplified *)
353
         let instr'_v = get_assign_lhs instr' in
354
         (match instr'_v.value_desc with
355
          | Var v' ->
356
             if not (is_memory m v') then
357
               (* We define v' = v. Don't need to update the records. *)
358
               let instr = eliminate m subst (update_instr_desc instr (mk_assign m instr_v instr'_v)) in
359
	       subst, instr :: instrs
360
             else ( (* Last case, v', the lhs of the previous similar
361
                       definition is, itself, a memory *)
362
363
               (* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *)
364
               (* Filtering out the list of instructions: 
365
                  - we copy in the same order the list of instr in instrs (fold_right)
366
                  - if the current instr is this instr' then apply 
367
                    the elimination with v' -> v on instr' before recording it as an instruction.  
368
                *)
369
               let subst_v' = IMap.add v'.var_id instr_v IMap.empty in
370
	       let instrs' =
371
                 snd
372
                   (List.fold_right
373
                      (fun instr (ok, instrs) ->
374
                        (ok || instr = instr',
375
                         if ok then
376
                           instr :: instrs
377
                         else
378
                           if instr = instr' then
379
                             instrs
380
                           else
381
                             eliminate m subst_v' instr :: instrs))
382
                      instrs (false, []))
383
               in
384
	       IMap.add v'.var_id instr_v subst, instr :: instrs'
385
             )
386
          | _           -> assert false)
387
       )
388 c287ba28 xthirioux
    | _          -> assert false
389 c35de73b ploc
                  
390
  with Not_found ->
391
    (* No such equivalent expr: keeping the definition *)
392
    subst, instr :: instrs
393
                
394 c287ba28 xthirioux
(** Common sub-expression elimination for machine instructions *)
395
(* - [subst] : hashtable from ident to (simple) definition
396
               it is an equivalence table
397
   - [elim]   : set of eliminated variables
398
   - [instrs] : previous instructions, which [instr] is compared against
399
   - [instr] : current instruction, normalized by [subst]
400
*)
401 c35de73b ploc
let rec instr_cse m (subst, instrs) instr =
402 3ca27bc7 ploc
  match get_instr_desc instr with
403 c287ba28 xthirioux
  (* Simple cases*)
404 04a63d25 xthirioux
  | MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
405 c35de73b ploc
      -> instr_cse m (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
406 d7b73fed xthirioux
  | MLocalAssign(v, expr) when is_unfoldable_expr 2 expr
407 c287ba28 xthirioux
      -> (IMap.add v.var_id expr subst, instr :: instrs)
408
  | _ when is_assign instr
409 c35de73b ploc
      -> subst_instr m subst instrs instr
410 c287ba28 xthirioux
  | _ -> (subst, instr :: instrs)
411
412
(** Apply common sub-expression elimination to a sequence of instrs
413
*)
414 c35de73b ploc
let instrs_cse m subst instrs =
415 c287ba28 xthirioux
  let subst, rev_instrs = 
416 c35de73b ploc
    List.fold_left (instr_cse m) (subst, []) instrs
417 c287ba28 xthirioux
  in subst, List.rev rev_instrs
418
419
(** Apply common sub-expression elimination to a machine
420
    - iterate through step instructions and remove simple local assigns
421
*)
422
let machine_cse subst machine =
423
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)
424 c35de73b ploc
  let subst, instrs = instrs_cse machine subst machine.mstep.step_instrs in
425 017eec6a ploc
  let assigned = assigns_instrs instrs VSet.empty
426 c287ba28 xthirioux
  in
427
  {
428
    machine with
429 017eec6a ploc
      mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
430 c287ba28 xthirioux
      mstep = { 
431
	machine.mstep with 
432 017eec6a ploc
	  step_locals = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mstep.step_locals;
433 c287ba28 xthirioux
	  step_instrs = instrs
434
      }
435
  }
436
437
let machines_cse machines =
438
  List.map
439
    (machine_cse IMap.empty)
440
    machines
441
442 45c13277 xthirioux
(* variable substitution for optimizing purposes *)
443
444
(* checks whether an [instr] is skip and can be removed from program *)
445
let rec instr_is_skip instr =
446 3ca27bc7 ploc
  match get_instr_desc instr with
447 c35de73b ploc
  | MLocalAssign (i, { value_desc = (Var v) ; _}) when i = v -> true
448
  | MStateAssign (i, { value_desc = Var v; _}) when i = v -> true
449 45c13277 xthirioux
  | MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
450
  | _               -> false
451
and instrs_are_skip instrs =
452
  List.for_all instr_is_skip instrs
453
454
let instr_cons instr cont =
455
 if instr_is_skip instr then cont else instr::cont
456
457
let rec instr_remove_skip instr cont =
458 3ca27bc7 ploc
  match get_instr_desc instr with
459 c35de73b ploc
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v -> cont
460
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v -> cont
461 3ca27bc7 ploc
  | MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont
462 45c13277 xthirioux
  | _               -> instr::cont
463
464
and instrs_remove_skip instrs cont =
465
  List.fold_right instr_remove_skip instrs cont
466
467
let rec value_replace_var fvar value =
468 04a63d25 xthirioux
  match value.value_desc with
469 45c13277 xthirioux
  | Cst c -> value
470 c35de73b ploc
  | Var v -> { value with value_desc = Var (fvar v) }
471 04a63d25 xthirioux
  | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
472
  | Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
473
  | Access (t, i) -> { value with value_desc = Access(value_replace_var fvar t, i)}
474
  | Power (v, n) -> { value with value_desc = Power(value_replace_var fvar v, n)}
475 45c13277 xthirioux
476
let rec instr_replace_var fvar instr cont =
477 3ca27bc7 ploc
  match get_instr_desc instr with
478 1fd3d002 ploc
  | MSpec _ | MComment _          -> instr_cons instr cont
479 3ca27bc7 ploc
  | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
480
  | MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
481 45c13277 xthirioux
  | MReset i            -> instr_cons instr cont
482 eb837d74 xthirioux
  | MNoReset i          -> instr_cons instr cont
483 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
484
  | 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
485 45c13277 xthirioux
486
and instrs_replace_var fvar instrs cont =
487
  List.fold_right (instr_replace_var fvar) instrs cont
488
489
let step_replace_var fvar step =
490
  (* Some outputs may have been replaced by locals.
491
     We then need to rename those outputs
492
     without changing their clocks, etc *)
493
  let outputs' =
494
    List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs in
495
  let locals'  =
496
    List.fold_left (fun res l ->
497
      let l' = fvar l in
498
      if List.exists (fun o -> o.var_id = l'.var_id) outputs'
499
      then res
500
      else Utils.add_cons l' res)
501
      [] step.step_locals in
502
  { step with
503
    step_checks = List.map (fun (l, v) -> (l, value_replace_var fvar v)) step.step_checks;
504
    step_outputs = outputs';
505
    step_locals = locals';
506
    step_instrs = instrs_replace_var fvar step.step_instrs [];
507
}
508
509
let rec machine_replace_variables fvar m =
510
  { m with
511
    mstep = step_replace_var fvar m.mstep
512
  }
513
514
let machine_reuse_variables m reuse =
515
  let fvar v =
516
    try
517
      Hashtbl.find reuse v.var_id
518
    with Not_found -> v in
519
  machine_replace_variables fvar m
520
521 04a63d25 xthirioux
let machines_reuse_variables prog reuse_tables =
522 45c13277 xthirioux
  List.map 
523
    (fun m -> 
524 04a63d25 xthirioux
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables)
525 45c13277 xthirioux
    ) prog
526
527 b1655a21 xthirioux
let rec instr_assign res instr =
528 3ca27bc7 ploc
  match get_instr_desc instr with
529 b1655a21 xthirioux
  | MLocalAssign (i, _) -> Disjunction.CISet.add i res
530
  | MStateAssign (i, _) -> Disjunction.CISet.add i res
531
  | MBranch (g, hl)     -> List.fold_left (fun res (h, b) -> instrs_assign res b) res hl
532
  | MStep (il, _, _)    -> List.fold_right Disjunction.CISet.add il res
533
  | _                   -> res
534
535
and instrs_assign res instrs =
536
  List.fold_left instr_assign res instrs
537
538
let rec instr_constant_assign var instr =
539 3ca27bc7 ploc
  match get_instr_desc instr with
540 04a63d25 xthirioux
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
541
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var
542 b1655a21 xthirioux
  | MBranch (g, hl)                     -> List.for_all (fun (h, b) -> instrs_constant_assign var b) hl
543
  | _                                   -> false
544
545
and instrs_constant_assign var instrs =
546
  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
547
548
let rec instr_reduce branches instr1 cont =
549 3ca27bc7 ploc
  match get_instr_desc instr1 with
550 04a63d25 xthirioux
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
551
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
552 3ca27bc7 ploc
  | MBranch (g, hl)                     -> (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl))) :: cont
553 b1655a21 xthirioux
  | _                                   -> instr1 :: cont
554
555
and instrs_reduce branches instrs cont =
556
 match instrs with
557
 | []        -> cont
558
 | [i]       -> instr_reduce branches i cont
559
 | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont
560
561
let rec instrs_fusion instrs =
562 3ca27bc7 ploc
  match instrs, List.map get_instr_desc instrs with
563
  | [], []
564
  | [_], [_]                                                               ->
565 b1655a21 xthirioux
    instrs
566 c35de73b ploc
  | i1::i2::q, i1_desc::(MBranch ({ value_desc = Var v; _}, hl))::q_desc when instr_constant_assign v i1 ->
567 b1655a21 xthirioux
    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)
568 3ca27bc7 ploc
  | i1::i2::q, _                                                         ->
569 b1655a21 xthirioux
    i1 :: instrs_fusion (i2::q)
570 3ca27bc7 ploc
  | _ -> assert false (* Other cases should not happen since both lists are of same size *)
571
     
572 b1655a21 xthirioux
let step_fusion step =
573
  { step with
574
    step_instrs = instrs_fusion step.step_instrs;
575
  }
576
577
let rec machine_fusion m =
578
  { m with
579
    mstep = step_fusion m.mstep
580
  }
581
582
let machines_fusion prog =
583
  List.map machine_fusion prog
584 cf78a589 ploc
585 13507742 ploc
586
(*** Main function ***)
587
    
588
let optimize prog node_schs machine_code =
589
  let machine_code =
590
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
591
      begin
592
	Log.report ~level:1 
593
	  (fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,");
594
	let machine_code = machines_cse machine_code in
595 2863281f ploc
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "pp_machines machine_code);
596 13507742 ploc
	machine_code
597
      end
598
    else
599
      machine_code
600
  in
601
  (* Optimize machine code *)
602
  let machine_code, removed_table = 
603 1fd3d002 ploc
    if !Options.optimization >= 2
604
       && !Options.output <> "emf" (*&& !Options.output <> "horn"*)
605
    then
606 13507742 ploc
      begin
607
	Log.report ~level:1 (fun fmt -> Format.fprintf fmt 
608
	  ".. machines optimization: const. inlining (partial eval. with const)@,");
609
	let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in
610
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ "
611 c35de73b ploc
	  (pp_imap (pp_elim empty_machine)) removed_table);
612 2863281f ploc
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (const inlining):@ %a@ "pp_machines machine_code);	
613 13507742 ploc
	machine_code, removed_table
614
      end
615
    else
616
      machine_code, IMap.empty
617
  in  
618
  (* Optimize machine code *)
619
  let machine_code =
620
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then
621
      begin
622
	Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
623
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
624
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
625
	machines_fusion (machines_reuse_variables machine_code reuse_tables)
626
      end
627
    else
628
      machine_code
629
  in
630
  
631
632 1fd3d002 ploc
   List.rev machine_code  
633 13507742 ploc
    
634
    
635 cf78a589 ploc
(* Local Variables: *)
636
(* compile-command:"make -C .." *)
637
(* End: *)