Revision 7ee5f69e
Added by LĂ©lio Brun 9 months ago
src/optimize_machine.ml  

20  20  
21  21  
22  22 
let pp_elim m fmt elim = 
23 
begin 

24 
Format.fprintf fmt "@[{ /* elim table: */@ "; 

25 
IMap.iter (fun v expr > Format.fprintf fmt "%s > %a@ " v (pp_val m) expr) elim; 

26 
Format.fprintf fmt "}@ @]"; 

27 
end 

23 
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 "@]@ }@]" *) 

28  27  
29  28 
let rec eliminate m elim instr = 
30  29 
let e_expr = eliminate_expr m elim in 
...  ...  
246  245 

247  246 
*) 
248  247 
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)); 

248 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "machine_unfold %s %a@ " 

249 
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 
...  ...  
291  291 
contracts. *) 
292  292 
let machines_unfold consts node_schs machines = 
293  293 
List.fold_right (fun m (machines, removed) > 
294 
let is_contract = match m.mspec with Some (Contract _) > true  _ > false in 

294 
let is_contract = match m.mspec.mnode_spec with 

295 
 Some (Contract _) > true 

296 
 _ > false in 

295  297 
if is_contract then 
296 
m::machines, removed


298 
m :: machines, removed


297  299 
else 
298  300 
let fanin = (IMap.find m.mname.node_id node_schs).Scheduling_type.fanin_table in 
299  301 
let elim_consts, _ = instrs_unfold m fanin IMap.empty (List.map instr_of_const consts) in 
...  ...  
688  690 
*) 
689  691 
let optimize params prog node_schs machine_code = 
690  692 
let machine_code = 
691 
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then 

692 
begin


693 
Log.report ~level:1


694 
(fun fmt > Format.fprintf fmt ".. machines optimization: subexpression elimination@,");


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);


697 
machine_code


698 
end


699 
else 

693 
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then begin


694 
Log.report ~level:1


695 
(fun fmt > Format.fprintf fmt "@ @[<v 2>.. machines optimization: subexpression elimination@ ");


696 
let machine_code = machines_cse machine_code in


697 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "@[<v 2>.. generated machines (subexpr elim):@ %a@]@ "


698 
pp_machines machine_code);


699 
Log.report ~level:1 (fun fmt > Format.fprintf fmt "@]");


700 
machine_code


701 
end else


700  702 
machine_code 
701  703 
in 
702  704 
(* Optimize machine code *) 
703  705 
let prog, machine_code, removed_table = 
704  706 
if !Options.optimization >= 2 
705 
&& !Options.output <> "emf" (*&& !Options.output <> "horn"*)


706 
then 

707 
begin


708 
Log.report ~level:1


709 
(fun fmt >


710 
Format.fprintf fmt


711 
".. machines optimization: const. inlining (partial eval. with const)@,");


712 
let machine_code, removed_table =


713 
machines_unfold (Corelang.get_consts prog) node_schs machine_code in


714 
Log.report ~level:3


715 
(fun fmt >


716 
Format.fprintf fmt "\t@[Eliminated flows: @[%a@]@]@ "


717 
(pp_imap (fun fmt m > pp_elim empty_machine fmt (IMap.map fst m))) removed_table);


718 
Log.report ~level:3


719 
(fun fmt >


720 
Format.fprintf fmt


721 
".. generated machines (const inlining):@ %a@ "


722 
pp_machines machine_code);


723 
(* If variables were eliminated, relaunch the


724 
normalization/machine generation *)


707 
&& !Options.output <> "emf" (*&& !Options.output <> "horn"*) 

708 
then begin


709 
Log.report ~level:1


710 
(fun fmt >


711 
Format.fprintf fmt


712 
"@ @[<v 2>.. machines optimization: const. inlining (partial eval. with const)@ ");


713 
let machine_code, removed_table =


714 
machines_unfold (Corelang.get_consts prog) node_schs machine_code in


715 
Log.report ~level:3


716 
(fun fmt >


717 
Format.fprintf fmt "@ Eliminated flows: %a@ "


718 
(pp_imap (fun fmt m > pp_elim empty_machine fmt (IMap.map fst m))) removed_table);


719 
Log.report ~level:3


720 
(fun fmt >


721 
Format.fprintf fmt


722 
"@ @[<v 2>.. generated machines (const inlining):@ %a@]@ "


723 
pp_machines machine_code);


724 
(* If variables were eliminated, relaunch the


725 
normalization/machine generation *)


726 
let prog, machine_code, removed_table =


725  727 
if IMap.is_empty removed_table then 
726 
(* stopping here, no need to reupdate the prog *)


728 
(* stopping here, no need to reupdate the prog *)


727  729 
prog, machine_code, removed_table 
728  730 
else ( 
729  731 
let prog = elim_prog_variables prog removed_table in 
...  ...  
734  736 
alg. loop since this should have been handled before *) 
735  737 
let prog, node_schs = Scheduling.schedule_prog prog in 
736  738 
let machine_code = Machine_code.translate_prog prog node_schs in 
737 
(* Mini stage2 machine optimiation *)


739 
(* Mini stage2 machine optimiation *)


738  740 
let machine_code, removed_table = 
739  741 
machines_unfold (Corelang.get_consts prog) node_schs machine_code in 
740 
prog, machine_code, removed_table


742 
prog, machine_code, removed_table


741  743 
) 
744 
in 

745 
Log.report ~level:1 (fun fmt > Format.fprintf fmt "@]"); 

746 
prog, machine_code, removed_table 

742  747  
743 
end 

744 
else 

748 
end else 

745  749 
prog, machine_code, IMap.empty 
746  750 
in 
747  751 
(* Optimize machine code *) 
748  752 
let machine_code = 
749  753 
if !Options.optimization >= 3 && not (Backends.is_functional ()) then 
750  754 
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


754 
machines_fusion (machines_reuse_variables machine_code reuse_tables)


755 
Log.report ~level:1 (fun fmt > Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");


756 
let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in


757 
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in


758 
machines_fusion (machines_reuse_variables machine_code reuse_tables)


755  759 
end 
756  760 
else 
757  761 
machine_code 
758  762 
in 
759 


763  
760  764  
761  765 
prog, List.rev machine_code 
762 


766  
763  767 

764  768 
(* Local Variables: *) 
765  769 
(* compilecommand:"make C .." *) 
Also available in: Unified diff
corrections on loggers + spec in AST