Revision 9c4cc944
Added by Corentin Lauverjat over 1 year ago
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: subexpression elimination@,"); 
695  695 
let machine_code = machines_cse machine_code in 
696 
Log.report ~level:3 (fun fmt > Format.fprintf fmt ".. generated machines (subexpr elim):@ %a@ "pp_machines machine_code); 

696 
Lustrec.Log.report ~level:3 (fun fmt > Format.fprintf fmt ".. generated machines (subexpr 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
Transition to dune build system
Improvement of opam integration
Dockerfile based on Alpine
Dockerfile based on Ubuntu
Update the README.md