Project

General

Profile

« Previous | Next » 

Revision 7ee5f69e

Added by LĂ©lio Brun 9 months ago

corrections on loggers + spec in AST

View differences:

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: sub-expression elimination@,");
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);
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: sub-expression elimination@ ");
696
      let machine_code = machines_cse machine_code in
697
      Log.report ~level:3 (fun fmt -> Format.fprintf fmt "@[<v 2>.. generated machines (sub-expr 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
                 (* compile-command:"make -C .." *)

Also available in: Unified diff