Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/optimize_machine.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open Lustre_types 
13
open Lustre_types
14 14
open Machine_code_types
15 15
open Corelang
16 16
open Causality
......
18 18
open Dimension
19 19
module Mpfr = Lustrec_mpfr
20 20

  
21

  
22 21
let pp_elim m fmt elim =
23 22
  pp_imap ~comment:"/* elim table: */" (pp_val m) fmt elim
24
  (* Format.fprintf fmt "@[<hv 0>@[<hv 2>{ /* elim table: */";
25
   * IMap.iter (fun v expr -> Format.fprintf fmt "@ %s |-> %a," v (pp_val m) expr) elim;
26
   * Format.fprintf fmt "@]@ }@]" *)
23
(* Format.fprintf fmt "@[<hv 0>@[<hv 2>{ /* elim table: */";
24
 * IMap.iter (fun v expr -> Format.fprintf fmt "@ %s |-> %a," v (pp_val m) expr) elim;
25
 * Format.fprintf fmt "@]@ }@]" *)
27 26

  
28 27
let rec eliminate m elim instr =
29 28
  let e_expr = eliminate_expr m elim in
30 29
  match get_instr_desc instr with
31
  | 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))
30
  | MLocalAssign (i, v) ->
31
    update_instr_desc instr (MLocalAssign (i, e_expr v))
32
  | MStateAssign (i, v) ->
33
    update_instr_desc instr (MStateAssign (i, e_expr v))
33 34
  | MSetReset _
34 35
  | MNoReset _
35 36
  | MClearReset
36 37
  | MResetAssign _
37 38
  | MSpec _
38
  | MComment _         -> instr
39
  | MStep (il, i, vl)  -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
40
  | MBranch (g,hl)     -> 
41
     update_instr_desc instr (
42
       MBranch
43
	 (e_expr g, 
44
	  (List.map 
45
	     (fun (l, il) -> l, List.map (eliminate m elim) il) 
46
	     hl
47
	  )
48
	 )
49
     )
50
    
39
  | MComment _ ->
40
    instr
41
  | MStep (il, i, vl) ->
42
    update_instr_desc instr (MStep (il, i, List.map e_expr vl))
43
  | MBranch (g, hl) ->
44
    update_instr_desc instr
45
      (MBranch
46
         ( e_expr g,
47
           List.map (fun (l, il) -> l, List.map (eliminate m elim) il) hl ))
48

  
51 49
and eliminate_expr m elim expr =
52 50
  let eliminate_expr = eliminate_expr m in
53 51
  match expr.value_desc with
54
  | Var v -> if is_memory m v then
55
               expr
56
             else
57
               (try IMap.find v.var_id elim with Not_found -> expr)
58
  | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
59
  | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
60
  | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
61
  | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
62
  | Cst _ | ResetFlag -> expr
52
  | Var v -> (
53
    if is_memory m v then expr
54
    else try IMap.find v.var_id elim with Not_found -> expr)
55
  | Fun (id, vl) ->
56
    { expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl) }
57
  | Array vl ->
58
    { expr with value_desc = Array (List.map (eliminate_expr elim) vl) }
59
  | Access (v1, v2) ->
60
    {
61
      expr with
62
      value_desc = Access (eliminate_expr elim v1, eliminate_expr elim v2);
63
    }
64
  | Power (v1, v2) ->
65
    {
66
      expr with
67
      value_desc = Power (eliminate_expr elim v1, eliminate_expr elim v2);
68
    }
69
  | Cst _ | ResetFlag ->
70
    expr
63 71

  
64 72
let eliminate_dim elim dim =
65
  Dimension.expr_replace_expr 
66
    (fun v -> try
67
		dimension_of_value (IMap.find v elim) 
68
      with Not_found -> mkdim_ident dim.dim_loc v) 
73
  Dimension.expr_replace_expr
74
    (fun v ->
75
      try dimension_of_value (IMap.find v elim)
76
      with Not_found -> mkdim_ident dim.dim_loc v)
69 77
    dim
70 78

  
71

  
72 79
(* 8th Jan 2016: issues when merging salsa with horn_encoding: The following
73
   functions seem unsused. They have to be adapted to the new type for expr
74
*)
80
   functions seem unsused. They have to be adapted to the new type for expr *)
75 81

  
76 82
let unfold_expr_offset m offset expr =
77 83
  List.fold_left
78 84
    (fun res -> function
79
       | Index i ->
80
         mk_val (Access (res, value_of_dimension m i))
81
           (Types.array_element_type res.value_type)
82
       | Field _ ->
83
         Format.eprintf "internal error: not yet implemented !";
84
         assert false)
85
      | Index i ->
86
        mk_val
87
          (Access (res, value_of_dimension m i))
88
          (Types.array_element_type res.value_type)
89
      | Field _ ->
90
        Format.eprintf "internal error: not yet implemented !";
91
        assert false)
85 92
    expr offset
86 93

  
87 94
let rec simplify_cst_expr m offset typ cst =
88
    match offset, cst with
89
    | []          , _
90
      -> mk_val (Cst cst) typ
91
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i
92
      -> let elt_typ = Types.array_element_type typ in
93
         simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const_dimension i))
94
    | Index i :: q, Const_array cl
95
      -> let elt_typ = Types.array_element_type typ in
96
         unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
97
    | Field f :: q, Const_struct fl
98
      -> let fld_typ = Types.struct_field_type typ f in
99
         simplify_cst_expr m q fld_typ (List.assoc f fl)
100
    | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false)
95
  match offset, cst with
96
  | [], _ ->
97
    mk_val (Cst cst) typ
98
  | Index i :: q, Const_array cl when Dimension.is_dimension_const i ->
99
    let elt_typ = Types.array_element_type typ in
100
    simplify_cst_expr m q elt_typ
101
      (List.nth cl (Dimension.size_const_dimension i))
102
  | Index i :: q, Const_array cl ->
103
    let elt_typ = Types.array_element_type typ in
104
    unfold_expr_offset m [ Index i ]
105
      (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
106
  | Field f :: q, Const_struct fl ->
107
    let fld_typ = Types.struct_field_type typ f in
108
    simplify_cst_expr m q fld_typ (List.assoc f fl)
109
  | _ ->
110
    Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@."
111
      Printers.pp_const cst;
112
    assert false
101 113

  
102 114
let simplify_expr_offset m expr =
103 115
  let rec simplify offset expr =
104 116
    match offset, expr.value_desc with
105
    | Field _ ::_ , _                -> failwith "not yet implemented"
106
    | _           , Fun (id, vl) when Basic_library.is_value_internal_fun expr
107
                                     -> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
108
    | _           , Fun _
109
    | _           , Var _            -> unfold_expr_offset m offset expr
110
    | _           , Cst cst          -> simplify_cst_expr m offset expr.value_type cst
111
    | _           , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr
112
    | _           , ResetFlag        -> expr
113
    | []          , _                -> expr
114
    | Index _ :: q, Power (expr, _)  -> simplify q expr
115
    | Index i :: q, Array vl when Dimension.is_dimension_const i
116
                                     -> simplify q (List.nth vl (Dimension.size_const_dimension i))
117
    | Index i :: q, Array vl         -> unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type)
118
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
119
     with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
120
  in simplify [] expr
117
    | Field _ :: _, _ ->
118
      failwith "not yet implemented"
119
    | _, Fun (id, vl) when Basic_library.is_value_internal_fun expr ->
120
      mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
121
    | _, Fun _ | _, Var _ ->
122
      unfold_expr_offset m offset expr
123
    | _, Cst cst ->
124
      simplify_cst_expr m offset expr.value_type cst
125
    | _, Access (expr, i) ->
126
      simplify (Index (dimension_of_value i) :: offset) expr
127
    | _, ResetFlag ->
128
      expr
129
    | [], _ ->
130
      expr
131
    | Index _ :: q, Power (expr, _) ->
132
      simplify q expr
133
    | Index i :: q, Array vl when Dimension.is_dimension_const i ->
134
      simplify q (List.nth vl (Dimension.size_const_dimension i))
135
    | Index i :: q, Array vl ->
136
      unfold_expr_offset m [ Index i ]
137
        (mk_val (Array (List.map (simplify q) vl)) expr.value_type)
138
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr
139
      (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
140
      with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr
141
      (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
142
  in
143
  simplify [] expr
121 144

  
122 145
let rec simplify_instr_offset m instr =
123 146
  match get_instr_desc instr with
124
  | MLocalAssign (v, expr) -> update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
125
  | MStateAssign (v, expr) -> update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
147
  | MLocalAssign (v, expr) ->
148
    update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
149
  | MStateAssign (v, expr) ->
150
    update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
126 151
  | MSetReset _
127 152
  | MNoReset _
128 153
  | MClearReset
129 154
  | MResetAssign _
130 155
  | MSpec _
131
  | MComment _             -> instr
132
  | MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
133
  | MBranch (cond, brl)
134
    -> update_instr_desc instr (
135
      MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
136
    )
137

  
138
and simplify_instrs_offset m instrs =
139
  List.map (simplify_instr_offset m) instrs
156
  | MComment _ ->
157
    instr
158
  | MStep (outputs, id, inputs) ->
159
    update_instr_desc instr
160
      (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
161
  | MBranch (cond, brl) ->
162
    update_instr_desc instr
163
      (MBranch
164
         ( simplify_expr_offset m cond,
165
           List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl ))
166

  
167
and simplify_instrs_offset m instrs = List.map (simplify_instr_offset m) instrs
140 168

  
141 169
let is_scalar_const c =
142
  match c with
143
  | Const_real _
144
  | Const_int _
145
  | Const_tag _   -> true
146
  | _             -> false
147

  
148
(* An instruction v = expr may (and will) be unfolded iff:
149
   - either expr is atomic
150
     (no complex expressions, only const, vars and array/struct accesses)
151
   - or v has a fanin <= 1 (used at most once)
152
*)
170
  match c with Const_real _ | Const_int _ | Const_tag _ -> true | _ -> false
171

  
172
(* An instruction v = expr may (and will) be unfolded iff: - either expr is
173
   atomic (no complex expressions, only const, vars and array/struct accesses) -
174
   or v has a fanin <= 1 (used at most once) *)
153 175
let is_unfoldable_expr fanin expr =
154 176
  let rec unfold_const offset cst =
155 177
    match offset, cst with
156
    | _           , Const_int _
157
    | _           , Const_real _
158
    | _           , Const_tag _     -> true
159
    | Field f :: q, Const_struct fl -> unfold_const q (List.assoc f fl)
160
    | []          , Const_struct _  -> false
161
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i
162
                                    -> unfold_const q (List.nth cl (Dimension.size_const_dimension i))
163
    | _           , Const_array _   -> false
164
    | _                             -> assert false in
178
    | _, Const_int _ | _, Const_real _ | _, Const_tag _ ->
179
      true
180
    | Field f :: q, Const_struct fl ->
181
      unfold_const q (List.assoc f fl)
182
    | [], Const_struct _ ->
183
      false
184
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i ->
185
      unfold_const q (List.nth cl (Dimension.size_const_dimension i))
186
    | _, Const_array _ ->
187
      false
188
    | _ ->
189
      assert false
190
  in
165 191
  let rec unfold offset expr =
166 192
    match offset, expr.value_desc with
167
    | _           , Cst cst                      -> unfold_const offset cst
168
    | _           , Var _                        -> true
169
    | []          , Power _
170
    | []          , Array _                      -> false
171
    | Index _ :: q, Power (v, _)                 -> unfold q v
172
    | Index i :: q, Array vl when Dimension.is_dimension_const i
173
                                                 -> unfold q (List.nth vl (Dimension.size_const_dimension i))
174
    | _           , Array _                      -> false
175
    | _           , Access (v, i)                -> unfold (Index (dimension_of_value i) :: offset) v
176
    | _           , Fun (_, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
177
                                                 -> List.for_all (unfold offset) vl
178
    | _           , Fun _                        -> false
179
    | _                                          -> assert false
180
  in unfold [] expr
193
    | _, Cst cst ->
194
      unfold_const offset cst
195
    | _, Var _ ->
196
      true
197
    | [], Power _ | [], Array _ ->
198
      false
199
    | Index _ :: q, Power (v, _) ->
200
      unfold q v
201
    | Index i :: q, Array vl when Dimension.is_dimension_const i ->
202
      unfold q (List.nth vl (Dimension.size_const_dimension i))
203
    | _, Array _ ->
204
      false
205
    | _, Access (v, i) ->
206
      unfold (Index (dimension_of_value i) :: offset) v
207
    | _, Fun (_, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
208
      ->
209
      List.for_all (unfold offset) vl
210
    | _, Fun _ ->
211
      false
212
    | _ ->
213
      assert false
214
  in
215
  unfold [] expr
181 216

  
182 217
let basic_unfoldable_assign fanin v expr =
183 218
  try
184
    let d = Hashtbl.find fanin v.var_id
185
    in is_unfoldable_expr d expr
219
    let d = Hashtbl.find fanin v.var_id in
220
    is_unfoldable_expr d expr
186 221
  with Not_found -> false
187 222

  
188 223
let unfoldable_assign fanin v expr =
189
   (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
190
&& basic_unfoldable_assign fanin v expr
224
  (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
225
  && basic_unfoldable_assign fanin v expr
191 226

  
192 227
let merge_elim elim1 elim2 =
193 228
  let merge _ e1 e2 =
194 229
    match e1, e2 with
195
    | Some e1, Some e2 -> if e1 = e2 then Some e1 else None
196
    | _      , Some e2 -> Some e2
197
    | Some e1, _       -> Some e1
198
    | _                -> None
199
  in IMap.merge merge elim1 elim2
200

  
201
(* see if elim has to take in account the provided instr:
202
   if so, update elim and return the remove flag,
203
   otherwise, the expression should be kept and elim is left untouched *)
230
    | Some e1, Some e2 ->
231
      if e1 = e2 then Some e1 else None
232
    | _, Some e2 ->
233
      Some e2
234
    | Some e1, _ ->
235
      Some e1
236
    | _ ->
237
      None
238
  in
239
  IMap.merge merge elim1 elim2
240

  
241
(* see if elim has to take in account the provided instr: if so, update elim and
242
   return the remove flag, otherwise, the expression should be kept and elim is
243
   left untouched *)
204 244
let rec instrs_unfold m fanin elim instrs =
205
  let elim, rev_instrs = 
206
    List.fold_left (fun (elim, instrs) instr ->
207
      (* each subexpression in instr that could be rewritten by the elim set is
208
	 rewritten *)
209
      let instr = eliminate m (IMap.map fst elim) instr in
210
      (* if instr is a simple local assign, then (a) elim is simplified with it (b) it
211
	 is stored as the elim set *)
212
      instr_unfold m fanin instrs elim instr
213
    ) (elim, []) instrs
214
  in elim, List.rev rev_instrs
215

  
216
and instr_unfold m fanin instrs (elim:(value_t * eq) IMap.t) instr =
217
(*  Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*)
245
  let elim, rev_instrs =
246
    List.fold_left
247
      (fun (elim, instrs) instr ->
248
        (* each subexpression in instr that could be rewritten by the elim set
249
           is rewritten *)
250
        let instr = eliminate m (IMap.map fst elim) instr in
251
        (* if instr is a simple local assign, then (a) elim is simplified with
252
           it (b) it is stored as the elim set *)
253
        instr_unfold m fanin instrs elim instr)
254
      (elim, []) instrs
255
  in
256
  elim, List.rev rev_instrs
257

  
258
and instr_unfold m fanin instrs (elim : (value_t * eq) IMap.t) instr =
259
  (* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE
260
     IT@." pp_instr instr;*)
218 261
  match get_instr_desc instr with
219 262
  (* Simple cases*)
220
  | MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
221
    -> instr_unfold m fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
222
  | MLocalAssign(v, expr) when not (is_clock_dec_type v.var_dec_type.ty_dec_desc) && unfoldable_assign fanin v expr
223
    -> (* we don't eliminate clock definitions *)
224
     let new_eq =
225
       Corelang.mkeq
226
         (desome instr.lustre_eq).eq_loc
227
         ([v.var_id], (desome instr.lustre_eq).eq_rhs)
228
     in
229
     (IMap.add v.var_id (expr, new_eq )  elim, instrs)
230
  | MBranch(g, hl) when false
231
    -> let elim_branches = List.map (fun (h, l) -> (h, instrs_unfold m fanin elim l)) hl in
232
       let (elim, branches) =
233
	 List.fold_right
234
	   (fun (h, (e, l)) (elim, branches) -> (merge_elim elim e, (h, l)::branches))
235
	   elim_branches (elim, [])
236
       in elim, ((update_instr_desc instr (MBranch (g, branches))) :: instrs)
237
  | _
238
    -> (elim, instr :: instrs)
239
    (* default case, we keep the instruction and do not modify elim *)
240
  
241

  
242
(** We iterate in the order, recording simple local assigns in an accumulator
243
    1. each expression is rewritten according to the accumulator
244
    2. local assigns then rewrite occurrences of the lhs in the computed accumulator
245
*)
263
  | MStep ([ v ], id, vl)
264
    when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
265
    ->
266
    instr_unfold m fanin instrs elim
267
      (update_instr_desc instr
268
         (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
269
  | MLocalAssign (v, expr)
270
    when (not (is_clock_dec_type v.var_dec_type.ty_dec_desc))
271
         && unfoldable_assign fanin v expr ->
272
    (* we don't eliminate clock definitions *)
273
    let new_eq =
274
      Corelang.mkeq (desome instr.lustre_eq).eq_loc
275
        ([ v.var_id ], (desome instr.lustre_eq).eq_rhs)
276
    in
277
    IMap.add v.var_id (expr, new_eq) elim, instrs
278
  | MBranch (g, hl) when false ->
279
    let elim_branches =
280
      List.map (fun (h, l) -> h, instrs_unfold m fanin elim l) hl
281
    in
282
    let elim, branches =
283
      List.fold_right
284
        (fun (h, (e, l)) (elim, branches) ->
285
          merge_elim elim e, (h, l) :: branches)
286
        elim_branches (elim, [])
287
    in
288
    elim, update_instr_desc instr (MBranch (g, branches)) :: instrs
289
  | _ ->
290
    elim, instr :: instrs
291
(* default case, we keep the instruction and do not modify elim *)
292

  
293
(** We iterate in the order, recording simple local assigns in an accumulator 1.
294
    each expression is rewritten according to the accumulator 2. local assigns
295
    then rewrite occurrences of the lhs in the computed accumulator *)
246 296

  
247 297
let static_call_unfold elim (inst, (n, args)) =
248 298
  let replace v =
249
    try
250
      dimension_of_value (IMap.find v elim)
299
    try dimension_of_value (IMap.find v elim)
251 300
    with Not_found -> Dimension.mkdim_ident Location.dummy_loc v
252
  in (inst, (n, List.map (Dimension.expr_replace_expr replace) args))
301
  in
302
  inst, (n, List.map (Dimension.expr_replace_expr replace) args)
253 303

  
254
(** Perform optimization on machine code:
255
    - iterate through step instructions and remove simple local assigns
256
    
257
*)
304
(** Perform optimization on machine code: - iterate through step instructions
305
    and remove simple local assigns *)
258 306
let machine_unfold fanin elim machine =
259
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "machine_unfold %s %a@ "
260
                          machine.mname.node_id (pp_elim machine) (IMap.map fst elim));
307
  Log.report ~level:3 (fun fmt ->
308
      Format.fprintf fmt "machine_unfold %s %a@ " machine.mname.node_id
309
        (pp_elim machine) (IMap.map fst elim));
261 310
  let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
262
  let elim_vars, instrs = instrs_unfold machine fanin elim_consts machine.mstep.step_instrs in
311
  let elim_vars, instrs =
312
    instrs_unfold machine fanin elim_consts machine.mstep.step_instrs
313
  in
263 314
  let instrs = simplify_instrs_offset machine instrs in
264
  let checks = List.map
265
                 (fun (loc, check) ->
266
                   loc,
267
                   eliminate_expr machine (IMap.map fst elim_vars) check
268
                 ) machine.mstep.step_checks
315
  let checks =
316
    List.map
317
      (fun (loc, check) ->
318
        loc, eliminate_expr machine (IMap.map fst elim_vars) check)
319
      machine.mstep.step_checks
320
  in
321
  let locals =
322
    List.filter
323
      (fun v -> not (IMap.mem v.var_id elim_vars))
324
      machine.mstep.step_locals
269 325
  in
270
  let locals = List.filter (fun v -> not (IMap.mem v.var_id elim_vars)) machine.mstep.step_locals in
271 326
  let elim_consts = IMap.map fst elim_consts in
272
  let minstances = List.map (static_call_unfold elim_consts) machine.minstances in
273
  let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls
327
  let minstances =
328
    List.map (static_call_unfold elim_consts) machine.minstances
274 329
  in
275
  {
276
    machine with
277
      mstep = { 
278
	machine.mstep with 
279
	  step_locals = locals;
280
	  step_instrs = instrs;
281
	  step_checks = checks
282
      };
283
      mconst = mconst;
284
      minstances = minstances;
285
      mcalls = mcalls;
286
  },
287
  elim_vars
330
  let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls in
331
  ( {
332
      machine with
333
      mstep =
334
        {
335
          machine.mstep with
336
          step_locals = locals;
337
          step_instrs = instrs;
338
          step_checks = checks;
339
        };
340
      mconst;
341
      minstances;
342
      mcalls;
343
    },
344
    elim_vars )
288 345

  
289 346
let instr_of_const top_const =
290 347
  let const = const_of_top top_const in
291 348
  let loc = const.const_loc in
292 349
  let id = const.const_id in
293
  let vdecl = mkvar_decl loc (id, mktyp Location.dummy_loc Tydec_any, mkclock loc Ckdec_any, true, None, None) in
350
  let vdecl =
351
    mkvar_decl loc
352
      ( id,
353
        mktyp Location.dummy_loc Tydec_any,
354
        mkclock loc Ckdec_any,
355
        true,
356
        None,
357
        None )
358
  in
294 359
  let vdecl = { vdecl with var_type = const.const_type } in
295
  let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in
296
  mkinstr
297
    ~lustre_eq
360
  let lustre_eq =
361
    mkeq loc ([ const.const_id ], mkexpr loc (Expr_const const.const_value))
362
  in
363
  mkinstr ~lustre_eq
298 364
    (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
299 365

  
300
(* We do not perform this optimization on contract nodes since there
301
   is not explicit dependence btw variables and their use in
302
   contracts. *)
366
(* We do not perform this optimization on contract nodes since there is not
367
   explicit dependence btw variables and their use in contracts. *)
303 368
let machines_unfold consts node_schs machines =
304
  List.fold_right (fun m (machines, removed) ->
305
      let is_contract = match m.mspec.mnode_spec with
306
        | Some (Contract _) -> true
307
        | _ -> false in
308
      if is_contract then
309
        m :: machines, removed
310
      else 
311
        let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in
312
        let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in
313
        let (m, removed_m) =  machine_unfold fanin elim_consts m in
314
        (m::machines, IMap.add m.mname.node_id removed_m removed)
315
    )
316
    machines
317
    ([], IMap.empty)
369
  List.fold_right
370
    (fun m (machines, removed) ->
371
      let is_contract =
372
        match m.mspec.mnode_spec with Some (Contract _) -> true | _ -> false
373
      in
374
      if is_contract then m :: machines, removed
375
      else
376
        let fanin =
377
          (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table
378
        in
379
        let elim_consts, _ =
380
          instrs_unfold m fanin IMap.empty (List.map instr_of_const consts)
381
        in
382
        let m, removed_m = machine_unfold fanin elim_consts m in
383
        m :: machines, IMap.add m.mname.node_id removed_m removed)
384
    machines ([], IMap.empty)
318 385

  
319 386
let get_assign_lhs instr =
320 387
  match get_instr_desc instr with
321
  | MLocalAssign(v, e) -> mk_val (Var v) e.value_type
322
  | MStateAssign(v, e) -> mk_val (Var v) e.value_type
323
  | _                  -> assert false
388
  | MLocalAssign (v, e) ->
389
    mk_val (Var v) e.value_type
390
  | MStateAssign (v, e) ->
391
    mk_val (Var v) e.value_type
392
  | _ ->
393
    assert false
324 394

  
325 395
let get_assign_rhs instr =
326 396
  match get_instr_desc instr with
327
  | MLocalAssign(_, e)
328
  | MStateAssign(_, e) -> e
329
  | _                  -> assert false
397
  | MLocalAssign (_, e) | MStateAssign (_, e) ->
398
    e
399
  | _ ->
400
    assert false
330 401

  
331 402
let is_assign instr =
332 403
  match get_instr_desc instr with
333
  | MLocalAssign _
334
  | MStateAssign _ -> true
335
  | _              -> false
404
  | MLocalAssign _ | MStateAssign _ ->
405
    true
406
  | _ ->
407
    false
336 408

  
337 409
let mk_assign m v e =
338
 match v.value_desc with
339
 | Var v -> if is_memory m v then MStateAssign(v, e) else MLocalAssign(v, e)
340
 | _          -> assert false
410
  match v.value_desc with
411
  | Var v ->
412
    if is_memory m v then MStateAssign (v, e) else MLocalAssign (v, e)
413
  | _ ->
414
    assert false
341 415

  
342 416
let rec assigns_instr instr assign =
343
  match get_instr_desc instr with  
344
  | MLocalAssign (i,_)
345
  | MStateAssign (i,_) -> VSet.add i assign
346
  | MStep (ol, _, _)   -> List.fold_right VSet.add ol assign
347
  | MBranch (_,hl)     -> List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
348
  | _                  -> assign
417
  match get_instr_desc instr with
418
  | MLocalAssign (i, _) | MStateAssign (i, _) ->
419
    VSet.add i assign
420
  | MStep (ol, _, _) ->
421
    List.fold_right VSet.add ol assign
422
  | MBranch (_, hl) ->
423
    List.fold_right (fun (_, il) -> assigns_instrs il) hl assign
424
  | _ ->
425
    assign
349 426

  
350 427
and assigns_instrs instrs assign =
351 428
  List.fold_left (fun assign instr -> assigns_instr instr assign) assign instrs
352 429

  
353
(*    
354
and substitute_expr subst expr =
355
  match expr with
356
  | Var v -> (try IMap.find expr subst with Not_found -> expr)
357
  | Fun (id, vl) -> Fun (id, List.map (substitute_expr subst) vl)
358
  | Array(vl) -> Array(List.map (substitute_expr subst) vl)
359
  | Access(v1, v2) -> Access(substitute_expr subst v1, substitute_expr subst v2)
360
  | Power(v1, v2) -> Power(substitute_expr subst v1, substitute_expr subst v2)
361
  | Cst _  -> expr
362
*)
363
(** Finds a substitute for [instr] in [instrs], 
364
   i.e. another instr' with the same rhs expression.
365
   Then substitute this expression with the first assigned var
366
*)
430
(* and substitute_expr subst expr = match expr with | Var v -> (try IMap.find
431
   expr subst with Not_found -> expr) | Fun (id, vl) -> Fun (id, List.map
432
   (substitute_expr subst) vl) | Array(vl) -> Array(List.map (substitute_expr
433
   subst) vl) | Access(v1, v2) -> Access(substitute_expr subst v1,
434
   substitute_expr subst v2) | Power(v1, v2) -> Power(substitute_expr subst v1,
435
   substitute_expr subst v2) | Cst _ -> expr *)
436

  
437
(** Finds a substitute for [instr] in [instrs], i.e. another instr' with the
438
    same rhs expression. Then substitute this expression with the first assigned
439
    var *)
367 440
let subst_instr m subst instrs instr =
368 441
  (* Format.eprintf "subst instr: %a@." (pp_instr m) instr; *)
369 442
  let instr = eliminate m subst instr in
370
  let instr_v = get_assign_lhs instr in  
443
  let instr_v = get_assign_lhs instr in
371 444
  let instr_e = get_assign_rhs instr in
372 445
  try
373 446
    (* Searching for equivalent asssign *)
374
    let instr' = List.find (fun instr' -> is_assign instr' &&
375
                                            get_assign_rhs instr' = instr_e) instrs in
447
    let instr' =
448
      List.find
449
        (fun instr' -> is_assign instr' && get_assign_rhs instr' = instr_e)
450
        instrs
451
    in
376 452
    (* Registering the instr_v as instr'_v while replacing *)
377 453
    match instr_v.value_desc with
378
    | Var v ->
379
       let instr'_v = get_assign_lhs instr' in
380
         if not (is_memory m v) then
381
         (* The current instruction defines a local variables, ie not
382
            memory, we can just record the relationship and continue
383
          *)
384
         IMap.add v.var_id instr'_v subst, instrs
385
       else  (
386
         (* The current instruction defines a memory. We need to keep
387
            the definition, simplified *)
388
         (match instr'_v.value_desc with
389
          | Var v' ->
390
             if not (is_memory m v') then
391
               (* We define v' = v. Don't need to update the records. *)
392
               let instr = eliminate m subst (update_instr_desc instr (mk_assign m instr_v instr'_v)) in
393
	       subst, instr :: instrs
394
             else ( (* Last case, v', the lhs of the previous similar
395
                       definition is, itself, a memory *)
396

  
397
               (* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *)
398
               (* Filtering out the list of instructions: 
399
                  - we copy in the same order the list of instr in instrs (fold_right)
400
                  - if the current instr is this instr' then apply 
401
                    the elimination with v' -> v on instr' before recording it as an instruction.  
402
                *)
403
               let subst_v' = IMap.add v'.var_id instr_v IMap.empty in
404
	       let instrs' =
405
                 snd
406
                   (List.fold_right
407
                      (fun instr (ok, instrs) ->
408
                        (ok || instr = instr',
409
                         if ok then
410
                           instr :: instrs
411
                         else
412
                           if instr = instr' then
413
                             instrs
414
                           else
415
                             eliminate m subst_v' instr :: instrs))
416
                      instrs (false, []))
417
               in
418
	       IMap.add v'.var_id instr_v subst, instr :: instrs'
419
             )
420
          | _           -> assert false)
421
       )
422
    | _          -> assert false
423
                  
454
    | Var v -> (
455
      let instr'_v = get_assign_lhs instr' in
456
      if not (is_memory m v) then
457
        (* The current instruction defines a local variables, ie not memory, we
458
           can just record the relationship and continue *)
459
        IMap.add v.var_id instr'_v subst, instrs
460
      else
461
        (* The current instruction defines a memory. We need to keep the
462
           definition, simplified *)
463
        match instr'_v.value_desc with
464
        | Var v' ->
465
          if not (is_memory m v') then
466
            (* We define v' = v. Don't need to update the records. *)
467
            let instr =
468
              eliminate m subst
469
                (update_instr_desc instr (mk_assign m instr_v instr'_v))
470
            in
471
            subst, instr :: instrs
472
          else
473
            (* Last case, v', the lhs of the previous similar definition is,
474
               itself, a memory *)
475

  
476
            (* TODO regarder avec X. Il me semble qu'on peut faire plus simple: *)
477
            (* Filtering out the list of instructions: - we copy in the same
478
               order the list of instr in instrs (fold_right) - if the current
479
               instr is this instr' then apply the elimination with v' -> v on
480
               instr' before recording it as an instruction. *)
481
            let subst_v' = IMap.add v'.var_id instr_v IMap.empty in
482
            let instrs' =
483
              snd
484
                (List.fold_right
485
                   (fun instr (ok, instrs) ->
486
                     ( ok || instr = instr',
487
                       if ok then instr :: instrs
488
                       else if instr = instr' then instrs
489
                       else eliminate m subst_v' instr :: instrs ))
490
                   instrs (false, []))
491
            in
492
            IMap.add v'.var_id instr_v subst, instr :: instrs'
493
        | _ ->
494
          assert false)
495
    | _ ->
496
      assert false
424 497
  with Not_found ->
425 498
    (* No such equivalent expr: keeping the definition *)
426 499
    subst, instr :: instrs
427
                
500

  
501
(* - [subst] : hashtable from ident to (simple) definition it is an equivalence
502
   table - [elim] : set of eliminated variables - [instrs] : previous
503
   instructions, which [instr] is compared against - [instr] : current
504
   instruction, normalized by [subst] *)
505

  
428 506
(** Common sub-expression elimination for machine instructions *)
429
(* - [subst] : hashtable from ident to (simple) definition
430
               it is an equivalence table
431
   - [elim]   : set of eliminated variables
432
   - [instrs] : previous instructions, which [instr] is compared against
433
   - [instr] : current instruction, normalized by [subst]
434
*)
435 507
let rec instr_cse m (subst, instrs) instr =
436 508
  match get_instr_desc instr with
437 509
  (* Simple cases*)
438
  | MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
439
      -> instr_cse m (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
440
  | MLocalAssign(v, expr) when is_unfoldable_expr 2 expr
441
      -> (IMap.add v.var_id expr subst, instr :: instrs)
442
  | _ when is_assign instr
443
      -> subst_instr m subst instrs instr
444
  | _ -> (subst, instr :: instrs)
445

  
446
(** Apply common sub-expression elimination to a sequence of instrs
447
*)
510
  | MStep ([ v ], id, vl)
511
    when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
512
    ->
513
    instr_cse m (subst, instrs)
514
      (update_instr_desc instr
515
         (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
516
  | MLocalAssign (v, expr) when is_unfoldable_expr 2 expr ->
517
    IMap.add v.var_id expr subst, instr :: instrs
518
  | _ when is_assign instr ->
519
    subst_instr m subst instrs instr
520
  | _ ->
521
    subst, instr :: instrs
522

  
523
(** Apply common sub-expression elimination to a sequence of instrs *)
448 524
let instrs_cse m subst instrs =
449
  let subst, rev_instrs = 
450
    List.fold_left (instr_cse m) (subst, []) instrs
451
  in subst, List.rev rev_instrs
525
  let subst, rev_instrs = List.fold_left (instr_cse m) (subst, []) instrs in
526
  subst, List.rev rev_instrs
452 527

  
453
(** Apply common sub-expression elimination to a machine
454
    - iterate through step instructions and remove simple local assigns
455
*)
528
(** Apply common sub-expression elimination to a machine - iterate through step
529
    instructions and remove simple local assigns *)
456 530
let machine_cse subst machine =
457
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)
531
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@."
532
    pp_elim subst);*)
458 533
  let _, instrs = instrs_cse machine subst machine.mstep.step_instrs in
459
  let assigned = assigns_instrs instrs VSet.empty
460
  in
534
  let assigned = assigns_instrs instrs VSet.empty in
461 535
  {
462 536
    machine with
463
      mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
464
      mstep = { 
465
	machine.mstep with 
466
	  step_locals = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mstep.step_locals;
467
	  step_instrs = instrs
468
      }
537
    mmemory = List.filter (fun vdecl -> VSet.mem vdecl assigned) machine.mmemory;
538
    mstep =
539
      {
540
        machine.mstep with
541
        step_locals =
542
          List.filter
543
            (fun vdecl -> VSet.mem vdecl assigned)
544
            machine.mstep.step_locals;
545
        step_instrs = instrs;
546
      };
469 547
  }
470 548

  
471
let machines_cse machines =
472
  List.map
473
    (machine_cse IMap.empty)
474
    machines
549
let machines_cse machines = List.map (machine_cse IMap.empty) machines
475 550

  
476 551
(* variable substitution for optimizing purposes *)
477 552

  
478 553
(* checks whether an [instr] is skip and can be removed from program *)
479 554
let rec instr_is_skip instr =
480 555
  match get_instr_desc instr with
481
  | MLocalAssign (i, { value_desc = (Var v) ; _}) when i = v -> true
482
  | MStateAssign (i, { value_desc = Var v; _}) when i = v -> true
483
  | MBranch (_, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
484
  | _               -> false
485
and instrs_are_skip instrs =
486
  List.for_all instr_is_skip instrs
556
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
557
    true
558
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
559
    true
560
  | MBranch (_, hl) ->
561
    List.for_all (fun (_, il) -> instrs_are_skip il) hl
562
  | _ ->
563
    false
564

  
565
and instrs_are_skip instrs = List.for_all instr_is_skip instrs
487 566

  
488
let instr_cons instr cont =
489
 if instr_is_skip instr then cont else instr::cont
567
let instr_cons instr cont = if instr_is_skip instr then cont else instr :: cont
490 568

  
491 569
let rec instr_remove_skip instr cont =
492 570
  match get_instr_desc instr with
493
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v -> cont
494
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v -> cont
495
  | MBranch (g, hl) -> update_instr_desc instr (MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl)) :: cont
496
  | _               -> instr::cont
571
  | MLocalAssign (i, { value_desc = Var v; _ }) when i = v ->
572
    cont
573
  | MStateAssign (i, { value_desc = Var v; _ }) when i = v ->
574
    cont
575
  | MBranch (g, hl) ->
576
    update_instr_desc instr
577
      (MBranch (g, List.map (fun (h, il) -> h, instrs_remove_skip il []) hl))
578
    :: cont
579
  | _ ->
580
    instr :: cont
497 581

  
498 582
and instrs_remove_skip instrs cont =
499 583
  List.fold_right instr_remove_skip instrs cont
500 584

  
501 585
let rec value_replace_var fvar value =
502 586
  match value.value_desc with
503
  | Cst _ | ResetFlag -> value
504
  | Var v -> { value with value_desc = Var (fvar v) }
505
  | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
506
  | Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
507
  | Access (t, i) -> { value with value_desc = Access(value_replace_var fvar t, i)}
508
  | Power (v, n) -> { value with value_desc = Power(value_replace_var fvar v, n)}
587
  | Cst _ | ResetFlag ->
588
    value
589
  | Var v ->
590
    { value with value_desc = Var (fvar v) }
591
  | Fun (id, args) ->
592
    { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
593
  | Array vl ->
594
    { value with value_desc = Array (List.map (value_replace_var fvar) vl) }
595
  | Access (t, i) ->
596
    { value with value_desc = Access (value_replace_var fvar t, i) }
597
  | Power (v, n) ->
598
    { value with value_desc = Power (value_replace_var fvar v, n) }
509 599

  
510 600
let rec instr_replace_var fvar instr cont =
511 601
  match get_instr_desc instr with
512
  | MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
513
  | MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
602
  | MLocalAssign (i, v) ->
603
    instr_cons
604
      (update_instr_desc instr
605
         (MLocalAssign (fvar i, value_replace_var fvar v)))
606
      cont
607
  | MStateAssign (i, v) ->
608
    instr_cons
609
      (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v)))
610
      cont
514 611
  | MSetReset _
515 612
  | MNoReset _
516 613
  | MClearReset
517 614
  | MResetAssign _
518 615
  | MSpec _
519
  | MComment _          -> instr_cons instr cont
520
  | MStep (il, i, vl)   -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont
521
  | 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
616
  | MComment _ ->
617
    instr_cons instr cont
618
  | MStep (il, i, vl) ->
619
    instr_cons
620
      (update_instr_desc instr
621
         (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)))
622
      cont
623
  | MBranch (g, hl) ->
624
    instr_cons
625
      (update_instr_desc instr
626
         (MBranch
627
            ( value_replace_var fvar g,
628
              List.map (fun (h, il) -> h, instrs_replace_var fvar il []) hl )))
629
      cont
522 630

  
523 631
and instrs_replace_var fvar instrs cont =
524 632
  List.fold_right (instr_replace_var fvar) instrs cont
525 633

  
526 634
let step_replace_var fvar step =
527
  (* Some outputs may have been replaced by locals.
528
     We then need to rename those outputs
529
     without changing their clocks, etc *)
635
  (* Some outputs may have been replaced by locals. We then need to rename those
636
     outputs without changing their clocks, etc *)
530 637
  let outputs' =
531
    List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs in
532
  let locals'  =
533
    List.fold_left (fun res l ->
534
      let l' = fvar l in
535
      if List.exists (fun o -> o.var_id = l'.var_id) outputs'
536
      then res
537
      else Utils.add_cons l' res)
538
      [] step.step_locals in
539
  { step with
540
    step_checks = List.map (fun (l, v) -> (l, value_replace_var fvar v)) step.step_checks;
638
    List.map (fun o -> { o with var_id = (fvar o).var_id }) step.step_outputs
639
  in
640
  let locals' =
641
    List.fold_left
642
      (fun res l ->
643
        let l' = fvar l in
644
        if List.exists (fun o -> o.var_id = l'.var_id) outputs' then res
645
        else Utils.add_cons l' res)
646
      [] step.step_locals
647
  in
648
  {
649
    step with
650
    step_checks =
651
      List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks;
541 652
    step_outputs = outputs';
542 653
    step_locals = locals';
543 654
    step_instrs = instrs_replace_var fvar step.step_instrs [];
544
}
655
  }
545 656

  
546 657
let machine_replace_variables fvar m =
547
  { m with
548
    mstep = step_replace_var fvar m.mstep
549
  }
658
  { m with mstep = step_replace_var fvar m.mstep }
550 659

  
551 660
let machine_reuse_variables m reuse =
552
  let fvar v =
553
    try
554
      Hashtbl.find reuse v.var_id
555
    with Not_found -> v in
661
  let fvar v = try Hashtbl.find reuse v.var_id with Not_found -> v in
556 662
  machine_replace_variables fvar m
557 663

  
558 664
let machines_reuse_variables prog reuse_tables =
559
  List.map 
560
    (fun m -> 
561
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables)
562
    ) prog
665
  List.map
666
    (fun m ->
667
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables))
668
    prog
563 669

  
564 670
let rec instr_assign res instr =
565 671
  match get_instr_desc instr with
566
  | MLocalAssign (i, _) -> Disjunction.CISet.add i res
567
  | MStateAssign (i, _) -> Disjunction.CISet.add i res
568
  | MBranch (_, hl)     -> List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
569
  | MStep (il, _, _)    -> List.fold_right Disjunction.CISet.add il res
570
  | _                   -> res
571

  
572
and instrs_assign res instrs =
573
  List.fold_left instr_assign res instrs
672
  | MLocalAssign (i, _) ->
673
    Disjunction.CISet.add i res
674
  | MStateAssign (i, _) ->
675
    Disjunction.CISet.add i res
676
  | MBranch (_, hl) ->
677
    List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
678
  | MStep (il, _, _) ->
679
    List.fold_right Disjunction.CISet.add il res
680
  | _ ->
681
    res
682

  
683
and instrs_assign res instrs = List.fold_left instr_assign res instrs
574 684

  
575 685
let rec instr_constant_assign var instr =
576 686
  match get_instr_desc instr with
577 687
  | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
578
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var
579
  | MBranch (_, hl)                     -> List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
580
  | _                                   -> false
688
  | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) ->
689
    i = var
690
  | MBranch (_, hl) ->
691
    List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
692
  | _ ->
693
    false
581 694

  
582 695
and instrs_constant_assign var instrs =
583
  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
696
  List.fold_left
697
    (fun res i ->
698
      if Disjunction.CISet.mem var (instr_assign Disjunction.CISet.empty i) then
699
        instr_constant_assign var i
700
      else res)
701
    false instrs
584 702

  
585 703
let rec instr_reduce branches instr1 cont =
586 704
  match get_instr_desc instr1 with
587
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
588
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
589
  | MBranch (g, hl)                     -> (update_instr_desc instr1 (MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl))) :: cont
590
  | _                                   -> instr1 :: cont
705
  | MLocalAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
706
    instr1 :: (List.assoc c branches @ cont)
707
  | MStateAssign (_, { value_desc = Cst (Const_tag c); _ }) ->
708
    instr1 :: (List.assoc c branches @ cont)
709
  | MBranch (g, hl) ->
710
    update_instr_desc instr1
711
      (MBranch (g, List.map (fun (h, b) -> h, instrs_reduce branches b []) hl))
712
    :: cont
713
  | _ ->
714
    instr1 :: cont
591 715

  
592 716
and instrs_reduce branches instrs cont =
593
 match instrs with
594
 | []        -> cont
595
 | [i]       -> instr_reduce branches i cont
596
 | i1::i2::q -> i1 :: instrs_reduce branches (i2::q) cont
717
  match instrs with
718
  | [] ->
719
    cont
720
  | [ i ] ->
721
    instr_reduce branches i cont
722
  | i1 :: i2 :: q ->
723
    i1 :: instrs_reduce branches (i2 :: q) cont
597 724

  
598 725
let rec instrs_fusion instrs =
599 726
  match instrs, List.map get_instr_desc instrs with
600
  | [], []
601
  | [_], [_]                                                               ->
727
  | [], [] | [ _ ], [ _ ] ->
602 728
    instrs
603
  | i1::_::q, _::(MBranch ({ value_desc = Var v; _}, hl))::_ when instr_constant_assign v i1 ->
604
    instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)
605
  | i1::i2::q, _                                                         ->
606
    i1 :: instrs_fusion (i2::q)
607
  | _ -> assert false (* Other cases should not happen since both lists are of same size *)
608
     
609
let step_fusion step =
610
  { step with
611
    step_instrs = instrs_fusion step.step_instrs;
612
  }
729
  | i1 :: _ :: q, _ :: MBranch ({ value_desc = Var v; _ }, hl) :: _
730
    when instr_constant_assign v i1 ->
731
    instr_reduce
732
      (List.map (fun (h, b) -> h, instrs_fusion b) hl)
733
      i1 (instrs_fusion q)
734
  | i1 :: i2 :: q, _ ->
735
    i1 :: instrs_fusion (i2 :: q)
736
  | _ ->
737
    assert false
738
(* Other cases should not happen since both lists are of same size *)
613 739

  
614
let machine_fusion m =
615
  { m with
616
    mstep = step_fusion m.mstep
617
  }
740
let step_fusion step =
741
  { step with step_instrs = instrs_fusion step.step_instrs }
618 742

  
619
let machines_fusion prog =
620
  List.map machine_fusion prog
743
let machine_fusion m = { m with mstep = step_fusion m.mstep }
621 744

  
745
let machines_fusion prog = List.map machine_fusion prog
622 746

  
623 747
(* Additional function to modify the prog according to removed variables map *)
624 748

  
625 749
let elim_prog_variables prog removed_table =
626
  List.map (fun t -> match t.top_decl_desc with
627
      | Node nd ->
628
        begin match IMap.find_opt nd.node_id removed_table with
629
          | Some nd_elim_map ->
630
            (* Iterating through the elim map to compute
631
               - the list of variables to remove
632
               - the associated list of lustre definitions x = expr to
633
                 be used when removing these variables *)
634
            let vars_to_replace, defs = (* Recovering vid from node locals *)
635
              IMap.fold (fun v (_,eq) (accu_locals, accu_defs) ->
636
                  let locals =
637
                    try
638
                      List.find (fun v' -> v'.var_id = v) nd.node_locals
639
                      :: accu_locals
640
                    with Not_found -> accu_locals (* Variable v shall
641
                                                     be a global
642
                                                     constant, we do no
643
                                                     need to eliminate
644
                                                     it from the locals
645
                                                  *)
646
                  in
647
                  (* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc = e.expr_loc } in *)
648
                  let defs = eq::accu_defs in
649
                  locals, defs
650
                ) nd_elim_map ([], [])
651
            in
652

  
653
            let node_locals, node_stmts =
654
              List.fold_right (fun stmt (locals, res_stmts) ->
655
                  match stmt with
656
                  | Aut _ -> assert false (* should be processed by now *)
657
                  | Eq eq ->
658
                    begin match eq.eq_lhs with
659
                      | [] -> assert false (* shall not happen *)
660
                      | _::_::_ ->
661
                        (* When more than one lhs we just keep the
662
                           equation and do not delete it *)
663
                        let eq_rhs' = substitute_expr vars_to_replace defs eq.eq_rhs in
664
                        locals, (Eq { eq with eq_rhs = eq_rhs' })::res_stmts
665
                      | [lhs] ->
666
                        if List.exists (fun v -> v.var_id = lhs) vars_to_replace then
667
                          (* We remove the def *)
668
                          List.filter (fun v -> v.var_id <> lhs) locals,
669
                          res_stmts
670
                        else (* We keep it but modify any use of an eliminatend var *)
671
                          let eq_rhs' = substitute_expr vars_to_replace defs eq.eq_rhs in
672
                          locals,
673
                          (Eq { eq with eq_rhs = eq_rhs' })::res_stmts
674
                    end
675
                ) nd.node_stmts (nd.node_locals, [])
676
            in
677
            let nd' = { nd with node_locals; node_stmts } in
678
            { t with top_decl_desc = Node nd' }
679
          | None -> t
680
        end
681
      | _ -> t
682
  ) prog
750
  List.map
751
    (fun t ->
752
      match t.top_decl_desc with
753
      | Node nd -> (
754
        match IMap.find_opt nd.node_id removed_table with
755
        | Some nd_elim_map ->
756
          (* Iterating through the elim map to compute - the list of variables
757
             to remove - the associated list of lustre definitions x = expr to
758
             be used when removing these variables *)
759
          let vars_to_replace, defs =
760
            (* Recovering vid from node locals *)
761
            IMap.fold
762
              (fun v (_, eq) (accu_locals, accu_defs) ->
763
                let locals =
764
                  try
765
                    List.find (fun v' -> v'.var_id = v) nd.node_locals
766
                    :: accu_locals
767
                  with Not_found -> accu_locals
768
                  (* Variable v shall be a global constant, we do no need to
769
                     eliminate it from the locals *)
770
                in
771
                (* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc =
772
                   e.expr_loc } in *)
773
                let defs = eq :: accu_defs in
774
                locals, defs)
775
              nd_elim_map ([], [])
776
          in
777

  
778
          let node_locals, node_stmts =
779
            List.fold_right
780
              (fun stmt (locals, res_stmts) ->
781
                match stmt with
782
                | Aut _ ->
783
                  assert false (* should be processed by now *)
784
                | Eq eq -> (
785
                  match eq.eq_lhs with
786
                  | [] ->
787
                    assert false (* shall not happen *)
788
                  | _ :: _ :: _ ->
789
                    (* When more than one lhs we just keep the equation and do
790
                       not delete it *)
791
                    let eq_rhs' =
792
                      substitute_expr vars_to_replace defs eq.eq_rhs
793
                    in
794
                    locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts
795
                  | [ lhs ] ->
796
                    if List.exists (fun v -> v.var_id = lhs) vars_to_replace
797
                    then
798
                      (* We remove the def *)
799
                      List.filter (fun v -> v.var_id <> lhs) locals, res_stmts
800
                    else
801
                      (* We keep it but modify any use of an eliminatend var *)
802
                      let eq_rhs' =
803
                        substitute_expr vars_to_replace defs eq.eq_rhs
804
                      in
805
                      locals, Eq { eq with eq_rhs = eq_rhs' } :: res_stmts))
806
              nd.node_stmts (nd.node_locals, [])
807
          in
808
          let nd' = { nd with node_locals; node_stmts } in
809
          { t with top_decl_desc = Node nd' }
810
        | None ->
811
          t)
812
      | _ ->
813
        t)
814
    prog
683 815

  
684 816
(*** Main function ***)
685 817

  
686
(* 
687
This functions produces an optimzed prog * machines
688
It 
689
1- eliminates common sub-expressions (TODO how is this different from normalization?)
690
2- inline constants and eliminate duplicated variables 
691
3- try to reuse variables whenever possible
818
(* This functions produces an optimzed prog * machines It 1- eliminates common
819
   sub-expressions (TODO how is this different from normalization?) 2- inline
820
   constants and eliminate duplicated variables 3- try to reuse variables
821
   whenever possible
692 822

  
693
When item (2) identified eliminated variables, the initial prog is modified, its normalized recomputed, as well as its scheduling, before regenerating the machines.
823
   When item (2) identified eliminated variables, the initial prog is modified,
824
   its normalized recomputed, as well as its scheduling, before regenerating the
825
   machines.
694 826

  
695
The function returns both the (possibly updated) prog as well as the machines 
696

  
697

  
698
*)
827
   The function returns both the (possibly updated) prog as well as the machines *)
699 828
let optimize params prog node_schs machine_code =
700 829
  let machine_code =
701
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then begin
702
      Log.report ~level:1
703
        (fun fmt -> Format.fprintf fmt "@ @[<v 2>.. machines optimization: sub-expression elimination@ ");
830
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then (
831
      Log.report ~level:1 (fun fmt ->
832
          Format.fprintf fmt
833
            "@ @[<v 2>.. machines optimization: sub-expression elimination@ ");
704 834
      let machine_code = machines_cse machine_code in
705
      Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 2>.. generated machines (sub-expr elim):@ %a@]@ "
706
                              pp_machines machine_code);
835
      Log.report ~level:3 (fun fmt ->
836
          Format.fprintf fmt
837
            "@[<v 2>.. generated machines (sub-expr elim):@ %a@]@ " pp_machines
838
            machine_code);
707 839
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
708
      machine_code
709
    end else
710
      machine_code
840
      machine_code)
841
    else machine_code
711 842
  in
712 843
  (* Optimize machine code *)
713
  let prog, machine_code, removed_table = 
714
    if !Options.optimization >= 2
715
    && !Options.output <> "emf" (*&& !Options.output <> "horn"*)
716
    then begin
717
      Log.report ~level:1
718
        (fun fmt ->
719
           Format.fprintf fmt
720
             "@ @[<v 2>.. machines optimization: const. inlining (partial eval. with const)@ ");
844
  let prog, machine_code, removed_table =
845
    if
846
      !Options.optimization >= 2 && !Options.output <> "emf"
847
      (*&& !Options.output <> "horn"*)
848
    then (
849
      Log.report ~level:1 (fun fmt ->
850
          Format.fprintf fmt
851
            "@ @[<v 2>.. machines optimization: const. inlining (partial eval. \
852
             with const)@ ");
721 853
      let machine_code, removed_table =
722
        machines_unfold (Corelang.get_consts prog) node_schs machine_code in
723
      Log.report ~level:3
724
        (fun fmt ->
725
           Format.fprintf fmt "@ Eliminated flows: %a@ "
726
             (pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m))) removed_table);
727
      Log.report ~level:3
728
        (fun fmt ->
729
           Format.fprintf fmt
730
             "@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "
731
             pp_machines machine_code);
732
      (* If variables were eliminated, relaunch the
733
         normalization/machine generation *)
854
        machines_unfold (Corelang.get_consts prog) node_schs machine_code
855
      in
856
      Log.report ~level:3 (fun fmt ->
857
          Format.fprintf fmt "@ Eliminated flows: %a@ "
858
            (pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m)))
859
            removed_table);
860
      Log.report ~level:3 (fun fmt ->
861
          Format.fprintf fmt
862
            "@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "
863
            pp_machines machine_code);
864
      (* If variables were eliminated, relaunch the normalization/machine
865
         generation *)
734 866
      let prog, machine_code, removed_table =
735 867
        if IMap.is_empty removed_table then
736 868
          (* stopping here, no need to reupdate the prog *)
737 869
          prog, machine_code, removed_table
738
        else (
870
        else
739 871
          let prog = elim_prog_variables prog removed_table in
740 872
          (* Mini stage1 *)
741 873
          let prog = Normalization.normalize_prog params prog in
742 874
          let prog = SortProg.sort_nodes_locals prog in
743
          (* Mini stage2: note that we do not protect against
744
             alg. loop since this should have been handled before *)
875
          (* Mini stage2: note that we do not protect against alg. loop since
876
             this should have been handled before *)
745 877
          let prog, node_schs = Scheduling.schedule_prog prog in
746 878
          let machine_code = Machine_code.translate_prog prog node_schs in
747 879
          (* Mini stage2 machine optimiation *)
748 880
          let machine_code, removed_table =
749
            machines_unfold (Corelang.get_consts prog) node_schs machine_code in
881
            machines_unfold (Corelang.get_consts prog) node_schs machine_code
882
          in
750 883
          prog, machine_code, removed_table
751
        )
752
        in
753
        Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
754
        prog, machine_code, removed_table
755

  
756
    end else
757
      prog, machine_code, IMap.empty
758
  in  
884
      in
885
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]");
886
      prog, machine_code, removed_table)
887
    else prog, machine_code, IMap.empty
888
  in
759 889
  (* Optimize machine code *)
760 890
  let machine_code =
761
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then
762
      begin
763
        Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
764
        let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
765
        let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
766
        machines_fusion (machines_reuse_variables machine_code reuse_tables)
767
      end
768
    else
769
      machine_code
891
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then (
892
      Log.report ~level:1 (fun fmt ->
893
          Format.fprintf fmt
894
            ".. machines optimization: minimize stack usage by reusing \
895
             variables@,");
896
      let node_schs =
897
        Scheduling.remove_prog_inlined_locals removed_table node_schs
898
      in
899
      let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
900
      machines_fusion (machines_reuse_variables machine_code reuse_tables))
901
    else machine_code
770 902
  in
771 903

  
772

  
773 904
  prog, machine_code
774 905

  
775
          
776
                 (* Local Variables: *)
777
                 (* compile-command:"make -C .." *)
778
                 (* End: *)
906
(* Local Variables: *)
907
(* compile-command:"make -C .." *)
908
(* End: *)

Also available in: Unified diff