Revision 13507742
Added by Pierre-Loïc Garoche about 6 years ago
src/optimize_machine.ml | ||
---|---|---|
567 | 567 |
let machines_fusion prog = |
568 | 568 |
List.map machine_fusion prog |
569 | 569 |
|
570 |
|
|
571 |
(*** Main function ***) |
|
572 |
|
|
573 |
let optimize prog node_schs machine_code = |
|
574 |
let machine_code = |
|
575 |
if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then |
|
576 |
begin |
|
577 |
Log.report ~level:1 |
|
578 |
(fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,"); |
|
579 |
let machine_code = machines_cse machine_code in |
|
580 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code); |
|
581 |
machine_code |
|
582 |
end |
|
583 |
else |
|
584 |
machine_code |
|
585 |
in |
|
586 |
(* Optimize machine code *) |
|
587 |
let machine_code, removed_table = |
|
588 |
if !Options.optimization >= 2 && !Options.output <> "emf" (*&& !Options.output <> "horn"*) then |
|
589 |
begin |
|
590 |
Log.report ~level:1 (fun fmt -> Format.fprintf fmt |
|
591 |
".. machines optimization: const. inlining (partial eval. with const)@,"); |
|
592 |
let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in |
|
593 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ " |
|
594 |
(pp_imap pp_elim) removed_table); |
|
595 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code); |
|
596 |
machine_code, removed_table |
|
597 |
end |
|
598 |
else |
|
599 |
machine_code, IMap.empty |
|
600 |
in |
|
601 |
(* Optimize machine code *) |
|
602 |
let machine_code = |
|
603 |
if !Options.optimization >= 3 && not (Backends.is_functional ()) then |
|
604 |
begin |
|
605 |
Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,"); |
|
606 |
let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in |
|
607 |
let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in |
|
608 |
machines_fusion (machines_reuse_variables machine_code reuse_tables) |
|
609 |
end |
|
610 |
else |
|
611 |
machine_code |
|
612 |
in |
|
613 |
|
|
614 |
(* Salsa optimize machine code *) |
|
615 |
(* |
|
616 |
let machine_code = |
|
617 |
if !Options.salsa_enabled then |
|
618 |
begin |
|
619 |
check_main (); |
|
620 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,"); |
|
621 |
(* Selecting float constants for Salsa *) |
|
622 |
let constEnv = List.fold_left ( |
|
623 |
fun accu c_topdecl -> |
|
624 |
match c_topdecl.top_decl_desc with |
|
625 |
| Const c when Types.is_real_type c.const_type -> |
|
626 |
(c.const_id, c.const_value) :: accu |
|
627 |
| _ -> accu |
|
628 |
) [] (Corelang.get_consts prog) |
|
629 |
in |
|
630 |
List.map |
|
631 |
(Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) |
|
632 |
machine_code |
|
633 |
end |
|
634 |
else |
|
635 |
machine_code |
|
636 |
in |
|
637 |
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ " |
|
638 |
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
|
639 |
machine_code); |
|
640 |
*) |
|
641 |
|
|
642 |
|
|
643 |
machine_code |
|
644 |
|
|
645 |
|
|
570 | 646 |
(* Local Variables: *) |
571 | 647 |
(* compile-command:"make -C .." *) |
572 | 648 |
(* End: *) |
Also available in: Unified diff
Refactored some code: optimization of machine