Project

General

Profile

Revision 3769b712 src/optimize_machine.ml

View differences:

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

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

  
21 21

  
......
60 60
  | Cst _ -> expr
61 61

  
62 62
let eliminate_dim elim dim =
63
  Dimension.expr_replace_expr 
63
  Lustrec.Dimension.expr_replace_expr 
64 64
    (fun v -> try
65 65
		dimension_of_value (IMap.find v elim) 
66 66
      with Not_found -> mkdim_ident dim.dim_loc v) 
......
74 74
let unfold_expr_offset m offset expr =
75 75
  List.fold_left
76 76
    (fun res -> (function | Index i -> mk_val (Access (res, value_of_dimension m i))
77
					      (Types.array_element_type res.value_type)
77
					      (Lustrec.Types.array_element_type res.value_type)
78 78
                          | Field f -> Format.eprintf "internal error: not yet implemented !"; assert false))
79 79
    expr offset
80 80

  
......
82 82
    match offset, cst with
83 83
    | []          , _
84 84
      -> mk_val (Cst cst) typ
85
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i
86
      -> let elt_typ = Types.array_element_type typ in
87
         simplify_cst_expr m q elt_typ (List.nth cl (Dimension.size_const_dimension i))
85
    | Index i :: q, Const_array cl when Lustrec.Dimension.is_dimension_const i
86
      -> let elt_typ = Lustrec.Types.array_element_type typ in
87
         simplify_cst_expr m q elt_typ (List.nth cl (Lustrec.Dimension.size_const_dimension i))
88 88
    | Index i :: q, Const_array cl
89
      -> let elt_typ = Types.array_element_type typ in
89
      -> let elt_typ = Lustrec.Types.array_element_type typ in
90 90
         unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
91 91
    | Field f :: q, Const_struct fl
92
      -> let fld_typ = Types.struct_field_type typ f in
92
      -> let fld_typ = Lustrec.Types.struct_field_type typ f in
93 93
         simplify_cst_expr m q fld_typ (List.assoc f fl)
94
    | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false)
94
    | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Lustrec.Printers.pp_const cst; assert false)
95 95

  
96 96
let simplify_expr_offset m expr =
97 97
  let rec simplify offset expr =
98 98
    match offset, expr.value_desc with
99 99
    | Field f ::q , _                -> failwith "not yet implemented"
100
    | _           , Fun (id, vl) when Basic_library.is_value_internal_fun expr
100
    | _           , Fun (id, vl) when Lustrec.Basic_library.is_value_internal_fun expr
101 101
                                     -> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
102 102
    | _           , Fun _
103 103
    | _           , Var _            -> unfold_expr_offset m offset expr
......
105 105
    | _           , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr
106 106
    | []          , _                -> expr
107 107
    | Index _ :: q, Power (expr, _)  -> simplify q expr
108
    | Index i :: q, Array vl when Dimension.is_dimension_const i
109
                                     -> simplify q (List.nth vl (Dimension.size_const_dimension i))
108
    | Index i :: q, Array vl when Lustrec.Dimension.is_dimension_const i
109
                                     -> simplify q (List.nth vl (Lustrec.Dimension.size_const_dimension i))
110 110
    | Index i :: q, Array vl         -> unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type)
111
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
112
     with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
111
    (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Lustrec.Utils.fprintf_list ~sep:"" Lustrec.Printers.pp_offset) offset pp_val res; res)
112
     with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Lustrec.Utils.fprintf_list ~sep:"" Lustrec.Printers.pp_offset) offset; raise e*)
113 113
  in simplify [] expr
114 114

  
115 115
let rec simplify_instr_offset m instr =
......
148 148
    | _           , Const_tag _     -> true
149 149
    | Field f :: q, Const_struct fl -> unfold_const q (List.assoc f fl)
150 150
    | []          , Const_struct _  -> false
151
    | Index i :: q, Const_array cl when Dimension.is_dimension_const i
152
                                    -> unfold_const q (List.nth cl (Dimension.size_const_dimension i))
151
    | Index i :: q, Const_array cl when Lustrec.Dimension.is_dimension_const i
152
                                    -> unfold_const q (List.nth cl (Lustrec.Dimension.size_const_dimension i))
153 153
    | _           , Const_array _   -> false
154 154
    | _                             -> assert false in
155 155
  let rec unfold offset expr =
......
159 159
    | []          , Power _
160 160
    | []          , Array _                      -> false
161 161
    | Index i :: q, Power (v, _)                 -> unfold q v
162
    | Index i :: q, Array vl when Dimension.is_dimension_const i
163
                                                 -> unfold q (List.nth vl (Dimension.size_const_dimension i))
162
    | Index i :: q, Array vl when Lustrec.Dimension.is_dimension_const i
163
                                                 -> unfold q (List.nth vl (Lustrec.Dimension.size_const_dimension i))
164 164
    | _           , Array _                      -> false
165 165
    | _           , Access (v, i)                -> unfold (Index (dimension_of_value i) :: offset) v
166
    | _           , Fun (id, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
166
    | _           , Fun (id, vl) when fanin < 2 && Lustrec.Basic_library.is_value_internal_fun expr
167 167
                                                 -> List.for_all (unfold offset) vl
168 168
    | _           , Fun _                        -> false
169 169
    | _                                          -> assert false
......
176 176
  with Not_found -> false
177 177

  
178 178
let unfoldable_assign fanin v expr =
179
   (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
179
   (if !Lustrec.Options.mpfr then Mpfr.unfoldable_value expr else true)
180 180
&& basic_unfoldable_assign fanin v expr
181 181

  
182 182
let merge_elim elim1 elim2 =
......
207 207
(*  Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*)
208 208
  match get_instr_desc instr with
209 209
  (* Simple cases*)
210
  | MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
210
  | MStep([v], id, vl) when Lustrec.Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
211 211
    -> instr_unfold m fanin instrs elim (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
212 212
  | MLocalAssign(v, expr) when not (is_clock_dec_type v.var_dec_type.ty_dec_desc) && unfoldable_assign fanin v expr
213 213
    -> (* we don't eliminate clock definitions *)
214 214
     let new_eq =
215
       Corelang.mkeq
215
       Lustrec.Corelang.mkeq
216 216
         (desome instr.lustre_eq).eq_loc
217 217
         ([v.var_id], (desome instr.lustre_eq).eq_rhs)
218 218
     in
......
238 238
  let replace v =
239 239
    try
240 240
      dimension_of_value (IMap.find v elim)
241
    with Not_found -> Dimension.mkdim_ident Location.dummy_loc v
242
  in (inst, (n, List.map (Dimension.expr_replace_expr replace) args))
241
    with Not_found -> Lustrec.Dimension.mkdim_ident Lustrec.Location.dummy_loc v
242
  in (inst, (n, List.map (Lustrec.Dimension.expr_replace_expr replace) args))
243 243

  
244 244
(** Perform optimization on machine code:
245 245
    - iterate through step instructions and remove simple local assigns
246 246
    
247 247
*)
248 248
let machine_unfold fanin elim machine =
249
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "machine_unfold %s %a@." machine.mname.node_id (pp_elim machine) (IMap.map fst elim)); 
249
  Lustrec.Log.report ~level:3 (fun fmt -> Format.fprintf fmt "machine_unfold %s %a@." machine.mname.node_id (pp_elim machine) (IMap.map fst elim)); 
250 250
  let elim_consts, mconst = instrs_unfold machine fanin elim machine.mconst in
251 251
  let elim_vars, instrs = instrs_unfold machine fanin elim_consts machine.mstep.step_instrs in
252 252
  let instrs = simplify_instrs_offset machine instrs in
......
279 279
  let const = const_of_top top_const in
280 280
  let loc = const.const_loc in
281 281
  let id = const.const_id in
282
  let vdecl = mkvar_decl loc (id, mktyp Location.dummy_loc Tydec_any, mkclock loc Ckdec_any, true, None, None) in
282
  let vdecl = mkvar_decl loc (id, mktyp Lustrec.Location.dummy_loc Tydec_any, mkclock loc Ckdec_any, true, None, None) in
283 283
  let vdecl = { vdecl with var_type = const.const_type } in
284 284
  let lustre_eq = mkeq loc ([const.const_id], mkexpr loc (Expr_const const.const_value)) in
285 285
  mkinstr
......
295 295
      if is_contract then
296 296
        m::machines, removed
297 297
      else 
298
        let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in
298
        let fanin = (IMap.find m.mname.node_id node_schs).Lustrec.Scheduling_type.fanin_table in
299 299
        let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in
300 300
        let (m, removed_m) =  machine_unfold fanin elim_consts m in
301 301
        (m::machines, IMap.add m.mname.node_id removed_m removed)
......
422 422
let rec instr_cse m (subst, instrs) instr =
423 423
  match get_instr_desc instr with
424 424
  (* Simple cases*)
425
  | MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
425
  | MStep([v], id, vl) when Lustrec.Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
426 426
      -> instr_cse m (subst, instrs) (update_instr_desc instr (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type)))
427 427
  | MLocalAssign(v, expr) when is_unfoldable_expr 2 expr
428 428
      -> (IMap.add v.var_id expr subst, instr :: instrs)
......
441 441
    - iterate through step instructions and remove simple local assigns
442 442
*)
443 443
let machine_cse subst machine =
444
  (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)
444
  (*Lustrec.Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)
445 445
  let subst, instrs = instrs_cse machine subst machine.mstep.step_instrs in
446 446
  let assigned = assigns_instrs instrs VSet.empty
447 447
  in
......
518 518
      let l' = fvar l in
519 519
      if List.exists (fun o -> o.var_id = l'.var_id) outputs'
520 520
      then res
521
      else Utils.add_cons l' res)
521
      else Lustrec.Utils.add_cons l' res)
522 522
      [] step.step_locals in
523 523
  { step with
524 524
    step_checks = List.map (fun (l, v) -> (l, value_replace_var fvar v)) step.step_checks;
......
542 542
let machines_reuse_variables prog reuse_tables =
543 543
  List.map 
544 544
    (fun m -> 
545
      machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables)
545
      machine_reuse_variables m (Lustrec.Utils.IMap.find m.mname.node_id reuse_tables)
546 546
    ) prog
547 547

  
548 548
let rec instr_assign res instr =
......
688 688
*)
689 689
let optimize params prog node_schs machine_code =
690 690
  let machine_code =
691
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
691
    if !Lustrec.Options.optimization >= 4 (* && !Lustrec.Options.output <> "horn" *) then
692 692
      begin
693
	Log.report ~level:1 
693
	Lustrec.Log.report ~level:1 
694 694
	  (fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,");
695 695
	let machine_code = machines_cse machine_code in
696
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "pp_machines machine_code);
696
	Lustrec.Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "pp_machines machine_code);
697 697
	machine_code
698 698
      end
699 699
    else
......
701 701
  in
702 702
  (* Optimize machine code *)
703 703
  let prog, machine_code, removed_table = 
704
    if !Options.optimization >= 2
705
       && !Options.output <> "emf" (*&& !Options.output <> "horn"*)
704
    if !Lustrec.Options.optimization >= 2
705
       && !Lustrec.Options.output <> "emf" (*&& !Lustrec.Options.output <> "horn"*)
706 706
    then
707 707
      begin
708
	Log.report ~level:1
708
	Lustrec.Log.report ~level:1
709 709
          (fun fmt ->
710 710
            Format.fprintf fmt 
711 711
	      ".. machines optimization: const. inlining (partial eval. with const)@,");
712 712
	let machine_code, removed_table =
713
          machines_unfold (Corelang.get_consts prog) node_schs machine_code in
714
  Log.report ~level:3
713
          machines_unfold (Lustrec.Corelang.get_consts prog) node_schs machine_code in
714
  Lustrec.Log.report ~level:3
715 715
          (fun fmt ->
716 716
            Format.fprintf fmt "\t@[Eliminated flows: @[%a@]@]@ "
717 717
	      (pp_imap (fun fmt m -> pp_elim empty_machine fmt (IMap.map fst m))) removed_table); 
718
	Log.report ~level:3
718
	Lustrec.Log.report ~level:3
719 719
          (fun fmt ->
720 720
            Format.fprintf fmt
721 721
              ".. generated machines (const inlining):@ %a@ "
......
728 728
        else (
729 729
          let prog = elim_prog_variables prog removed_table in
730 730
          (* Mini stage1 *)
731
          let prog = Normalization.normalize_prog params prog in
731
          let prog = Lustrec.Normalization.normalize_prog params prog in
732 732
          let prog = SortProg.sort_nodes_locals prog in
733 733
          (* Mini stage2: note that we do not protect against
734 734
             alg. loop since this should have been handled before *)
735
          let prog, node_schs = Scheduling.schedule_prog prog in
736
          let machine_code = Machine_code.translate_prog prog node_schs in
735
          let prog, node_schs = Lustrec.Scheduling.schedule_prog prog in
736
          let machine_code = Lustrec.Machine_code.translate_prog prog node_schs in
737 737
	  (* Mini stage2 machine optimiation *)
738 738
          let machine_code, removed_table =
739
            machines_unfold (Corelang.get_consts prog) node_schs machine_code in
739
            machines_unfold (Lustrec.Corelang.get_consts prog) node_schs machine_code in
740 740
	  prog, machine_code, removed_table
741 741
        )
742 742

  
......
746 746
  in  
747 747
  (* Optimize machine code *)
748 748
  let machine_code =
749
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then
749
    if !Lustrec.Options.optimization >= 3 && not (Lustrec.Backends.is_functional ()) then
750 750
      begin
751
	Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
752
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
753
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
751
	Lustrec.Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
752
	let node_schs    = Lustrec.Scheduling.remove_prog_inlined_locals removed_table node_schs in
753
	let reuse_tables = Lustrec.Scheduling.compute_prog_reuse_table node_schs in
754 754
	machines_fusion (machines_reuse_variables machine_code reuse_tables)
755 755
      end
756 756
    else

Also available in: Unified diff