(*
The Compcert verified compiler

Compiler.vexpand -> Compiler.v

Expand the list of RTL compiler passes into Compiler.v

David Monniaux, CNRS, VERIMAG
 *)

type is_partial = TOTAL | PARTIAL;;
type print_result = Noprint | Print of string;;
type when_triggered = Always | Option of string;;
type needs_require = Require | NoRequire;;

let rtl_tunneling = PARTIAL, Always, Require, (Some "RTL Branch Tunneling"), "RTLTunneling"

(* FIXME - The gestion of NoRequire is a bit ugly right now. *)
let rtl_passes =
[|
TOTAL, (Option "optim_tailcalls"), Require, (Some "Tail calls"), "Tailcall";
PARTIAL, Always, Require, (Some "Inlining"), "Inlining";
TOTAL, (Option "profile_arcs"), Require, (Some "Profiling insertion"), "Profiling";
TOTAL, (Option "branch_probabilities"), Require, (Some "Profiling use"), "ProfilingExploit";
TOTAL, (Option "optim_move_loop_invariants"), Require, (Some "Inserting initial nop"), "FirstNop";
TOTAL, Always, Require, (Some "Renumbering"), "Renumber";
PARTIAL, (Option "optim_CSE"), Require, (Some "CSE"), "CSE";
PARTIAL, Always, NoRequire, (Some "Static Prediction + inverting conditions"), "Staticpredict";
PARTIAL, Always, NoRequire, (Some "Unrolling one iteration out of innermost loops"), "Unrollsingle";
TOTAL, Always, NoRequire, (Some "Renumbering pre tail duplication"), "Renumber";
PARTIAL, Always, NoRequire, (Some "Performing tail duplication"), "Tailduplicate";
TOTAL, Always, NoRequire, (Some "Renumbering pre unrolling"), "Renumber";
PARTIAL, Always, NoRequire, (Some "Unrolling the body of innermost loops"), "Unrollbody";
TOTAL, Always, NoRequire, (Some "Renumbering pre constprop"), "Renumber";
TOTAL, (Option "optim_constprop"), Require, (Some "Constant propagation"), "Constprop";
TOTAL, Always, NoRequire, (Some "Renumbering pre CSE"), "Renumber";
PARTIAL, (Option "optim_CSE"), Require, (Some "CSE"), "CSE";
TOTAL, (Option "optim_CSE2"), Require, (Some "CSE2"), "CSE2";
PARTIAL, (Option "optim_CSE3"), Require, (Some "CSE3"), "CSE3";
TOTAL, (Option "optim_CSE3"), Require, (Some "Kill useless moves after CSE3"), "KillUselessMoves";
TOTAL, (Option "optim_forward_moves"), Require, (Some "Forwarding moves"), "ForwardMoves";
PARTIAL, (Option "optim_redundancy"), Require, (Some "Redundancy elimination"), "Deadcode";
rtl_tunneling;
TOTAL, Always, Require, (Some "Renumbering pre rotate"), "Renumber";
PARTIAL, Always, NoRequire, (Some "Loop Rotate"), "Looprotate";
TOTAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Renumbering for LICM"), "Renumber";
PARTIAL, (Option "optim_move_loop_invariants"), Require, (Some "LICM"), "LICM";
TOTAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Renumbering for LICM"), "Renumber";
PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "CSE3 for LICM"), "CSE3";
PARTIAL, (Option "optim_move_loop_invariants"), NoRequire, (Some "Redundancy elimination for LICM"), "Deadcode";
TOTAL, (Option "all_loads_nontrap"), Require, None, "Allnontrap";
PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob";
|];;

let post_rtl_passes =
[|
  PARTIAL, Always, Require, (Some "BTL generation"), "RTLtoBTL", Noprint;
  PARTIAL, Always, Require, (Some "Prepass scheduling"), "BTL_Scheduler", Noprint;
  PARTIAL, Always, Require,  (Some "Projection to RTL"), "BTLtoRTL", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1)));
  PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1");
  PARTIAL, Always, Require, (Some "LTL Branch tunneling"), "LTLTunneling", (Print "LTL 2");
  PARTIAL, Always, Require, (Some "CFG linearization"), "Linearize", Noprint;
  TOTAL, Always, Require, (Some "Label cleanup"), "CleanupLabels", Noprint;
  PARTIAL, (Option "debug"), Require, (Some "Debugging info for local variables"), "Debugvar", Noprint;
  PARTIAL, Always, Require, (Some "Mach generation"), "Stacking", (Print "Mach")
|];;

let all_passes =
  Array.concat
    [Array.mapi
       (fun i (a,b,r,c,d) -> (a,b,r,c,d, Print (Printf.sprintf "RTL %d" (i+1))))
       rtl_passes;
     post_rtl_passes];;

let totality = function TOTAL -> "total" | PARTIAL -> "partial";;

let print_rtl_require oc =
  Array.iter (fun (partial, trigger, require, time_label, pass_name, printing) ->
      match require with Require -> 
        Printf.fprintf oc "Require %s.\n" pass_name
      | _ -> ()
    ) all_passes;;

let print_rtl_require_proof oc =
  Array.iter (fun (partial, trigger, require, time_label, pass_name, printing) ->
      match require with Require -> 
      Printf.fprintf oc "Require %sproof.\n" pass_name
      | _ -> ()
    ) all_passes;;

let print_rtl_transf oc =
  Array.iteri
    (fun i (partial, trigger, require, time_label, pass_name, printing) ->
      output_string oc (match partial with
                        | TOTAL -> "   @@ "
                        | PARTIAL -> "  @@@ ");
      (match trigger with
       | Always -> ()
       | Option s ->
          Printf.fprintf oc "%s_if Compopts.%s " (totality partial) s);
      output_char oc '(';
      (match time_label with
       | None -> ()
       | Some s ->
          Printf.fprintf oc "time \"%s\" " s);
      Printf.fprintf oc "%s.transf_program)\n" pass_name;
      (match printing with
       | Noprint -> ()
       | Print s ->
           Printf.fprintf oc "   @@ print (print_%s)\n" s)
    ) all_passes;;

let print_rtl_mkpass oc =
  Array.iter (fun (partial, trigger, require, time_label, pass_name, printing) ->
      output_string oc "  ::: mkpass (";
      (match trigger with
       | Always -> ()
       | Option s ->
          Printf.fprintf oc "match_if Compopts.%s " s);
      Printf.fprintf oc "%sproof.match_prog)\n" pass_name)
    all_passes;;

let print_if kind oc = function
  | Always -> ()
  | Option s -> Printf.fprintf oc "%s_if %s " kind s;;

let numbering_base = 7
                   
let print_rtl_proof oc =
  Array.iteri (fun i (partial, trigger, require, time_label, pass_name, printing) ->
      let j = i+numbering_base in
      match partial with
      | TOTAL ->
         Printf.fprintf oc "set (p%d := %a%s.transf_program p%d) in *.\n"
           j (print_if "total") trigger pass_name (pred j)
      | PARTIAL ->
         Printf.fprintf oc "destruct (%a%s.transf_program p%d) as [p%d|e] eqn:P%d; cbn in T; try discriminate.\n"
           (print_if "partial") trigger pass_name (pred j) j j)
    all_passes;;

let print_rtl_proof2 oc =
  Array.iteri (fun i (partial, trigger, require, time_label, pass_name, printing) ->
      let j = i+numbering_base in
      Printf.fprintf oc "  exists p%d; split. " j;
      (match trigger with
       | Always -> ()
       | Option _ ->
          (match partial with
           | TOTAL -> output_string oc "apply total_if_match. "
           | PARTIAL -> output_string oc "eapply partial_if_match; eauto. "));
      Printf.fprintf oc "apply %sproof.transf_program_match; auto.\n" pass_name)
    all_passes;;

let print_rtl_forward_simulations oc =
  Array.iter (fun (partial, trigger, require, time_label, pass_name) ->
      output_string oc "  eapply compose_forward_simulations.\n    ";
      (match trigger with
       | Always -> ()
       | Option s -> output_string oc "eapply match_if_simulation. eassumption. ");
      Printf.fprintf oc "eapply %sproof.transf_program_correct; eassumption." pass_name
    )
    rtl_passes;;

if (Array.length Sys.argv)<>3
then exit 1;;

let filename_in = Sys.argv.(1) and filename_out = Sys.argv.(2) in
    let ic = open_in filename_in and oc = open_out filename_out in
    try
      while true
      do
        match input_line ic with
        | "EXPAND_RTL_TRANSF_PROGRAM" ->
           print_rtl_transf oc
        | "EXPAND_RTL_REQUIRE" ->
           print_rtl_require oc
        | "EXPAND_RTL_REQUIRE_PROOF" ->
           print_rtl_require_proof oc
        | "EXPAND_RTL_MKPASS" ->
           print_rtl_mkpass oc
        | "EXPAND_RTL_PROOF" ->
           print_rtl_proof oc
        | "EXPAND_RTL_PROOF2" ->
           print_rtl_proof2 oc
        | "EXPAND_ASM_SEMANTICS" ->
           Printf.fprintf oc "    (Asm.semantics p%d)\n"
             ((Array.length all_passes) + 7)
        | "EXPAND_RTL_FORWARD_SIMULATIONS" ->
           print_rtl_forward_simulations oc
        | line -> (output_string oc line;
                   output_char oc '\n')
      done
    with End_of_file ->
      (close_in ic; close_out oc);;