Module RTLofRTLinjectproof

Require Import
   Coqlib Values Maps Registers
   Traces Errors Globalenvs
   Simulations TSOsimulation
.

Require Import
   Utf8 Classical
   Utils Common
   RTLinject RTLinjectlow RTL
   RTLofRTLinject
   RTLofRTLinjectspec.

Section CORRECT.

  Variable bi : backend_info.
  Hypothesis OK_BI: ok_bi bi.

    Inductive match_fundef : RTLinject.fundef → RTL.fundef → Prop :=
    | MFI sg param ssz c c' ep
        (SIG: ∀t, In t sg.(Ast.sig_args) → t = Ast.Tint)
        (CODE: match_code bi c c')
      : match_fundef
          (Ast.Internal (RTLinject.mkfunction sg param ssz c ep))
          (Ast.Internal (RTL.mkfunction sg (map xO param) ssz c' ep))
    | MFE f
      : match_fundef (Ast.External f) (Ast.External f)
    .

  Remark transl_fundef_correct {f f'} : transl_fundef bi f = OK f' → match_fundef f f'.

  Definition genv_rel : RTLinject.genv → RTL.genv → Prop :=
    fun x y => Genv.genv_match (fun a b => transl_fundef bi a = Errors.OK b) y x.

  Definition match_prg p p' := transf_program bi p = OK p'.

  Section SIM.

    Variables (ge: RTLinject.genv) (tge: RTL.genv).
    Hypothesis TRANSF: genv_rel ge tge.

    Let lts := mklts thread_labels (rtl_step' ge).
    Let tlts := mklts thread_labels (rtl_step tge).

    Definition match_regset : INJECT.regset → RTL.regset → Prop :=
      fun x y =>
        ∀ r, Val.lessdef (x r) (y # (xO r)).

    Definition match_inject_regset : INJECT.regset → RTL.regset → Prop :=
      fun x y =>
        ∀ r, Val.lessdef (x r) (y # (xI r)).

    Lemma match_regset_upd rs rs' :
      match_regset rs rs' →
      ∀ v v',
        Val.lessdef v v' →
        ∀ r,
          match_regset (upd rs r v) (rs' # (xO r) <- v').

    Lemma match_regset_iupd rs rs' :
      match_regset rs rs' →
      ∀ v v',
        Val.lessdef v v' →
        ∀ r,
          match_regset rs (rs' # (xI r) <- v').

    Lemma match_iregset_upd rs rs' :
      match_inject_regset rs rs' →
      ∀ v v',
        Val.lessdef v v' →
        ∀ r,
          match_inject_regset (INJECT.upd_regset rs r v) (rs' # (xI r) <- v').
    Hint Resolve match_regset_upd match_regset_iupd match_iregset_upd.

    Lemma match_args_lessdef {rs rs'} :
      match_regset rs rs' →
      ∀args,
        Val.lessdef_list (map rs args) (rs' ## (map xO args)).

    Lemma match_iargs_lessdef {rs rs'} :
      match_inject_regset rs rs' →
      ∀args,
        Val.lessdef_list (map rs args) (rs' ## (map xI args)).

    Lemma match_init_regs :
      ∀ param,
      forall args' args,
        Val.lessdef_list args args' →
        match_regset (reg_upd (fun _ : reg => Vundef) param args)
                     (init_regs args' (map xO param)).

    Lemma match_find_function {rs rs'} :
      match_regset rs rs' →
      ∀ros fd,
        RTLinject.find_function ge ros rs = Some fd →
        ∃fd',
          RTL.find_function tge (match ros with inl f => inl Ast.ident (xO f) | inr f => inr _ f end) rs' = Some fd'
        ∧ match_fundef fd fd'.

    Lemma match_eval_addressing {ad sp v a a'} :
      Val.lessdef_list a a' →
      Op.eval_addressing ge sp ad a = Some v →
      Op.eval_addressing tge sp ad a' = Some v.

    Lemma match_eval_op {op args args' sp v} :
      INJECT.ok_op op →
      Val.lessdef_list args args' →
      Op.eval_operation ge sp op args = Some v →
      ∃v',
        Op.eval_operation tge sp op args' = Some v'
      ∧ Val.lessdef v v'.

    Definition only_int : RTL.regset → Prop :=
      fun rs => ∀r, Val.has_type (rs # r) Ast.Tint.

    Lemma only_int_update rs v r :
      only_int rs →
      Val.has_type v Ast.Tint →
      only_int (rs # r <- v).
    Hint Resolve only_int_update.

    Lemma eval_op_int {rs' sp op args v} :
      only_int rs' →
      INJECT.ok_op op →
      Op.eval_operation tge sp op (rs' ## args) = Some v →
      Val.has_type v Ast.Tint.

    Inductive match_stack_frame : stack_frame → stackframe → Prop :=
    | MSF res rs rs' c c' sp pc
        (INTS: only_int rs')
        (REGS: match_regset rs rs')
        (CODE: match_code bi c c')
      : match_stack_frame (mksf res c sp pc rs) (Stackframe (xO res) c' sp pc rs').

    Definition match_stack : stack → list stackframe → Prop := list_forall2 match_stack_frame.

    Inductive tr_cont (c: RTL.code) (exit: node) (dst: list reg) : INJECT.continuation → node → node → Prop :=
    | TKstmt s k ns nk nd
        (TKS: tr_stmt bi c s ns dst exit nk)
        (TKK: tr_cont c exit dst k nk nd)
      : tr_cont c exit dst (INJECT.Kstmt s k) ns nd
    | TKend nd
      : tr_cont c exit dst INJECT.Kend nd nd
    .

    Inductive match_state : RTLinject.intra_state → RTL.state → Prop :=
    | MSCS stk stk' f f' args args'
        (STK: match_stack stk stk')
        (FD: match_fundef f f')
        (ARGS: Val.lessdef_list args args')
        (INTS: ∀a, In a args' → Val.has_type a Ast.Tint)
      : match_state (RICallState stk f args) (Callstate stk' f' args')
    | MSBS stk stk' sg
        (STK: match_stack stk stk')
      : match_state (RIBlockedState stk sg) (Blockedstate stk' sg)
    | MSRS stk stk' res res'
        (STK: match_stack stk stk')
        (RES: Val.lessdef res res')
        (INT: Val.has_type res' Ast.Tint)
      : match_state (RIRetState stk res) (Returnstate stk' res')
    | MSS stk stk' c c' sp pc rs rs'
        (STK: match_stack stk stk')
        (CODE: match_code bi c c')
        (REGS: match_regset rs rs')
        (INTS: only_int rs')
      : match_state (RIState stk c sp pc rs) (State stk' c' sp pc rs')
    | MSI stk stk' c c' sp pc pc' rs rs' dst irs is ik nk
        (STK: match_stack stk stk')
        (CODE: match_code bi c c')
        (REGS: match_regset rs rs')
        (IREGS: match_inject_regset irs rs')
        (INTS: only_int rs')
        (TS: tr_stmt bi c' is pc' (map xO dst) pc nk)
        (TK: tr_cont c' pc (map xO dst) ik nk pc)
      : match_state (RIInjectState stk c sp pc rs dst (INJECT.NormalState irs is ik))
                    (State stk' c' sp pc' rs')
    .

    Section M.
     Import INJECT.
     Open Scope nat_scope.

     Fixpoint measure_stmt (stmt: statement) : nat :=
       match stmt with
         | Sskip
         | Sreturn _ => 1
         | Sfreeperm
         | Leak _ _ _
         | Sop _ _ _
         | Sload _ _ _ _
         | Sstore _ _ _ _ _
         | Satomicmem _ _ _ _
         | Sfence false
         | Srequestperm _ _ _
         | Sabort _ false _
         | Sassume _ _
         | Srelease
           => 2
         | Sabort _ true _
         | Sfence true
           => 3
         | Sseq s s'
         | Sbranch s s'
         | Sifthenelse _ _ s s' => 1 + measure_stmt s + measure_stmt s'
         | Satomic _ s
         | Sloop s
         | Swhile _ _ s => 1 + measure_stmt s
         | Srepeat s _ _ => 3 + measure_stmt s + measure_stmt s
       end.

     Fixpoint measure_cont (k: continuation) : nat :=
       match k with
         | Kstmt s k' => measure_stmt s + measure_cont k'
         | Kendatomic _ k' => measure_cont k'
         | Kend => O
       end.

     Definition measure_state (s: state) : nat :=
       match s with
         | NormalState _ s k => measure_stmt s + measure_cont k
         | ReturnState => O
       end.
    End M.

    Definition measure_intra_state (s: RTLinject.intra_state) : nat :=
      match s with
        | RIInjectState _ _ _ _ _ _ is => measure_state is
        | _ => O
      end.

    Definition inject_order : RTLinject.intra_state → RTLinject.intra_state → Prop :=
      ltof _ measure_intra_state.

    Lemma inject_order_wf : well_founded inject_order.

    Lemma begin_inject_inv stk' c' sp :
      forall {nd args param ns},
      tr_init c' ns args param nd →
      ∀ rs',
      taustar tlts (State stk' c' sp ns rs')
              (State stk' c' sp nd (fold_left2 (fun q p a => q # (xI p) <- (q # (xO a))) rs' param args)).

    Lemma begin_inject_match_reg rs :
      ∀ args param rs',
      match_regset rs rs' →
      match_regset rs (fold_left2 (fun q p a => q # (xI p) <- (q # (xO a))) rs' param args).

    Lemma begin_inject_match_ireg rs :
      ∀ args param rs',
      ∀ acc acc',
      match_regset rs rs' →
      match_regset rs acc' →
      match_inject_regset acc acc' →
      match_inject_regset (fold_left2 upd acc param (map rs args))
                          (fold_left2 (fun q p a => q # (xI p) <- (q # (xO a))) acc' param args).

    Lemma begin_inject_only_int :
      ∀ args param rs',
        only_int rs' →
        only_int (fold_left2 (fun q p a => q # (xI p) <- (q # (xO a))) rs' param args).

    Lemma end_inject_inv stk' c' sp :
      forall {ns res dst ne nd},
      res ≠ nil →
      tr_stmt bi c' (INJECT.Sreturn res) ns dst ne nd →
      ∀ rs',
      ∃ t,
        stepr tlts (State stk' c' sp ns rs') Events.TEtau t
      ∧ taustar tlts t
      (State stk' c' sp ne (fold_right2 (fun q p a => q # p <- (q # (xI a))) rs' dst res)).

    Lemma end_inject_match_reg rs irs rs':
      match_regset rs rs' →
      match_inject_regset irs rs' →
      ∀ res dst,
        match_regset (reg_upd rs dst (map irs res))
                     (fold_right2 (fun q p a => q # p <- (q # (xI a)))
                                  rs' (map xO dst) res).

    Lemma end_inject_only_int rs':
      only_int rs' →
      ∀ res dst,
        only_int (fold_right2 (fun q p a => q # p <- (q # (xI a)))
                              rs' (map xO dst) res).

    Lemma fw_sim : forward_sim_with_undefs2 lts tlts match_state inject_order.

    Definition bsim_rel := @bsr _ lts tlts match_state.
    Definition bsim_order := @bsc _ tlts.

    Lemma init_sim_succ:
      forall {p vals vals' tinit},
        rtl_init tge p vals = Some tinit ->
        Val.lessdef_list vals' vals →
        exists sinit, rtl_inject_init ge p vals' = Some sinit /\ bsim_rel tinit sinit.

    Lemma init_sim_fail:
      forall p vals vals',
        rtl_init tge p vals = None ->
        Val.lessdef_list vals' vals →
        rtl_inject_init ge p vals' = None.

  End SIM.

Ltac bind_inv :=
  match goal with
    | [H: bind ?f ?g = OK ?y |- _] =>
      destruct (bind_inversion f g H) as
          (? & ?Hbind & ?Hbind' );
      clear H
  end.

 Theorem rtlgen_sim : Sim.sim RtlInjectSem rtl_sem match_prg.

End CORRECT.