Module CompAnnot

Require Import Compiler.
Require ProductSimulation.
Require UnLoad.
Require CSEannot.
Require Renumber2.
Import Utf8.
Import Errors.
Import Compopts.
Import ToString.
Import Coqlib.
Import Util.
Import Integers.

Definition parallel {X Y Z} (f: X -> res Y) (g: X -> res Z) (x: X) : res (Y * Z) :=
  match f x with
  | Error m => Error m
  | OK y => match g x with
            | Error m => Error m
            | OK z => OK (y, z)
            end
  end.

Notation "p |+| q" := (parallel p q) (at level 40).

Definition cminorannot_of_csyntax (unload stack: bool) (p: Csyntax.program) : res Csharpminorannot.program :=
  OK p
  @@@ time "Clight generation" SimplExpr.transl_program
   @@ print print_Clight
  @@@ time "Simplification of locals" SimplLocals.transf_program
  @@@ time "C#minor generation" Cshmgen.transl_program
   @@ (if unload then time "Unload" UnLoad.doit else id)
  @@@ time "C#minorannot generation" Cshmannotgen.transl_program
  @@@ (if stack then time "C#minorannot stack generation" Cshmstackgen.transl_program else OK)
  @@@ (λ p,
       match time "Annotation inference" (CsharpminorAnalysis.vanalysis (num_dom tt) (max_concretize tt) (trace tt) (verbose tt) (unroll tt)) p with
       | (tt, (nil, log)) =>
         time "C#minor annotation" (Annotagen.doit log) p
       | (_, (alarms, _)) => Errors.Error (Errors.msg ("Alarms:"
                           ++ new_line
                           ++ @ListToString _ (λ a, (a tt)) alarms))
       end)
.

Definition cminor_of_cminorannot no (p: Csharpminorannot.program) : res Cminor.program :=
   OK p
  @@@ time "Cminor generation" Cminorgen.transl_program
   @@ print (print_Cminor no).

Definition rtl_of_cminor (cse2: bool) (shift: Z -> Z) (p: Cminor.program) : res RTL.program :=
  let print (n: Z) := print (print_RTL (shift n)) in
   OK p
  @@@ time "Instruction selection" Selection.sel_program
  @@@ time "RTL generation" RTLgen.transl_program
   @@ print 0
   @@ total_if Compopts.optim_tailcalls (time "Tail calls" Tailcall.transf_program)
   @@ print 1
  @@@ time "Inlining" Inlining.transf_program
   @@ print 2
   @@ time "Renumbering" Renumber.transf_program
   @@ print 3
   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
   @@ print 4
   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
   @@ print 5
  @@@ partial_if Compopts.optim_CSE (time "CSE" (if cse2 then CSE2.transf_program else CSE.transf_program))
   @@ print 6
  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
   @@ print 7
  @@@ time "Unused globals" Unusedglob.transform_program
   @@ print 8.

Definition mach_of_rtl (p: RTL.program) : res Mach.program :=
   OK p
  @@@ time "Register allocation" Allocation.transf_program
   @@ print print_LTL
   @@ time "Branch tunneling" Tunneling.tunnel_program
  @@@ time "CFG linearization" Linearize.transf_program
   @@ time "Label cleanup" CleanupLabels.transf_program
  @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program)
  @@@ time "Mach generation" Stacking.transf_program
  @@ print print_Mach.

Definition asm_of_rtl (p: RTL.program) : res Asm.program :=
  mach_of_rtl p
  @@@ time "Asm generation" Asmgen.transf_program.

Definition doit (unload stack check: bool) (p: Csyntax.program)
  : res (RTL.program * RTL.program * RTL.program) :=
    cminorannot_of_csyntax unload stack p @@@ (λ cshma,
   (cminor_of_cminorannot 0 cshma @@@ rtl_of_cminor false id)
   @@@
   (
   OK
   |+|
   (λ rtla,
    let annotations := MoreRTL.collect_annot rtla in
    OK cshma
     @@@ time "C#minorannotdef generation" (Cshmdefgen.transl_program (λ n, MoreRTL.mem n annotations))
      @@@ (λ p,
          if check then
          match time "Defensive program safety validation" (CsharpminorAnalysis.vanalysis (num_dom tt) (max_concretize tt) (trace tt) (verbose tt) (unroll tt)) p with
          | (_, (nil, _)) => OK p
          | (_, (alarms, _)) =>
            Error (msg ("Alarms:"
                           ++ new_line
                           ++ @ListToString _ (λ a, (a tt)) alarms))
          end
         else OK p)
     @@@ (cminor_of_cminorannot 1)
     @@@ rtl_of_cminor true (Z.add 10)
      @@ print (print_RTL 19)
     @@@ (λ p, if RTLperm.no_fancy_builtin p then OK p else Error (msg "DEF1 program has external functions or other crazy stuff"))
   )
   |+|
   (λ rtla,
    (OK rtla
     @@@ time "RTLdefgen" RTLdefgen.transf_program
     @@@ time "Renumbering" Renumber2.transf_program
      @@ print (print_RTL 20)
    )
   )
   )).

Definition equivalence_check printer (def1 def2: RTL.program) (fuel: nat) : res unit :=
  ProductSimulation.validate _ eq_dec xO xI (@time)
                             Pos.max Pos.succ def2 def1 fuel printer.

Definition doit' (unload stack: bool) (p: Csyntax.program)
  : res (RTL.program * RTL.program * RTL.program) :=
  cminorannot_of_csyntax unload stack p @@@
                         (λ cshma,
                          (OK cshma
                              @@@ (λ p,
                                   match time "program safety validation" (CsharpminorAnalysis.vanalysis (num_dom tt) (max_concretize tt) (trace tt) (verbose tt) (unroll tt)) p with
                                   | (_, (nil, _)) => OK p
                                   | (_, (alarms, _)) =>
                                     Error (msg "program is not valid")
                                   end)
                              @@@ cminor_of_cminorannot 0 @@@ rtl_of_cminor false id)
   @@@
   (
   OK
   |+|
   (λ rtla,
    let annotations := MoreRTL.collect_annot rtla in
    OK cshma
     @@@ time "C#minorannotdef generation" (Cshmdefgen.transl_program (λ n, MoreRTL.mem n annotations))
     @@@ (λ p,
          match time "Defensive program safety validation" (CsharpminorAnalysis.vanalysis (num_dom tt) (max_concretize tt) (trace tt) (verbose tt) (unroll tt)) p with
          | (_, (nil, _)) => OK p
          | (_, (alarms, _)) =>
            Error (msg "Defensive program is not valid")
          end)
     @@@ (cminor_of_cminorannot 1)
     @@@ rtl_of_cminor true (Z.add 10)
      @@ print (print_RTL 19)
     @@@ (λ p, if RTLperm.no_fancy_builtin p then OK p else Error (msg "DEF1 program has external functions or other crazy stuff"))
   )
   |+|
   (λ rtla,
    (OK rtla
     @@@ time "RTLdefgen" RTLdefgen.transf_program
     @@@ time "Renumbering" Renumber2.transf_program
      @@ print (print_RTL 20)
    )
   )
   )).

Definition cse_bench (unload stack: bool) (p: Csyntax.program) : res (RTL.program * RTL.program) :=
  let print (n: Z) := print (print_RTL n) in
  cminorannot_of_csyntax unload stack p @@@
  cminor_of_cminorannot 0
  @@@ time "Instruction selection" Selection.sel_program
  @@@ time "RTL generation" RTLgen.transl_program
   @@ print 0
   @@ total_if Compopts.optim_tailcalls (time "Tail calls" Tailcall.transf_program)
   @@ print 1
  @@@ time "Inlining" Inlining.transf_program
   @@ print 2
   @@ time "Renumbering" Renumber.transf_program
   @@ print 3
   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
   @@ print 4
   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
   @@ print 5
  @@@ (
       (λ rtl, time "CSE" CSE.transf_program rtl @@ print 61)
       |+|
       (λ rtl,
        time "CSE" CSEannot.transf_program rtl
             @@ print 62
             @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
             @@ print 7
             @@@ time "Unused globals" Unusedglob.transform_program
             @@ print 8)
       ).