Require Import Linking IPass Errors Globalenvs.
Require Import Coqlib RTL Maps Compopts.
Require Import RTLtoBTL RTLtoBTLproof.
Require Import BTLtoRTL BTLtoRTLproof.
Require Import BTL_Invariants BTL_SEsimuref.
Require Import BTL_BlockSimulation BTL_BlockSimulationproof BTL_AnalysisLib.
Require BTL_ValueAnalysis BTL_ZIntervalAnalysis.

RTL to BTL passes

Translate from RTL to BTL with basic-blocks

Module RTLtoBTL_BBlocksOracle <: RTLtoBTL_TranslationOracle.
Axiom rtl2btl: RTL.function -> BTL.code * node * function_info * (PTree.t node).
Extract Constant rtl2btl => "RTLtoBTLaux.rtl2btl_BB".
End RTLtoBTL_BBlocksOracle.

Module RTLtoBTL_BBlocks := RTLtoBTL_Translationproof RTLtoBTL_BBlocksOracle.

Translate from RTL to BTL with basic-blocks *and* synthetic nodes insertion

Module RTLtoBTL_BBlocksSNodesOracle <: RTLtoBTL_TranslationOracle.
Axiom rtl2btl: RTL.function -> BTL.code * node * function_info * (PTree.t node).
Extract Constant rtl2btl => "RTLtoBTLaux.rtl2btl_BBSN".
End RTLtoBTL_BBlocksSNodesOracle.

Module RTLtoBTL_BBlocksSNodes := RTLtoBTL_Translationproof RTLtoBTL_BBlocksSNodesOracle.

Translate from RTL to BTL with superblocks

Module RTLtoBTL_SuperBlocksOracle <: RTLtoBTL_TranslationOracle.
Axiom rtl2btl: RTL.function -> BTL.code * node * function_info * (PTree.t node).
Extract Constant rtl2btl => "RTLtoBTLaux.rtl2btl_SB".
End RTLtoBTL_SuperBlocksOracle.

Module RTLtoBTL_SuperBlocks := RTLtoBTL_Translationproof RTLtoBTL_SuperBlocksOracle.

BTL to RTL passes

Translate from BTL to RTL

Module BTLtoRTL_ClassicOracle <: BTLtoRTL_TranslationOracle.
Axiom btl2rtl: BTL.function -> RTL.code * node * (PTree.t node).
Extract Constant btl2rtl => "BTLtoRTLaux.btl2rtl".
End BTLtoRTL_ClassicOracle.

Module BTLtoRTL_Classic := BTLtoRTL_Translationproof BTLtoRTL_ClassicOracle.

BTL Block Simulation passes

Expansions (unfolding RTL pseudo-instructions) pass (can operates on any kind of btl block)

Module BTL_ExpansionsOracle <: BTL_BlockSimulationCompConfig.
  Axiom btl_optim_oracle: BTL.function -> BTL.code * function_info * gluemap.
  Extract Constant btl_optim_oracle => "BTL_BlockOptimizer.btl_expansions_oracle".
  Axiom btl_rrules: unit -> rrules_set.
  Extract Constant btl_rrules => "BTL_BlockOptimizer.btl_expansions_rrules".
  Definition analyse := ipass_refl (sem AnnotTrap).
End BTL_ExpansionsOracle.

Module BTL_Expansions := BTL_BlockSimulationComp BTL_ExpansionsOracle.

Int promotion pass

Module BTL_IntPromotionOracle <: BTL_BlockSimulationCompConfig.
  Axiom btl_optim_oracle: BTL.function -> BTL.code * function_info * gluemap.
  Extract Constant btl_optim_oracle => "BTL_BlockOptimizer.btl_int_promotion_oracle".
  Definition btl_rrules (_ : unit) := RRpromotion.
  Module AN := BTL_AnnotateAnalysis BTL_ZIntervalAnalysis.BTL_ZIntervalAADomain_Annotate.
  Definition analyse := AN.ipass.
End BTL_IntPromotionOracle.

Module BTL_IntPromotion := BTL_BlockSimulationComp BTL_IntPromotionOracle.

Module ValueAnalysis_AnnotConfig <: BTL_ValueAnalysis.AnnotConfig.
  Definition conservative_bot : bool := true.
End ValueAnalysis_AnnotConfig.
Module ValueAnalysis_AnnotD := BTL_ValueAnalysis.BTL_ValueAADomain_Annotate ValueAnalysis_AnnotConfig.
Module ValueAnalysis_Annot := BTL_AnnotateAnalysis ValueAnalysis_AnnotD.

Lazy Code Transformations pass (operates over basic-blocks + synthetic nodes)

Module BTL_LazyCodeOracle <: BTL_BlockSimulationCompConfig.
  Axiom btl_optim_oracle: BTL.function -> BTL.code * function_info * gluemap.
  Extract Constant btl_optim_oracle => "BTL_BlockOptimizer.btl_lazy_code_oracle".
  Axiom btl_rrules: unit -> rrules_set.
  Extract Constant btl_rrules => "BTL_BlockOptimizer.btl_lazy_code_rrules".
  Axiom btl_annotate_analysis: unit -> bool.
  Extract Constant btl_annotate_analysis => "BTL_BlockOptimizer.btl_lazy_code_annotate_analysis".
  Definition analyse := ipass_opt btl_annotate_analysis ValueAnalysis_Annot.ipass.
End BTL_LazyCodeOracle.

Module BTL_LazyCode := BTL_BlockSimulationComp BTL_LazyCodeOracle.

Store motion

Module BTL_StoreMotionOracle <: BTL_BlockSimulationCompConfig.
  Axiom btl_optim_oracle: BTL.function -> BTL.code * function_info * gluemap.
  Extract Constant btl_optim_oracle => "BTL_BlockOptimizer.btl_store_motion_oracle".
  Axiom btl_rrules: unit -> rrules_set.
  Extract Constant btl_rrules => "BTL_BlockOptimizer.btl_store_motion_rrules".
  Axiom btl_annotate_analysis: unit -> bool.
  Extract Constant btl_annotate_analysis => "BTL_BlockOptimizer.btl_store_motion_annotate_analysis".
  Definition analyse := ipass_opt btl_annotate_analysis ValueAnalysis_Annot.ipass.
End BTL_StoreMotionOracle.

Module BTL_StoreMotion := BTL_BlockSimulationComp BTL_StoreMotionOracle.

Superblocks scheduling pass

Module BTL_SchedulingOracle <: BTL_BlockSimulationCompConfig.
  Axiom btl_optim_oracle: BTL.function -> BTL.code * function_info * gluemap.
  Extract Constant btl_optim_oracle => "BTL_BlockOptimizer.btl_scheduling_oracle".
  Axiom btl_rrules: unit -> rrules_set.
  Extract Constant btl_rrules => "BTL_BlockOptimizer.btl_scheduling_rrules".
  Axiom btl_annotate_analysis: unit -> bool.
  Extract Constant btl_annotate_analysis => "BTL_BlockOptimizer.btl_scheduling_annotate_analysis".
  Definition analyse
    := ipass_if btl_annotate_analysis ValueAnalysis_Annot.ipass (ipass_refl _).
End BTL_SchedulingOracle.

Module BTL_Scheduling := BTL_BlockSimulationComp BTL_SchedulingOracle.

BTL composed passes (to have a single RTL to RTL pass in the end)

Module Type IPassModule.
  Parameter ipass : IPass RTL.semantics RTL.semantics.
  Parameter transf_program : RTL.program -> res RTL.program.
  Axiom transf_program_eq : transf_program = ipass_impl ipass.
End IPassModule.

Module IPassProofModule (P : IPassModule).
  Include P.
  Definition match_prog := pass_match P.ipass.(ipass_spec).

  Lemma transf_program_match p tp:
    transf_program p = OK tp -> match_prog p tp.

Proof.

rewrite P.transf_program_eq. apply P.ipass.(ipass_match). Qed.

  Lemma transf_program_correct p tp:
    match_prog p tp -> Smallstep.forward_simulation (RTL.semantics p) (RTL.semantics tp).

Proof.

apply P.ipass.(ipass_correct). Qed.

Global Instance TransfIPassProof : TransfLink match_prog := pass_match_link P.ipass.(ipass_spec).

End IPassProofModule.

Local Open Scope ipass_scope.

Int Promotion pass: This pass aims to replace some int instruction by instructions on long, that are supported by the SR of the LCT pass. It is called before the move forwarding pass.

Module BTL_IntPromotionpasses <: IPassModule.
  Definition ipass :=
    RTLtoBTL_BBlocks.ipass :::
    BTL_IntPromotion.ipass :::
    BTLtoRTL_Classic.ipass.

  Definition transf_program (p : RTL.program) : res RTL.program
    := Eval cbn in ipass_impl ipass p.
  Definition transf_program_eq : transf_program = ipass_impl ipass := eq_refl.
  Global Opaque transf_program.
End BTL_IntPromotionpasses.

Module BTL_IntPromotionpassesproof := IPassProofModule BTL_IntPromotionpasses.

Basic-blocks transformations composed passes: If Compopts.btl_bb is false, the pass is not called; Activated if either expansions, lct or store motion are on; Convert into BTL with basic-blocks, and with synthetic nodes only in the lct and store motion cases; LCT, store motion and expansion are applied sequentially and verified separately (not using the same set of rewriting rules); Code is translated back to RTL using the classical way. RTL -> BTL (BB \/ BBSN) -> BTL (Lazy code optim) -> BTL (Store motion) -> BTL (Expansed) -> RTL

Module BTL_BBpasses <: IPassModule.
  Definition need_snodes (_ : unit) :=
    Compopts.optim_lct tt || Compopts.optim_store_motion tt.

  Definition ipass :=
    ipass_if (fun _ => negb (need_snodes tt))
      RTLtoBTL_BBlocks.ipass
      RTLtoBTL_BBlocksSNodes.ipass :::
    BTL_ResetAnnots.ipass _ :::
    ipass_if Compopts.optim_lct
      (BTL_LazyCodeOracle.analyse :::
       ipass_simu Trap_to_Undef.transf_program :::
       BTL_LazyCode.Simu.ipass)
      (ipass_simu Trap_to_Undef.transf_program) :::
    ipass_opt Compopts.optim_store_motion
      (ipass_opt
         (fun _ => negb (Compopts.optim_lct tt &&
                     bool_eq (BTL_LazyCodeOracle.btl_annotate_analysis tt)
                             (BTL_StoreMotionOracle.btl_annotate_analysis tt)))
         (ipass_simu Undef_to_Lax.transf_program :::
          BTL_ResetAnnots.ipass _ :::
          BTL_StoreMotionOracle.analyse :::
          ipass_simu Trap_to_Undef.transf_program) :::
       BTL_StoreMotion.Simu.ipass) :::
    ipass_simu Undef_to_Lax.transf_program :::
    ipass_opt Compopts.optims_expanse BTL_Expansions.ipass :::
    BTLtoRTL_Classic.ipass.

  Definition transf_program (p : RTL.program) : res RTL.program
    := Eval cbn in ipass_impl ipass p.
  Definition transf_program_eq : transf_program = ipass_impl ipass := eq_refl.
  Global Opaque transf_program.
End BTL_BBpasses.

Module BTL_BBpassesproof := IPassProofModule BTL_BBpasses.

Superblocks scheduling composed passes: RTL -> BTL (superblocks) -> BTL (scheduled) -> RTL

Module BTL_SBpasses <: IPassModule.
  Definition ipass :=
    RTLtoBTL_SuperBlocks.ipass :::
    BTL_Scheduling.ipass :::
    BTLtoRTL_Classic.ipass.

  Definition transf_program (p : RTL.program) : res RTL.program
    := Eval cbn in ipass_impl ipass p.
  Definition transf_program_eq : transf_program = ipass_impl ipass := eq_refl.
  Global Opaque transf_program.
End BTL_SBpasses.

Module BTL_SBpassesproof := IPassProofModule BTL_SBpasses.

Module BTLpasses

RTL to BTL passes

BTL to RTL passes

BTL Block Simulation passes

BTL composed passes (to have a single RTL to RTL pass in the end)